[Agda] It feels like there isn't a way to do a partial subtraction nicely ... and a feature suggestion :)

[Tristan Wibberley]

On Sun, 2008-03-23 at 20:28 +0100, Ulf Norell wrote:

> Defining True to be the record type with no fields is what's going to
> make this possible. Records support eta equality, which means that any
> record element "r" is equal to the record build by projecting the
> fields of "r". In the case of True this means that any element of True
> is equal to any other element of True. In particular, if the type
> checker is trying to find something of type True there's only one
> choice. Now, instead of defining NatLTE inductively you can define it
> recursively:
> 
> NatLTE : Nat -> Nat -> Set
> NatLTE zero m = True
> NatLTE (suc n) zero = False
> NatLTE (suc n) (suc m) = NatLTE n m
> 
> The type of minus is what you suggest:
> 
> _-_ : (a : Nat) -> (b : Nat) -> {c : NatLTE b a} -> Nat
> _-_ m zero = m
> _-_ zero (suc _) {}  -- there can be no proof here
> _-_ (suc n) (suc m) {p} = _-_ n m {p}
>        -- a proof that suc n =< suc m is the same as a proof that n =<
> m

Do you mind if I add this to the documentation section of the wiki?

I'll make a howto section to which other high-level templates can be
added.

-- 
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.