An agda proposition used in the type -- what does it mean?

Question

The p in your example is the proof that the number you're dividing (n) is indeed even. When you want to divide a number using your div function, it is not sufficient to only give the number! Agda represents that by giving you back another function - a function which consumes a proof that 2 is even and gives back 1.

Let's write a few tests to see how it works:

test₁ : ℕ
test₁ = div 4 ?

The type of the hole in this case is, unsuprisingly, ⊤. even 4 reduces to ⊤ in two steps, so you can easily fill in the empty record or just give an underscore - there's only one possible value and Agda can fill that in:

test₁ = div 4 _

When, on the other hand, you give it an odd number, for example:

test₂ : ℕ
test₂ = div 3 ?

The type of the hole reduces to ⊥. ⊥ is the empty type; giving a value of such type amounts to proving a contradiction in your logic. So we're stuck here - which is exactly what we wanted.

Now, you'd like to make it feel a bit more... implicit and perhaps introduce a compilation error when we try to give it an odd number.

Agda can fill in the implicit stuff only via unification. While the unification can do some complicated stuff, there are some problems it cannot help with; guessing proofs is one of them. If we want to keep the proof implicit, we have to keep it simple. even is a fine example: we can compute it completly just from the number we're dividing and it gives back either ⊤ (which can be trivially filled in) or ⊥ (which means there's something wrong).

div-implicit : (n : ℕ) {p : even n} → ℕ
div-implicit n {p} = div n p

Even numbers are fine:

test₃ : ℕ
test₃ = div-implicit 4

Odd numbers give a compilation error, see my previous answer on this matter. We get bright yellow and I-don't-know-what-to-fill-in error:

___10 : ⊥  [ at D:\Agda\SO6.agda:27,9-23 ]

Here's a cookbook on how to make trivial proof obligations guessable by Agda:

Firstly, we need a function which determines whether the argument is okay. Usually, this is a function returning a Bool or Dec.

check : ℕ → Bool

Next, we transform the Bool into a proposition:

-- The Bool is true.
True : Bool → Set
True true  = ⊤
True false = ⊥

-- The Bool is false.
False : Bool → Set
False true  = ⊥
False false = ⊤

And finally, we can include an implicit argument that Agda will fill in if the arguments are okay or give back bright yellow:

f : (n : ℕ) {p : True (check n)} → ℕ

Agda allows you to omit right hand side of a function equation if you find that one of the arguments doesn't make sense, so to speak. More technically, when you write down a () as a pattern, you're asserting that there's no way anyone could provide argument of that type - and if no-one can actually call the functions with those arguments, why bother writing a right hand side? Consider an example:

f : (m n : ℕ) → m ≡ n → ℕ
f zero (suc zero) p = ?
f _ _ _ = ?

What is the type of p? It is a proof that 0 ≡ 1 - which is obviously a nonsense, no-one can possibly call f 0 1 and give a proof that 0 ≡ 1. We are justified to replace p with () and leave out the right hand side:

f zero (suc zero) ()

Applying this to the div example:

div (suc zero) p = ?

Now, the type of p is ⊥. There's no way anyone could give a value of type ⊥. So again, we inform Agda this case is impossible:

div (suc zero) ()

Now, what are those question marks? The nice thing about agda-mode is that it helps you build your program in a cooperative manner. When you write a ? somewhere, you're telling agda-mode "I don't know what goes here, let's find out together".

When you then check the file via C-c C-l Agda takes those ?s and turns them into holes (these are the { }0 you're seeing). You can have more than one hole in a program, which explains the number behind.

Now, I said these allow you to build program in cooperative manner, where's the cooperation? There's a number of actions you can do with a hole. You can for example ask its type (via C-c C-,):

div : (n : ℕ) → even n → ℕ
div zero          p  = zero
div (suc (suc n)) p  = { }0
div (suc zero)    ()

-- Agda information buffer
Goal: ℕ
————————————————————————————————————————————————————————————
p : even n
n : ℕ

These three lines tell you that you ultimately have to write down an expreesion of type ℕ (the goal) and in scope you have p of type even n and n of type ℕ.

You can even write stuff inside the hole and ask what's the type of what you've currently written (via C-c C-.):

div (suc (suc n)) p = {n }0

-- Agda information buffer
Goal: ℕ
Have: ℕ
————————————————————————————————————————————————————————————
p : even n
n : ℕ

When you are satisfied, you can replace the hole with whatever you've written inside (well, as long as it typechecks) via C-c C-space.

If you don't care about the implementation (for example, you're writing a proof and anything will do), you can also tell Agda to try to guess it by C-c C-a. This is very useful when you have plenty of trivial cases.

And then there's case split. When you write a function you usually have to do pattern matching to learn more about the arguments. Agda allows you to save some of the pain of manually writing all those function equations.

_+_ : (m n : ℕ) → ℕ
m + n = { }0

We write a variable on which we want to do a case split inside the hole:

_+_ : (m n : ℕ) → ℕ
m + n = {m }0

And press the magical C-c C-c and voila:

_+_ : (m n : ℕ) → ℕ
zero + n = { }0
suc m + n = { }1