Lists: decidability of Subset+Disjoint relations (#2399)

Author: omelkonian

CHANGELOG.md

@@ -211,6 +211,18 @@ New modules
   Data.Vec.Bounded.Show
   ```
 
+* Decidability for the subset relation on lists:
+  ```agda
+  Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_)
+  Data.List.Relation.Binary.Subset.DecPropositional
+  ```
+
+* Decidability for the disjoint relation on lists:
+  ```agda
+  Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?)
+  Data.List.Relation.Binary.Disjoint.DecPropositional
+  ```
+
 Additions to existing modules
 -----------------------------
 

src/Data/List/Membership/DecSetoid.agda

@@ -6,13 +6,14 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.Bundles using (DecSetoid)
-open import Relation.Nullary.Decidable using (¬?)
 
 module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
 
 open import Data.List.Relation.Unary.Any using (any?)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Nullary.Decidable using (¬?)
+
 open DecSetoid DS
 
 ------------------------------------------------------------------------

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,29 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decidability of the disjoint relation over setoid equality.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary.Bundles using (DecSetoid)
+
+module Data.List.Relation.Binary.Disjoint.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
+
+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.Definitions using (Decidable)
+open import Relation.Nullary using (yes; no; decidable-stable)
+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∈ , decidable-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 Relation.Binary.Bundles using (DecSetoid)
+
+module Data.List.Relation.Binary.Subset.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
+
+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.Definitions using (Decidable)
+open import Relation.Nullary using (yes; no)
+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∈