------------------------------------------------------------------------
-- The Agda standard library
--
-- Sublist-related properties
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Sublist.Propositional.Properties where

open import Data.Empty
open import Data.List.Base hiding (lookup)
open import Data.List.Properties
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.List.Relation.Unary.Any.Properties using (here-injective; there-injective)
open import Data.List.Membership.Propositional
open import Data.List.Relation.Binary.Sublist.Propositional
open import Data.Maybe as Maybe using (nothing; just)
open import Data.Maybe.Relation.Unary.All as MAll using (nothing; just)
open import Data.Nat.Base
open import Data.Nat.Properties

open import Function
import Function.Bijection as Bij
open import Function.Equivalence as Equiv using (_⇔_ ; equivalence)
import Function.Injection as Inj

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as Eq hiding ([_])
open import Relation.Nullary
import Relation.Nullary.Decidable as D
open import Relation.Unary as U using (Pred)

------------------------------------------------------------------------
-- The `loookup` function induced by a proof that `xs ⊆ ys` is injective

module _ {a} {A : Set a} where

  lookup-injective :  {x : A} {xs ys} {p : xs  ys} {v w : x  xs} 
                     lookup p v  lookup p w  v  w
  lookup-injective {p = skip p} {v} {w} eq =
    lookup-injective (there-injective eq)
  lookup-injective {p = keep p} {here px} {here qx} refl = refl
  lookup-injective {p = keep p} {there v} {there w} eq =
    cong there (lookup-injective (there-injective eq))
  -- impossible cases
  lookup-injective {p = keep p} {here px} {there w} ()
  lookup-injective {p = keep p} {there v} {here qx} ()
  lookup-injective {p = base} {}

  []∈-irrelevant : U.Irrelevant {A = List A} ([] ⊆_)
  []∈-irrelevant base     base     = refl
  []∈-irrelevant (skip p) (skip q) = cong skip ([]∈-irrelevant p q)

  [x]⊆xs↔x∈xs :  {x : A} {xs}  ([ x ]  xs) Bij.⤖ (x  xs)
  [x]⊆xs↔x∈xs {x} =
    Bij.bijection to∈ from∈ (to∈-injective _ _ refl) to∈∘from∈≗id

    where

    to∈-injective :
       {xs x y} (p : [ x ]  xs) (q : [ y ]  xs) (eq : x  y) 
      to∈ p  lookup q (here eq) 
      subst ((_⊆ xs)  [_]) eq p  q
    to∈-injective (skip p) (skip q) refl eq =
      cong skip (to∈-injective p q refl (there-injective eq))
    to∈-injective (keep p) (keep q) eq refl =
      cong keep ([]∈-irrelevant p q)
    to∈-injective (skip p) (keep q) refl ()
    to∈-injective (keep p) (skip q) refl ()

    to∈∘from∈≗id :  {xs} (p : x  xs)  to∈ (from∈ p)  p
    to∈∘from∈≗id (here refl) = refl
    to∈∘from∈≗id (there p)   = cong there (to∈∘from∈≗id p)

------------------------------------------------------------------------
-- Some properties

module _ {a} {A : Set a} where

  ⊆-length :  {xs ys : List A}  xs  ys  length xs  length ys
  ⊆-length base     = ≤-refl
  ⊆-length (skip p) = ≤-step (⊆-length p)
  ⊆-length (keep p) = s≤s (⊆-length p)

------------------------------------------------------------------------
-- Relational properties

