search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
570 stars 234 forks source link

Redefine Data.Integer._⊖_ to use Data.Nat._≤?_ and Data.Nat._∸_ #1302

Closed Taneb closed 3 years ago

Taneb commented 3 years ago

This function can be defined as:

_⊖_ : ℕ → ℕ → ℤ
m ⊖ n with m ℕ.≤? n
m ⊖ n | yes p = - + (n ℕ.∸ m)
m ⊖ n | no ¬p = + (m ℕ.∸ n)

(although either Data.Nat or Data.Nat.Properties needs to be imported for _≤?_)

This would mean that all of the integer arithmetic operations are backed by built-ins, so should be a lot faster in compiled code, as well as improving the speed of compiled code using Data.Rational, too.

Making this change would require changing a lot of proofs in Data.Integer.Properties.

Taneb commented 3 years ago

An alternative for this would be to make _⊖_ itself a builtin.

MatthewDaggitt commented 3 years ago

This would mean that all of the integer arithmetic operations are backed by built-ins, so should be a lot faster in compiled code, as well as improving the speed of compiled code using Data.Rational, too.

For those initially confused about this comment as I was, _⊖_ is used subsequently to define _+_ and _-_ for integers which are then used to define their rational counterparts.

You definitely raise a valid point and this problem should be addressed somehow! As you point out, the problem with your proposed definition is that we'd need to add Data.Nat.Properties to the dependencies of Data.Integer.Base which we've spent quite a lot of effort trying to avoid as it makes loading it and any modules that depends on it very slow.

One alternative would be to define it in terms of the boolean comparison operator _<ᵇ_ rather than _≤?_ but that would make it a lot harder to prove properties about. The backwards incompatibility is also an issue as you point out.

All-in-all I think your suggestion of adding it as a builtin is the best way to go. You could open a PR to the Agda repository?

gallais commented 3 years ago

One alternative would be to define it in terms of the boolean comparison operator _<ᵇ_ rather than _≤?_ but that would make it a lot harder to prove properties about. The backwards incompatibility is also an issue as you point out.

Alternatively we could define _≤ᵇ_ in terms of _<ᵇ_ in Data.Nat.Base and prove in .Properties that Reflects (m ≤ᵇ n) (m ≤ n) (i.e. essentially the proof part of _≤?_).

Then we can use _≤ᵇ_ to implement _⊖_ and the proofs should not be too bad using with m ≤ᵇ n | reflects-≤ᵇ-≤ m n.

gallais commented 3 years ago

There's something soothing about tracking & fixing the broken proofs. The version of Agda I have installed seems incompatible with master so I don't know if the PR builds but Data.Integer.Properties should be fine.

Don't hesitate to keep pushing to that branch: I am not sure whether I'll find time to put in another big session any time soon.