------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the heterogeneous infix relation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Infix.Heterogeneous.Properties where

open import Level
open import Data.Bool.Base using (true; false)
open import Data.Empty using (⊥-elim)
open import Data.List.Base as List using (List; []; _∷_; length; map; filter; replicate)
open import Data.Nat.Base using (zero; suc; _≤_)
import Data.Nat.Properties as ℕₚ
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function.Base using (case_of_; _$′_)

open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_)
open import Relation.Nullary.Negation using (¬_; contradiction)
open import Relation.Unary as U using (Pred)
open import Relation.Binary.Core using (REL; _⇒_)
open import Relation.Binary.Definitions using (Decidable; Trans; Antisym)
open import Relation.Binary.PropositionalEquality.Core using (_≢_; refl; cong)
open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
open import Data.List.Relation.Binary.Infix.Heterogeneous
open import Data.List.Relation.Binary.Prefix.Heterogeneous
  as Prefix using (Prefix; []; _∷_)
import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties as Prefixₚ
open import Data.List.Relation.Binary.Suffix.Heterogeneous
  as Suffix using (Suffix; here; there)

private
  variable
    a b r s : Level
    A : Set a
    B : Set b
    R : REL A B r
    S : REL A B s

------------------------------------------------------------------------
-- Conversion functions

fromPointwise :  {as bs}  Pointwise R as bs  Infix R as bs
fromPointwise pw = here (Prefixₚ.fromPointwise pw)

fromSuffix :  {as bs}  Suffix R as bs  Infix R as bs
fromSuffix (here pw) = fromPointwise pw
fromSuffix (there p) = there (fromSuffix p)

module _ {c t} {C : Set c} {T : REL A C t} where

  fromPrefixSuffix : Trans R S T  Trans (Prefix R) (Suffix S) (Infix T)
  fromPrefixSuffix tr p (here q)  = here (Prefixₚ.trans tr p (Prefixₚ.fromPointwise q))
  fromPrefixSuffix tr p (there q) = there (fromPrefixSuffix tr p q)

  fromSuffixPrefix : Trans R S T  Trans (Suffix R) (Prefix S) (Infix T)
  fromSuffixPrefix tr (here p)  q       = here (Prefixₚ.trans tr (Prefixₚ.fromPointwise p) q)
  fromSuffixPrefix tr (there p) (_  q) = there (fromSuffixPrefix tr p q)

∷⁻ :  {as b bs}  Infix R as (b  bs)  Prefix R as (b  bs)  Infix R as bs
∷⁻ (here pref) = inj₁ pref
∷⁻ (there inf) = inj₂ inf

------------------------------------------------------------------------
-- length

length-mono :  {as bs}  Infix R as bs  length as  length bs
length-mono (here pref) = Prefixₚ.length-mono pref
length-mono (there p)   = ℕₚ.m≤n⇒m≤1+n (length-mono p)

------------------------------------------------------------------------
-- As an order

