------------------------------------------------------------------------
-- The Agda standard library
--
-- Sorted lists
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Sorted.TotalOrder.Properties where

open import Data.List.Base
open import Data.List.Relation.Unary.All using (All)
open import Data.List.Relation.Unary.AllPairs using (AllPairs)
open import Data.List.Relation.Unary.Linked as Linked
  using (Linked; []; [-]; _∷_; _∷′_; head′; tail)
import Data.List.Relation.Unary.Linked.Properties as Linked
import Data.List.Relation.Binary.Equality.Setoid as Equality
import Data.List.Relation.Binary.Sublist.Setoid as Sublist
import Data.List.Relation.Binary.Sublist.Setoid.Properties as SublistProperties
import Data.List.Relation.Binary.Permutation.Setoid as Permutation
import Data.List.Relation.Binary.Permutation.Setoid.Properties as PermutationProperties
import Data.List.Relation.Binary.Pointwise as Pointwise
open import Data.List.Relation.Unary.Sorted.TotalOrder as Sorted hiding (head)

open import Data.Fin.Base as Fin hiding (_<_; _≤_)
import Data.Fin.Properties as Fin
open import Data.Fin.Permutation
open import Data.Product using (_,_)
open import Data.Maybe.Base using (just; nothing)
open import Data.Maybe.Relation.Binary.Connected using (Connected; just)
open import Data.Nat.Base as  using (; z≤n; s≤s; zero; suc)
import Data.Nat.Properties as 
open import Function.Base using (_∘_; const)
open import Function.Bundles using (Inverse)
open import Function.Consequences.Propositional using (inverseʳ⇒injective)
open import Level using (Level)
open import Relation.Binary.Core using (_Preserves_⟶_; Rel)
open import Relation.Binary.Bundles using (TotalOrder; DecTotalOrder; Preorder)
import Relation.Binary.Properties.TotalOrder as TotalOrderProperties
import Relation.Binary.Reasoning.PartialOrder as PosetReasoning
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (contradiction)
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Binary.PropositionalEquality.Core as  using (_≡_)

private
  variable
    a b p ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level

------------------------------------------------------------------------
-- Relationship to other predicates
------------------------------------------------------------------------

module _ (O : TotalOrder a ℓ₁ ℓ₂) where
  open TotalOrder O

  AllPairs⇒Sorted :  {xs}  AllPairs _≤_ xs  Sorted O xs
  AllPairs⇒Sorted = Linked.AllPairs⇒Linked

  Sorted⇒AllPairs :  {xs}  Sorted O xs  AllPairs _≤_ xs
  Sorted⇒AllPairs = Linked.Linked⇒AllPairs trans

------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for list operations
------------------------------------------------------------------------
-- map

module _ (O₁ : TotalOrder a ℓ₁ ℓ₂) (O₂ : TotalOrder a ℓ₁ ℓ₂) where
  private
    module O₁ = TotalOrder O₁
    module O₂ = TotalOrder O₂

  map⁺ :  {f xs}  f Preserves O₁._≤_  O₂._≤_ 
         Sorted O₁ xs  Sorted O₂ (map f xs)
  map⁺ pres xs↗ = Linked.map⁺ (Linked.map pres xs↗)

  map⁻ :  {f xs}  (∀ {x y}  f x O₂.≤ f y  x O₁.≤ y) 
         Sorted O₂ (map f xs)  Sorted O₁ xs
  map⁻ pres fxs↗ = Linked.map pres (Linked.map⁻ fxs↗)

------------------------------------------------------------------------
-- _++_

module _ (O : TotalOrder a ℓ₁ ℓ₂) where
  open TotalOrder O

  ++⁺ :  {xs ys}  Sorted O xs  Connected _≤_ (last xs) (head ys) 
        Sorted O ys  Sorted O (xs ++ ys)
  ++⁺ = Linked.++⁺

------------------------------------------------------------------------
-- applyUpTo

module _ (O : TotalOrder a ℓ₁ ℓ₂) where
  open TotalOrder O

  applyUpTo⁺₁ :  f n  (∀ {i}  suc i ℕ.< n  f i  f (suc i)) 
                Sorted O (applyUpTo f n)
  applyUpTo⁺₁ = Linked.applyUpTo⁺₁

  applyUpTo⁺₂ :  f n  (∀ i  f i  f (suc i)) 
                Sorted O (applyUpTo f n)
  applyUpTo⁺₂ = Linked.applyUpTo⁺₂

------------------------------------------------------------------------
-- applyDownFrom

module _ (O : TotalOrder a ℓ₁ ℓ₂) where
  open TotalOrder O

  applyDownFrom⁺₁ :  f n  (∀ {i}  suc i ℕ.< n  f (suc i)  f i) 
                    Sorted O (applyDownFrom f n)
  applyDownFrom⁺₁ = Linked.applyDownFrom⁺₁

  applyDownFrom⁺₂ :  f n  (∀ i  f (suc i)  f i) 
                    Sorted O (applyDownFrom f n)
  applyDownFrom⁺₂ = Linked.applyDownFrom⁺₂


