在本例中证明 Isabelle/HOL 中存在

Question

我正在尝试学习如何将 Isabelle/Isar 与 HOL 一起使用，我决定一个好的方法是发展一些初等数论。我定义了自己的加号和乘号操作，这样证明方法就不会为我做所有的工作，因为在 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"

Answer 1

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

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 官方文档的一部分。另外，我想推荐以下资源："Concrete Semantics with Isabelle/HOL" Tobias Nipkow 和 Gerwin Klein 以及 "A Proof Assistant for Higher-Order Logic" Tobias Nipkow 等人

问题陈述修改后的更新

下面的清单给出了一个仅依赖最基本方法和直接规则应用的证明：

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)

在本例中证明 Isabelle/HOL 中存在

Proving existence in Isabelle/HOL in this example

isabelle