module _ {c t} {C : Set c} {T : REL A C t} where

  Prefix-Infix-trans : Trans R S T  Trans (Prefix R) (Infix S) (Infix T)
  Prefix-Infix-trans tr p (here q)  = here (Prefixₚ.trans tr p q)
  Prefix-Infix-trans tr p (there q) = there (Prefix-Infix-trans tr p q)

  Infix-Prefix-trans : Trans R S T  Trans (Infix R) (Prefix S) (Infix T)
  Infix-Prefix-trans tr (here p)  q       = here (Prefixₚ.trans tr p q)
  Infix-Prefix-trans tr (there p) (_  q) = there (Infix-Prefix-trans tr p q)

  Suffix-Infix-trans : Trans R S T  Trans (Suffix R) (Infix S) (Infix T)
  Suffix-Infix-trans tr p (here q)  = fromSuffixPrefix tr p q
  Suffix-Infix-trans tr p (there q) = there (Suffix-Infix-trans tr p q)

  Infix-Suffix-trans : Trans R S T  Trans (Infix R) (Suffix S) (Infix T)
  Infix-Suffix-trans tr p (here q)  = Infix-Prefix-trans tr p (Prefixₚ.fromPointwise q)
  Infix-Suffix-trans tr p (there q) = there (Infix-Suffix-trans tr p q)

  trans : Trans R S T  Trans (Infix R) (Infix S) (Infix T)
  trans tr p (here q)  = Infix-Prefix-trans tr p q
  trans tr p (there q) = there (trans tr p q)

  antisym : Antisym R S T  Antisym (Infix R) (Infix S) (Pointwise T)
  antisym asym (here p) (here q) = Prefixₚ.antisym asym p q
  antisym asym {i = a  as} {j = bs} p@(here _) (there q)
    = ⊥-elim $′ ℕₚ.<-irrefl refl $′ begin-strict
      length as <⟨ length-mono p 
      length bs ≤⟨ length-mono q 
      length as  where open ℕₚ.≤-Reasoning
  antisym asym {i = as} {j = b  bs} (there p) q@(here _)
    = ⊥-elim $′ ℕₚ.<-irrefl refl $′ begin-strict
      length bs <⟨ length-mono q 
      length as ≤⟨ length-mono p 
      length bs  where open ℕₚ.≤-Reasoning
  antisym asym {i = a  as} {j = b  bs} (there p) (there q)
    = ⊥-elim $′ ℕₚ.<-irrefl refl $′ begin-strict
      length as <⟨ length-mono p 
      length bs <⟨ length-mono q 
      length as  where open ℕₚ.≤-Reasoning

------------------------------------------------------------------------
-- map

module _ {c d r} {C : Set c} {D : Set d} {R : REL C D r} where

  map⁺ :  {as bs} (f : A  C) (g : B  D) 
         Infix  a b  R (f a) (g b)) as bs 
         Infix R (List.map f as) (List.map g bs)
  map⁺ f g (here p)  = here (Prefixₚ.map⁺ f g p)
  map⁺ f g (there p) = there (map⁺ f g p)

  map⁻ :  {as bs} (f : A  C) (g : B  D) 
         Infix R (List.map f as) (List.map g bs) 
         Infix  a b  R (f a) (g b)) as bs
  map⁻ {bs = []}     f g (here p)  = here (Prefixₚ.map⁻ f g p)
  map⁻ {bs = b  bs} f g (here p)  = here (Prefixₚ.map⁻ f g p)
  map⁻ {bs = b  bs} f g (there p) = there (map⁻ f g p)

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

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

  filter⁺ :  {as bs}  Infix R as bs  Infix R (filter P? as) (filter Q? bs)
  filter⁺ (here p) = here (Prefixₚ.filter⁺ P? Q?  _  P⇒Q)  _  Q⇒P) p)
  filter⁺ {bs = b  bs} (there p) with does (Q? b)
  ... | true = there (filter⁺ p)
  ... | false = filter⁺ p

------------------------------------------------------------------------
-- replicate

replicate⁺ :  {m n a b}  m  n  R a b 
             Infix R (replicate m a) (replicate n b)
replicate⁺ m≤n r = here (Prefixₚ.replicate⁺ m≤n r)

replicate⁻ :  {m n a b}  m  0 
             Infix R (replicate m a) (replicate n b)  R a b
replicate⁻ {m = m} {n = zero}  m≢0 (here p)  = Prefixₚ.replicate⁻ m≢0 p
replicate⁻ {m = m} {n = suc n} m≢0 (here p)  = Prefixₚ.replicate⁻ m≢0 p
replicate⁻ {m = m} {n = suc n} m≢0 (there p) = replicate⁻ m≢0 p

------------------------------------------------------------------------
-- decidability

infix? : Decidable R  Decidable (Infix R)
infix? R? [] [] = yes (here [])
infix? R? (a  as) [] = no  where (here ()))
infix? R? as bbs@(_  bs) =
  map′ [ here , there ]′ ∷⁻
  (Prefixₚ.prefix? R? as bbs ⊎-dec infix? R? as bs)