Lattice from decidable total order

[andreasabel]

I was expecting that DecTotalOrder gives me operations to compute the minimum and maximum, but could not find them. (These are declared in the Lattice hierarchy.)
I think it would make sense to provide standard implementations for these operations using the total function. I have done this for minimum below.

Question to the architects: How should that be integrated into the current DecTotalOrder?

------------------------------------------------------------------------
-- Infimum from decidable total order on A.

open import Relation.Binary.Bundles using (DecTotalOrder)

module Infimum {ℓ₁ ℓ₂ ℓ₃} (O : DecTotalOrder ℓ₁ ℓ₂ ℓ₃) where

open import Data.Product                        using (_,_)
open import Data.Sum                            using (inj₁; inj₂)
open import Function                            using (case_of_)

open import Relation.Binary.Lattice.Bundles     using (MeetSemilattice)
open import Relation.Binary.Lattice.Definitions using (Infimum)

-- We create a module for record O (with the same name, O).
-- This allows us to use the content of O conveniently
-- when constructing new records.

module O where
  open DecTotalOrder O public

  _∧_ : (x y : Carrier) → Carrier
  x ∧ y = case total x y of λ where
    (inj₁ x≤y) → x
    (inj₂ y≤x) → y

  infimum : Infimum _≤_ _∧_
  infimum x y with total x y
  ... | inj₁ x≤y = refl , x≤y , λ _ z≤x _ → z≤x
  ... | inj₂ y≤x = y≤x , refl , λ _ _ z≤y → z≤y

meetSemilattice : MeetSemilattice _ _ _
meetSemilattice = record
  { O
  ; isMeetSemilattice = record { O }
  }

[gallais]

We do have them in

http://agda.github.io/agda-stdlib/Algebra.Construct.NaturalChoice.Min.html
http://agda.github.io/agda-stdlib/Algebra.Construct.NaturalChoice.Max.html

[andreasabel]

Thanks for the pointers, @gallais!
I think I lack imagination for the meaning of algebra-construct-natural-choice.
Is natural choice a mathematical concept around orders?
Is there even a choice for min/max on a total order? Extensionally, these functions should be unique.
Intensionally, there could be other implementations, but is it likely that min can be made more efficient that total?

Tracing #1108, I found the other half of the lattice instantiation for decidable total orders at:

• agda-stdlib/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda

  Lines 27 to 31 in fb1d6f4

  	⊓-isSemilattice : IsSemilattice _⊓_
  	⊓-isSemilattice = record
  	{ isBand = ⊓-isBand
  	; comm = ⊓-comm
  	}

• https://github.com/agda/agda-stdlib/blob/fb1d6f494543af003e3f9000da85e9713e6787f3/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda

Let me try to piece this together...

[andreasabel]

Here is my attempt:

module O where
  open DecTotalOrder O public
  open import Algebra.Construct.NaturalChoice.Min totalOrder public
    renaming (_⊓_ to _∧_)
  open import Algebra.Lattice.Construct.NaturalChoice.MinOp minOperator public

  infimum : Infimum _≤_ _∧_
  infimum x y with total x y
  ... | inj₁ x≤y = refl , x≤y , λ _ z≤x _ → z≤x
  ... | inj₂ y≤x = y≤x , refl , λ _ _ z≤y → z≤y

meetSemilattice : MeetSemilattice _ _ _
meetSemilattice = record
  { O
  ; isMeetSemilattice = record { O }
  }

So, Algebra.Lattice.Construct.NaturalChoice.MinOp gives me the Semilattice instance, not the MeetSemilattice. This is a bit surprising. I have tried to guess what the design choices behind (Meet)Semilattice are, but to me it seems that Semilattice is derived as idempotent commutative semigroup, so coming from the minimum/maximum operation, whereas MeetSemilattice is connected to the concept of order. So, it should be more consequent to derive MeetSemilattice from TotalOrder, not Semilattice. Would you agree, @MatthewDaggitt @gallais ?

Concretely, it seems that I still have to prove the Infimum property by hand, while I expect it to be in the library.

Wouldn't a more natural factoring be that we can get a Semilattice from a Meet(/Join)Semilattice, if we want it from a TotalOrder?

[MatthewDaggitt]

Apologies for the delay in replying.

I think I lack imagination for the meaning of algebra-construct-natural-choice.
Is natural choice a mathematical concept around orders?
Is there even a choice for min/max on a total order? Extensionally, these functions should be unique.

Hmm, that's purely on me. "Natural choice" is what my PhD supervisor always called it and I picked the terminology up. You're right though, I can't find any references to it in the literature so it should be renamed. Open to suggestions? Just Choice?

So, Algebra.Lattice.Construct.NaturalChoice.MinOp gives me the Semilattice instance, not the MeetSemilattice. This is a bit surprising. So, it should be more consequent to derive MeetSemilattice from TotalOrder, not Semilattice. Would you agree, @MatthewDaggitt @gallais ?

I agree, giving MeetSemilattice as well as Semilattice would make a lot of sense.

Concretely, it seems that I still have to prove the Infimum property by hand, while I expect it to be in the library.

Yes, that should be added.

Just a heads up, that for better or worse, we have two formalisations of lattices in the standard library. A purely algebraic approach in Algebra.Lattice, and an order theoretic approach in Relation.Binary.Lattice. Sounds like you might be looking for the latter rather than the former? Though the latter is even less developed than the former...