Email Gateway (Aug 22 2022 at 13:15): Email Gateway (Aug 22 2022 at 13:15):From: Rustom Mody <rustompmody@gmail.com>
Thanks Alfio and Daniel
After learning about induction instead of induct_tac some other proofs that
I was stuck with are not going through.
But I really dont know what's happening :-)
Can someone point me to references on the differences??
Thanks again
Rusi
Email Gateway (Aug 22 2022 at 13:15):From: Alfio Martini <alfio.martini@acm.org>
Hi Daniel,
,
I am especially also interested in knowing why the structured proofs goes
thorugh using just the simplifier
and the script fails to succeed. A lot of people in this list might be
able to give a sound explanation for it. I don't think it is related to the
use of induct_tac instead of induction. But I can't say much about it.
lemma "(dfs1 xs)@l = dfs2 xs l"
proof (induction xs arbitrary:l)
case Tip
show ?case by simp
next
case (Node tr1 a tr2)
show ?case
proof -
have "dfs1 (Node tr1 a tr2) @ l=((dfs1 tr1) @ (a# dfs1 tr2))@l" by
simp
also have "... = dfs1 tr1 @ ((a# dfs1 tr2)@l)" by simp
also have "... = dfs1 tr1 @ (a # (dfs1 tr2 @l))" by simp
also have "... = dfs1 tr1 @ (a # (dfs2 tr2 l))" using Node.IH by
simp
also have "... = dfs2 tr1 (a # (dfs2 tr2 l))" using Node.IH by simp
also have "... = dfs2 (Node tr1 a tr2) l " by simp
finally show ?case by this
qed
qed
lemma " (dfs1 xs)@l = dfs2 xs l"
apply(induction xs arbitrary:l)
apply (simp_all)
oops
Email Gateway (Aug 22 2022 at 13:16):From: Alfio Martini <alfio.martini@acm.org>
Hi Daniel,
,
In this case, I am especially also interested in knowing why the structured
proofs goes thorugh using just the simplifier
and the script fails to succeed. A lot of people in this list might be
able to give a sound explanation for it. I don't think it is related to the
use of induct_tac instead of induction, but I can't say much about it.
lemma "(dfs1 xs)@l = dfs2 xs l"
proof (induction xs arbitrary:l)
case Tip
show ?case by simp
next
case (Node tr1 a tr2)
show ?case
proof -
have "dfs1 (Node tr1 a tr2) @ l=((dfs1 tr1) @ (a# dfs1 tr2))@l" by
simp
also have "... = dfs1 tr1 @ ((a# dfs1 tr2)@l)" by simp
also have "... = dfs1 tr1 @ (a # (dfs1 tr2 @l))" by simp
also have "... = dfs1 tr1 @ (a # (dfs2 tr2 l))" using Node.IH by
simp
also have "... = dfs2 tr1 (a # (dfs2 tr2 l))" using Node.IH by simp
also have "... = dfs2 (Node tr1 a tr2) l " by simp
finally show ?case by this
qed
qed
lemma " (dfs1 xs)@l = dfs2 xs l"
apply(induction xs arbitrary:l)
apply (simp_all)
oops
Email Gateway (Aug 22 2022 at 13:16):From: Daniel Horne <d.horne@danielhorne.co.uk>
The best I've found is in the isar-ref document
(http://isabelle.in.tum.de/dist/Isabelle2016/doc/isar-ref.pdf) -
induction is described on page 147, where induct_tac is on page 289.
Email Gateway (Aug 22 2022 at 13:16):From: Daniel Horne <d.horne@danielhorne.co.uk>
Also, I had another look at doing it with induct_tac, as such:
lemma "∀ list .(dfs1 xs)@list = dfs2 xs list"
apply(induct_tac xs)
apply(auto)
by (metis Cons_eq_appendI append_assoc)
As induct_tac doesn't have the "arbitrary" parameter, I had to specify
that by putting the universal quantifier on it instead.
I've previously been cautioned against doing this, but it might help
understand the difference.
Email Gateway (Aug 22 2022 at 13:16):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Alfio Martini wrote:
When faced with proving
"dfs1 (Node tr1 a tr2) @ xs = dfs2 (Node tr1 a tr2) xs"
the simplifier first unfolds the left-hand side to
"(dfs1 tr1 @ a # dfs1 tr2) @ xs"
At this point, there are two possibilities:
a) use the induction hypothesis and rewrite that term further to
"dfs2 tr1 (a # dfs1 tr2) @ xs"
at which point the simplifier gets stuck; in fact it's hard to
make progress from here because the xs is outside of the call
"dfs2 tr1 ...", but the right-hand side will expand to
"dfs2 tr1 (a # dfs2 tr2 xs)" with the xs inside of the
"dfs2 tr1 ..." call.
b) use the associativity of append and its definition to obtain
"dfs1 tr1 @ a # dfs1 tr2 @ xs"
and only then apply the induction hypothesis which results in
"dfs2 tr1 (a # dfs2 tr2 xs)"
Unfortunately, if the induction hypothesis is available for
simplification, the simplifier prefers a) and the proof fails.
The following works, but looks fragile:
lemma "dfs1 tr @ xs = dfs2 tr xs"
proof (induction tr arbitrary: xs)
case Tip
show ?case by simp
next
case (Node tr1 a tr2)
show ?case
apply simp
apply (simp add: Node.IH)
done
qed
I would prove the symmetric version of the lemma which avoids these
complications:
lemma dfs2_dfs1_conv: "dfs2 t xs = dfs1 t @ xs"
by (induct t arbitrary: xs) auto
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 13:16):From: Alfio Martini <alfio.martini@acm.org>
Very nice explanation Bertram. Thanks a lot!
Email Gateway (Aug 22 2022 at 13:26):From: Rustom Mody <rustompmody@gmail.com>
Trying to prove a little proof on trees [thy attached]?
Should be trivial at least from informal pov.
Any suggestions?
dfs.thy
Email Gateway (Aug 22 2022 at 13:27):From: Daniel Horne <d.horne@danielhorne.co.uk>
Played about with it a bit, and the following went through OK:
lemma "(dfs1 xs)@list = dfs2 xs list"
apply(induction xs arbitrary:list)
apply(auto)
by (metis Cons_eq_appendI append_assoc)
induction is a newer method than induct_tac, though I don't know the
details. Once I'd changed that, sledgehammer came up with the.."by
(metis Cons_eq_appendI append_assoc)"
Email Gateway (Aug 22 2022 at 13:27):From: Alfio Martini <alfio.martini@acm.org>
Hi Rustom and Daniel,
This was my trial using a structured proof. It goes trough using just the
simplifier.
lemma "(dfs1 xs)@l = dfs2 xs l"
proof (induction xs arbitrary:l)
case Tip
show ?case by simp
next
case (Node tr1 a tr2)
show ?case
proof -
have "dfs1 (Node tr1 a tr2) @ l=((dfs1 tr1) @ (a# dfs1 tr2))@l" by
simp
also have "... = dfs1 tr1 @ ((a# dfs1 tr2)@l)" by simp
also have "... = dfs1 tr1 @ (a # (dfs1 tr2 @l))" by simp
also have "... = dfs1 tr1 @ (a # (dfs2 tr2 l))" using Node.IH by simp
also have "... = dfs2 tr1 (a # (dfs2 tr2 l))" using Node.IH by simp
also have "... = dfs2 (Node tr1 a tr2) l " by simp
finally show ?case by this
qed
qed
Email Gateway (Aug 22 2022 at 13:27):From: Rustom Mody <rustompmody@gmail.com>
Thanks Alfio, Daniel for your suggestions
Last updated: Apr 27 2024 at 01:05 UTC