Agda: how does one obtain a value of a dependent type?

Question

I recently asked this question: An agda proposition used in the type -- what does it mean? and received a very well thought out answer on how to make types implicit and get a real compile time error.

However, it is still unclear to me, how to create a value with a dependent type.

Consider:

div : (n : N) -> even n -> N
div zero p = zero
div (succ (succ n)) p= succ (div n p)
div (succ zero) ()

Where N is the natural numbers and even is the following proposition.

even : N -> Set
even zero = \top
even (succ zero) = \bot
even (succ (succ n)) = even n
data \bot : Set where
record \top : Set where

Suppose I want to write a function as follows:

f : N -> N
f n = if even n then div n else div (succ n)

I have no idea how to do something like this in the way I want... In my eyes the best thing to do would be have a proof that (not (even n)) \to even (succ n). I don't really know how to express this in agda. I am able to write

g : (n:N) -> (even n) -> (even (succ n)) -> N
g n p q = if evenB n then (div n p) else (div (succ n) q)

From this, I could do things like:

g 5 _ _ 

and evaluate to normal form ... to get an answer. If I want to write f, I can then do

f n = g n ? ?

And I get f n = g n { }1 { }2 where ?1 = even n, and ?2 = even (succ n). I can then do things like f five and evaluate to a normal form. I don't really understand why this is valid... Is there a way I can tell agda more information about f defined in this way. Can I tell for sure that if ?1 fails ?2 will succeed, and so tell agda that evaluating f always makes sense?

I interpret g as a function which takes a number n, a proof that n is even, a proof that (succ n) is even, and gives back a number. (Is this the correct way to read this -- or can anyone suggest a better way to read this?) I would really love to understand exactly (or more precisely) how the above type checks. Does it use induction -- does it connect (evenB n) with p : even n?? Etc. I am confused for now because it knows that

if evenB n then (div n q) else (whatever)
if evenB n then div (succ n) q else div n p

are incorrect. The first I understand why -- the q is for succ n, so it doesn't match. But the second fails, and the reason is more mysterious, and seems like Agda is more powerful than I would have guessed...

Here is a first step I would really love if I could figure out how to do (if it makes sense).

g : (n : N) -> (even n) -> N
g n p = if evenB n then (div n p) else (div (succ n) (odd p))

Where odd p is a proof that if even n is absurd then succ n is even. I guess, this would require me to able to work with values that are dependently typed.

Ultimately, I would love to be able to write something like this:

g : N -> N
g n = 
  let p = proofthat n is even
  in
      if evenB n then div n p else (div (succ n) (odd p))

Or something along those lines. Or even

g : N -> N
g n = if evenB n then let p = proofThatEven n in div n p else let q = proofThatEven succ n in div n q

I would really like to know how to make a proof that corresponds to a dependent type, so that I can use it in the program. Any suggestions?

Answer 1

Functions and propositions

There is a crucial difference between encoding stuff as propositions and functions. Let's take a look at the _+_ implemented as a relation on numbers and as a function.

Function is trivial, of course:

_+_ : (m n : ℕ) → ℕ
zero  + n = n
suc m + n = suc (m + n)

_+_ as a proposition is a ternary relation on numbers. For numbers m, n and o, it should hold precisely when m + n = o:

data _+_≡_ : ℕ → ℕ → ℕ → Set where
  zero : ∀ {  n  }             → zero  + n ≡ n
  suc  : ∀ {m n o} → m + n ≡ o → suc m + n ≡ suc o

We can for example show that 2 + 3 ≡ 5:

proof : 2 + 3 ≡ 5
proof = suc (suc zero)

Now, functions are more strict about what is allowed: it must pass the termination checker, there must be a unique result, all cases must be covered and so on; in return, they give us computability. Propositions allow redundancy, inconsistency, partial coverage and so on, but to actually show that 2 + 3 = 5, the programer must be involved.

This is of course a show stopper for your if: you need to be able to compute its first argument!

Is it even?

But there is hope: we can show that your even proposition is actually computable (I should say decidable) for every natural number. How do we show that? By writing a function to decide it.

We'll need a negation on propositions:

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

Next, we'll write down a data type to tell us whether the propositon holds or not:

data Dec (P : Set) : Set where
  yes :   P → Dec P
  no  : ¬ P → Dec P

And lastly, we'll define what it means for even to be decidable:

EvenDecidable : Set
EvenDecidable = ∀ n → Dec (even n)

This reads: even is decidable if for any natural number n we can show that either even n or ¬ (even n). Let's show that this is indeed true:

isEven : EvenDecidable
isEven zero          = yes _
isEven (suc zero)    = no λ ()
isEven (suc (suc n)) = isEven n

