------------------------------------------------------------------------
-- The Agda standard library
--
-- Core lemmas needed to make list argmin/max functions work
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Definitions using (Trans)
open import Relation.Binary.Bundles using (TotalOrder; Setoid)

module Data.List.Extrema.Core
  {b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where

open import Algebra.Core
open import Algebra.Definitions
import Algebra.Construct.NaturalChoice.Min as Min
import Algebra.Construct.NaturalChoice.Max as Max
open import Data.Product.Base using (_×_; _,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)

open import Algebra.Construct.LiftedChoice

open TotalOrder totalOrder renaming (Carrier to B)
open import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_
  using (_<_; <-≤-trans; ≤-<-trans)

------------------------------------------------------------------------
-- Setup

-- open NonStrictToStrict totalOrder using (_<_; ≤-<-trans; <-≤-trans)

open Max totalOrder
open Min totalOrder

private

  variable
    a : Level
    A : Set a

  <-transʳ : Trans _≤_ _<_ _<_
  <-transʳ = ≤-<-trans trans antisym ≤-respˡ-≈

  <-transˡ : Trans _<_ _≤_ _<_
  <-transˡ = <-≤-trans Eq.sym trans antisym ≤-respʳ-≈

  module _ (f : A → B) where

    lemma₁ : ∀ {x y v} → f x ≤ v → f x ⊓ f y ≈ f y → f y ≤ v
    lemma₁ fx≤v fx⊓fy≈fy = trans (x⊓y≈y⇒y≤x fx⊓fy≈fy) fx≤v

    lemma₂ : ∀ {x y v} → f y ≤ v → f x ⊓ f y ≈ f x → f x ≤ v
    lemma₂ fy≤v fx⊓fy≈fx = trans (x⊓y≈x⇒x≤y fx⊓fy≈fx) fy≤v

    lemma₃ : ∀ {x y v} → f x < v → f x ⊓ f y ≈ f y → f y < v
    lemma₃ fx<v fx⊓fy≈fy = <-transʳ (x⊓y≈y⇒y≤x fx⊓fy≈fy) fx<v

    lemma₄ : ∀ {x y v} → f y < v → f x ⊓ f y ≈ f x → f x < v
    lemma₄ fx<v fx⊓fy≈fy = <-transʳ (x⊓y≈x⇒x≤y fx⊓fy≈fy) fx<v

------------------------------------------------------------------------
-- Definition of lifted max and min

⊓ᴸ : (A → B) → Op₂ A
⊓ᴸ = Lift _≈_ _⊓_ ⊓-sel

⊔ᴸ : (A → B) → Op₂ A
⊔ᴸ = Lift _≈_ _⊔_ ⊔-sel

------------------------------------------------------------------------
-- Properties of ⊓ᴸ

⊓ᴸ-sel : ∀ f → Selective {A = A} _≡_ (⊓ᴸ f)
⊓ᴸ-sel f = sel-≡ ⊓-isSelectiveMagma f

⊓ᴸ-presᵒ-≤v : ∀ f {v} (x y : A) → f x ≤ v ⊎ f y ≤ v → f (⊓ᴸ f x y) ≤ v
⊓ᴸ-presᵒ-≤v f = preservesᵒ ⊓-isSelectiveMagma f (lemma₁ f) (lemma₂ f)

⊓ᴸ-presᵒ-<v : ∀ f {v} (x y : A) → f x < v ⊎ f y < v → f (⊓ᴸ f x y) < v
⊓ᴸ-presᵒ-<v f = preservesᵒ ⊓-isSelectiveMagma f (lemma₃ f) (lemma₄ f)

⊓ᴸ-presᵇ-v≤ : ∀ f {v} {x y : A} → v ≤ f x → v ≤ f y → v ≤ f (⊓ᴸ f x y)
⊓ᴸ-presᵇ-v≤ f {v} = preservesᵇ ⊓-isSelectiveMagma {P = λ x → v ≤ f x} f

⊓ᴸ-presᵇ-v< : ∀ f {v} {x y : A} → v < f x → v < f y → v < f (⊓ᴸ f x y)
⊓ᴸ-presᵇ-v< f {v} = preservesᵇ ⊓-isSelectiveMagma {P = λ x → v < f x} f

⊓ᴸ-forcesᵇ-v≤ : ∀ f {v} (x y : A) → v ≤ f (⊓ᴸ f x y) → v ≤ f x × v ≤ f y
⊓ᴸ-forcesᵇ-v≤ f {v} = forcesᵇ ⊓-isSelectiveMagma f
  (λ v≤fx fx⊓fy≈fx → trans v≤fx (x⊓y≈x⇒x≤y fx⊓fy≈fx))
  (λ v≤fy fx⊓fy≈fy → trans v≤fy (x⊓y≈y⇒y≤x fx⊓fy≈fy))

------------------------------------------------------------------------
-- Properties of ⊔ᴸ

⊔ᴸ-sel : ∀ f → Selective {A = A} _≡_ (⊔ᴸ f)
⊔ᴸ-sel f = sel-≡ ⊔-isSelectiveMagma f

⊔ᴸ-presᵒ-v≤ : ∀ f {v} (x y : A) → v ≤ f x ⊎ v ≤ f y → v ≤ f (⊔ᴸ f x y)
⊔ᴸ-presᵒ-v≤ f {v} = preservesᵒ ⊔-isSelectiveMagma f
  (λ v≤fx fx⊔fy≈fy → trans v≤fx (x⊔y≈y⇒x≤y fx⊔fy≈fy))
  (λ v≤fy fx⊔fy≈fx → trans v≤fy (x⊔y≈x⇒y≤x fx⊔fy≈fx))

⊔ᴸ-presᵒ-v< : ∀ f {v} (x y : A) → v < f x ⊎ v < f y → v < f (⊔ᴸ f x y)
⊔ᴸ-presᵒ-v< f {v} = preservesᵒ ⊔-isSelectiveMagma f
  (λ v<fx fx⊔fy≈fy → <-transˡ v<fx (x⊔y≈y⇒x≤y fx⊔fy≈fy))
  (λ v<fy fx⊔fy≈fx → <-transˡ v<fy (x⊔y≈x⇒y≤x fx⊔fy≈fx))

⊔ᴸ-presᵇ-≤v : ∀ f {v} {x y : A} → f x ≤ v → f y ≤ v → f (⊔ᴸ f x y) ≤ v
⊔ᴸ-presᵇ-≤v f {v} = preservesᵇ ⊔-isSelectiveMagma {P = λ x → f x ≤ v} f

⊔ᴸ-presᵇ-<v : ∀ f {v} {x y : A} → f x < v → f y < v → f (⊔ᴸ f x y) < v
⊔ᴸ-presᵇ-<v f {v} = preservesᵇ ⊔-isSelectiveMagma {P = λ x → f x < v} f

⊔ᴸ-forcesᵇ-≤v : ∀ f {v} (x y : A) → f (⊔ᴸ f x y) ≤ v → f x ≤ v × f y ≤ v
⊔ᴸ-forcesᵇ-≤v f {v} = forcesᵇ ⊔-isSelectiveMagma f
  (λ fx≤v fx⊔fy≈fx → trans (x⊔y≈x⇒y≤x fx⊔fy≈fx) fx≤v)
  (λ fy≤v fx⊔fy≈fy → trans (x⊔y≈y⇒x≤y fx⊔fy≈fy) fy≤v)