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