------------------------------------------------------------------------ -- The Agda standard library -- -- Properties of min and max operators specified over a total -- preorder. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator) open import Relation.Binary.Bundles using (TotalPreorder) module Algebra.Construct.NaturalChoice.MinMaxOp {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) (maxOp : MaxOperator O) where open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]) open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_; flip) open import Relation.Binary.Core using (_Preserves_⟶_) open TotalPreorder O renaming ( Carrier to A ; _≲_ to _≤_ ; ≲-resp-≈ to ≤-resp-≈ ; ≲-respʳ-≈ to ≤-respʳ-≈ ; ≲-respˡ-≈ to ≤-respˡ-≈ ) open MinOperator minOp open MaxOperator maxOp open import Algebra.Definitions _≈_ open import Algebra.Structures _≈_ open import Algebra.Consequences.Setoid Eq.setoid open import Relation.Binary.Reasoning.Preorder preorder ------------------------------------------------------------------------ -- Re-export properties of individual operators open import Algebra.Construct.NaturalChoice.MinOp minOp public open import Algebra.Construct.NaturalChoice.MaxOp maxOp public ------------------------------------------------------------------------ -- Joint algebraic structures ⊓-distribˡ-⊔ : _⊓_ DistributesOverˡ _⊔_ ⊓-distribˡ-⊔ x y z with total y z ... | inj₁ y≤z = begin-equality x ⊓ (y ⊔ z) ≈⟨ ⊓-congˡ x (x≤y⇒x⊔y≈y y≤z) ⟩ x ⊓ z ≈⟨ x≤y⇒x⊔y≈y (⊓-monoʳ-≤ x y≤z) ⟨ (x ⊓ y) ⊔ (x ⊓ z) ∎ ... | inj₂ y≥z = begin-equality x ⊓ (y ⊔ z) ≈⟨ ⊓-congˡ x (x≥y⇒x⊔y≈x y≥z) ⟩ x ⊓ y ≈⟨ x≥y⇒x⊔y≈x (⊓-monoʳ-≤ x y≥z) ⟨ (x ⊓ y) ⊔ (x ⊓ z) ∎ ⊓-distribʳ-⊔ : _⊓_ DistributesOverʳ _⊔_ ⊓-distribʳ-⊔ = comm∧distrˡ⇒distrʳ ⊔-cong ⊓-comm ⊓-distribˡ-⊔ ⊓-distrib-⊔ : _⊓_ DistributesOver _⊔_ ⊓-distrib-⊔ = ⊓-distribˡ-⊔ , ⊓-distribʳ-⊔ ⊔-distribˡ-⊓ : _⊔_ DistributesOverˡ _⊓_ ⊔-distribˡ-⊓ x y z with total y z ... | inj₁ y≤z = begin-equality x ⊔ (y ⊓ z) ≈⟨ ⊔-congˡ x (x≤y⇒x⊓y≈x y≤z) ⟩ x ⊔ y ≈⟨ x≤y⇒x⊓y≈x (⊔-monoʳ-≤ x y≤z) ⟨ (x ⊔ y) ⊓ (x ⊔ z) ∎ ... | inj₂ y≥z = begin-equality x ⊔ (y ⊓ z) ≈⟨ ⊔-congˡ x (x≥y⇒x⊓y≈y y≥z) ⟩ x ⊔ z ≈⟨ x≥y⇒x⊓y≈y (⊔-monoʳ-≤ x y≥z) ⟨ (x ⊔ y) ⊓ (x ⊔ z) ∎ ⊔-distribʳ-⊓ : _⊔_ DistributesOverʳ _⊓_ ⊔-distribʳ-⊓ = comm∧distrˡ⇒distrʳ ⊓-cong ⊔-comm ⊔-distribˡ-⊓ ⊔-distrib-⊓ : _⊔_ DistributesOver _⊓_ ⊔-distrib-⊓ = ⊔-distribˡ-⊓ , ⊔-distribʳ-⊓ ⊓-absorbs-⊔ : _⊓_ Absorbs _⊔_ ⊓-absorbs-⊔ x y with total x y ... | inj₁ x≤y = begin-equality x ⊓ (x ⊔ y) ≈⟨ ⊓-congˡ x (x≤y⇒x⊔y≈y x≤y) ⟩ x ⊓ y ≈⟨ x≤y⇒x⊓y≈x x≤y ⟩ x ∎ ... | inj₂ y≤x = begin-equality x ⊓ (x ⊔ y) ≈⟨ ⊓-congˡ x (x≥y⇒x⊔y≈x y≤x) ⟩ x ⊓ x ≈⟨ ⊓-idem x ⟩ x ∎ ⊔-absorbs-⊓ : _⊔_ Absorbs _⊓_ ⊔-absorbs-⊓ x y with total x y ... | inj₁ x≤y = begin-equality x ⊔ (x ⊓ y) ≈⟨ ⊔-congˡ x (x≤y⇒x⊓y≈x x≤y) ⟩ x ⊔ x ≈⟨ ⊔-idem x ⟩ x ∎ ... | inj₂ y≤x = begin-equality x ⊔ (x ⊓ y) ≈⟨ ⊔-congˡ x (x≥y⇒x⊓y≈y y≤x) ⟩ x ⊔ y ≈⟨ x≥y⇒x⊔y≈x y≤x ⟩ x ∎ ⊔-⊓-absorptive : Absorptive _⊔_ _⊓_ ⊔-⊓-absorptive = ⊔-absorbs-⊓ , ⊓-absorbs-⊔ ⊓-⊔-absorptive : Absorptive _⊓_ _⊔_ ⊓-⊔-absorptive = ⊓-absorbs-⊔ , ⊔-absorbs-⊓ ------------------------------------------------------------------------ -- Other joint properties private _≥_ = flip _≤_ antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≈_ ⟶ _≈_ → f Preserves _≤_ ⟶ _≥_ → ∀ x y → f (x ⊓ y) ≈ f x ⊔ f y antimono-≤-distrib-⊓ {f} cong antimono 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 (antimono 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 (antimono y≤x) ⟨ f x ⊔ f y ∎ antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≈_ ⟶ _≈_ → f Preserves _≤_ ⟶ _≥_ → ∀ x y → f (x ⊔ y) ≈ f x ⊓ f y antimono-≤-distrib-⊔ {f} cong antimono x y with total x y ... | inj₁ x≤y = begin-equality f (x ⊔ y) ≈⟨ cong (x≤y⇒x⊔y≈y x≤y) ⟩ f y ≈⟨ x≥y⇒x⊓y≈y (antimono x≤y) ⟨ f x ⊓ f y ∎ ... | inj₂ y≤x = begin-equality f (x ⊔ y) ≈⟨ cong (x≥y⇒x⊔y≈x y≤x) ⟩ f x ≈⟨ x≤y⇒x⊓y≈x (antimono y≤x) ⟨ f x ⊓ f y ∎ x⊓y≤x⊔y : ∀ x y → x ⊓ y ≤ x ⊔ y x⊓y≤x⊔y x y = begin x ⊓ y ∼⟨ x⊓y≤x x y ⟩ x ∼⟨ x≤x⊔y x y ⟩ x ⊔ y ∎