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.
This modification to your proof works:
The problem is twofold:
impI
. The problem is that you only apply this once which leaves you with the assumptionA -> A -> B
and the remaining goalA -> B
. As a result, you do not yet have the assumptionA
which you are assuming you have as this requires a second use ofimpI
to obtain. Instead, by usingproof(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 theimpI
introduction rule as often as it can (i.e. twice). Alternatively,proof(rule impI, rule impI)
would also work here with the same effect.then obtain
onwards, is not finishing the proof: you are notshow
ing anything! By using an explicitshow
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 factsA -> B
andA
was not incorrect if your only goal is to deriveB
. 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:where the fact
B
is obtained on the first line, and the second line trivially uses this fact to refine the open goalB
.