------------------------------------------------------------------------
-- merge

module _ (DO : DecTotalOrder a ℓ₁ ℓ₂) where
  open DecTotalOrder DO using (_≤_; _≤?_) renaming (totalOrder to O)
  open TotalOrderProperties O using (≰⇒≥)

  private
    merge-con :  {v xs ys} 
                Connected _≤_ (just v) (head xs) 
                Connected _≤_ (just v) (head ys) 
                Connected _≤_ (just v) (head (merge _≤?_ xs ys))
    merge-con {xs = []}              cxs cys = cys
    merge-con {xs = x  xs} {[]}     cxs cys = cxs
    merge-con {xs = x  xs} {y  ys} cxs cys with x ≤? y
    ... | yes x≤y = cxs
    ... | no  x≰y = cys

  merge⁺ :  {xs ys}  Sorted O xs  Sorted O ys  Sorted O (merge _≤?_ xs ys)
  merge⁺ {[]}              rxs rys = rys
  merge⁺ {x  xs} {[]}     rxs rys = rxs
  merge⁺ {x  xs} {y  ys} rxs rys
   with x ≤? y  | merge⁺ (Linked.tail rxs) rys
                      | merge⁺ rxs (Linked.tail rys)
  ... | yes x≤y | rec | _   = merge-con (head′ rxs)      (just x≤y)  ∷′ rec
  ... | no  x≰y | _   | rec = merge-con (just (≰⇒≥ x≰y)) (head′ rys) ∷′ rec

  -- Reexport ⊆-mergeˡʳ

  S = Preorder.Eq.setoid (DecTotalOrder.preorder DO)
  open Sublist S using (_⊆_)
  module SP = SublistProperties S

  ⊆-mergeˡ :  xs ys  xs  merge _≤?_ xs ys
  ⊆-mergeˡ = SP.⊆-mergeˡ _≤?_

  ⊆-mergeʳ :  xs ys  ys  merge _≤?_ xs ys
  ⊆-mergeʳ = SP.⊆-mergeʳ _≤?_

------------------------------------------------------------------------
-- filter

module _ (O : TotalOrder a ℓ₁ ℓ₂) {P : Pred _ p} (P? : Decidable P) where
  open TotalOrder O

  filter⁺ :  {xs}  Sorted O xs  Sorted O (filter P? xs)
  filter⁺ = Linked.filter⁺ P? trans

------------------------------------------------------------------------
-- lookup

module _ (O : TotalOrder a ℓ₁ ℓ₂) where
  open TotalOrder O

  lookup-mono-≤ :  {xs}  Sorted O xs 
                   {i j}  i Fin.≤ j  lookup xs i  lookup xs j
  lookup-mono-≤ {x  xs} xs↗ {zero}  {zero}  z≤n       = refl
  lookup-mono-≤ {x  xs} xs↗ {zero}  {suc j} z≤n       = Linked.lookup trans xs↗ (just refl) (suc j)
  lookup-mono-≤ {x  xs} xs↗ {suc i} {suc j} (s≤s i≤j) = lookup-mono-≤ (Sorted.tail O {y = x} xs↗) i≤j

------------------------------------------------------------------------
-- Relationship to binary relations
------------------------------------------------------------------------

module _ (O : TotalOrder a ℓ₁ ℓ₂) where
  open TotalOrder O
  open Equality Eq.setoid
  open Permutation Eq.setoid hiding (refl; trans)
  open PermutationProperties Eq.setoid
  open PosetReasoning poset

  -- Proof that any two sorted lists that are a permutation of each
  -- other are pointwise equal
  ↗↭↗⇒≋ :  {xs ys}  Sorted O xs  Sorted O ys  xs  ys  xs  ys
  ↗↭↗⇒≋ {xs} {ys} xs↗ ys↗ xs↭ys = Pointwise.lookup⁻
    (xs↭ys⇒|xs|≡|ys| xs↭ys)
     i≡j  antisym
      (↗↭↗⇒≤ (↭-sym xs↭ys) ys↗ xs↗ (≡.sym i≡j))
      (↗↭↗⇒≤ xs↭ys  xs↗ ys↗ i≡j))
    where
    ↗↭↗⇒≤ :  {xs ys}
              (xs↭ys : xs  ys) 
              Sorted O xs  Sorted O ys 
               {i j}  toℕ i  toℕ j 
              lookup ys j  lookup xs i
    ↗↭↗⇒≤ {xs} {ys} xs↭ys xs↗ ys↗ {i} {j} i≡j
      with Fin.injective⇒existsPivot (inverseʳ⇒injective _ (Inverse.inverseʳ (onIndices xs↭ys))) i
    ... | (k , k≤i , i≤π[k]) = begin
      lookup ys j                         ≤⟨ lookup-mono-≤ O ys↗ (≡.subst (ℕ._≤ _) i≡j i≤π[k]) 
      lookup ys (onIndices xs↭ys ⟨$⟩ʳ k)  ≈⟨ onIndices-lookup xs↭ys k 
      lookup xs k                         ≤⟨ lookup-mono-≤ O xs↗ k≤i 
      lookup xs i