{-# 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)
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
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)
module _ {A : Set a} {xss} where
concat⁺ : All Unique xss → AllPairs Disjoint xss → Unique (concat xss)
concat⁺ = Setoid.concat⁺ (setoid A)
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)
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)
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)
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⁺ : ∀ n → Unique (upTo n)
upTo⁺ n = applyUpTo⁺₁ id n (λ i<j _ → <⇒≢ i<j)
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⁺ : ∀ n → Unique (downFrom n)
downFrom⁺ n = applyDownFrom⁺₁ id n (λ j<i _ → <⇒≢ j<i ∘ sym)
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⁺ : ∀ n → Unique (allFin n)
allFin⁺ n = tabulate⁺ id
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 _)