对两个变量进行归纳？答案

【问题标题】：Induct on two variables?对两个变量进行归纳？
【发布时间】：2019-03-02 18:14:42
【问题描述】：

给定一个生成相同项目列表的函数，我希望证明生成的列表在所有位置都包含给定的自然数，与列表长度无关。

fun pattern_n :: "nat ⇒ nat ⇒ nat list" where
"pattern_n _ 0  = []" |
"pattern_n n lng = n # (pattern_n n (lng - 1))"

lemma pattern_n_1: "lng > 0 ∧ pos ≥ 0 ∧ pos < lng ∧ n ≥ 0 ⟹ (pattern_n n lng ! pos) = n"

很明显，证明应该基于对生成列表长度的归纳，但 pos 似乎也是一个归纳变量候选者。对于如何继续进行此证明，我将不胜感激。

【问题讨论】：

到目前为止您尝试过什么？什么不起作用/你被困在哪里？尝试按照您认为正确的方式应用归纳法。会发生什么？
ThreeFx，我尝试通过 apply(induction lng absolute: n) 和 apply(simp) 对 lng 进行归纳，之后 Isabelle 仍然需要对归纳步骤进行证明。对于像 pattern_n 这样的简单函数，还可以添加哪些知识来证明归纳步骤？我唯一的想法是项目位置也应该用作归纳变量。

标签： isabelle induction

【解决方案1】：

函数pattern_n等价于标准库中的函数replicate（理论List）。标准库还包含函数replicate 的定理nth_replicate，它与您要证明的定理几乎相同：

fun pattern_n :: "nat ⇒ nat ⇒ nat list" where
  "pattern_n _ 0  = []" |
  "pattern_n n lng = n # (pattern_n n (lng - 1))"
    
lemma "pattern_n n k = replicate k n"
  by (induction k) auto
    
thm nth_replicate

更新

或者，您可以使用归纳法来证明结果。通常使用下面函数pattern_n'提供的形式定义会更方便，因为定义函数时自动生成的定理更符合这种形式。

fun pattern_n :: "nat ⇒ nat ⇒ nat list" where
  "pattern_n _ 0  = []" |
  "pattern_n n lng = n # (pattern_n n (lng - 1))"

fun pattern_n' :: "nat ⇒ nat ⇒ nat list" where
  "pattern_n' n 0  = []" |
  "pattern_n' n (Suc lng) = n # (pattern_n' n lng)"

lemma "pattern_n n lng = pattern_n' n lng"
  by (induct lng) auto

lemma pattern_n_1_via_replicate: 
  "pos < lng ⟹ (pattern_n val lng) ! pos = val"
proof(induct lng arbitrary: pos)
  case 0 then show ?case by simp
next
  case (Suc lng) then show ?case by (fastforce simp: less_Suc_eq_0_disj)
qed

伊莎贝尔版本：伊莎贝尔2020

【讨论】：

xanonec，感谢您的回答，但不幸的是，这并不能帮助我理解要点。我正在研究比这个更复杂的模式生成器，这样复制就不能作为替代品。
@AttilaKaroly 感谢您的评论。我提供了更新。此外，使用我的第一个答案来推断标准库中用于证明相同定理的方法可能对您仍然有用。
xanonec，pattern_n_1_via_replicate 是我要找的。感谢您的热心帮助。
另一个问题：我在哪里可以了解更多关于less_Suc_eq_0_disj 等规则的信息？我在 Isabelle 的资料中没有发现任何关于此的内容，其他类似的规则似乎记录得非常松散。
@AttilaKaroly less_Suc_eq_0_disj 在理论Nat 中定义。如果您不知道，如果您使用 jEdit，那么您应该能够将鼠标悬停在证明中的 less_Suc_eq_0_disj 上并使用 cntrl+lmb（可能因操作系统不同而不同）快速导航到规则所在的理论指定的。作为旁注，有许多不同的方法可以证明您想要证明的定理。也许，如果您从标准库中研究 nth_replicate 的证明，就可以推断出最好的方法，正如我在第一条评论中已经提到的那样。