如何在 Isabelle/HOL 中使用 tactics/Isar 进行归纳？

Question

我正在努力理解为什么下面的每个示例都有效或无效，更抽象地说，归纳法与战术 vs Isar 是如何相互作用的。我正在 Isabelle/HOL（2016 年 12 月）在 Windows 10 上使用最新的 Isabelle/HOL（2016-1）

进行编程和验证中的 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

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

我们正处于新的发布阶段，希望归纳法和非原子项的问题能尽快解决。

拉里保尔森

如何在 Isabelle/HOL 中使用 tactics/Isar 进行归纳？

How do you use induction with tactics/Isar in Isabelle/HOL?

theorem-proving

proofs

isabelle