module _ {a} {A : Set a} where

  ⊆-reflexive : _≡_  _⊆_ {A = A}
  ⊆-reflexive {[]}     refl = base
  ⊆-reflexive {x  xs} refl = keep (⊆-reflexive refl)

  ⊆-refl : Reflexive {A = List A} _⊆_
  ⊆-refl = ⊆-reflexive refl

  ⊆-trans : Transitive {A = List A} _⊆_
  ⊆-trans p        base     = p
  ⊆-trans p        (skip q) = skip (⊆-trans p q)
  ⊆-trans (skip p) (keep q) = skip (⊆-trans p q)
  ⊆-trans (keep p) (keep q) = keep (⊆-trans p q)

  open ≤-Reasoning

  ⊆-antisym : Antisymmetric {A = List A} _≡_ _⊆_
  ⊆-antisym = λ p q  ⊆-antisym′ p q refl
    where
    ⊆-antisym′ :  {xs ys zs}  xs  ys  ys  zs  xs  zs  xs  ys
    -- Positive cases
    ⊆-antisym′ base     base     refl = refl
    ⊆-antisym′ (keep p) (keep q) eq   =
      cong (_ ∷_) (⊆-antisym′ p q (cong (drop 1) eq))
    -- Dismissing the impossible cases
    ⊆-antisym′ {x  xs} {y  ys} (skip p) (skip q) refl =
      ⊥-elim $ 1+n≰n $ begin
        length (y  ys) ≤⟨ ⊆-length q 
        length xs       ≤⟨ n≤1+n (length xs) 
        length (x  xs) ≤⟨ ⊆-length p 
        length ys       
    ⊆-antisym′ {x  xs} {y  ys} (skip p) (keep q) refl =
      ⊥-elim $ 1+n≰n $ begin
        length (x  xs) ≤⟨ ⊆-length p 
        length ys       ≤⟨ ⊆-length q 
        length xs       
    ⊆-antisym′ {x  xs} {y  ys} (keep p) (skip q) refl =
      ⊥-elim $ 1+n≰n $ begin
        length (y  ys) ≤⟨ ⊆-length q 
        length xs       ≤⟨ ⊆-length p 
        length ys       

  ⊆-minimum : Minimum (_⊆_ {A = A}) []
  ⊆-minimum = []⊆_

module _ {a} (A : Set a) where

  ⊆-isPreorder : IsPreorder _≡_ (_⊆_ {A = A})
  ⊆-isPreorder = record
    { isEquivalence = isEquivalence
    ; reflexive     = ⊆-reflexive
    ; trans         = ⊆-trans
    }

  ⊆-preorder : Preorder _ _ _
  ⊆-preorder = record
    { isPreorder = ⊆-isPreorder
    }

  ⊆-isPartialOrder : IsPartialOrder _≡_ _⊆_
  ⊆-isPartialOrder = record
    { isPreorder = ⊆-isPreorder
    ; antisym    = ⊆-antisym
    }

  ⊆-poset : Poset _ _ _
  ⊆-poset = record
    { isPartialOrder = ⊆-isPartialOrder
    }

import Relation.Binary.Reasoning.PartialOrder as POR

module ⊆-Reasoning {a} {A : Set a}  where
  private module P = POR (⊆-poset A)
  open P public
    renaming (_≤⟨_⟩_ to _⊆⟨_⟩_)
    hiding (_≈⟨_⟩_; _≈˘⟨_⟩_; _≈⟨⟩_)

------------------------------------------------------------------------
-- Various functions' outputs are sublists

module _ {a} {A : Set a} where

  tail-⊆ : (xs : List A)  MAll.All (_⊆ xs) (tail xs)
  tail-⊆ []       = nothing
  tail-⊆ (x  xs) = just (skip ⊆-refl)

  take-⊆ :  n (xs : List A)  take n xs  xs
  take-⊆ zero    xs       = []⊆ xs
  take-⊆ (suc n) []       = []⊆ []
  take-⊆ (suc n) (x  xs) = keep (take-⊆ n xs)

  drop-⊆ :  n (xs : List A)  drop n xs  xs
  drop-⊆ zero    xs       = ⊆-refl
  drop-⊆ (suc n) []       = []⊆ []
  drop-⊆ (suc n) (x  xs) = skip (drop-⊆ n xs)

module _ {a p} {A : Set a} {P : Pred A p} (P? : U.Decidable P) where

  takeWhile-⊆ :  xs  takeWhile P? xs  xs
  takeWhile-⊆ []       = []⊆ []
  takeWhile-⊆ (x  xs) with P? x
  ... | yes p = keep (takeWhile-⊆ xs)
  ... | no ¬p = []⊆ x  xs

  dropWhile-⊆ :  xs  dropWhile P? xs  xs
  dropWhile-⊆ []       = []⊆ []
  dropWhile-⊆ (x  xs) with P? x
  ... | yes p = skip (dropWhile-⊆ xs)
  ... | no ¬p = ⊆-refl

  filter-⊆ :  xs  filter P? xs  xs
  filter-⊆ []       = []⊆ []
  filter-⊆ (x  xs) with P? x
  ... | yes p = keep (filter-⊆ xs)
  ... | no ¬p = skip (filter-⊆ xs)

------------------------------------------------------------------------
-- Various functions are increasing wrt _⊆_


