Email Gateway (Aug 18 2022 at 10:43): Email Gateway (Aug 18 2022 at 10:43):From: Richard Warburton <richard.warburton@gmail.com>
I have an equivalence relation that I am trying to prove symmetric,
which is defined as
lemma "(p,q) : \<smile> ==> (q,p) : \<smile>"
It seems a very trivia proof to me, simply unfold the definition of
the induction, use the symmetry of disjunction and equality and then
apply the rules of the inductive definition, I want to do something
like:
lemma "(p,q) : \<smile> ==> (q,p) : \<smile>" (* symmetry *)
proof -
assume "(p, q) : \<smile>"
hence "(ALL i. (terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)) |
(terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)))))" by (rule
terminequivalent.induct)
hence "(ALL i. (terminated(exec(q,i)) --> (exec(q,i) = exec(p,i)) |
(terminated(exec(p,i)) --> (exec(q,i) = exec(p,i)))))" by simp
thus "(q, p) : \<smile>" by (rule terminequivalent.step)
qed
However the middle simp step fails, it is happy to deduce "(ALL i.
(terminated(exec(q,i)) --> (exec(q,i) = exec(p,i)) |
(terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)))))" or "(ALL i.
(terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)) |
(terminated(exec(p,i)) --> (exec(q,i) = exec(p,i)))))" but it (and
successive simp attempts) fail to recognise that equality is
symmetric. I initially thought this might be a precedence/binding
problem (which motivated the extensive bracket use) but it didn't seem
to resolve anything. I apologise if this seems like a trivial
problem, but I am rather confused as to why simp is happy to exchange
the terms in either place, but not both.
Richard
Email Gateway (Aug 18 2022 at 10:43):From: Steven Obua <obua@in.tum.de>
Richard Warburton wrote:
maybe "auto" instead of "simp" works there.
Steven
Email Gateway (Aug 18 2022 at 10:44):From: Brian Huffman <brianh@cs.pdx.edu>
I discovered some interesting simplifier quirks when I tried this out.
This term:
"(ALL i. (terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)) |
(terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)))))"
simplifies to this:
"ALL i. terminated (exec (p, i)) -->
terminated (exec (q, i)) --> exec (p, i) = exec (q, i)"
When the above term is present in the assumptions, I assumed that the
simplifier would add a conditional rewrite like this:
"!!i. [| terminated (exec (p, i)); terminated (exec (q, i)) |]
==> exec (p, i) == exec (q, i)"
That rewrite would have been sufficient to solve the next subgoal. But when I
looked at the simplifier trace, I found this rewrite instead:
"!!i. [| terminated (exec (p, i)); terminated (exec (q, i)) |]
==> (exec (p, i) = exec (q, i)) == True"
Very strange!
I tried tracing a few simple examples to figure out how the simplifier
converts assumptions into rewrites, and here is what I found:
Assumption: "P --> x = y"
Rewrite: "P ==> x == y"
Assumption: "P y --> x = y"
Rewrite: "P y ==> x == y"
Assumption: "P x --> x = y"
Rewrite: "P x ==> y == x" (* notice reversed orientation! *)
Assumption: "P x y --> x = y"
Rewrite: "P x y ==> (x = y) == True" (* similar to example above *)
I imagine that this behavior took some extra work to implement, so there must
have been a reason for it. Can anyone explain?
Email Gateway (Aug 18 2022 at 10:44):From: Richard Warburton <richard.warburton@gmail.com>
Thanks for the suggestion, but I have already tried auto as well, in
fact I have even tried the more powerful methods like best. Its also
the case that this fails to prove in a two step scenario, ie I can't
simplify to one of the intermediate goals and then simplify again to
the desired goal. Is there a way of seeing a 'trace' of the automatic
method in order to better identify what is happening?
Richard
Email Gateway (Aug 18 2022 at 10:44):From: Tobias Nipkow <nipkow@in.tum.de>
Brian Huffman schrieb:
On Tuesday 14 August 2007, Richard Warburton wrote:
lemma "(p,q) : \<smile> ==> (q,p) : \<smile>" (* symmetry *)
proof -
assume "(p, q) : \<smile>"
hence "(ALL i. (terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)) |
(terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)))))" by (rule
terminequivalent.induct)
hence "(ALL i. (terminated(exec(q,i)) --> (exec(q,i) = exec(p,i)) |
(terminated(exec(p,i)) --> (exec(q,i) = exec(p,i)))))" by simp
thus "(q, p) : \<smile>" by (rule terminequivalent.step)
qedHowever the middle simp step fails, it is happy to deduce "(ALL i.
(terminated(exec(q,i)) --> (exec(q,i) = exec(p,i)) |
(terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)))))" or "(ALL i.
(terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)) |
(terminated(exec(p,i)) --> (exec(q,i) = exec(p,i)))))" but it (and
successive simp attempts) fail to recognise that equality is
symmetric.I discovered some interesting simplifier quirks when I tried this out.
This term:
"(ALL i. (terminated(exec(p,i)) --> (exec(p,i) = exec(q,i)) |
(terminated(exec(q,i)) --> (exec(p,i) = exec(q,i)))))"simplifies to this:
"ALL i. terminated (exec (p, i)) -->
terminated (exec (q, i)) --> exec (p, i) = exec (q, i)"When the above term is present in the assumptions, I assumed that the
simplifier would add a conditional rewrite like this:
"!!i. [| terminated (exec (p, i)); terminated (exec (q, i)) |]
==> exec (p, i) == exec (q, i)"That rewrite would have been sufficient to solve the next subgoal. But when I
looked at the simplifier trace, I found this rewrite instead:
"!!i. [| terminated (exec (p, i)); terminated (exec (q, i)) |]
==> (exec (p, i) = exec (q, i)) == True"Very strange!
Admittedly, I had to ponder this for quite some time before I realized
what was going on: Isabelle tried to orient the rule in either direction
but failed because this would immediately lead to death by
nontermination: both exec(p,i) and exec(q,i) appear in the premises and
this would lead to a recursive call of the simplifier again and again.
Hence all that is left is the == True version - better than nothing.
I tried tracing a few simple examples to figure out how the simplifier
converts assumptions into rewrites, and here is what I found:Assumption: "P --> x = y"
Rewrite: "P ==> x == y"Assumption: "P y --> x = y"
Rewrite: "P y ==> x == y"Assumption: "P x --> x = y"
Rewrite: "P x ==> y == x" (* notice reversed orientation! *)
This one is easy. The direction x==y is no good: which y should we take
when applying the rule? The chosen orientation means that any y will get
rewritten to some x for which we happen to have the fact "P x" available.
Assumption: "P x y --> x = y"
Rewrite: "P x y ==> (x = y) == True" (* similar to example above *)
Same as above, this is the only way to avoid nontermination.
I imagine that this behavior took some extra work to implement, so there must
have been a reason for it. Can anyone explain?
Yes :-)
- Brian
Tobias
Last updated: May 03 2024 at 04:19 UTC