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

Question

对不起，标题奇怪，我不知道这些概念的实际命名方式。

我正在学习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

[基本情况很简单，在使用refl解决后将其替换为C-c C-r。但是，感应外壳（孔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

似乎都没有用

Answer 1

{ }1为只读

此消息在两种情况下显示：

• 您正在尝试删除带有退格键的孔，该孔将无法正常工作。但是，如果孔为空，则可以使用C-backspace
• 您正在尝试在插入/覆盖模式下编辑一个空洞，这同样行不通

经验法则是，您始终使用C-c C-SPC精制一个孔，且该孔的类型等于目标。在您的情况下，这意味着从begin ?开始，然后给出(suc m + n) + p ≡⟨⟩ ?，依此类推。

有两种方法可以缩小孔：

• C-c C-r：在给定功能时为您创建新的孔。例如。使用此设置：

  test : Bool
  test = {!!}
  

  如果在孔中键入not，则>

  test : Bool
  test = {!not!}
  并优化，您将得到

  test : Bool
  test = not {!!}
  即将自动为参数创建新的孔。

  [通过这种方式或完善的漏洞，Agda还会按照自己喜欢的方式重新格式化您的代码，我不喜欢这种方式，因此我通常不使用它。

• C-c C-SPC：不会为参数创建新的孔，也不会重新格式化您的代码