Lists: decidability of Subset+Disjoint relations

Author: omelkonian

src/Data/List/Membership/DecSetoid.agda

@@ -9,10 +9,11 @@
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Nullary.Decidable using (¬?)
+open import Relation.Nullary using (Stable; decidable-stable)
+open import Data.List.Relation.Unary.Any using (any?)
 
 module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
 
-open import Data.List.Relation.Unary.Any using (any?)
 open DecSetoid DS
 
 ------------------------------------------------------------------------
@@ -30,3 +31,6 @@ x ∈? xs = any? (x ≟_) xs
 
 _∉?_ : Decidable _∉_
 x ∉? xs = ¬? (x ∈? xs)
+
+∈-stable : ∀ {xs ys} → Stable (xs ∈ ys)
+∈-stable = decidable-stable (_ ∈? _)

src/Data/List/Relation/Binary/Disjoint/DecPropositional.agda

@@ -0,0 +1,21 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidability of the disjoint relation over propositional equality.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Definitions using (DecidableEquality)
+
+module Data.List.Relation.Binary.Disjoint.DecPropositional
+  {a} {A : Set a} (_≟_ : DecidableEquality A)
+  where
+
+------------------------------------------------------------------------
+-- Re-export core definitions and operations
+
+open import Data.List.Relation.Binary.Disjoint.Propositional {A = A} public
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
+open import Data.List.Relation.Binary.Disjoint.DecSetoid (decSetoid _≟_) public
+  using (disjoint?)

src/Data/List/Relation/Binary/Disjoint/DecSetoid.agda

@@ -0,0 +1,30 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidability of the disjoint relation over setoid equality.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Function.Base using (_$_)
+open import Data.Product.Base using (_,_)
+open import Data.List.Relation.Unary.Any using (map)
+open import Data.List.Relation.Unary.All using (all?; lookupₛ)
+open import Data.List.Relation.Unary.All.Properties using (¬All⇒Any¬)
+open import Relation.Binary.Bundles using (DecSetoid)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Nullary using (yes; no)
+
+module Data.List.Relation.Binary.Disjoint.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
+
+open DecSetoid S
+open import Data.List.Relation.Binary.Equality.DecSetoid S
+open import Data.List.Relation.Binary.Disjoint.Setoid setoid public
+open import Data.List.Membership.DecSetoid S
+
+disjoint? : Decidable Disjoint
+disjoint? xs ys with all? (_∉? ys) xs
+... | yes xs♯ys = yes λ (v∈ , v∈′) →
+  lookupₛ setoid (λ x≈y ∉ys ∈ys → ∉ys (map (trans x≈y) ∈ys)) xs♯ys v∈ v∈′
+... | no ¬xs♯ys = let (x , x∈ , ¬∉ys) = find (¬All⇒Any¬ (_∉? _) _ ¬xs♯ys) in
+  no λ p → p (x∈ , ∈-stable ¬∉ys)

src/Data/List/Relation/Binary/Subset/DecPropositional.agda

@@ -0,0 +1,21 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidability of the subset relation over propositional equality.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Definitions using (DecidableEquality)
+
+module Data.List.Relation.Binary.Subset.DecPropositional
+  {a} {A : Set a} (_≟_ : DecidableEquality A)
+  where
+
+------------------------------------------------------------------------
+-- Re-export core definitions and operations
+
+open import Data.List.Relation.Binary.Subset.Propositional {A = A} public
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
+open import Data.List.Relation.Binary.Subset.DecSetoid (decSetoid _≟_) public
+  using (_⊆?_)

src/Data/List/Relation/Binary/Subset/DecSetoid.agda

@@ -0,0 +1,33 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidability of the subset relation over setoid equality.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Function.Base using (_∘_)
+open import Data.List.Base using ([]; _∷_)
+open import Data.List.Relation.Unary.Any using (here; there; map)
+open import Relation.Binary.Bundles using (DecSetoid)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Nullary using (yes; no)
+
+module Data.List.Relation.Binary.Subset.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
+
+open DecSetoid S
+open import Data.List.Relation.Binary.Equality.DecSetoid S
+open import Data.List.Membership.DecSetoid S
+
+-- Re-export definitions
+open import Data.List.Relation.Binary.Subset.Setoid setoid public
+
+infix 4 _⊆?_
+_⊆?_ : Decidable _⊆_
+[]       ⊆? _   = yes λ ()
+(x ∷ xs) ⊆? ys  with x ∈? ys
+... | no  x∉ys  = no λ xs⊆ys → x∉ys (xs⊆ys (here refl))
+... | yes x∈ys  with xs ⊆? ys
+... | no  xs⊈ys = no λ xs⊆ys → xs⊈ys (xs⊆ys ∘ there)
+... | yes xs⊆ys = yes λ where (here refl) → map (trans refl) x∈ys
+                              (there x∈)  → xs⊆ys x∈