[Agda] Dependent Types at Work

[Tristan Wibberley]

On Fri, 2008-03-21 at 10:42 -0400, Dan Licata wrote:
> On Mar21, Tristan Wibberley wrote:
> > On Fri, 2008-03-21 at 09:57 +0100, Peter Dybjer wrote:
> 
> Hi Tristan,
> 
> I think I unnecessarily confused you by using the proof of
> less-than-or-equal-to as the second number.  You can also solve the
> problem with an external proof:
> 
>   data LTE : Nat -> Nat -> Set where
>     lte/z  : {m : Nat} -> LTE zero m
>     lte/ss : {n m : Nat} -> LTE n m -> LTE (succ n) (succ m) 
> 
>   _-_ : (n m : Nat) -> LTE m n -> Nat
>   n - m = ?

Perhaps I should approach this face of dependent types from the shallow
end because I can't grok this.

So I've tried relating what _+_ does to LTE (less than or equal to):

    module first where
    
    data Nat : Set where
      zero : Nat
      succ : Nat -> Nat
    
    _+_ : Nat -> Nat -> Nat
    _+_ zero b = b
    _+_ (succ a) b = a + (succ b)

    data LTE : Nat -> Nat -> Set where
      lte/z : {m : Nat} -> LTE zero m
      lte/ss : {n m : Nat} -> LTE n m -> LTE (succ n) (succ m)

    {- this is supposed to say that the first operand of _+_ is less
       than or equal to the result:
       "The definitions of _+/relatefirstoperand_ prove that if you
        prove that something "a" is a Nat and that something "b" is a
        Nat you prove LTE a (a + b).
    -}
    _+/relatefirstoperand_ : (a : Nat) -> (b : Nat) -> LTE a (a + b)
    zero +/relatefirstoperand n = lte/z {n}
    (succ m) +/relatefirstoperand n = lte/ss (m +/relatefirstoperand n)

I was expecting this to load successfully but I got an error for the
right hand side of (succ m) +/relatefirstoperand n:

succ (m + n) != m + succ n of type Nat

but I've checked the canonical forms of both of those (C-c C-n in emacs
with concrete m and n) and they are identical.

Can anybody explain what is going wrong here?