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

Answer 1

{ }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