# Re: [isabelle] Strange behavior of equality?

Hello Christian,
> 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

`The problem here is that you use meta-implication "==>" within the
``"show" statement. "show" only tries to match the assumptions made by
``"assume" and the conclusion of the "show" with the goals to decide which
``goal to solve. Since you have no assumes, "R' n m" unifies with the
``first goal and the assumptions in the "show" statement become your new
``proof goals. However, the solved goal contained the assumption "R n m",
``so this is normally not a problem as qed can discharge this.
`
If you look at the proof state after the first sorry, you see the two goals:
"R n m ==> R n m"
"R' n m ==> R n m"

`Unfortunately, your next "show" has the conclusion "R n m", which
``unifies with the first goal, so the first goal gets solved again instead
``of the second.
`

`A simple solution would be to insert "prefer 2" between your two proofs,
``but it would be better style to use proper assumes:
`
lemma "R n m = R' n m"
proof (rule iffI)
assume "R n m" thus "R' n m" sorry
next
assume "R' n m" thus "R n m" sorry
qed
Regards,
Andreas Lochbihler

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