search

idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.53k stars 378 forks source link

[ libs ] Add `public export` modifiers to arithmetic inequality proofs #3377

Open elkcl opened 2 months ago

elkcl commented 2 months ago

Description

This PR adds public export modifiers to multiple functions (mostly inequality proofs) in Data.Nat and Data.Nat.Order.Properties, allowing the compiler to reduce them when used in types containing inequalities. It also changes divCeilNZ from covering to total.

Should this change go in the CHANGELOG?

mattpolzin commented 2 months ago

I've used many of these proofs extensively in rewrites which don't require them to reduce at compile time so mostly out of curiosity would you mind providing a motivating example or two for this change? You've described it in the abstract in the PR description but I'd be interested in seeing how it manifests in an example.

elkcl commented 2 months ago

Sure. For example, in my project I have a datatype FinInc (which is kinda like Fin, but includes the upper bound and is implemented as a Nat and LTE instead of using a successor function like Data.Fin.Fin) and some arithmetic functions on it that manipulate the bounds:

record FinInc n where
    constructor MkFinInc
    val : Nat
    prf : LTE val n

divCeilNZBounds : (a : Nat) -> (b : Nat) -> (n : Nat) -> (0 nz : NonZero b) -> LTE a (n * b) -> LTE (divCeilNZ a b nz) n

divCeilFlipWeak : {n : Nat} -> {r : Nat} -> (b : Nat) -> (0 _ : NonZero b) => (a : FinInc (minus (n * b) r)) -> FinInc n
divCeilFlipWeak b @{nz} (MkFinInc va pa) = MkFinInc (divCeilNZ va b nz) (divCeilNZBounds va b n nz (transitive pa (minusLTE r (n * b))))

These functions are then used in a different dependent type, and some FinInc arithmetic is performed in the types of its constructors (not in rewrite rules), making it important for certain bounds to be equal, and that requires being able to compute them at compile time. It's kind of hard to make a minimal illustrative example here, but I did have issues with Idris not being able to solve certain constraints until I made at least divCeilNZ and minusLTE public export.