Email Gateway (Aug 18 2022 at 13:23): Email Gateway (Aug 18 2022 at 13:23):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
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):
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?
smime.p7s
Email Gateway (Aug 18 2022 at 13:23):From: Brian Huffman <brianh@cs.pdx.edu>
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
On Wed, Apr 15, 2009 at 3:25 AM, Christian Doczkal <
c.doczkal@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
beginconsts
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 -- "*"
qeduntil * i get:
Successful attempt to solve goal by exported rule:
R n m ==> R' n mSuccessful attempt to solve goal by exported rule:
R' n m ==> R n mBut the proof state is still:
goal (2 subgoals):
1. R n m ==> R' n m
2. R' n m ==> R n mand 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)
qedCan someone reproduce this or explain what is going on?
--
Gruß
Christian Doczkal
Email Gateway (Aug 18 2022 at 13:23):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 13:23):From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
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
Last updated: May 03 2024 at 04:19 UTC