Agda - Building proofs interactively - How to use the hole syntax?

Question

Sorry for the strange title, I have no idea how these concepts are actually named.

I'm following an Agda tutorial and there's a section explaining how to build proofs inductively: https://plfa.github.io/Induction/#building-proofs-interactively

It's pretty cool that you can expand your proof step by step and have the hole (this { }0) update its contents to tell you what's going on. However, it is only explained how to do that when using the rewrite syntax.

How does this work when I want to "manually" do the proof within a begin block, for example:

+-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)
  ∎

The problem is the following. Let's start with the proposition and start of the evidence:

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc m n p = ?

This evaluates to:

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc m n p = { }0

In this case, I want to do a proof by induction, so I split these using C-c C-c using the variable m:

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p = { }0
+-assoc (suc m) n p = { }1

The base case is trivial and is replaced with refl after resolving it using C-c C-r. However, the inductive case (hole 1) needs some work. How can I turn this { }1 hole into the following structure to do the proof:

begin
  -- my proof
  ∎

My editor (spacemacs) says { }1 is read-only. I cannot delete it, only insert stuff between the braces. I can force-delete it but that's clearly not intended.

What are you supposed to do to expand the hole into a begin block? Something like this

{ begin }1

does not work and leads to an error message

Thanks!

EDIT:

Okay, so the following seems to work:

{ begin ? }1

This turns it into this:

+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-assoc zero n p = refl
+-assoc (suc m) n p = begin { }0

That's a progress :D. But now I can't figure out where to put the actual steps of the proof:

...
+-assoc (suc m) n p = begin (suc m + n) + p { }0
-- or
+-assoc (suc m) n p = begin { (suc m + n) + p }0

Neither seems to be working

"{ }1 is read-only" -- are you by any chance typing in the insert/overwrite mode? Typing in a hole is supposed to work indeed. You should type something like {begin ? ∎}, hit C-c C-SPC and that will reify the code. — user3237465
Sorry, maybe I wasn't clear about this: I can type stuff in between { and }, just the braces themselves are read-only. And writing { begin ? }1 actually does work (only without the \qed). It turns the text into begin { }1 which is progress :D But how do I continue? I can't figure out where to put the first step — Quantm
You should always fill a hole with an expression whose type is equal to the goal. (suc m + n) + p is a natural number, which is not the goal. Try to put (suc m + n) + p ≡⟨⟩ ? inside the hole. — user3237465

user3237465 user3237465 · Accepted Answer · 2020-05-14T11:47:30

{ }1 is read-only

This message is shown in two cases:

you're trying to delete a hole with backspace, which is not going to work. You can use C-backspace, though, if the hole is empty
you're trying to edit an empty hole in the insert/overwrite mode, which is also not going to work

A rule of thumb is that you always refine a hole with C-c C-SPC with an expression of the type that is equal to the goal. In your case this means starting with begin ?, then giving (suc m + n) + p ≡⟨⟩ ? and so on.

There are two ways to refine a hole:

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

Agda - Building proofs interactively - How to use the hole syntax?

1 Answers