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

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

open import Relation.Binary using (Trans; 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 using (_×_; _,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality 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)