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

[Tristan Wibberley]

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

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