Open andreasabel opened 2 years ago
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:
Let me try to piece this together...
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
?
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...
I was expecting that
DecTotalOrder
gives me operations to compute the minimum and maximum, but could not find them. (These are declared in theLattice
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
?