open import Graded.Modality
module Graded.Modality.Properties.PartialOrder
{a} {M : Set a} (𝕄 : Semiring-with-meet M) where
open Semiring-with-meet 𝕄
open import Tools.Function
open import Tools.Nullary
open import Tools.Product
open import Tools.PropositionalEquality as PE
open import Tools.Relation
private
variable
p p′ q q′ r r′ : M
≤-refl : p ≤ p
≤-refl {p} = sym (∧-idem p)
≤-trans : p ≤ q → q ≤ r → p ≤ r
≤-trans {p} {q} {r} p≤q q≤r = trans p≤q
(trans (∧-congˡ q≤r)
(sym (trans (∧-congʳ p≤q) (∧-assoc p q r))))
≤-antisym : p ≤ q → q ≤ p → p ≡ q
≤-antisym {p} {q} p≤q q≤p = trans p≤q (trans (∧-comm p q) (sym q≤p))
≤-reflexive : p ≡ q → p ≤ q
≤-reflexive {p} p≡q = trans (sym (∧-idem p)) (∧-congˡ p≡q)
≤-preorder : IsPreorder _≡_ _≤_
≤-preorder = record
{ isEquivalence = PE.isEquivalence
; reflexive = ≤-reflexive
; trans = ≤-trans
}
≤-partial : IsPartialOrder _≡_ _≤_
≤-partial = record
{ isPreorder = ≤-preorder
; antisym = ≤-antisym
}
≤-poset : Poset _ _ _
≤-poset = record
{ Carrier = M
; _≈_ = _≡_
; _≤_ = _≤_
; isPartialOrder = ≤-partial
}
≡-decidable→≤-decidable : Decidable (_≡_ {A = M}) → Decidable _≤_
≡-decidable→≤-decidable _≡?_ p q = p ≡? (p ∧ q)
≡-decidable→<-decidable : Decidable (_≡_ {A = M}) → Decidable _<_
≡-decidable→<-decidable _≡?_ p q with ≡-decidable→≤-decidable _≡?_ p q
… | no p≰q = no (p≰q ∘→ proj₁)
… | yes p≤q with p ≡? q
… | no p≢q = yes (p≤q , p≢q)
… | yes p≡q = no ((_$ p≡q) ∘→ proj₂)
<→≰ : p < q → ¬ q ≤ p
<→≰ (p≤q , p≢q) q≤p = p≢q (≤-antisym p≤q q≤p)