抱歉标题有点奇怪,我不知道这些概念的实际名称。
我正在跟随一个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
在这种情况下,我想进行归纳证明,因此我使用变量m
使用C-c C-c
将它们拆分成多个部分:
+-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
似乎两者都没有起作用。
{ }1
is read-only" -- 你是不是在输入/覆盖模式下输入?在一个洞中输入确实应该有效。你应该输入类似{begin ? ∎}
的内容,然后按下C-c C-SPC
来实现代码化。 - effectfullybegin { }1
,这是进展 :D 但是接下来该怎么办呢?我无法弄清楚应该在哪里放置第一步。 - SwiftedMind(suc m + n) + p
是一个自然数,但它并不是我们的目标。尝试将(suc m + n) + p ≡⟨⟩ ?
放入空缺中。 - effectfully