<div dir="ltr"><div>Dear all,</div> The second RFC (request for comment) for v2.0 of the standard library closely relates to the first one. In the same way that many numeric operations and proofs require that one of their arguments is non-zero, many proofs require that one of their arguments is positive/non-negative/non-positive/negative.<br><br>**The current situation**<br><br>Currently the standard library is very inconsistent about how it handles such constraints. Proofs tend to be defined in one of two ways:<br>1. They either enforce the requirement via explicitly applying the relevant constructor, e.g. `≤-steps : ∀ n → i ≤ j → i ≤ + n + j` where the requirement that the `+ n` is non-negative is enforced by the fact that it is of the form `+ _`.<br><br>2. They require the user to always explicitly construct and pass the relevant proof: `*-monoʳ-≤-nonNeg : ∀ r → NonNegative r → (_* r) Preserves _≤_ ⟶ _≤_`<br><br>**The current problems**<br><br>Although approach 1. has the advantage that you never have to explicitly pass in a proof of `NonNegative`, it does mean that when the argument is not in the form `+ _`, (e.g. `| a | + | b |`), then you can't apply the proof and the user is forced to do all sorts of ugly pattern matching to massage the argument into the required form.<br><br>Although approach 2. has the advantage that it doesn't require the argument to be explicitly in the form of `+_`, it requires you explicitly construct and pass the proof, resulting in significant boilerplate in proofs, even when it is "obvious" that the argument is non-negative.<br><br>**Proposed solution**<br><br>We want to have our cake and eat it, and so we propose to use the same trick as used for `NonZero` proofs, and pass the proofs as irrelevant instance arguments, e.g.<br>```agda<br>≤-steps : ∀ k .{{_ : NonNegative k}} → i ≤ j → i ≤ k + j<br>*-monoʳ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (_* r) Preserves _≤_ ⟶ _≤_<br>```<br>The advantages of this are as follows:<br>1. By declaring basic instances of `NonNegative` etc.<br>```agda<br>instance<br>    nonNeg : ∀ {n} → NonNegative (+ n)<br>    nonNeg = _<br>```<br> we get the advantages of solution 1 as Agda will automatically fill in the generated instance arguments when the argument is in the right form `+_`.<br><br>2. By not explicitly using the `+_` constructors, we retain the advantages of solution 2 in that we're not restricted to passing in arguments in the right form. <br><br>3. Currently, in the case where you were applying the proofs to something like `| a | + | b |` (which is non-negative, but that fact is not immediately inferrable by Agda) you would still have to explicitly construct and provide the proof of non-negativity. However this will be easier than before, as we provide constructors for `NonNegative` and other predicates. However, if <a href="https://github.com/agda/agda/issues/5494">https://github.com/agda/agda/issues/5494</a> gets implemented in Agda 2.6.3 then we would be able to define further additional instances:<br>```agda<br>instance<br>    |-|-nonNeg : ∀ {i} → NonNegative | i |<br>    |-|-nonNeg = _<br> <br>    +-nonNeg : ∀ {i j} .{{_ : NonNegative i}} .{{_ : NonNegative j}} → NonNegative (i + j)<br>    +-nonNeg <br>```<br>which would allow Agda to entirely automate the process of constructing the proofs. Additional such instances could be defined by users for their own custom operations.<br><br>**Backwards incompatibilities**<br><br>When adapting code that uses proofs that currently use approach 1. then the form of the numeric argument passed will have to change, e.g. instead of passing `n` you will have to pass `+ n`. For proofs that currently use approach 2., if the proof is findable by instance search then the proof argument can simply be removed, otherwise the proof argument will have to be wrapped in instance brackets `{{_}}`.<br><br>**Feedback**<br><br>I've opened a PR with the proposed changes. Please feel free to give any feedback you have on the proposal:<br><a href="https://github.com/agda/agda-stdlib/pull/1581">https://github.com/agda/agda-stdlib/pull/1581</a><br><div><br></div><div>Cheers,</div><div>Matthew</div></div>