{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Membership.Setoid.Properties where
open import Algebra using (Op₂; Selective)
open import Data.Bool.Base using (true; false)
open import Data.Fin.Base using (Fin; zero; suc)
open import Data.Fin.Properties using (suc-injective)
open import Data.List.Base hiding (find)
import Data.List.Membership.Setoid as Membership
import Data.List.Relation.Binary.Equality.Setoid as Equality
open import Data.List.Relation.Unary.All as All using (All)
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
import Data.List.Relation.Unary.Any.Properties as Any
import Data.List.Relation.Unary.Unique.Setoid as Unique
open import Data.Nat.Base using (suc; z<s; _<_)
open import Data.Product.Base as Product using (∃; _×_; _,_ ; ∃₂)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function.Base using (_$_; flip; _∘_; _∘′_; id)
open import Function.Bundles using (_↔_)
open import Level using (Level)
open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_; _Preserves_⟶_)
open import Relation.Binary.Definitions as Binary hiding (Decidable)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
open import Relation.Nullary.Decidable using (does; _because_; yes; no)
open import Relation.Nullary.Negation using (¬_; contradiction)
open import Relation.Nullary.Reflects using (invert)
open import Relation.Unary as Unary using (Decidable; Pred)
open Setoid using (Carrier)
private
variable
c c₁ c₂ c₃ p ℓ ℓ₁ ℓ₂ ℓ₃ : Level
module _ (S : Setoid c ℓ) where
open Setoid S
open Equality S
open Membership S
∈-resp-≈ : ∀ {xs} → (_∈ xs) Respects _≈_
∈-resp-≈ x≈y x∈xs = Any.map (trans (sym x≈y)) x∈xs
∉-resp-≈ : ∀ {xs} → (_∉ xs) Respects _≈_
∉-resp-≈ v≈w v∉xs w∈xs = v∉xs (∈-resp-≈ (sym v≈w) w∈xs)
∈-resp-≋ : ∀ {x} → (x ∈_) Respects _≋_
∈-resp-≋ = Any.lift-resp (flip trans)
∉-resp-≋ : ∀ {x} → (x ∉_) Respects _≋_
∉-resp-≋ xs≋ys v∉xs v∈ys = v∉xs (∈-resp-≋ (≋-sym xs≋ys) v∈ys)
index-injective : ∀ {x₁ x₂ xs} (x₁∈xs : x₁ ∈ xs) (x₂∈xs : x₂ ∈ xs) →
Any.index x₁∈xs ≡ Any.index x₂∈xs → x₁ ≈ x₂
index-injective (here x₁≈x) (here x₂≈x) _ = trans x₁≈x (sym x₂≈x)
index-injective (there x₁∈xs) (there x₂∈xs) eq = index-injective x₁∈xs x₂∈xs (suc-injective eq)
module _ (S : Setoid c ℓ) where
open Setoid S
open Unique S
open Membership S
private
∉×∈⇒≉ : ∀ {x y xs} → All (y ≉_) xs → x ∈ xs → x ≉ y
∉×∈⇒≉ = All.lookupWith λ y≉z x≈z x≈y → y≉z (trans (sym x≈y) x≈z)
unique⇒irrelevant : Binary.Irrelevant _≈_ → ∀ {xs} → Unique xs → Unary.Irrelevant (_∈ xs)
unique⇒irrelevant ≈-irr _ (here p) (here q) =
≡.cong here (≈-irr p q)
unique⇒irrelevant ≈-irr (_ ∷ u) (there p) (there q) =
≡.cong there (unique⇒irrelevant ≈-irr u p q)
unique⇒irrelevant ≈-irr (≉s ∷ _) (here p) (there q) =
contradiction p (∉×∈⇒≉ ≉s q)
unique⇒irrelevant ≈-irr (≉s ∷ _) (there p) (here q) =
contradiction q (∉×∈⇒≉ ≉s p)
module _ (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂) where
open Setoid S₁ renaming (Carrier to A₁; _≈_ to _≈₁_; refl to refl₁)
open Setoid S₂ renaming (Carrier to A₂; _≈_ to _≈₂_; refl to refl₂)
open Equality S₁ using ([]; _∷_) renaming (_≋_ to _≋₁_)
open Equality S₂ using () renaming (_≋_ to _≋₂_)
open Membership S₁
mapWith∈-cong : ∀ {xs ys} → xs ≋₁ ys →
(f : ∀ {x} → x ∈ xs → A₂) →
(g : ∀ {y} → y ∈ ys → A₂) →
(∀ {x y} → x ≈₁ y → (x∈xs : x ∈ xs) (y∈ys : y ∈ ys) →
f x∈xs ≈₂ g y∈ys) →
mapWith∈ xs f ≋₂ mapWith∈ ys g
mapWith∈-cong [] f g cong = []
mapWith∈-cong (x≈y ∷ xs≋ys) f g cong =
cong x≈y (here refl₁) (here refl₁) ∷
mapWith∈-cong xs≋ys (f ∘ there) (g ∘ there)
(λ x≈y x∈xs y∈ys → cong x≈y (there x∈xs) (there y∈ys))
mapWith∈≗map : ∀ f xs → mapWith∈ xs (λ {x} _ → f x) ≋₂ map f xs
mapWith∈≗map f [] = []
mapWith∈≗map f (x ∷ xs) = refl₂ ∷ mapWith∈≗map f xs
module _ (S : Setoid c ℓ) where
open Setoid S
open Membership S
length-mapWith∈ : ∀ {a} {A : Set a} xs {f : ∀ {x} → x ∈ xs → A} →
length (mapWith∈ xs f) ≡ length xs
length-mapWith∈ [] = ≡.refl
length-mapWith∈ (x ∷ xs) = ≡.cong suc (length-mapWith∈ xs)
mapWith∈-id : ∀ xs → mapWith∈ xs (λ {x} _ → x) ≡ xs
mapWith∈-id [] = ≡.refl
mapWith∈-id (x ∷ xs) = ≡.cong (x ∷_) (mapWith∈-id xs)
map-mapWith∈ : ∀ {a b} {A : Set a} {B : Set b} →
∀ xs (f : ∀ {x} → x ∈ xs → A) (g : A → B) →
map g (mapWith∈ xs f) ≡ mapWith∈ xs (g ∘′ f)
map-mapWith∈ [] f g = ≡.refl
map-mapWith∈ (x ∷ xs) f g = ≡.cong (_ ∷_) (map-mapWith∈ xs (f ∘ there) g)
module _ (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂) where
open Setoid S₁ renaming (_≈_ to _≈₁_)
open Setoid S₂ renaming (_≈_ to _≈₂_)
private module M₁ = Membership S₁; open M₁ using (find) renaming (_∈_ to _∈₁_)
private module M₂ = Membership S₂; open M₂ using () renaming (_∈_ to _∈₂_)
∈-map⁺ : ∀ {f} → f Preserves _≈₁_ ⟶ _≈₂_ →
∀ {v xs} → v ∈₁ xs → f v ∈₂ map f xs
∈-map⁺ pres x∈xs = Any.map⁺ (Any.map pres x∈xs)
∈-map⁻ : ∀ {v xs f} → v ∈₂ map f xs →
∃ λ x → x ∈₁ xs × v ≈₂ f x
∈-map⁻ x∈map = find (Any.map⁻ x∈map)
map-∷= : ∀ {f} (pres : f Preserves _≈₁_ ⟶ _≈₂_) →
∀ {xs x v} → (x∈xs : x ∈₁ xs) →
map f (x∈xs M₁.∷= v) ≡ ∈-map⁺ pres x∈xs M₂.∷= f v
map-∷= pres (here x≈y) = ≡.refl
map-∷= pres (there x∈xs) = ≡.cong (_ ∷_) (map-∷= pres x∈xs)
module _ (S : Setoid c ℓ) where
open Membership S using (_∈_)
open Setoid S
open Equality S using (_≋_; _∷_; ≋-refl)
∈-++⁺ˡ : ∀ {v xs ys} → v ∈ xs → v ∈ xs ++ ys
∈-++⁺ˡ = Any.++⁺ˡ
∈-++⁺ʳ : ∀ {v} xs {ys} → v ∈ ys → v ∈ xs ++ ys
∈-++⁺ʳ = Any.++⁺ʳ
∈-++⁻ : ∀ {v} xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
∈-++⁻ = Any.++⁻
∈-++⁺∘++⁻ : ∀ {v} xs {ys} (p : v ∈ xs ++ ys) →
[ ∈-++⁺ˡ , ∈-++⁺ʳ xs ]′ (∈-++⁻ xs p) ≡ p
∈-++⁺∘++⁻ = Any.++⁺∘++⁻
∈-++⁻∘++⁺ : ∀ {v} xs {ys} (p : v ∈ xs ⊎ v ∈ ys) →
∈-++⁻ xs ([ ∈-++⁺ˡ , ∈-++⁺ʳ xs ]′ p) ≡ p
∈-++⁻∘++⁺ = Any.++⁻∘++⁺
∈-++↔ : ∀ {v xs ys} → (v ∈ xs ⊎ v ∈ ys) ↔ v ∈ xs ++ ys
∈-++↔ = Any.++↔
∈-++-comm : ∀ {v} xs ys → v ∈ xs ++ ys → v ∈ ys ++ xs
∈-++-comm = Any.++-comm
∈-++-comm∘++-comm : ∀ {v} xs {ys} (p : v ∈ xs ++ ys) →
∈-++-comm ys xs (∈-++-comm xs ys p) ≡ p
∈-++-comm∘++-comm = Any.++-comm∘++-comm
∈-++↔++ : ∀ {v} xs ys → v ∈ xs ++ ys ↔ v ∈ ys ++ xs
∈-++↔++ = Any.++↔++
∈-insert : ∀ xs {ys v w} → v ≈ w → v ∈ xs ++ [ w ] ++ ys
∈-insert xs = Any.++-insert xs
∈-∃++ : ∀ {v xs} → v ∈ xs → ∃₂ λ ys zs → ∃ λ w →
v ≈ w × xs ≋ ys ++ [ w ] ++ zs
∈-∃++ (here px) = [] , _ , _ , px , ≋-refl
∈-∃++ (there {d} v∈xs) =
let hs , _ , _ , v≈v′ , eq = ∈-∃++ v∈xs
in d ∷ hs , _ , _ , v≈v′ , refl ∷ eq
module _ (S : Setoid c ℓ) where
open Setoid S using (_≈_)
open Membership S using (_∈_)
open Equality S using (≋-setoid)
open Membership ≋-setoid using (find) renaming (_∈_ to _∈ₗ_)
∈-concat⁺ : ∀ {v xss} → Any (v ∈_) xss → v ∈ concat xss
∈-concat⁺ = Any.concat⁺
∈-concat⁻ : ∀ {v} xss → v ∈ concat xss → Any (v ∈_) xss
∈-concat⁻ = Any.concat⁻
∈-concat⁺′ : ∀ {v vs xss} → v ∈ vs → vs ∈ₗ xss → v ∈ concat xss
∈-concat⁺′ v∈vs = ∈-concat⁺ ∘ Any.map (flip (∈-resp-≋ S) v∈vs)
∈-concat⁻′ : ∀ {v} xss → v ∈ concat xss → ∃ λ xs → v ∈ xs × xs ∈ₗ xss
∈-concat⁻′ xss v∈c[xss] =
let xs , xs∈xss , v∈xs = find (∈-concat⁻ xss v∈c[xss]) in xs , v∈xs , xs∈xss
module _ (S : Setoid c ℓ) where
open Membership S using (_∈_)
reverse⁺ : ∀ {x xs} → x ∈ xs → x ∈ reverse xs
reverse⁺ = Any.reverse⁺
reverse⁻ : ∀ {x xs} → x ∈ reverse xs → x ∈ xs
reverse⁻ = Any.reverse⁻
module _ (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂) (S₃ : Setoid c₃ ℓ₃) where
open Setoid S₁ renaming (_≈_ to _≈₁_; refl to refl₁)
open Setoid S₂ renaming (_≈_ to _≈₂_)
open Setoid S₃ renaming (_≈_ to _≈₃_)
open Membership S₁ renaming (_∈_ to _∈₁_)
open Membership S₂ renaming (_∈_ to _∈₂_)
open Membership S₃ renaming (_∈_ to _∈₃_)
∈-cartesianProductWith⁺ : ∀ {f} → f Preserves₂ _≈₁_ ⟶ _≈₂_ ⟶ _≈₃_ →
∀ {xs ys a b} → a ∈₁ xs → b ∈₂ ys →
f a b ∈₃ cartesianProductWith f xs ys
∈-cartesianProductWith⁺ pres = Any.cartesianProductWith⁺ _ pres
∈-cartesianProductWith⁻ : ∀ f xs ys {v} → v ∈₃ cartesianProductWith f xs ys →
∃₂ λ a b → a ∈₁ xs × b ∈₂ ys × v ≈₃ f a b
∈-cartesianProductWith⁻ f (x ∷ xs) ys v∈c with ∈-++⁻ S₃ (map (f x) ys) v∈c
... | inj₁ v∈map =
let b , b∈ys , v≈fxb = ∈-map⁻ S₂ S₃ v∈map
in x , b , here refl₁ , b∈ys , v≈fxb
... | inj₂ v∈com =
let a , b , a∈xs , b∈ys , v≈fab = ∈-cartesianProductWith⁻ f xs ys v∈com
in a , b , there a∈xs , b∈ys , v≈fab
module _ (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂) where
open Setoid S₁ renaming (Carrier to A)
open Setoid S₂ renaming (Carrier to B)
open Membership S₁ renaming (_∈_ to _∈₁_)
open Membership S₂ renaming (_∈_ to _∈₂_)
open Membership (S₁ ×ₛ S₂) renaming (_∈_ to _∈₁₂_)
∈-cartesianProduct⁺ : ∀ {x y xs ys} → x ∈₁ xs → y ∈₂ ys →
(x , y) ∈₁₂ cartesianProduct xs ys
∈-cartesianProduct⁺ = Any.cartesianProduct⁺
∈-cartesianProduct⁻ : ∀ xs ys {xy@(x , y) : A × B} →
xy ∈₁₂ cartesianProduct xs ys →
x ∈₁ xs × y ∈₂ ys
∈-cartesianProduct⁻ xs ys = Any.cartesianProduct⁻ xs ys
module _ (S : Setoid c ℓ) where
open Setoid S using (_≈_; refl)
open Membership S using (_∈_)
∈-applyUpTo⁺ : ∀ f {i n} → i < n → f i ∈ applyUpTo f n
∈-applyUpTo⁺ f = Any.applyUpTo⁺ f refl
∈-applyUpTo⁻ : ∀ {v} f {n} → v ∈ applyUpTo f n →
∃ λ i → i < n × v ≈ f i
∈-applyUpTo⁻ = Any.applyUpTo⁻
∈-applyDownFrom⁺ : ∀ f {i n} → i < n → f i ∈ applyDownFrom f n
∈-applyDownFrom⁺ f = Any.applyDownFrom⁺ f refl
∈-applyDownFrom⁻ : ∀ {v} f {n} → v ∈ applyDownFrom f n →
∃ λ i → i < n × v ≈ f i
∈-applyDownFrom⁻ = Any.applyDownFrom⁻
module _ (S : Setoid c ℓ) where
open Setoid S using (_≈_; refl) renaming (Carrier to A)
open Membership S using (_∈_)
∈-tabulate⁺ : ∀ {n} {f : Fin n → A} i → f i ∈ tabulate f
∈-tabulate⁺ i = Any.tabulate⁺ i refl
∈-tabulate⁻ : ∀ {n} {f : Fin n → A} {v} →
v ∈ tabulate f → ∃ λ i → v ≈ f i
∈-tabulate⁻ = Any.tabulate⁻
module _ (S : Setoid c ℓ) {P : Pred (Carrier S) p}
(P? : Decidable P) (resp : P Respects (Setoid._≈_ S)) where
open Setoid S using (_≈_; sym)
open Membership S using (_∈_)
∈-filter⁺ : ∀ {v xs} → v ∈ xs → P v → v ∈ filter P? xs
∈-filter⁺ {xs = x ∷ _} (here v≈x) Pv with P? x
... | true because _ = here v≈x
... | false because [¬Px] = contradiction (resp v≈x Pv) (invert [¬Px])
∈-filter⁺ {xs = x ∷ _} (there v∈xs) Pv with does (P? x)
... | true = there (∈-filter⁺ v∈xs Pv)
... | false = ∈-filter⁺ v∈xs Pv
∈-filter⁻ : ∀ {v xs} → v ∈ filter P? xs → v ∈ xs × P v
∈-filter⁻ {xs = x ∷ xs} v∈f[x∷xs] with P? x
... | false because _ = Product.map there id (∈-filter⁻ v∈f[x∷xs])
... | true because [Px] with v∈f[x∷xs]
... | here v≈x = here v≈x , resp (sym v≈x) (invert [Px])
... | there v∈fxs = Product.map there id (∈-filter⁻ v∈fxs)
module _ (S : Setoid c ℓ) {R : Rel (Carrier S) ℓ₂} (R? : Binary.Decidable R) where
open Setoid S using (_≈_)
open Membership S using (_∈_)
∈-derun⁺ : _≈_ Respectsʳ R → ∀ {xs z} → z ∈ xs → z ∈ derun R? xs
∈-derun⁺ ≈-resp-R z∈xs = Any.derun⁺ R? ≈-resp-R z∈xs
∈-deduplicate⁺ : _≈_ Respectsʳ (flip R) → ∀ {xs z} →
z ∈ xs → z ∈ deduplicate R? xs
∈-deduplicate⁺ ≈-resp-R z∈xs = Any.deduplicate⁺ R? ≈-resp-R z∈xs
∈-derun⁻ : ∀ xs {z} → z ∈ derun R? xs → z ∈ xs
∈-derun⁻ xs z∈derun[R,xs] = Any.derun⁻ R? z∈derun[R,xs]
∈-deduplicate⁻ : ∀ xs {z} → z ∈ deduplicate R? xs → z ∈ xs
∈-deduplicate⁻ xs z∈dedup[R,xs] = Any.deduplicate⁻ R? z∈dedup[R,xs]
module _ (S : Setoid c ℓ) where
open Membership S using (_∈_)
∈-length : ∀ {x xs} → x ∈ xs → 0 < length xs
∈-length (here px) = z<s
∈-length (there x∈xs) = z<s
module _ (S : Setoid c ℓ) where
open Setoid S using (refl)
open Membership S using (_∈_)
∈-lookup : ∀ xs i → lookup xs i ∈ xs
∈-lookup (x ∷ xs) zero = here refl
∈-lookup (x ∷ xs) (suc i) = there (∈-lookup xs i)
module _ (S : Setoid c ℓ) {_•_ : Op₂ (Carrier S)} where
open Setoid S using (_≈_; refl; sym; trans)
open Membership S using (_∈_)
foldr-selective : Selective _≈_ _•_ → ∀ e xs →
(foldr _•_ e xs ≈ e) ⊎ (foldr _•_ e xs ∈ xs)
foldr-selective •-sel i [] = inj₁ refl
foldr-selective •-sel i (x ∷ xs) with •-sel x (foldr _•_ i xs)
... | inj₁ x•f≈x = inj₂ (here x•f≈x)
... | inj₂ x•f≈f with foldr-selective •-sel i xs
... | inj₁ f≈i = inj₁ (trans x•f≈f f≈i)
... | inj₂ f∈xs = inj₂ (∈-resp-≈ S (sym x•f≈f) (there f∈xs))
module _ (S : Setoid c ℓ) where
open Setoid S
open Membership S
∈-∷=⁺-updated : ∀ {xs x v} (x∈xs : x ∈ xs) → v ∈ (x∈xs ∷= v)
∈-∷=⁺-updated (here px) = here refl
∈-∷=⁺-updated (there pxs) = there (∈-∷=⁺-updated pxs)
∈-∷=⁺-untouched : ∀ {xs x y v} (x∈xs : x ∈ xs) → (¬ x ≈ y) → y ∈ xs → y ∈ (x∈xs ∷= v)
∈-∷=⁺-untouched (here x≈z) x≉y (here y≈z) = contradiction (trans x≈z (sym y≈z)) x≉y
∈-∷=⁺-untouched (here x≈z) x≉y (there y∈xs) = there y∈xs
∈-∷=⁺-untouched (there x∈xs) x≉y (here y≈z) = here y≈z
∈-∷=⁺-untouched (there x∈xs) x≉y (there y∈xs) = there (∈-∷=⁺-untouched x∈xs x≉y y∈xs)
∈-∷=⁻ : ∀ {xs x y v} (x∈xs : x ∈ xs) → (¬ y ≈ v) → y ∈ (x∈xs ∷= v) → y ∈ xs
∈-∷=⁻ (here x≈z) y≉v (here y≈v) = contradiction y≈v y≉v
∈-∷=⁻ (here x≈z) y≉v (there y∈) = there y∈
∈-∷=⁻ (there x∈xs) y≉v (here y≈z) = here y≈z
∈-∷=⁻ (there x∈xs) y≉v (there y∈) = there (∈-∷=⁻ x∈xs y≉v y∈)