CODEWITHSUNDEEP
isabelleproofisar
Nick Hu
Nick Hu

Reputation: 43

How to use obtain to make forward elimination proofs easier to read?

I'm trying to do basic natural deduction proofs in Isabelle, following this document (particularly slide 23).

I know I can do things like

theorem ‹(A ⟶ B) ⟶ A ⟶ B›
proof -
  {
    assume ‹A ⟶ B›
    {
      assume ‹A›
      with ‹A ⟶ B› have ‹B› ..
    }
    hence ‹A ⟶ B› ..
  }
  thus ‹(A ⟶ B) ⟶ A ⟶ B› ..
qed

But also

theorem ‹(A ⟶ B) ⟶ A ⟶ B›
proof
  assume ‹A ⟶ B› and ‹A›
  then obtain ‹B› ..
qed

achieves the same goal.

So when I try to write the proof

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof -
  {
    assume ‹A ⟶ A ⟶ B›
    {
      assume ‹A›
      with ‹A ⟶ A ⟶ B› have ‹A ⟶ B› ..
      hence ‹B› using ‹A› ..
    }
    hence ‹A ⟶ B› ..
  }
  thus ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B› ..
qed

like

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then obtain ‹B› using ‹A› ..
qed

why does Isabelle complain that

Failed to finish proof:
goal (1 subgoal):
 1. A ⟶ A ⟶ B ⟹ A ⟶ B

I'm aware that these are very simple things that Isabelle can prove in one step: the goal here is to produce a concise proof which is human readable (to the extent that Natural Deduction is), without having to consult Isabelle.

Upvotes: 3

Views: 112

Answers (1)

Dominic Mulligan
Dominic Mulligan

Reputation: 466

This modification to your proof works:

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof(intro impI)
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then show ‹B› using ‹A› ..
qed

The problem is twofold:

  1. The opening of the proof block applied a 'standard' introduction rule automatically based on the shape of the goal you were trying to prove. In your case this was implication introduction, i.e. the theorem impI. The problem is that you only apply this once which leaves you with the assumption A -> A -> B and the remaining goal A -> B. As a result, you do not yet have the assumption A which you are assuming you have as this requires a second use of impI to obtain. Instead, by using proof(intros impI) I am telling Isabelle to refrain from using its standard set of introduction and elimination rules as a first step in the proof and instead apply the impI introduction rule as often as it can (i.e. twice). Alternatively, proof(rule impI, rule impI) would also work here with the same effect.
  2. Second, your final line then obtain onwards, is not finishing the proof: you are not showing anything! By using an explicit show you are signalling to Isabelle that you would like to 'refine' an open goal and actually conclude what it is you set out to prove at the start of the block.

Note that your use of obtain here to work forward from the facts A -> B and A was not incorrect if your only goal is to derive B. The problem is you are trying to work forward from facts to derive new ones at the same time as refine an open goal. For instance, this also works:

theorem ‹(A ⟶ A ⟶ B) ⟶ A ⟶ B›
proof(intro impI)
  assume ‹A ⟶ A ⟶ B› and ‹A›
  hence ‹A ⟶ B› ..
  then obtain ‹B› using ‹A› ..
  then show ‹B› .
qed

where the fact B is obtained on the first line, and the second line trivially uses this fact to refine the open goal B.

Upvotes: 0

Related Questions