------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of unique lists (setoid equality)
------------------------------------------------------------------------

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

module Data.List.Relation.Unary.Unique.Propositional.Properties where

open import Data.List.Base using (map; _++_; concat; cartesianProductWith;
  cartesianProduct; drop; take; applyUpTo; upTo; applyDownFrom; downFrom;
  tabulate; allFin; filter)
open import Data.List.Relation.Binary.Disjoint.Propositional
  using (Disjoint)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
import Data.List.Relation.Unary.Unique.Setoid.Properties as Setoid
open import Data.Fin.Base using (Fin)
open import Data.Nat.Base using (_<_)
open import Data.Nat.Properties using (<⇒≢)
open import Data.Product.Base using (_×_; _,_)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (≡⇒≡×≡)
open import Function.Base using (id; _∘_)
open import Level using (Level)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality.Core
  using (refl; _≡_; _≢_; sym)
open import Relation.Binary.PropositionalEquality.Properties using (setoid)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary.Negation using (¬_)

private
  variable
    a b c p : Level

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

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

  map⁺ :  {f}  (∀ {x y}  f x  f y  x  y) 
          {xs}  Unique xs  Unique (map f xs)
  map⁺ = Setoid.map⁺ (setoid A) (setoid B)

------------------------------------------------------------------------
-- ++

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

  ++⁺ : Unique xs  Unique ys  Disjoint xs ys  Unique (xs ++ ys)
  ++⁺ = Setoid.++⁺ (setoid A)

------------------------------------------------------------------------
-- concat

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

  concat⁺ : All Unique xss  AllPairs Disjoint xss  Unique (concat xss)
  concat⁺ = Setoid.concat⁺ (setoid A)

------------------------------------------------------------------------
-- cartesianProductWith

module _ {A : Set a} {B : Set b} {C : Set c} {xs ys} where

  cartesianProductWith⁺ :  f  (∀ {w x y z}  f w y  f x z  w  x × y  z) 
                          Unique xs  Unique ys 
                          Unique (cartesianProductWith f xs ys)
  cartesianProductWith⁺ = Setoid.cartesianProductWith⁺ (setoid A) (setoid B) (setoid C)

------------------------------------------------------------------------
-- cartesianProduct

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

  cartesianProduct⁺ :  {xs ys}  Unique xs  Unique ys 
                      Unique (cartesianProduct xs ys)
  cartesianProduct⁺ xs ys = AllPairs.map (_∘ ≡⇒≡×≡)
    (Setoid.cartesianProduct⁺ (setoid A) (setoid B) xs ys)

------------------------------------------------------------------------
-- take & drop

module _ {A : Set a} where

  drop⁺ :  {xs} n  Unique xs  Unique (drop n xs)
  drop⁺ = Setoid.drop⁺ (setoid A)

  take⁺ :  {xs} n  Unique xs  Unique (take n xs)
  take⁺ = Setoid.take⁺ (setoid A)

------------------------------------------------------------------------
-- applyUpTo & upTo

module _ {A : Set a} where

  applyUpTo⁺₁ :  f n  (∀ {i j}  i < j  j < n  f i  f j) 
                Unique (applyUpTo f n)
  applyUpTo⁺₁ = Setoid.applyUpTo⁺₁ (setoid A)

  applyUpTo⁺₂ :  f n  (∀ i j  f i  f j) 
                Unique (applyUpTo f n)
  applyUpTo⁺₂ = Setoid.applyUpTo⁺₂  (setoid A)

------------------------------------------------------------------------
-- upTo

upTo⁺ :  n  Unique (upTo n)
upTo⁺ n = applyUpTo⁺₁ id n  i<j _  <⇒≢ i<j)

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

module _ {A : Set a} where

  applyDownFrom⁺₁ :  f n  (∀ {i j}  j < i  i < n  f i  f j) 
                    Unique (applyDownFrom f n)
  applyDownFrom⁺₁ = Setoid.applyDownFrom⁺₁ (setoid A)

  applyDownFrom⁺₂ :  f n  (∀ i j  f i  f j) 
                    Unique (applyDownFrom f n)
  applyDownFrom⁺₂ = Setoid.applyDownFrom⁺₂ (setoid A)

------------------------------------------------------------------------
-- downFrom

downFrom⁺ :  n  Unique (downFrom n)
downFrom⁺ n = applyDownFrom⁺₁ id n  j<i _  <⇒≢ j<i  sym)

------------------------------------------------------------------------
-- tabulate

module _ {A : Set a} where

  tabulate⁺ :  {n} {f : Fin n  A}  (∀ {i j}  f i  f j  i  j) 
              Unique (tabulate f)
  tabulate⁺ = Setoid.tabulate⁺ (setoid A)

------------------------------------------------------------------------
-- allFin

allFin⁺ :  n  Unique (allFin n)
allFin⁺ n = tabulate⁺ id

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

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

  filter⁺ :  {xs}  Unique xs  Unique (filter P? xs)
  filter⁺ = Setoid.filter⁺ (setoid A) P?