你如何在 Isabelle/HOL 中将归纳与战术/Isar 结合使用？

Question

我很难理解为什么下面的每个示例都有效或无效，以及更抽象地说，归纳与战术与 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)
  done

7.结构化长引理和非结构化证明

(* 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

Answer 1

我将此发布到 cl-isabelle-users@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

也就是说，您可以为证明提供假设，如图所示（“使用”）。我们甚至可以通过这种方式获得正确的案例。

我们处于新的发布阶段，但我希望能够及时修复涉及归纳方法和非原子术语的问题。

拉里·保尔森