归纳两个变量？

Question

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

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 似乎也是一个归纳变量候选。对于如何继续进行此证明的任何帮助，我将不胜感激。

Answer 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

归纳两个变量？

Induct on two variables?

induction

isabelle