Instances for Pseudolattice and OrderedCommRing

[LorenzoMolena]

This PR adds instances for Nat and Int as Pseudolattice, and for Int as OrderedCommRing.
It also introduces a helper function constructing a Pseudolattice from a Poset, which is used here to define these instances.

[anshwad10]

likewise for this lemma

[LorenzoMolena]

I'm fine with making it public in Data.Int.Order, but I'm not sure what would be the best name for it.

It's quite a specific lemma only needed for one of the fields in the IsOrderedCommRing record.
Also, I noticed that in other modules (for example Semilattice.Instances.NatMax) the required fields are proved locally when constructing the instance (even for something as basic as maxAssoc).

Other than that, I agree with the other comments and I will apply those changes.

[anshwad10]

Upon closer inspection, this seems to be a special case of cotransitivity of <ℤ which would definitely be useful elsewhere and surprisingly does not already seem to be in Cubical.Data.Int, so perhaps you could prove it in more generality there?
Also, this is just my opinion, but I don't like having private lemmas, and I think maxAssoc, maxRId, and maxIdem should not be in a private where-block in Semilattice.Instances.NatMax

[LorenzoMolena]

Thank you for the suggestion, but I don't see how it follows from cotransitivity, as it seems to have the arguments in the opposite order.
After reasoning a bit about it, I found out that this is actually a consequence of weak linearity of <ℤ:

isOrderedCommRingℤ : IsOrderedCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_ _<ℤ_ _≤ℤ_
    [...]
    isOrderedCommRingℤ .posSum→pos∨pos  = λ x y 0<x+y →
      subst ((0 <ℤ x) L.⊔′_)
        (hPropExt (isProp< {n = x +ℤ y}) (isProp< {0})
                  (<-o+-cancel {m = 0})  (<-o+ {m = 0}))
        (Z<SO.is-weakly-linear 0 (x +ℤ y) x 0<x+y)
      where open module Z<SO = StrictOrderStr (ℤ<StrictOrder .snd)
    [...]

More in general, this field can be derived from:

• isStrictOrder
• isCommRing
• +MonoR<

The first provides is-prop-valued and weak linearity, while the other two allow deriving <-o+ and <-o+-cancel from +MonoR< using easy algebraic manipulations, such as commutativity of +.

I don't think we need to remove the field from the IsOrderedCommRing record, as the defintion is adapted from a standard source: the definition of an Ordered Field from the HoTT Book (Definition 11.2.7), which includes both weak linearity and the condition 0 < x + y ⇒ 0 < x ∨ 0 < y.
Still, if required, I have no objection to removing the field itself.

I could add a helper function to avoid filling in this redundant field manually in most cases, while still allowing it to be specified explicitly when convenient.

[anshwad10]

Yes, I think the helper function would be useful, and it is also how its done for other algebraic structures.
Also, let me explain what I meant by "special case of cotransitivity": Suppose 0 < x + y. Then by cotransitivity we have either 0 < x or x < x + y, and in the second case we can subtract x on both sides to get 0 < y.

[anshwad10]

Oh wait I feel stupid 😅 What I was calling "cotransitivity" is what you were calling "weak linearity", my bad. I didn't notice they were two different things in Relation.Binary.Base

[LorenzoMolena]

I just found a preprint which says that < on the reals is cotransitive (actually meaning weakly linear under the convention used in the Cubical Agda library), so it might be that the naming is not entirely standard, assuming of course that it's not just an error.

Coming back to the helper function, Here it is shown more generally that the posSum→pos∨pos field can be derived from the others, giving an alternative makeIsOrderedCommRing', which is then used to build the instance of Int as OCR.

However, after talking with @marcinjangrzybowski, I was thinking it might be preferable to use lemma0<+, as it is not inductive and therefore faster when deciding which of 0 < x or 0 < y is satisfied. The weak linearity proof, on the other hand, relies on the trichotomy of <, which is less efficient in the current implementation.

If that sounds reasonable, I think this PR could be in good shape to merge as it is. I can add the helper later on, together with some additional properties for OrderedCommRing, in a follow-up PR.

What are the maintainers’ thoughts on this? @felixwellen @mortberg