Re: [isabelle] Strange behavior of equality?



I have been annoyed by this behavior as well. To understand what is going
on, it is helpful to look at the intermediate proof state using "next":

lemma "R n m = R' n m"
proof (rule iffI)

The initial proof state is what you would expect:
> goal (2 subgoals):
>  1. R n m ==> R' n m
>  2. R' n m ==> R n m

 show "R n m ==> R' n m" sorry
next

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

Instead of solving the first subgoal, it just replaced it with another one.
Basically, it has applied "R n m ==> R' n m" to the first subgoal, as an
introduction rule.

 show "R' n m ==> R n m" sorry
next

After this step, the proof state is:
> goal (2 subgoals):
>  1. R n m ==> R' n m
>  2. R' n m ==> R n m

Apparently, it applied "R' n m ==> R n m" to the first subgoal, which
returns us to the original proof state. If it had applied the rule to the
second subgoal instead, then qed would have worked. Evidently, Isar works by
applying the rule to the first subgoal that matches.

By the way, I just realized that your proof script works if you prove the
subgoals in the opposite order:

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

Using "next" just before the "qed" shows the proof state to be nothing but
trivial implications, which can be discharged by "qed".
> goal (2 subgoals):
>  1. R n m ==> R n m
>  2. R' n m ==> R' n m

Basically, it seems that using "show" with a meta-implication (==>)
discharges the first subgoal that matches the conclusion, and adds new
subgoals corresponding to each assumption. I would be surprised if this is
an intentional feature of Isar; my guess is that it is an accidental feature
of the way Isar proofs are implemented.

Here's a proof script that I came up with that takes advantage of this
"feature".

lemma "Q & P ==> P & Q"
proof -
  show "P ==> Q ==> P & Q" by (rule conjI)
  show "Q & P ==> P" by (rule conjunct2)
  show "Q & P ==> Q" by (rule conjunct1)
qed

- Brian


On Wed, Apr 15, 2009 at 3:25 AM, Christian Doczkal <
c.doczkal at stud.uni-saarland.de> wrote:

> Hello
>
> I want to prove that two relations are equal (I removed the actual
> proofs since they do not matter here, rule iffI is also selected as
> default rule)
>
> theory Scratch
> imports Main
> begin
>
> consts
>  R :: "nat => nat => bool"
>  R' :: "nat => nat => bool"
>
> 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.
>
> Strangely applying the initial rule at the end works as in:
>
> lemma "R n m = R' n m"
> proof -
>  have "R n m ==> R' n m" sorry
>  moreover have "R' n m ==> R n m" sorry
>  ultimately show ?thesis by (rule iffI)
> qed
>
> Can someone reproduce this or explain what is going on?
>
>
>
> --
> Gruß
> Christian Doczkal
>




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