你是如何在伊莎贝尔/霍尔的战术/Isar中使用归纳的？
我很难理解为什么下面的每一个例子要么有效，要么不起作用，更抽象地说，归纳是如何与策略与Isar交互作用的。我正在用最新的Isabelle/HOL (2016-1)在Windows 10上编写和证明在Isabelle/HOL (2016年12月)上的4.3个程序。
有8种情况:引理要么是长的(包括显式名称)，要么是短的、结构化的(使用assumes和shows)或者是非结构化的(使用箭头)，证明要么是结构化的(Isar)，要么是非结构化的(战术)。
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.结构化短引理&结构化证明
(* 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.非结构化短引理&结构化证明
(* 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.结构化长引理&结构化证明
(* 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.非结构化长引理&结构化证明
(* 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.结构化短引理和非结构化证明*
(* 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.非结构化短引理&非结构化证明
(* 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)
done7.结构化长引理&非结构化证明
(* 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.非结构化长引理&非结构化证明
lemma " ev n ⟹ n = (Suc (Suc m)) ⟹ ev m "
apply(induction " n " arbitrary: " m " rule: ev.induct)
apply(auto)
done
end回答 1
Stack Overflow用户
发布于 2017-09-08 17:42:18
我把这篇文章发到了cl user@lists.cam.ac.uk，并收到了拉里·保尔森的以下回复。我把它复制到下面。
谢谢你的询问。你的一些问题与以正确的方式为归纳提供前提有关，但这里至少有两个大问题。
(* 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)这样做，你的假设是看不见的，目标只是“ev m”，所以归纳是不适用的。但是，这个错误会导致归纳方法循环，这是非常糟糕的。
(* 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在这里，你会发现错误“没有完善任何待定的目标”，这破坏了其他证据。你得到这个错误信息的原因是，由于某种原因，你拥有的目标和归纳方法认为你拥有的目标不匹配。事实上，这个证据可以直接写出来，但它的形状是非常出人意料的。这也是非常糟糕的。
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您的(3,7,8)是与您的(1)相同的问题，除了归纳方法(正确)失败。显然，"Suc (Suc M)“是由于某种原因导致归纳方法循环的，就像在您的(5)中一样。
(* 6. Unstructured short lemma & unstructured proof *)
(* This goes through no problem (``arbitrary: " m "`` seems to be optional, why?) *)简单地说，只有一些证明需要“任意”，即当归纳假设涉及需要泛化的变量时。
你的(7)可以写成这样：
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也就是说，你可以提供假设的证据，如所示(“使用”)。我们甚至能找到合适的案子这样做。
我们正处于一个新的发布阶段，但我希望有关归纳方法和非原子项的问题能够及时得到解决。
拉里·保尔森
https://stackoverflow.com/questions/46024686
复制相似问题
腾讯云开发者
