这个伊莎贝尔证明有什么问题？

Question

此模式生成器在给定位置生成一个给定数字的列表，所有其他值为零。

fun pattern_one_value :: "nat ⇒ nat ⇒ nat ⇒ nat ⇒ nat list" where
"pattern_one_value _   _    _   0   = []" |
"pattern_one_value pos pos1 val lng = 
    (if pos = pos1 then val else 0) # (pattern_one_value pos (pos1 + 1) val (lng - 1))"

以下引理旨在证明生成的列表在给定位置包含正确的值。

lemma pattern_one_value_check [simp]: "∀pos val. pos < lng ⟹ pattern_one_value pos 0 val lng ! pos = val"
    proof(induct lng)
        case 0         then show ?case by simp
    next
        case (Suc lng) then show ?case by auto
    qed

看来证明是正确的；然而，将生成函数的 cons 表达式中的 val 更改为任意数字，如 (if pos = pos1 then 7 else 0) # ...，证明仍然成立，因为基础假设和归纳假设都是错误的。我哪里错了？感谢您的帮助。

Answer 1

It seems to be a correct proof; however, changing val in the cons expression of the generator function into an arbitrary number like (if pos = pos1 then 7 else 0) # ..., the proof still holds because both the base and the induction hypothesis are false. Where am I wrong?

我认为问题与将 HOL 的全称量词 ∀ 等同于 Pure 的全称量词 ⋀ 的尝试有关。实际上，如您的问题所述，可以从定理 pattern_one_value_check 的前提证明任何事情。确实：

lemma pattern_one_value_check'[simp]:
  "(∀pos val::nat. pos < (lng::nat)) = False"
  by auto

lemma pattern_one_value_check''[simp]: 
  "(∀pos val::nat. pos < (lng::nat)) ⟹ P"
  by auto

我相信您打算在定理的陈述中使用 Pure 的全称量化，例如

lemma pattern_one_value_check [simp]: 
  "⋀pos val. pos < lng ⟹ pattern_one_value pos 0 val lng ! pos = val"
proof(induct lng)
  case 0 then show ?case by simp
next
  case (Suc lng) then show ?case sorry
qed

其实连这个都没有必要。以下定理一旦被证明，将在上下文中与上述定理相同：

lemma pattern_one_value_check' [simp]: 
  "pos < lng ⟹ pattern_one_value pos 0 val lng ! pos = val"
proof(induct lng)
  case 0 then show ?case by simp
next
  case (Suc lng) then show ?case sorry
qed

如果您寻求更详细的解释，请参阅 Isar-ref 中的第 2.1 节和文档 "Programming and Proving in Isabelle/HOL"，两者都是官方文档的一部分。

作为旁注，我不得不提一下，也许有更简单的方法来定义 pattern_one_value。在这种情况下，pattern_one_value_check的证明也似乎更容易：

definition pattern_one_value :: "nat ⇒ nat ⇒ nat ⇒ nat list"
  where "pattern_one_value val pos len = list_update (replicate len 0) pos val"

lemma pattern_one_value_check:
  assumes "pos < len" 
  shows "pattern_one_value val pos len ! pos = val"  
  using assms unfolding pattern_one_value_def
  apply(induct len)
  subgoal by auto
  subgoal by (metis length_replicate nth_list_update)
  done

这个伊莎贝尔证明有什么问题？

What is wrong with this Isabelle proof?

isabelle