[Agda] [RFC stdlib v2.0] 1. Numeric ops with non-zero proofs

[Matthew Daggitt]

Dear all,
To kick things off, the first RFC (request for comment) for v2.0 of the
Agda standard library is about proposed changes to how numeric operations
that require non-zero proofs (e.g. division) work.

The current situation

Currently operations such as division are defined as follows
<https://github.com/agda/agda-stdlib/blob/516c545f28aca931d695a86fbdf7941154b0a64f/src/Data/Nat/DivMod.agda#L43>
:

_/_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ

taking an implicit proof that the result of the decision procedure of
testing whether it is zero reduces to false. This is preferable to passing
a direct proof of the form divisor ≢ 0 as it means that when divisor normalises
to something of the form suc n then the type of the proof reduces to
unit ⊤ which
Agda automatically fills in. Consequently you can write 7 / 3 or m /
sucn without
having to explicitly construct the proof.

The current problems

   1. When the denominator is not in the form suc _, Agda can't infer the
   proof and therefore it must always be passed explicitly even when the proof
   is in scope. This leads to having to write the ugly code like the following:

∀ m n {gcd≢0 : NonZero (gcd m n)} → Coprime ((m / gcd m n) {gcd≢0})
((n / gcd m n) {gcd≢0})


   1.

   When proving equalities over _/_ you can't use cong₂ from
   Relation.Binary.PropositionalEquality directly as Agda requires that you
   explicitly prove the proofs of non-zeroness do not affect the result. This
   makes it very finicky to use equational reasoning.
   2.

   The use of the decision procedure _≟_ means that the definition must
   depend on Data.Nat.Properties where _≟_ lives. This means that a)
   type-checking anything involving _/_ requires type-checking a much
   larger proportion of the library that one would expect and b) _/_ can't
   live in Data.Nat.Base.
   3.

   Constructing a proof of the type False (divisor ≟ 0) is much trickier
   than a proof of divisor ≢ 0and requires extra imports from
   Relation.Nullary.

Proposed solution

We propose to take a leaf out of Ulf Norell's Prelude library and instead
pass the proofs as *irrelevant*, *instance* arguments that use the new
NonZero predicates introduced in v1.5:

_/_ : (dividend divisor : ℕ) {{.(NonZero divisor)}} → ℕ

which preserves the ability to not provide the proofs for divisors of the
form suc _ and fixes the problems listed above as follows:

   1. Agda automatically fills in instance arguments if they are in scope,
   therefore removing the need to supply them to every place in the expression
   where they can't be inferred. For example we would then be able to write
   the much nicer:

∀ m n {{NonZero (gcd m n)}} → Coprime (m / gcd m n) (n / gcd m n)


   1.

   Agda doesn't consider irrelevant arguments when proving propositional
   equality. Therefore to prove m / n and x / y are propositionally equal
   will only require that we prove m equals x and n equals y and will not
   require us to explicitly prove that the result doesn't depend on the proofs
   of non-zeroness.
   2.

   The NonZero predicate is much more lightweight than the decidability
   proof and lives in Data.Nat.Base rather than Data.Nat.Properties.
   3.

   The NonZero predicate comes with nice constructors nonZero-< and
   nonZero-≢ that makes constructing such proofs much easier.

This has an additional advantage in that for certain operations that always
result in a non-zero result, e.g. factorial, it will be possible to declare
a proof of the non-zeroness as an instance and you will never have to
explicitly pass a proof.

Backwards incompatibilities

In cases where the proof is already automatically inferred nothing will
need to change. In places where the proof has to be passed explicitly, then
the type of the proof will need to change and will need to be passed using
instance brackets {{_}} rather than implict brackets {_}. As mentioned
above, NonZero comes with constructors so constructing the new proofs
should be much easier.

Feedback

Any feedback would be greatly appreciated! Please feel free to reply in one
of the following issues:
https://github.com/agda/agda-stdlib/issues/921
https://github.com/agda/agda-stdlib/issues/1170
https://github.com/agda/agda-stdlib/issues/1408
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210706/1bffc86a/attachment.html>