Data.Nat.Properties.≤-total should be implemented with _<ᵇ_

[Taneb]

It's very slow for ≤-total to decide which constructor to use, especially compared to ≤?. This is an issue using Data.Nat with code generic over a TotalOrder - it's far slower than it could be.

[jamesmckinna]

Given your comment about ≤?, is there an alternative, but still generic, implementation of ≤-total going via Decidable _≤_ rather than TotalOrder?

[Taneb]

@jamesmckinna I don't understand your question. I noticed this problem when I wrote some code generic over a TotalOrder (a record containing a proof that an order is total, i.e. every pair of elements is comparable - ≤-total witnesses this for ℕ). Data.Nat.Properties exports ≤-totalOrder, an instance of this record, using ≤-total.

We could define ≤-total in terms of _≤?_ and ≰⇒≥, but this requires some annoying reordering of Data.Nat.Properties. Here's what this might look like:

≤-total : Total _≤_
≤-total m n with m ≤? n
... | yes m≤n = inj₁ m≤n
... | no m≰n = inj₂ (≰⇒≥ m≰n)

[gallais]

We could define ≤-total in terms of _≤?_ and ≰⇒≥, but this requires some annoying reordering of Data.Nat.Properties.

I think that was the suggestion, and I think it's worth the reorganisation.

[jamesmckinna]

Yes, sorry if my comment was too oblique... @gallais is correct. Cf. my v2.0 refactorings of Data.Nat.DivMod in #2182 ...

Moreover, the proof you offer, modulo the equivalence of _≤?_ and _<ᵇ_, is morally the/a reimplementation of the issue's title, or not?

But I did even wonder if such a (re-)definition should moreover be under Relation.Binary.* (somewhere as Properties or Consequences of being a DecPoset?), and then that proof be instantiated in Nat-specific terms?

Not sure why the reordering of Data.Nat.Properties should be so annoying, other than the fact that refactoring/reimplementation might have such dependency reordering as a knock on consequence?

[jamesmckinna]

@gallais does this qualify as a bug though?

[JacquesCarette]

I'm not sure how much we should change things wrt efficiency. What I mean is that it makes a lot of sense to have (at least) two different definitions of many concepts, one 'conceptually clean' and one 'efficient'. There's quite a number of things in (for example) Data.Rational that would be better off existing in two version. A number already do.

I think it's a false choice to "choose" between certain definitions. Rather we should have parallel hierarchies of definitions (and equivalence proofs). I'd be happy with, say, Data.Rational.Efficient (and same for Data.Integer and likely many more).

There was a reason for that paper on "Realms"!!

[Taneb]

@JacquesCarette in this case, there shouldn't be anything downstream of ≤-total depending on its implementation. If we provide a choice between ≤-total and ≤-total-fast, there'd be no reason for a user to use ≤-total over ≤-total-fast, other than perhaps avoiding a single extra import. I'd be more inclined to accept your argument in cases where we do prove properties using specific implementation details (such as Data.Nat.Base._⊔_/_⊔′_, where we do exactly that)

[gallais]

I would be strongly against -fast suffixes: the fast version should IMO
be the default and we can have a -spec variant for the equivalent but
more proof-friendly version.

[Taneb]

I wasn't advocating using a -fast suffix! I was trying to argue against having two different versions at all