[Agda] [RFC stdlib v2.0] 2. Numeric proofs which restrict their arguments to be positive/non-negative etc.

[Matthew Daggitt]

Dear all,
 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.

**The current situation**

Currently the standard library is very inconsistent about how it handles
such constraints. Proofs tend to be defined in one of two ways:
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 `+ _`.

2. They require the user to always explicitly construct and pass the
relevant proof: `*-monoʳ-≤-nonNeg : ∀ r → NonNegative r → (_* r) Preserves
_≤_ ⟶ _≤_`

**The current problems**

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.

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.

**Proposed solution**

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.
```agda
≤-steps : ∀ k .{{_ : NonNegative k}} → i ≤ j → i ≤ k + j
*-monoʳ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (_* r) Preserves _≤_ ⟶ _≤_
```
The advantages of this are as follows:
1. By declaring basic instances of `NonNegative` etc.
```agda
instance
    nonNeg : ∀ {n} → NonNegative (+ n)
    nonNeg = _
```
 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 `+_`.

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.

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 https://github.com/agda/agda/issues/5494 gets
implemented in Agda 2.6.3 then we would be able to define further
additional instances:
```agda
instance
    |-|-nonNeg : ∀ {i} → NonNegative | i |
    |-|-nonNeg = _

    +-nonNeg : ∀ {i j} .{{_ : NonNegative i}} .{{_ : NonNegative j}} →
NonNegative (i + j)
    +-nonNeg
```
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.

**Backwards incompatibilities**

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 `{{_}}`.

**Feedback**

I've opened a PR with the proposed changes. Please feel free to give any
feedback you have on the proposal:
https://github.com/agda/agda-stdlib/pull/1581

Cheers,
Matthew
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210820/8b3d9fb5/attachment.html>