Interacting in agda-mode with agda?

Question

It feels super awkward to interact with agda.

Consider the proof state:

_ = begin
  5 ∸ 3
  ≡⟨⟩
   4 ∸ 2 ≡⟨⟩
   3 ∸ 1 ≡⟨⟩
   2 ∸ 0 ≡⟨⟩  { 2 <cursor-goes-here> }0

When I type C-c C-l (type-check), it says

?0 : 2 ∸ 0 ≡ _y_131
_y_131 : ℕ  [ at /home/bollu/work/plfa/src/plfa/part1/Naturals.lagda.md:586,5-10 ]

which doesn't seem like a great error? Nor does a refine (C-c C-r) give me a good error message: It only tells me:

cannot refine

1. How do I get adga to tell me:

You've finished the proof, except for a missing \qed

2. In general, what is the "preferred mode of interaction" when building proofs?

Answer 1

The overall issue

Your post starts by the following assumption:

It feels super awkward to interact with agda.

The reason that could explain your feeling is that you seem to assume that Agda can both infer a term and its type, in other words, both the property you wish to prove and a proof of it. Agda can often do one of these, but asking for both does not make much sense. As a comparison, imagine being on a bench in a park, when a complete strangers comes and sits next to you, saying nothing. You can see he would very much enjoy to ask you something, but, despite your efforts at making him speak, he remains silent. After a few minutes, the stranger yells at you that, despite him being thirsty, you did not bring the drink he was expected. In this metaphor, the stranger is you, and you are Agda. There is no way you could have known he was thirsty, and even less bring him his drink.

Concretely

You gave the following piece of code:

_ = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩  { 2 <cursor-goes-here> }0

This piece of code lacks a type signature which will allow Agda to help you more. Agda tells you so when you type check by providing you with the inferred type of the goal:

?0 : 2 ∸ 0 ≡ _y_131
_y_131 : ℕ  [ at /home/bollu/work/plfa/src/plfa/part1/Naturals.lagda.md:586,5-10 ]

Here Agda says that your proof goal is that 2 ∸ 0 is equal to some unknown natural number y. This number being unknown there is very little chance Agda can help you go further in your proof effort because it does not even know what you wish to prove. As far as it knows, your goal could turn out to be 5 ∸ 3 ≡ 3 for wish there exists no proof term.

Getting back to our metaphor, you lacks the statement "I am thirsty". Should the stranger provide this piece of information, you could - possibly - react, which means Agda can try and help.

The solution

I'm assuming you wish to prove that the result of your subtraction is two, in which case the code is as follows:

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ {!!}

In this case, you can interact with Agda in various ways, which all lead to Agda providing you with a sound proof term:

You can call Agsy to solve the problem for you (CTRL-c CTRL-a), which leads to:

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ refl

You can try and refine the goal directly (CTRL-c CTRL-r), asking Agda if there exists any unique constructor which has the right type, which leads to the same:

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ refl

If you wish to wrap up your proof using \qed you can try and input _∎ into the hole after which refining (CTRL-c CTRL-r) gives:

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ {!!} ∎

Calling Agsy in the resulting goal naturally gives:

test : 5 ∸ 3 ≡ 2
test = begin
  5 ∸ 3 ≡⟨⟩
  4 ∸ 2 ≡⟨⟩
  3 ∸ 1 ≡⟨⟩
  2 ∸ 0 ≡⟨⟩ 2 ∎