Agda - 交互式构建证明 - 如何使用洞语法？

Question

Agda - 交互式构建证明 - 如何使用洞语法？

agdaagda-mode

3

抱歉标题有点奇怪，我不知道这些概念的实际名称。

我正在跟随一个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

似乎两者都没有起作用。

- SwiftedMind

我正在使用 spacemacs。我在插入模式下输入（使用 vim 模式）。 - SwiftedMind

1

"{ }1 is read-only" -- 你是不是在输入/覆盖模式下输入？在一个洞中输入确实应该有效。你应该输入类似{begin ? ∎}的内容，然后按下C-c C-SPC来实现代码化。 - effectfully

抱歉，也许我没有表达清楚：我可以在 { 和 } 之间输入内容，只是花括号本身是只读的。而且写 { begin ? }1 确实有效（只是没有 \qed）。它会将文本转换为 begin { }1，这是进展 :D 但是接下来该怎么办呢？我无法弄清楚应该在哪里放置第一步。 - SwiftedMind

我已更新问题的当前状态。 - SwiftedMind

1

你应该始终使用类型与目标相等的表达式来填补空缺。(suc m + n) + p 是一个自然数，但它并不是我们的目标。尝试将 (suc m + n) + p ≡⟨⟩ ? 放入空缺中。 - effectfully

哦，这很有道理。非常感谢，现在它按照预期工作了！你想把你的两个评论作为答案吗？那么我可以接受它。 - SwiftedMind

1个回答

阿里云服务器只需要99元/年，新老用户同享，点击查看详情

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，

- effectfully · Accepted Answer

{ }1是只读的

出现此消息的情况如下：

您正在尝试使用退格键删除一个空洞，这是无法工作的。但如果为空洞，则可以使用C-backspace。
您正在尝试在插入/覆盖模式下编辑空洞，这也是不起作用的。

一个经验法则是，您始终使用与目标相等类型的表达式使用C-c C-SPC精炼空洞。在您的情况下，这意味着从begin?开始，然后给出(suc m + n) + p ≡⟨⟩ ?等。

有两种方法可以完善空洞：

C-c C-r: creates new holes for you when given a function. E.g. with this setup:
```
test : Bool
test = {!!}
```
if you type not in the hole
```
test : Bool
test = {!not!}
```
and refine, you'll get
```
test : Bool
test = not {!!}
```
i.e. the new hole is created automatically for the argument.

With this way or refining a hole Agda also reformats your code the way it prefers, which I don't like, so I usually don't use it.
C-c C-SPC: doesn't create new holes for arguments and doesn't reformat your code