Agda-交互式构建证明-如何使用hole语法?

对不起,这个奇怪的标题,我不知道这些概念实际上是如何命名的。

我在跟踪一个 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
  ∎

我的编辑说 { }1 是只读的。我不能删除它,只能在大括号之间插入东西。我可以强制删除它,但这显然不是有意的。

开始 阻止?像这样的

{ 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

两者似乎都不起作用