Email Gateway (Aug 18 2022 at 10:42): Email Gateway (Aug 18 2022 at 10:42):From: Tim Newsham <newsham@lava.net>
[possible duplicate, I jumped the gun on sending the first before I was
properly subscribed].
I'm trying to prove a simple proof related to the "reverse" proof
in the tutorial (I have the rest of the tutorial theory here
as well including lemmas app_Nil2, app_assoc, rev_app and rev_rev):
--- snip ---
revH :: "'a list => 'a list => 'a list"
primrec
"revH [] ys = ys"
"revH (x # xs) ys = revH xs (x # ys)"
...
lemma rev_revH: "revH xs ys = rev xs @ ys"
apply(induct_tac xs)
apply(auto)
done
lemma rev_rev2: "rev xs = revH xs []"
apply(induct_tac xs)
apply(auto)
done
--- snip ---
when I evaluate the first lemma it is able to automatically reduce the problem
to the goal:
forall a list.
revH list ys = rev list @ ys ==>
revH list (a # ys) = rev list @ a # ys
To me this seems to imply that this is solved, but I guess Isabelle doesn't see
it that way. I tried to strengthen the proof by saying
"!! ys ." but that didn't seem to have any effect. What do I need to
do here to complete this proof?
Tim Newsham
http://www.thenewsh.com/~newsham/
Email Gateway (Aug 18 2022 at 10:43):From: Amine Chaieb <chaieb@in.tum.de>
In general it is much better to use the "induct" method insead of the
induct_tac. In your case you need to generalize over ys, since in the
recursive call ys is modified by revH.
The following works for me:
lemma rev_revH: "revH xs ys = rev xs @ ys"
by (induct xs arbitrary: ys, auto)
If you insist on induct_tac:
lemma rev_revH: "ALL ys. revH xs ys = rev xs @ ys"
apply (induct_tac xs)
apply simp_all
done
Amine.
Tim Newsham wrote:
Email Gateway (Aug 18 2022 at 10:43):From: Tim Newsham <newsham@lava.net>
lemma rev_revH: "revH xs ys = rev xs @ ys"
by (induct xs arbitrary: ys, auto)
when I try this I get
*** Error in method "HOL.induct":
*** method "induct": bad arguments
*** : ys
*** At command "by".
using the FreeBSD packages isabelle-2005 and proofgeneral-xemacs-3.6.
(I also tried without the colon and got a different error).
If you insist on induct_tac:
lemma rev_revH: "ALL ys. revH xs ys = rev xs @ ys"
apply (induct_tac xs)
apply simp_all
done
It's not so much that I insist as I was unaware that there is a separate
"induct" :) This worked fine for me and was what I was going for with my
"strengthened proof" I mentioned earlier. I thought (incorrectly) that
"!! ys ." would do what "ALL ys ." does. Its still not clear to me
what the difference is, and I guess I need to read up on this some more.
Amine.
Tim Newsham wrote:
[possible duplicate, I jumped the gun on sending the first before I was
properly subscribed].I'm trying to prove a simple proof related to the "reverse" proof
in the tutorial (I have the rest of the tutorial theory here
as well including lemmas app_Nil2, app_assoc, rev_app and rev_rev):--- snip ---
revH :: "'a list => 'a list => 'a list"primrec
"revH [] ys = ys"
"revH (x # xs) ys = revH xs (x # ys)"
...lemma rev_revH: "revH xs ys = rev xs @ ys"
apply(induct_tac xs)
apply(auto)
donelemma rev_rev2: "rev xs = revH xs []"
apply(induct_tac xs)
apply(auto)
done
--- snip ---when I evaluate the first lemma it is able to automatically reduce the
problem to the goal:forall a list.
revH list ys = rev list @ ys ==>
revH list (a # ys) = rev list @ a # ysTo me this seems to imply that this is solved, but I guess Isabelle doesn't
see it that way. I tried to strengthen the proof by saying
"!! ys ." but that didn't seem to have any effect. What do I need to
do here to complete this proof?Tim Newsham
http://www.thenewsh.com/~newsham/
Tim Newsham
http://www.thenewsh.com/~newsham/
Last updated: May 03 2024 at 08:18 UTC