------------------------------------------------------------------------
-- _∷_

module _ {a} {A : Set a} where

  ∷⁻ :  {x y} {us vs : List A}  x  us  y  vs  us  vs
  ∷⁻ (skip p) = ⊆-trans (skip ⊆-refl) p
  ∷⁻ (keep p) = p

-- map

module _ {a b} {A : Set a} {B : Set b} where

  map⁺ :  {xs ys} (f : A  B)  xs  ys  map f xs  map f ys
  map⁺ f base     = base
  map⁺ f (skip p) = skip (map⁺ f p)
  map⁺ f (keep p) = keep (map⁺ f p)

  open Inj.Injection

  map⁻ :  {xs ys} (inj : A Inj.↣ B) 
         map (inj ⟨$⟩_) xs  map (inj ⟨$⟩_) ys  xs  ys
  map⁻ {[]}     {ys}     inj p = []⊆ ys
  map⁻ {x  xs} {[]}     inj ()
  map⁻ {x  xs} {y  ys} inj p
    with inj ⟨$⟩ x | inspect (inj ⟨$⟩_) x
       | inj ⟨$⟩ y | inspect (inj ⟨$⟩_) y
       | injective inj {x} {y}
  map⁻ {x  xs} {y  ys} inj (skip p)
    | fx | Eq.[ eq ] | fy | _ | _ = skip (map⁻ inj (coerce p))
    where coerce = subst  fx  fx  _  _) (sym eq)
  map⁻ {x  xs} {y  ys} inj (keep p)
    | fx | _      | fx | _ | eq
    rewrite eq refl = keep (map⁻ inj p)

-- _++_

module _ {a} {A : Set a} where

  ++⁺ :  {xs ys us vs : List A}  xs  ys  us  vs  xs ++ us  ys ++ vs
  ++⁺ base     q = q
  ++⁺ (skip p) q = skip (++⁺ p q)
  ++⁺ (keep p) q = keep (++⁺ p q)

  ++⁻ :  xs {us vs : List A}  xs ++ us  xs ++ vs  us  vs
  ++⁻ []       p = p
  ++⁻ (x  xs) p = ++⁻ xs (∷⁻ p)

  skips :  {xs ys} (zs : List A)  xs  ys  xs  zs ++ ys
  skips zs = ++⁺ ([]⊆ zs)

-- take / drop

  ≤-take-⊆ :  {m n}  m  n  (xs : List A)  take m xs  take n xs
  ≤-take-⊆ z≤n     xs       = []⊆ take _ xs
  ≤-take-⊆ (s≤s p) []       = []⊆ []
  ≤-take-⊆ (s≤s p) (x  xs) = keep (≤-take-⊆ p xs)

  ≥-drop-⊆ :  {m n}  m  n  (xs : List A)  drop m xs  drop n xs
  ≥-drop-⊆ {m} z≤n     xs       = drop-⊆ m xs
  ≥-drop-⊆     (s≤s p) []       = []⊆ []
  ≥-drop-⊆     (s≤s p) (x  xs) = ≥-drop-⊆ p xs

  drop⁺ :  n {xs ys : List A}  xs  ys  drop n xs  drop n ys
  drop⁺ zero    p        = p
  drop⁺ (suc n) base     = []⊆ []
  drop⁺ (suc n) (keep p) = drop⁺ n p
  drop⁺ (suc n) {xs} {y  ys} (skip p) = begin
    drop (suc n) xs ⊆⟨ ≥-drop-⊆ (n≤1+n n) xs 
    drop n xs       ⊆⟨ drop⁺ n p 
    drop n ys        where open ⊆-Reasoning

module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q}
         (P? : U.Decidable P) (Q? : U.Decidable Q) where

  ⊆-takeWhile-⊆ : (P U.⊆ Q)   xs  takeWhile P? xs  takeWhile Q? xs
  ⊆-takeWhile-⊆ P⊆Q []       = []⊆ []
  ⊆-takeWhile-⊆ P⊆Q (x  xs) with P? x | Q? x
  ... | yes px | yes qx = keep (⊆-takeWhile-⊆ P⊆Q xs)
  ... | yes px | no ¬qx = ⊥-elim $ ¬qx (P⊆Q px)
  ... | no ¬px | _      = []⊆ _

  ⊇-dropWhile-⊆ : (P U.⊇ Q)   xs  dropWhile P? xs  dropWhile Q? xs
  ⊇-dropWhile-⊆ P⊇Q []       = []⊆ []
  ⊇-dropWhile-⊆ P⊇Q (x  xs) with P? x | Q? x
  ... | yes px | yes qx = ⊇-dropWhile-⊆ P⊇Q xs
  ... | yes px | no ¬qx = skip (dropWhile-⊆ P? xs)
  ... | no ¬px | yes qx = ⊥-elim $ ¬px (P⊇Q qx)
  ... | no ¬px | no ¬qx = ⊆-refl

