I am struggling to understand why each of the examples below either works or doesn't work and more abstractly how induction interacts with tactics vs Isar. I'm working on 4.3 in Programming and Proving in Isabelle/HOL (Dec 2016) on Windows 10 with the latest Isabelle/HOL (2016-1)
There are 8 cases: the lemma is either long (includes explicit name) or short, structured (using assumes and shows) or unstructred (using the arrows) and the proof is either structured (Isar) or unstructured (tactical).
theory Confusing_Induction
imports Main
begin
(* 4.3 *)
inductive ev :: " nat ⇒ bool " where
ev0: " ev 0 " |
evSS: " ev n ⟹ ev (n + 2) "
fun evn :: " nat ⇒ bool " where
" evn 0 = True " |
" evn (Suc 0) = False " |
" evn (Suc (Suc n)) = evn n "
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)" arbitrary: " m " rule: ev.induct)
*)
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) " arbitrary: " m " rule: ev.induct)
case ev0
then show ?case sorry
next
case (evSS n)
then show ?case sorry
qed
*)
3. Structured long lemma & structured proof
(* And neither of these can apply the induction *)
(*
lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m "
proof (induction " n " arbitrary: " m " rule: ev.induct)
lemma assumes a1: " n = (Suc (Suc m)) " and a2: "ev n " shows " ev m "
proof (induction " n " arbitrary: " m " rule: ev.induct)
*)
(* But this one can ?! *)
(*
lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m "
proof -
from a1 and a2 show " ev m "
proof (induction " n " arbitrary: " m " rule: ev.induct)
case ev0
then show ?case by simp
next
case (evSS n) thus ?case by simp
qed
qed
*)
4. Unstructured long lemma & structured proof
(* And this is the manually expanded form of the Advanced Rule Induciton from 4.4.6 *)
lemma tmp: " ev n ⟹ n = (Suc (Suc m)) ⟹ ev m "
proof (induction " n " arbitrary: " m " rule: ev.induct)
case ev0 thus ?case by simp
next
case (evSS n) thus ?case by simp
qed
lemma " ev (Suc (Suc m)) ⟹ ev m "
using tmp by blast
**5. Structured short lemma & unstructured proof*
(* Also gets stuck/hangs *)
(*
lemma assumes a: " ev (Suc (Suc m)) " shows " ev m "
apply(induction "Suc (Suc m)" arbitrary: " m " rule: ev.induct)
*)
6. Unstructured short lemma & unstructured proof
(* This goes through no problem (``arbitrary: " m "`` seems to be optional, why?) *)
lemma " ev (Suc(Suc m)) ⟹ ev m "
apply(induction "Suc (Suc m)" arbitrary: " m " rule: ev.induct)
apply(auto)
done
7. Structured long lemma & unstructured proof
(* But both of these "fail to apply the proof method" *)
(*
lemma assumes a1: " n = (Suc (Suc m)) " and a2: " ev n" shows " ev m "
apply(induction " n " arbitrary: " m " rule: ev.induct)
lemma assumes a1: " ev n " and a2: " n = (Suc (Suc m)) " shows " ev m "
apply(induction " n " arbitrary: " m " rule: ev.induct)
*)
8. Unstructured long lemma & unstructured proof
lemma " ev n ⟹ n = (Suc (Suc m)) ⟹ ev m "
apply(induction " n " arbitrary: " m " rule: ev.induct)
apply(auto)
done
end
I posted this to the cl-isabelle-users@lists.cam.ac.uk and received the following response from Larry Paulson. I've reproduced it below.
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 method 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