Monus _∸_ is right adjoint to addition _+_ across usual _≤_ preorder

[jamesmckinna]

Surprised that these properties are not already there; they may induce downstream a number of simplification to proofs of properties of monus. But not for this PR!

Separately, in view of the right->left direction of the adjunction: monus is defined as a total function _-_ in Agda.Builtin.Nat, and reimported as _∸_... why don't we define an alternative function n ∸ m only on those arguments satisfying m ≤ n (by an easy recursion on the inductive definition of that relation; alternatively with an irrelevant instance argument of that type, and then simply definitionally equal to Agda.Builtin.Nat._-_) and then prove the two definitions extensionally equal? The fact that _-_ has certain properties provable outright, without further ordering assumptions here or there, seems moot: the only ones which matter are those restricted to the partial domain... but our library setup doesn't typically take account for that. A case of strict(er) specification, but (more) permissive implementation?

[MatthewDaggitt]

why don't we define an alternative function n ∸ m only on those arguments satisfying m ≤ n

Sure but we probably couldn't use the name ∸ without breaking a whole lot of code.

[jamesmckinna]

Regarding renamings (even though I couldn't in all conscience propose such things this time around): I almost feel that the builtin _-_ is the correct name for the total function, and that we should reserve the more 'occult' name for the more occult function, viz. the m ≤ n-guarded version of monus,,,; but then again, just as equally, but only almost, I could take the monus symbol for the total function (occult symbol/occult behaviour), and use _-_ for the guarded version, precisely because under the guard, it is computing subtraction, etc. Oh well, that's one to leave for @JacquesCarette 's 'stdlib-5.0'... ;-)

[Taneb]

I'm not sure I see the point of a guarded version of this function. What does it give us over the current definition when a proof of m ≤ n is floating around in the scope?

[jamesmckinna]

@Taneb well, as I indicated, I wouldn't advocate for it in this PR. In a subsequent one, I might say that insisting on having the guard explicitly in scope (but perhaps making the definition take an instance argument, so that 'floating around' would indeed suffice?) has at least one contra and one pro:

• con: the range of applicability of a lemma/the function itself is tightened
• pro: the range of applicability of a lemma/the function itself is tightened

This is not trying to be facetious: it irks/irked me that the right->left direction of the adjunction requires the additional condition (the left->right does not), but that draws attention to the statement not really making sense (and even: leading to a contradiction) otherwise. So a question perhaps of consistent, if excessive, 'hygiene'?

[gallais]

why don't we define an alternative function n ∸ m

It (c/sh)ould be easily obtained by composing ≤⇒≤″ with the projection extracting the nat from the record.

[jamesmckinna]

@gallais hmmm... that seems a fairly monstrous detour? In any case, I'm also on a mission (#1919/#1948) to redefine _≤″_ (although the record projection is still reasonably easily definable with some gymnastics).

What I have been thinking about since @Taneb's comment, and while preparing this addition, is to make z≤n and s≤s instance constructors... after all, the relation is Irrelevant; but propagating such a change would be a much bigger job. Another time, perhaps?