------------------------------------------------------------------------ -- The Agda standard library -- -- Properties satisfied by posets ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (Poset; StrictPartialOrder) module Relation.Binary.Properties.Poset {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where open import Data.Product.Base using (_,_) open import Function.Base using (flip; _∘_) open import Relation.Binary.Core using (Rel; _Preserves_⟶_) import Relation.Binary.Consequences as Consequences using (mono⇒cong; antimono⇒cong) open import Relation.Binary.Definitions using (_Respectsˡ_; _Respectsʳ_; Decidable) open import Relation.Binary.Structures using (IsPartialOrder; IsStrictPartialOrder; IsDecPartialOrder) open import Relation.Nullary.Decidable.Core using (yes; no) open import Relation.Nullary.Negation.Core using (¬_; contradiction) open Poset P renaming (Carrier to A) import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict import Relation.Binary.Properties.Preorder preorder as PreorderProperties ------------------------------------------------------------------------ -- The _≥_ relation is also a poset. open PreorderProperties public using () renaming ( converse-isPreorder to ≥-isPreorder ; converse-preorder to ≥-preorder ) ≥-isPartialOrder : IsPartialOrder _≈_ _≥_ ≥-isPartialOrder = record { isPreorder = ≥-isPreorder ; antisym = flip antisym } ≥-poset : Poset p₁ p₂ p₃ ≥-poset = record { isPartialOrder = ≥-isPartialOrder } open Poset ≥-poset public using () renaming ( refl to ≥-refl ; reflexive to ≥-reflexive ; trans to ≥-trans ; antisym to ≥-antisym ) ------------------------------------------------------------------------ -- Negated order ≰-respˡ-≈ : _≰_ Respectsˡ _≈_ ≰-respˡ-≈ x≈y = _∘ ≤-respˡ-≈ (Eq.sym x≈y) ≰-respʳ-≈ : _≰_ Respectsʳ _≈_ ≰-respʳ-≈ x≈y = _∘ ≤-respʳ-≈ (Eq.sym x≈y) ------------------------------------------------------------------------ -- Partial orders can be turned into strict partial orders infix 4 _<_ _<_ : Rel A _ _<_ = ToStrict._<_ <-isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ <-isStrictPartialOrder = ToStrict.<-isStrictPartialOrder isPartialOrder <-strictPartialOrder : StrictPartialOrder _ _ _ <-strictPartialOrder = record { isStrictPartialOrder = <-isStrictPartialOrder } open StrictPartialOrder <-strictPartialOrder public using (_≮_; <-resp-≈; <-respʳ-≈; <-respˡ-≈) renaming ( irrefl to <-irrefl ; asym to <-asym ; trans to <-trans ) <⇒≉ : ∀ {x y} → x < y → x ≉ y <⇒≉ = ToStrict.<⇒≉ ≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y ≤∧≉⇒< = ToStrict.≤∧≉⇒< <⇒≱ : ∀ {x y} → x < y → y ≰ x <⇒≱ = ToStrict.<⇒≱ antisym ≤⇒≯ : ∀ {x y} → x ≤ y → y ≮ x ≤⇒≯ = ToStrict.≤⇒≯ antisym ------------------------------------------------------------------------ -- If ≤ is decidable then so is ≈ ≤-dec⇒≈-dec : Decidable _≤_ → Decidable _≈_ ≤-dec⇒≈-dec _≤?_ x y with x ≤? y | y ≤? x ... | yes x≤y | yes y≤x = yes (antisym x≤y y≤x) ... | yes x≤y | no y≰x = no λ x≈y → contradiction (reflexive (Eq.sym x≈y)) y≰x ... | no x≰y | _ = no λ x≈y → contradiction (reflexive x≈y) x≰y ≤-dec⇒isDecPartialOrder : Decidable _≤_ → IsDecPartialOrder _≈_ _≤_ ≤-dec⇒isDecPartialOrder _≤?_ = record { isPartialOrder = isPartialOrder ; _≟_ = ≤-dec⇒≈-dec _≤?_ ; _≤?_ = _≤?_ } ------------------------------------------------------------------------ -- Other properties mono⇒cong : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → f Preserves _≈_ ⟶ _≈_ mono⇒cong = Consequences.mono⇒cong _≈_ _≈_ Eq.sym reflexive antisym antimono⇒cong : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → f Preserves _≈_ ⟶ _≈_ antimono⇒cong = Consequences.antimono⇒cong _≈_ _≈_ Eq.sym reflexive antisym