如何为参数化归纳集编写自定义归纳规则？应用遇不可证分支

嘿，看起来你在Isabelle里自定义归纳规则时遇到了额外分支的麻烦——我之前也碰到过类似的情况，多半是归纳规则的结构或者应用方式没踩对Isabelle的预期。咱们一步步来捋清楚：

1. 先看自动生成的归纳原理（找基准） #

首先，你可以先查一下Isabelle为你的iterate归纳集自动生成的归纳原理，敲thm iterate.induct就能看到：

iterate f x y ⟹
(⋀a. P a a) ⟹
(⋀a b c. f a b ⟹ iterate f b c ⟹ P b c ⟹ P a c) ⟹
P x y

哎，这不和你写的my_iterate_induct几乎一模一样？那问题大概率出在证明自定义规则的过程或者应用归纳规则的方式上。

先确认你证明my_iterate_induct的方法对不对——正确的做法应该直接复用自动生成的归纳原理，比如：

theorem my_iterate_induct:
  "iterate f x y ⟹ (⋀a. P a a) ⟹ (⋀a b c. f a b ⟹ iterate f b c ⟹ P b c ⟹ P a c) ⟹ P x y"
  using iterate.induct by simp

这样证出来的定理和系统自动生成的完全一致，不会带额外的隐藏假设。

2. 排查应用时的额外分支 #

如果你用induction rule: my_iterate_induct时出现多余分支，十有八九是没明确指定归纳变量。比如你有个目标：

lemma "iterate f a b ⟹ Q a b"

正确的调用方式得明确告诉Isabelle对哪两个变量归纳：

apply (induction a b rule: my_iterate_induct)

或者更精准地绑定参数：

apply (induction rule: my_iterate_induct[of f a b Q])

要是省略了变量，Isabelle会自动泛化所有可能的变量，自然就多出没必要的分支了。

3. 自定义归纳规则的常见坑点 #

我整理了几个容易踩的坑，你可以对照检查：

• 量词顺序错配：归纳步骤里的⋀a b c顺序得和构造子iter_step的参数顺序对应——你的构造子是f a b ⇒ iterate f b c ⇒ iterate f a c，所以归纳假设的顺序是对的，这点没问题。
• 证明时引入额外假设：要是你证明my_iterate_induct时用了assume或者其他带额外条件的战术，定理里会藏着看不见的假设，应用时就会多出分支。
• 归纳变量没绑定：目标里的变量如果有未约束的情况，Isabelle会尝试泛化，导致分支爆炸。

4. 完整可运行的示例 #

我写了个完整的示例，你可以照着试：

inductive iterate :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for f where
iter_refl [simp]: "iterate f a a" |
iter_step [elim]: "f a b ⟹ iterate f b c ⟹ iterate f a c"

-- 自定义归纳规则（正确证明方式）
theorem my_iterate_induct:
  "iterate f x y ⟹ (⋀a. P a a) ⟹ (⋀a b c. f a b ⟹ iterate f b c ⟹ P b c ⟹ P a c) ⟹ P x y"
  using iterate.induct by simp

-- 测试自定义归纳规则的应用
lemma test_iterate:
  assumes "iterate f x y"
  shows "iterate f y x ⟹ iterate f x x"
proof (induction x y rule: my_iterate_induct)
  case (1 a)
  show ?case by simp  -- 对应自反构造子的情况
next
  case (2 a b c)
  -- 这里是归纳步骤，对应iter_step构造子
  assume "f a b" "iterate f b c" "iterate f c b ⟹ iterate f b b" "iterate f y x"
  ultimately show ?case by (auto intro: iter_step)
qed

这个示例里应用自定义归纳规则后，只会出现两个分支，正好对应iter_refl和iter_step，不会有多余的无法证明的分支。

最后再排查一遍 #

要是还是有问题，你可以检查这几点：

1. 证明my_iterate_induct时是不是用了带额外条件的战术，导致定理有隐藏假设；
2. 应用induction时有没有明确指定归纳变量；
3. 目标里的变量是不是都有约束，有没有未泛化的自由变量。

内容的提问来源于stack exchange，提问作者Zyzzyva