------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of a min operator derived from a spec over a total order.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Algebra.Core
open import Algebra.Bundles
open import Algebra.Construct.NaturalChoice.Base
open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_])
open import Data.Product using (_,_)
open import Function.Base using (id; _∘_)
open import Relation.Binary
open import Relation.Binary.Consequences

module Algebra.Construct.NaturalChoice.MinOp
  {a ℓ₁ ℓ₂} {O : TotalPreorder a ℓ₁ ℓ₂} (minOp : MinOperator O) where

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 = ≤-respˡ-≈ (Eq.sym (x≤y⇒x⊓y≈x x≤y)) refl
... | 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 = ≤-respˡ-≈ (Eq.sym (x≥y⇒x⊓y≈y y≤x)) refl

------------------------------------------------------------------------
-- 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
  }

⊓-isSemilattice : IsSemilattice _⊓_
⊓-isSemilattice = record
  { isBand = ⊓-isBand
  ; comm   = ⊓-comm
  }

⊓-isSelectiveMagma : IsSelectiveMagma _⊓_
⊓-isSelectiveMagma = record
  { isMagma = ⊓-isMagma
  ; sel     = ⊓-sel
  }

⊓-isMonoid :  {}  Maximum _≤_   IsMonoid _⊓_ 
⊓-isMonoid max = record
  { isSemigroup = ⊓-isSemigroup
  ; identity    = ⊓-identity max
  }

------------------------------------------------------------------------
-- Raw bandles

⊓-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
  }

⊓-semilattice : Semilattice _ _
⊓-semilattice = record
  { isSemilattice = ⊓-isSemilattice
  }

⊓-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)