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

[Ulf Norell]

On Sun, Mar 23, 2008 at 7:57 PM, Tristan Wibberley <tristan at wibberley.org>
wrote:

> Hi all,
>
> I think the way to achieve what I'm looking for might need a new
> feature.
>
> Given:
>
> data Nat : Set where
>  zero : Nat
>  succ : Nat -> Nat
>
> data NateLTE : Nat -> Nat -> Set where
>  lte/z  : {m : Nat} -> NatLTE zero m
>  lte/ss : {n m : Nat} -> NatLTE n m -> NatLTE (succ n) (succ m)
>
> I think want to define:
>
> _-_ : (a : Nat) -> (b : Nat) -> {c : NatLTE b a} -> Nat
>
>
> and say, somewhere else (separate from the definitions of zero and succ
> and separate from the definition of _-_), that use of succ to obtain "a"
> or "b" suggests a proof object to consider as a proof of "NatLTE b a" so
> "(succ zero) - zero" can be done, but not "zero - (succ zero)".
>
> Such a suggested proof of "NatLTE b a" could also be associated with _
> +_, for example so "((succ zero) + (succ zero) - (succ zero)" can be
> done, but not "(succ zero) - ((succ zero) + (succ zero))"
>
> Then the typechecker would look at what is used in the function that
> uses _-_ to get the arguments "a" and "b" and consider their respective
> proofs of "NatLTE b" a in deducing "c".
>
> Cases for _-_ could then be not-required where NatLTE restricts them.
>
> It would also be nice to be able to give a tailored proof just within
> the scope of a function for when the functions you've used within do not
> have full proofs associated and must be composed to prove "NatLTE b a"
> from that the function's arguments (without having to clutter "a - b" by
> needing to write "(a - b) {proof_of_NatLTE_b_a}" as currently required).
>
>
> However, this futile self-inflicted exercise has been most instructive
> in usage of agda2 :)


It is possible to do something like what you're asking for. First, let's
define the empty and the singleton types False and True:

data False : Set where
record True : Set where

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

Now you can say suc (suc (suc zero)) - suc (suc zero) and the proof will be
filled in automatically. Even suc (suc n) - suc (suc zero) will work, but as
soon as the proof obligation does not reduce to True you would have to fill
in the proof yourself. For instance, in the recursive call in the definition
of _-_ there is no way the type checker would figure that the proof object
should be "p".

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080323/7a4bf193/attachment.html