# 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.*