时间戳

首页 > 解决方案 > 在这个例子中证明 Isabelle/HOL 的存在

isabelle - 在这个例子中证明 Isabelle/HOL 的存在

问题描述

我正在尝试学习如何将 Isabelle/Isar 与 HOL 一起使用，我决定一个好的方法是开发一些基本数论。我定义了自己的 plus 和 times 操作，这样证明方法就不会为我完成所有工作，因为在 Main 中已经有很多关于 +, * 的证明。我的版本定义为：

fun p:: "nat ⇒ nat ⇒ nat" (infix "⊕" 80) where
  p_0: "0 ⊕ n =n" |
  p_rec: " (Suc m) ⊕ n = Suc (m ⊕ n)"

fun t:: "nat ⇒ nat ⇒ nat" (infix "⊗" 90) where
  t_0: "0 ⊗ n= 0" |
  t_rec: "Suc m ⊗ n = n + m ⊗ n"

我已经证明了乘法和加法在分配律中是可交换的。然后我尝试显示以下内容：

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r"
proof (induction n)
  case 0
  have "0= 0 ⊗ m" by auto
  hence "∃q. 0 =q ⊗ m" by auto

但它告诉我它无法完成最后一步的证明。我尝试了各种方法，但我不知道如何告诉伊莎贝尔，我只是为我要证明的存在陈述作证。我怎样才能让伊莎贝尔认识到这一点？

编辑：

xanonec 帮助我完成了这一步，但我立即被一个看似相似的问题困在了下一步。最终我想展示：

"∃ q r. 0 = q ⊗ m⊕r"

但我不知道如何同时引入两个存在量化变量

"0 = 0 ⊗ m ⊕ 0"

标签： isabelle

解决方案

解决方案的合适策略可能是直接规则应用程序（在 jEdit 中，您可以cntrl+LMB 或cmd+LMB onexI导航到其语句）：

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r"
proof(induction n)
  case 0
  have "0 = 0 ⊗ m" by auto
  hence "∃q. 0 = q ⊗ m" by (rule exI)    
qed

更一般地说，在许多类似的情况下sledgehammer可以找到合适的（但通常是次优的）证明。使用教程sledgehammer是 Isabelle 官方文档的一部分。另外，我想推荐以下资源： Tobias Nipkow 和 Gerwin Klein 的“Concrete Semantics with Isabelle/HOL”和 Tobias Nipkow 等人的“A Proof Assistant for Higher-Order Logic”。

对问题陈述进行修改后的更新

以下清单提供了一个仅依赖于最基本方法和直接规则应用的证明：

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r"
proof (induction n)
  case 0 show ?case
  proof-
    have "0 = 0 ⊗ m ⊕ 0" by simp
    then have "∃r. 0 = 0 ⊗ m ⊕ r" by (rule exI)
    then show "∃q r. 0 = q ⊗ m ⊕ r" by (rule exI) 
  qed
  case (Suc n) show ?case sorry
qed

但是，如果您有能力更多地依赖证明自动化，那么您可以用它metis来证明整个定理：

lemma euclidean_division_existence: "∃q r. n=q⊗m⊕r" by (metis p_0 t_0)

推荐阅读