[Agda] Dependent Types at Work

[Dan Licata]

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 = ?

> I'd like to be able to allow:
> 
> one - zero
> two - one
> three - one
> foo one zero
> foo two one
> foo three one
> 
> but not:
> 
> zero - one
> one - two
> one - three
> foo zero one
> foo one two
> foo one three

Now, you can make the first calls, because you can create the necessary
proof object.  You can't make the second ones, because you can't prove
the necessary fact.

> But that I'd like to write inductive proofs over all Nats that are
> NatLTEs (I just need to figure out how).
> 
> something like (pseudo proof conclusion - probably not observational):
> 

These are lemmas about LTE.  

> forall (n:Nat) . (a:NatLTE n) -> (a:Nat)

You don't need this one when the proof object is external.

> forall (n:Nat) . (n:Successor a) -> (a:NatLTE n)

  lte/succ : (n : Nat) -> LTE n (succ n)
  lte/succ = ?

> forall (n:Nat) . (n:Nat) -> (n:NatLTE n)
 
  lte/refl : (n : Nat) -> LTE n n
  lte/refl = ?

-Dan