【发布时间】：2020-05-14 19:47:30
【问题描述】：
对不起，奇怪的标题，我不知道这些概念实际上是如何命名的。
我正在关注Agda 教程，其中有一节解释了如何以归纳方式构建证明：https://plfa.github.io/Induction/#building-proofs-interactively
您可以逐步扩展您的证明并让漏洞（{ }0）更新其内容以告诉您发生了什么，这真是太酷了。但是，仅说明了使用 rewrite 语法时如何执行此操作。
当我想“手动”在 begin 块内进行证明时，这是如何工作的，例如：
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p =
begin
(zero + n) + p
≡⟨⟩ n + p
≡⟨⟩ zero + (n + p)
∎
+-assoc (suc m) n p =
begin
(suc m + n) + p
≡⟨⟩ suc (m + n) + p
≡⟨⟩ suc ((m + n) + p)
≡⟨ cong suc (+-assoc m n p) ⟩
suc (m + (n + p))
≡⟨⟩ suc m + (n + p)
∎
问题如下。让我们从命题和证据开始：
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc m n p = ?
计算结果为：
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc m n p = { }0
在这种情况下，我想通过归纳进行证明，所以我使用C-c C-c 使用变量m 拆分这些：
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p = { }0
+-assoc (suc m) n p = { }1
基本情况是微不足道的，在使用C-c C-r 解决后被refl 替换。但是，感应案例（孔 1）需要做一些工作。我怎样才能把这个{ }1洞变成下面的结构来做证明：
begin
-- my proof
∎
我的编辑器（spacemacs）说{ }1 是只读的。我不能删除它，只能在大括号之间插入东西。我可以强制删除它，但这显然不是故意的。
你应该怎么做才能把洞扩大成begin 块？像这样的
{ begin }1
不起作用并导致错误消息
谢谢！
编辑：
好的，所以以下似乎可行：
{ begin ? }1
这就变成了这样：
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p = refl
+-assoc (suc m) n p = begin { }0
这是一个进步 :D。但是现在我不知道在哪里放置证明的实际步骤：
...
+-assoc (suc m) n p = begin (suc m + n) + p { }0
-- or
+-assoc (suc m) n p = begin { (suc m + n) + p }0
似乎都没有工作
【问题讨论】：
-
我正在使用 spacemacs。我在插入模式下输入（使用 vim 模式）
-
"
{ }1是只读的" -- 您是否有机会在插入/覆盖模式下输入？在孔中打字应该确实有效。您应该输入类似{begin ? ∎}的内容，然后点击C-c C-SPC，这将具体化代码。 -
抱歉，我可能不太清楚：我可以在 { 和 } 之间输入内容，只是大括号本身是只读的。并写{开始？ }1 实际上确实有效（仅在没有 \qed 的情况下）。它将文本变成
begin { }1，这是进步:D 但是我该如何继续呢？我不知道该把第一步放在哪里 -
我用当前状态更新了问题
-
您应该始终使用类型等于目标的表达式来填充漏洞。
(suc m + n) + p是一个自然数，这不是目标。尝试将(suc m + n) + p ≡⟨⟩ ?放入孔内。