------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of a min operator derived from a spec over a total -- preorder. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (TotalPreorder) open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MinOp⇒MaxOp) module Algebra.Construct.NaturalChoice.MinOp {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where open import Algebra.Core using (Op₂) open import Algebra.Bundles using (RawMagma; Magma; Semigroup; Band; CommutativeSemigroup; SelectiveMagma; Monoid) open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]) open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_) open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.Definitions using (Maximum; Minimum) open TotalPreorder O renaming ( Carrier to A ; _≲_ to _≤_ ; ≲-resp-≈ to ≤-resp-≈ ; ≲-respʳ-≈ to ≤-respʳ-≈ ; ≲-respˡ-≈ to ≤-respˡ-≈ ) open MinOperator minOp open import Algebra.Definitions _≈_ open import Algebra.Structures _≈_ open import Relation.Binary.Reasoning.Preorder preorder ------------------------------------------------------------------------ -- Helpful properties x⊓y≤x : ∀ x y → x ⊓ y ≤ x x⊓y≤x x y with total x y ... | inj₁ x≤y = reflexive (x≤y⇒x⊓y≈x x≤y) ... | inj₂ y≤x = ≤-respˡ-≈ (Eq.sym (x≥y⇒x⊓y≈y y≤x)) y≤x x⊓y≤y : ∀ x y → x ⊓ y ≤ y x⊓y≤y x y with total x y ... | inj₁ x≤y = ≤-respˡ-≈ (Eq.sym (x≤y⇒x⊓y≈x x≤y)) x≤y ... | inj₂ y≤x = reflexive (x≥y⇒x⊓y≈y y≤x) ------------------------------------------------------------------------ -- Algebraic properties ⊓-comm : Commutative _⊓_ ⊓-comm x y with total x y ... | inj₁ x≤y = Eq.trans (x≤y⇒x⊓y≈x x≤y) (Eq.sym (x≥y⇒x⊓y≈y x≤y)) ... | inj₂ y≤x = Eq.trans (x≥y⇒x⊓y≈y y≤x) (Eq.sym (x≤y⇒x⊓y≈x y≤x)) ⊓-congˡ : ∀ x → Congruent₁ (x ⊓_) ⊓-congˡ x {y} {r} y≈r with total x y ... | inj₁ x≤y = begin-equality x ⊓ y ≈⟨ x≤y⇒x⊓y≈x x≤y ⟩ x ≈⟨ x≤y⇒x⊓y≈x (≤-respʳ-≈ y≈r x≤y) ⟨ x ⊓ r ∎ ... | inj₂ y≤x = begin-equality x ⊓ y ≈⟨ x≥y⇒x⊓y≈y y≤x ⟩ y ≈⟨ y≈r ⟩ r ≈⟨ x≥y⇒x⊓y≈y (≤-respˡ-≈ y≈r y≤x) ⟨ x ⊓ r ∎ ⊓-congʳ : ∀ x → Congruent₁ (_⊓ x) ⊓-congʳ x {y₁} {y₂} y₁≈y₂ = begin-equality y₁ ⊓ x ≈⟨ ⊓-comm x y₁ ⟨ x ⊓ y₁ ≈⟨ ⊓-congˡ x y₁≈y₂ ⟩ x ⊓ y₂ ≈⟨ ⊓-comm x y₂ ⟩ y₂ ⊓ x ∎ ⊓-cong : Congruent₂ _⊓_ ⊓-cong {x₁} {x₂} {y₁} {y₂} x₁≈x₂ y₁≈y₂ = Eq.trans (⊓-congˡ x₁ y₁≈y₂) (⊓-congʳ y₂ x₁≈x₂) ⊓-assoc : Associative _⊓_ ⊓-assoc x y r with total x y | total y r ⊓-assoc x y r | inj₁ x≤y | inj₁ y≤r = begin-equality (x ⊓ y) ⊓ r ≈⟨ ⊓-congʳ r (x≤y⇒x⊓y≈x x≤y) ⟩ x ⊓ r ≈⟨ x≤y⇒x⊓y≈x (trans x≤y y≤r) ⟩ x ≈⟨ x≤y⇒x⊓y≈x x≤y ⟨ x ⊓ y ≈⟨ ⊓-congˡ x (x≤y⇒x⊓y≈x y≤r) ⟨ x ⊓ (y ⊓ r) ∎ ⊓-assoc x y r | inj₁ x≤y | inj₂ r≤y = begin-equality (x ⊓ y) ⊓ r ≈⟨ ⊓-congʳ r (x≤y⇒x⊓y≈x x≤y) ⟩ x ⊓ r ≈⟨ ⊓-congˡ x (x≥y⇒x⊓y≈y r≤y) ⟨ x ⊓ (y ⊓ r) ∎ ⊓-assoc x y r | inj₂ y≤x | _ = begin-equality (x ⊓ y) ⊓ r ≈⟨ ⊓-congʳ r (x≥y⇒x⊓y≈y y≤x) ⟩ y ⊓ r ≈⟨ x≥y⇒x⊓y≈y (trans (x⊓y≤x y r) y≤x) ⟨ x ⊓ (y ⊓ r) ∎ ⊓-idem : Idempotent _⊓_ ⊓-idem x = x≤y⇒x⊓y≈x (refl {x}) ⊓-sel : Selective _⊓_ ⊓-sel x y = Sum.map x≤y⇒x⊓y≈x x≥y⇒x⊓y≈y (total x y) ⊓-identityˡ : ∀ {⊤} → Maximum _≤_ ⊤ → LeftIdentity ⊤ _⊓_ ⊓-identityˡ max = x≥y⇒x⊓y≈y ∘ max ⊓-identityʳ : ∀ {⊤} → Maximum _≤_ ⊤ → RightIdentity ⊤ _⊓_ ⊓-identityʳ max = x≤y⇒x⊓y≈x ∘ max ⊓-identity : ∀ {⊤} → Maximum _≤_ ⊤ → Identity ⊤ _⊓_ ⊓-identity max = ⊓-identityˡ max , ⊓-identityʳ max ⊓-zeroˡ : ∀ {⊥} → Minimum _≤_ ⊥ → LeftZero ⊥ _⊓_ ⊓-zeroˡ min = x≤y⇒x⊓y≈x ∘ min ⊓-zeroʳ : ∀ {⊥} → Minimum _≤_ ⊥ → RightZero ⊥ _⊓_ ⊓-zeroʳ min = x≥y⇒x⊓y≈y ∘ min ⊓-zero : ∀ {⊥} → Minimum _≤_ ⊥ → Zero ⊥ _⊓_ ⊓-zero min = ⊓-zeroˡ min , ⊓-zeroʳ min ------------------------------------------------------------------------ -- Structures ⊓-isMagma : IsMagma _⊓_ ⊓-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ⊓-cong } ⊓-isSemigroup : IsSemigroup _⊓_ ⊓-isSemigroup = record { isMagma = ⊓-isMagma ; assoc = ⊓-assoc } ⊓-isBand : IsBand _⊓_ ⊓-isBand = record { isSemigroup = ⊓-isSemigroup ; idem = ⊓-idem } ⊓-isCommutativeSemigroup : IsCommutativeSemigroup _⊓_ ⊓-isCommutativeSemigroup = record { isSemigroup = ⊓-isSemigroup ; comm = ⊓-comm } ⊓-isSelectiveMagma : IsSelectiveMagma _⊓_ ⊓-isSelectiveMagma = record { isMagma = ⊓-isMagma ; sel = ⊓-sel } ⊓-isMonoid : ∀ {⊤} → Maximum _≤_ ⊤ → IsMonoid _⊓_ ⊤ ⊓-isMonoid max = record { isSemigroup = ⊓-isSemigroup ; identity = ⊓-identity max } ------------------------------------------------------------------------ -- Raw bundles ⊓-rawMagma : RawMagma _ _ ⊓-rawMagma = record { _≈_ = _≈_ ; _∙_ = _⊓_ } ------------------------------------------------------------------------ -- Bundles ⊓-magma : Magma _ _ ⊓-magma = record { isMagma = ⊓-isMagma } ⊓-semigroup : Semigroup _ _ ⊓-semigroup = record { isSemigroup = ⊓-isSemigroup } ⊓-band : Band _ _ ⊓-band = record { isBand = ⊓-isBand } ⊓-commutativeSemigroup : CommutativeSemigroup _ _ ⊓-commutativeSemigroup = record { isCommutativeSemigroup = ⊓-isCommutativeSemigroup } ⊓-selectiveMagma : SelectiveMagma _ _ ⊓-selectiveMagma = record { isSelectiveMagma = ⊓-isSelectiveMagma } ⊓-monoid : ∀ {⊤} → Maximum _≤_ ⊤ → Monoid a ℓ₁ ⊓-monoid max = record { isMonoid = ⊓-isMonoid max } ------------------------------------------------------------------------ -- Other properties x⊓y≈x⇒x≤y : ∀ {x y} → x ⊓ y ≈ x → x ≤ y x⊓y≈x⇒x≤y {x} {y} x⊓y≈x with total x y ... | inj₁ x≤y = x≤y ... | inj₂ y≤x = reflexive (Eq.trans (Eq.sym x⊓y≈x) (x≥y⇒x⊓y≈y y≤x)) x⊓y≈y⇒y≤x : ∀ {x y} → x ⊓ y ≈ y → y ≤ x x⊓y≈y⇒y≤x {x} {y} x⊓y≈y = x⊓y≈x⇒x≤y (begin-equality y ⊓ x ≈⟨ ⊓-comm y x ⟩ x ⊓ y ≈⟨ x⊓y≈y ⟩ y ∎) mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≈_ ⟶ _≈_ → f Preserves _≤_ ⟶ _≤_ → ∀ x y → f (x ⊓ y) ≈ f x ⊓ f y mono-≤-distrib-⊓ {f} cong mono x y with total x y ... | inj₁ x≤y = begin-equality f (x ⊓ y) ≈⟨ cong (x≤y⇒x⊓y≈x x≤y) ⟩ f x ≈⟨ x≤y⇒x⊓y≈x (mono x≤y) ⟨ f x ⊓ f y ∎ ... | inj₂ y≤x = begin-equality f (x ⊓ y) ≈⟨ cong (x≥y⇒x⊓y≈y y≤x) ⟩ f y ≈⟨ x≥y⇒x⊓y≈y (mono y≤x) ⟨ f x ⊓ f y ∎ x≤y⇒x⊓z≤y : ∀ {x y} z → x ≤ y → x ⊓ z ≤ y x≤y⇒x⊓z≤y z x≤y = trans (x⊓y≤x _ z) x≤y x≤y⇒z⊓x≤y : ∀ {x y} z → x ≤ y → z ⊓ x ≤ y x≤y⇒z⊓x≤y y x≤y = trans (x⊓y≤y y _) x≤y x≤y⊓z⇒x≤y : ∀ {x} y z → x ≤ y ⊓ z → x ≤ y x≤y⊓z⇒x≤y y z x≤y⊓z = trans x≤y⊓z (x⊓y≤x y z) x≤y⊓z⇒x≤z : ∀ {x} y z → x ≤ y ⊓ z → x ≤ z x≤y⊓z⇒x≤z y z x≤y⊓z = trans x≤y⊓z (x⊓y≤y y z) ⊓-mono-≤ : _⊓_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_ ⊓-mono-≤ {x} {y} {u} {v} x≤y u≤v with ⊓-sel y v ... | inj₁ y⊓v≈y = ≤-respʳ-≈ (Eq.sym y⊓v≈y) (trans (x⊓y≤x x u) x≤y) ... | inj₂ y⊓v≈v = ≤-respʳ-≈ (Eq.sym y⊓v≈v) (trans (x⊓y≤y x u) u≤v) ⊓-monoˡ-≤ : ∀ x → (_⊓ x) Preserves _≤_ ⟶ _≤_ ⊓-monoˡ-≤ x y≤z = ⊓-mono-≤ y≤z (refl {x}) ⊓-monoʳ-≤ : ∀ x → (x ⊓_) Preserves _≤_ ⟶ _≤_ ⊓-monoʳ-≤ x y≤z = ⊓-mono-≤ (refl {x}) y≤z ⊓-glb : ∀ {x y z} → x ≤ y → x ≤ z → x ≤ y ⊓ z ⊓-glb {x} x≤y x≤z = ≤-respˡ-≈ (⊓-idem x) (⊓-mono-≤ x≤y x≤z) ⊓-triangulate : ∀ x y z → x ⊓ y ⊓ z ≈ (x ⊓ y) ⊓ (y ⊓ z) ⊓-triangulate x y z = begin-equality x ⊓ y ⊓ z ≈⟨ ⊓-congʳ z (⊓-congˡ x (⊓-idem y)) ⟨ x ⊓ (y ⊓ y) ⊓ z ≈⟨ ⊓-assoc x _ _ ⟩ x ⊓ ((y ⊓ y) ⊓ z) ≈⟨ ⊓-congˡ x (⊓-assoc y y z) ⟩ x ⊓ (y ⊓ (y ⊓ z)) ≈⟨ ⊓-assoc x y (y ⊓ z) ⟨ (x ⊓ y) ⊓ (y ⊓ z) ∎