-- filter

  ⊆-filter-⊆ : (P U.⊆ Q)   xs  filter P? xs  filter Q? xs
  ⊆-filter-⊆ P⊆Q []       = []⊆ []
  ⊆-filter-⊆ P⊆Q (x  xs) with P? x | Q? x
  ... | yes px | yes qx = keep (⊆-filter-⊆ P⊆Q xs)
  ... | yes px | no ¬qx = ⊥-elim $ ¬qx (P⊆Q px)
  ... | no ¬px | yes qx = skip (⊆-filter-⊆ P⊆Q xs)
  ... | no ¬px | no ¬qx = ⊆-filter-⊆ P⊆Q xs

module _ {a p} {A : Set a} {P : Pred A p} (P? : U.Decidable P) where

  filter⁺ :  {xs ys : List A}  xs  ys  filter P? xs  filter P? ys
  filter⁺                   base     = base
  filter⁺ {xs}     {y  ys} (skip p) with P? y
  ... | yes py = skip (filter⁺ p)
  ... | no ¬py = filter⁺ p
  filter⁺ {x  xs} {x  ys} (keep p) with P? x
  ... | yes px = keep (filter⁺ p)
  ... | no ¬px = filter⁺ p

-- reverse

module _ {a} {A : Set a} where

  open ⊆-Reasoning

  reverse⁺ : {xs ys : List A}  xs  ys  reverse xs  reverse ys
  reverse⁺ base = []⊆ []
  reverse⁺ {xs} {y  ys} (skip p) = begin
    reverse xs       ≡⟨ sym $ ++-identityʳ _ 
    reverse xs ++ [] ⊆⟨ ++⁺ (reverse⁺ p) ([]⊆ _) 
    reverse ys ∷ʳ y  ≡⟨ sym $ unfold-reverse y ys 
    reverse (y  ys) 
  reverse⁺ {x  xs} {x  ys} (keep p) = begin
    reverse (x  xs) ≡⟨ unfold-reverse x xs 
    reverse xs ∷ʳ x  ⊆⟨ ++⁺ (reverse⁺ p) ⊆-refl 
    reverse ys ∷ʳ x  ≡⟨ sym $ unfold-reverse x ys 
    reverse (x  ys) 

  reverse⁻ : {xs ys : List A}  reverse xs  reverse ys  xs  ys
  reverse⁻ {xs} {ys} p = cast (reverse⁺ p) where
    cast = subst₂ _⊆_ (reverse-involutive xs) (reverse-involutive ys)


------------------------------------------------------------------------
-- Inversion lemmas

module _ {a} {A : Set a} where

  keep⁻¹ :  (x : A) {xs ys}  (xs  ys)  (x  xs  x  ys)
  keep⁻¹ x = equivalence keep ∷⁻

  skip⁻¹ :  {x y : A} {xs ys}  x  y  (x  xs  ys)  (x  xs  y  ys)
  skip⁻¹ ¬eq = equivalence skip $ λ where
    (skip p)  p
    (keep p)  ⊥-elim (¬eq refl)

  ++⁻¹ :  (ps : List A) {xs ys}  (xs  ys)  (ps ++ xs  ps ++ ys)
  ++⁻¹ ps = equivalence (++⁺ ⊆-refl) (++⁻ ps)

------------------------------------------------------------------------
-- Decidability of the order

module Decidable
       {a} {A : Set a} (eq? : Decidable {A = A} _≡_) where

  infix 3 _⊆?_
  _⊆?_ : Decidable {A = List A} _⊆_
  []     ⊆? ys     = yes ([]⊆ ys)
  x  xs ⊆? []     = no λ ()
  x  xs ⊆? y  ys with eq? x y
  ... | yes refl = D.map (keep⁻¹ x) (xs ⊆? ys)
  ... | no ¬eq   = D.map (skip⁻¹ ¬eq) (x  xs ⊆? ys)