[Agda] Dependent Types at Work

[Dan Licata]

Hi Tristan,

On Mar20, Tristan Wibberley wrote:
> I'm reading this document as it is the best material I've found on the
> subject but there is one thing in particular lacking. One of the first
> exercises is to write a subtraction function and refers to "cut-off"
> which makes sense (it is only defined for first arguments greater in
> value than or equal in value to the second argument). 

You've got the right idea here, but easy way to solve this problem is to
paraphrase your idea a bit: 
Instead of saying

  subtraction is only defined for first arguments greater in
  value than or equal in value to the second argument

say

  subtraction is only defined for second arguments less in
  value than or equal in value to the first argument

So you want to give subtraction a type that says "give me any number n,
and another number less than or equal to n, and I'll give you a number".
One way of doing that is to use the following type to represent
numbers-less-than-or-equal-to n:

  data NatLTE : Nat -> Set where
    lzero : {n : Nat} -> NatLTE n
    lsucc : {n : Nat} -> NatLTE n -> NatLTE (S n)

You may want to compare this type NatLTE with the type Fin n on page 15.

Then your task is:

  sub : (n : Nat) -> NatLTE n -> Nat 
  sub = ?

Does that help?

-Dan