[Agda] Dependent Types at Work

[Tristan Wibberley]

On Fri, 2008-03-21 at 09:57 +0100, Peter Dybjer wrote:

> but at that early stage in the notes we don't expect the reader to be
> quite ready for such considerations.  Such an exercise could be added a
> little later after we have got into propositions as types.

I was starting to think that maybe a proposition would be the order of
the day.

Does anybody know a good resource to learn how to achieve this anyway? I
find it to be the most satisfying part of dependent typing.

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

given:

data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

foo : (n : Nat) -> NatLTE n -> Nat
foo a b = a - b

and I'm desperate to learn how to implement the missing parts of that
interface.

I expected to have to write proofs for things like

(succ zero) : NatLTE zero
(succ (succ (zero)) : NatLTE (succ zero)
(succ (succ (succ zero))) : NatLTE (succ zero)

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):

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

-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.