From Dec to Bool

Now, we have:

data Bool : Set where
  true false : Bool

if_then_else_ : {A : Set} → Bool → A → A → A
if true  then t else _ = t
if false then _ else f = f

and a function isEven which returns Dec, not Bool. We can go from Dec to Bool by simply forgetting the proof inside (⌊ can be entered via \clL, ⌋ via \clR):

⌊_⌋ : {P : Set} → Dec P → Bool
⌊ yes _ ⌋ = true
⌊ no  _ ⌋ = false

And finally, we can use isEven in if:

if ⌊ isEven n ⌋ then ? else ?

Deriving contradiction

Next, your g function: you require a proof of both even n and even (suc n). This won't work, because no-one can possibly give both of those. In fact, we can even derive a contradiction using those:

bad : ∀ n → even n → even (suc n) → ⊥
bad zero          p q = q
bad (suc zero)    p q = p
bad (suc (suc n)) p q = bad n p q

However, both

bad₂ : ∀ n → even n → even (suc n) → ℕ
bad₂ n p q = div (suc n) q

bad₃ : ∀ n → even n → even (suc n) → ℕ
bad₃ n p q = div n p

typecheck just fine, so I am not entirely sure why you have a problem with the second if.

Putting it all together

Now, we are getting to the main part, the odd function. If we know that number is not even, we should be able to show that the successor is even. We'll reuse the negation from before. agda-mode can fill right hand sides with just C-c C-a:

odd : ∀ n → ¬ even n → even (suc n)
odd zero          p = p _
odd (suc zero)    p = _
odd (suc (suc n)) p = odd n p

Now we have all ingredients to write your g function:

g : ℕ → ℕ
g n = ?

We'll ask whether the number is even using the isEven function:

g : ℕ → ℕ
g n with isEven n
... | isItEven = ?

Now, we'll pattern match on isItEven to find out what the result was:

g : ℕ → ℕ
g n with isEven n
... | yes e = ?
... | no  o = ?

e is a proof that the number is even, o is a proof that it is not even (it has a type ¬ even n). e can be used directly with div, for o we need to use the odd function defined before:

g : ℕ → ℕ
g n with isEven n
... | yes e = div n e
... | no  o = div (suc n) (odd n o)

if for Dec

You cannot implement the above version with just if, however. Booleans do not carry any additional information around; they most certainly don't carry the proof we need. We can write a variant of if that works with Dec rather than Bool. This gives us the ability to distribute the relevant proofs to the then and else branches.

if-dec_then_else_ : {P A : Set} → Dec P → (P → A) → (¬ P → A) → A
if-dec yes p then t else _ = t  p
if-dec no ¬p then _ else f = f ¬p

Notice that both branches are actually functions that take the proof as its first argument.

g : ℕ → ℕ
g n = if-dec isEven n
  then (λ e → div n e)
  else (λ o → div (suc n) (odd n o))

We can even create a fine syntax rule for this if; in this case it's mostly useless, though:

if-syntax = if-dec_then_else_

syntax if-syntax dec (λ yup → yupCase) (λ nope → nopeCase)
  = if-dec dec then[ yup ] yupCase else[ nope ] nopeCase

g : ℕ → ℕ
g n = if-dec isEven n
  then[ e ] div n e
  else[ o ] div (suc n) (odd n o)

What's with?

Now, I noticed that the with construct is mentioned in the later parts of the introduction you linked in the previous question. Here's how it works:

Sometimes you need to pattern match on intermediate expressions, such as isEven in the code above. To do that without with, you need to actually write two functions:

h₁ : (n : ℕ) → Dec (even n) → ℕ
h₁ n (yes e) = div n e
h₁ n (no  o) = div (suc n) (odd n o)

h₂ : ℕ → ℕ
h₂ n = h₁ n (isEven n)

h₂ sets up the expression we would like to pattern match on and h₁ does the actual pattern matching. Now, pattern matching on intermediate expressions like that is fairly frequent so Agda gives us far more compact notation.

h : ℕ → ℕ
h n with isEven n
h n | yes e = div n e
h n | no  o = div (suc n) (odd n o)

So, with behaves as if it added an extra argument which we can pattern match on. You can even use with on more than one expression at the same time:

i : ℕ → ℕ
i n with isCool n | isBig n
i n | cool | big = ?

We can then pattern match on cool and big as if the function had 3 arguments. Now, most of the time the original left hand side stays the same, as the previous functions show (in some cases it can actually be different, but we don't need to deal with that at the moment). For these cases we get a convenient shortcut (especially when the left hand side is long):

i : ℕ → ℕ
i n with isCool n | isBig n
... | cool | big = ?