------------------------------------------------------------------------
-- 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 ( List; _∷_; map; _++_; concat; cartesianProductWith
        ; cartesianProduct; drop; take; applyUpTo; upTo; applyDownFrom; downFrom
        ; tabulate; allFin; filter
        )
open import Data.List.Membership.Propositional using (_∉_)
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; cong)
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
    A : Set a
    x y : A
    xs : List A
 
------------------------------------------------------------------------
-- 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)
 
  map⁻ : ∀ {f xs} → Unique (map f xs) → Unique xs
  map⁻ = Setoid.map⁻ (setoid A) (setoid B) (cong _)
 
------------------------------------------------------------------------
-- ++
 
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?
 
------------------------------------------------------------------------
-- ∷
 
Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
Unique[x∷xs]⇒x∉xs = Setoid.Unique[x∷xs]⇒x∉xs (setoid _)