Re: [isabelle] Strange behavior of equality?



On Wed, 15 Apr 2009, Christian Doczkal wrote:

lemma "R n m = R' n m"
proof (rule iffI)
 show "R n m ==> R' n m" sorry
 show "R' n m ==> R n m" sorry -- "*"
qed

until * i get:
Successful attempt to solve goal by exported rule:
 R n m ==> R' n m

Successful attempt to solve goal by exported rule:
 R' n m ==> R n m

But the proof state is still:
goal (2 subgoals):
1. R n m ==> R' n m
2. R' n m ==> R n m

and hence the "qed" fails to finish the proof? Why are the goals not
removed after they have been successfully solved.

This surprising behaviour is mostly due to a misunderstanding how Isar works, and due to old-style tactic goal output that does not fully fit into the picture.

Whenever you see a subgoal like

  !!x. A x ==> B x

the system tells you that you may assume A x for some fixed x, and need to show B x in the end. So your standard answer will be like that:

  fix x
  assume "A x"
  show "B x"

As a rule of thumb, framework connectives !! / ==> rarely show up in structured texts at all (specifications and proofs). It is a bit like lambda abstraction in functional programming languages: most of the time you don't see them, even though they are present in the guts of the system.

So this is how to prove an equivalence:

  lemma "A <-> B"
  proof
    assume A then show B <proof>
  next
    assume B then show A <proof>
  qed


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.