Email Gateway (Aug 22 2022 at 16:01): Email Gateway (Aug 22 2022 at 16:01):From: Dhruv Makwana <dcm41@cam.ac.uk>
Hello,
I’m new to Isabelle/HOL and working through Prog & Proving. I’m nearly at the end but this example has troubled me a lot (4.3, prove ev (Suc (Suc m)) ==> ev m). I posted the full question to https://stackoverflow.com/questions/46024686/how-do-you-use-induction-with-tactics-isar-in-isabelle-hol so that it is easier to search for the answer for the next beginners, but have included the file here
Thanks,
Dhruv
Confusing_Induction.thy
Email Gateway (Aug 22 2022 at 16:04):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for your query. Some of your problems have to do with supplying premises to the induction in the correct way, but there are at least two big problems here.
(* 1. Structured short lemma & structured proof *)
(* Hangs/gets stuck/loops on the following *)
lemma assumes a: "ev (Suc(Suc m))” shows "ev m"
proof(induction "Suc (Suc m)" rule: ev.induct)
Doing it this way, your assumption is not visible, the goal is simply “ev m”, so induction isn’t applicable. But it’s absolutely bad that this mistake causes the induction lemon to loop.
(* 2. Unstructured short lemma & structured proof *)
(* And this one ends up having issues with
"Illegal application of proof command in state mode" *)
lemma "ev (Suc (Suc m)) ⟹ ev m"
proof(induction "Suc (Suc m)" rule: ev.induct)
case ev0
then show ?case
sorry
next
case (evSS n)
then show ?case sorry
qed
Here you are getting the error "Failed to refine any pending goal”, which breaks the rest of the proof. The reason you are getting this error message is that for some reason there is a mismatch between the goals you have and the goals that the induction methods thinks you have. In fact this proof can be written straightforwardly, but its shape is quite unexpected. This is also very bad.
lemma "ev (Suc (Suc m)) ⟹ ev m"
proof(induction "Suc (Suc m)" rule: ev.induct)
show "⋀n. ev n ⟹
(n = Suc (Suc m) ⟹ ev m) ⟹
n + 2 = Suc (Suc m) ⟹ ev m"
by simp
qed
Your (3,7,8) is the same problem as your (1) except that the induction method (correctly) fails. Clearly the argument "Suc (Suc m)” is causing the induction method to loop for some reason, as in your (5).
(* 6. Unstructured short lemma & unstructured proof *)
(* This goes through no problem (arbitrary: " m " seems to be optional, why?) *)
It is simply that only some proofs need “arbitrary”, namely when the induction hypothesis involves variables that need to be generalised.
Your (7) can be written like this:
lemma assumes "ev n" and " n = (Suc (Suc m)) " shows " ev m "
using assms
proof(induction " n " arbitrary: " m " rule: ev.induct)
case ev0
then show ?case
sorry
next
case (evSS n)
then show ?case
sorry
qed
That is, you can supply the assumptions to the proof as shown (“using”). We even get the right cases doing it this way.
We are in a new release phase, but I hope that the problems involving the induction method and non-atomic terms can be fixed promptly.
Larry Paulson
Email Gateway (Aug 22 2022 at 16:04):From: Dhruv Makwana <dcm41@cam.ac.uk>
Thank you very much! From what I can infer, structured assumes/shows aren’t the same as “==>” meta-logical arrows but can be massaged into that using the “using” keyword.
I have copied your answer to Stack Exchange so that others may find it easily.
Dhruv
Thanks for your query. Some of your problems have to do with supplying premises to the induction in the correct way, but there are at least two big problems here.
(* 1. Structured short lemma & structured proof *)
(* Hangs/gets stuck/loops on the following *)
lemma assumes a: "ev (Suc(Suc m))” shows "ev m"
proof(induction "Suc (Suc m)" rule: ev.induct)
Doing it this way, your assumption is not visible, the goal is simply “ev m”, so induction isn’t applicable. But it’s absolutely bad that this mistake causes the induction lemon to loop.
(* 2. Unstructured short lemma & structured proof *)
(* And this one ends up having issues with
"Illegal application of proof command in state mode" *)
lemma "ev (Suc (Suc m)) ⟹ ev m"
proof(induction "Suc (Suc m)" rule: ev.induct)
case ev0
then show ?case
sorry
next
case (evSS n)
then show ?case sorry
qed
Here you are getting the error "Failed to refine any pending goal”, which breaks the rest of the proof. The reason you are getting this error message is that for some reason there is a mismatch between the goals you have and the goals that the induction methods thinks you have. In fact this proof can be written straightforwardly, but its shape is quite unexpected. This is also very bad.
lemma "ev (Suc (Suc m)) ⟹ ev m"
proof(induction "Suc (Suc m)" rule: ev.induct)
show "⋀n. ev n ⟹
(n = Suc (Suc m) ⟹ ev m) ⟹
n + 2 = Suc (Suc m) ⟹ ev m"
by simp
qed
Your (3,7,8) is the same problem as your (1) except that the induction method (correctly) fails. Clearly the argument "Suc (Suc m)” is causing the induction method to loop for some reason, as in your (5).
(* 6. Unstructured short lemma & unstructured proof *)
(* This goes through no problem (arbitrary: " m " seems to be optional, why?) *)
It is simply that only some proofs need “arbitrary”, namely when the induction hypothesis involves variables that need to be generalised.
Your (7) can be written like this:
lemma assumes "ev n" and " n = (Suc (Suc m)) " shows " ev m "
using assms
proof(induction " n " arbitrary: " m " rule: ev.induct)
case ev0
then show ?case
sorry
next
case (evSS n)
then show ?case
sorry
qed
That is, you can supply the assumptions to the proof as shown (“using”). We even get the right cases doing it this way.
We are in a new release phase, but I hope that the problems involving the induction method and non-atomic terms can be fixed promptly.
Larry Paulson
Email Gateway (Aug 22 2022 at 16:04):From: Tobias Nipkow <nipkow@in.tum.de>
A remark about example 2. There is no "real" problem here. The confusion arises
because the proof outline suggested by Isabelle is too simplistic: the case
"ev0" has already been proved internally because 0 ~= Suc(Suc _). If you delete
that case, the second one is fine and you don't need to state a complicated
goal. It would be helpful if Isabelle complained about a proof that contains a
case that has already been proved.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 16:04):From: Lawrence Paulson <lp15@cam.ac.uk>
On 8 Sep 2017, at 18:38, Dhruv Makwana <dcm41@cam.ac.uk> wrote:
Thank you very much! From what I can infer, structured assumes/shows aren’t the same as “==>” meta-logical arrows but can be massaged into that using the “using” keyword.
They express the same theorem statement but create different proof states.
I have copied your answer to Stack Exchange so that others may find it easily.
Fine, but please change "induction lemon” to “induction method” (speech recognition artefact).
LP
Last updated: Nov 21 2024 at 12:39 UTC