Lists: extra subset lemmas about _∷_

Author: omelkonian

CHANGELOG.md

@@ -138,6 +138,7 @@ Additions to existing modules
                   y ∈₂ map f (filter P? xs)
   ∈-concatMap⁺  : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs
   ∈-concatMap⁻  : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs
+  ∉[]           : x ∉ []
   ```
 
 * In `Data.List.Membership.Propositional.Properties`:
@@ -152,6 +153,7 @@ Additions to existing modules
   map∷-decomp∈  : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
   map∷-decomp   : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × y ∷ ys ≡ xs
   ∈-map∷⁻       : xs ∈ map (x ∷_) xss → x ∈ xs
+  ∉[]           : x ∉ []
   ```
 
 * In `Data.List.Membership.Propositional.Properties.WithK`:
@@ -216,6 +218,20 @@ Additions to existing modules
   ∈-dedup      : x ∈ xs ⇔ x ∈ deduplicate _≟_ xs
   ```
 
+* In `Data.List.Relation.Binary.Permutation.Setoid.Properties`:
+  ```agda
+  ⊈[]    : x ∷ xs ⊈ []
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
+  ```
+
+* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
+  ```agda
+  ⊈[]    : x ∷ xs ⊈ []
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
+  ```
+
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`:
   ```agda
   dedup-++-↭ : Disjoint xs ys →

src/Data/List/Membership/Propositional/Properties/Core.agda

@@ -12,7 +12,7 @@
 
 module Data.List.Membership.Propositional.Properties.Core where
 
-open import Data.List.Base using (List)
+open import Data.List.Base using (List; [])
 open import Data.List.Membership.Propositional
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.Product.Base as Product using (_,_; ∃; _×_)
@@ -30,6 +30,12 @@ private
     x : A
     xs : List A
 
+------------------------------------------------------------------------
+-- Basics
+
+∉[] : x ∉ []
+∉[] ()
+
 ------------------------------------------------------------------------
 -- find satisfies a simple equality when the predicate is a
 -- propositional equality.

src/Data/List/Membership/Setoid/Properties.agda

@@ -1,4 +1,4 @@
-------------------------------------------------------------------------
+-----------------------------------------------------------------------
 -- The Agda standard library
 --
 -- Properties related to setoid list membership
@@ -42,6 +42,16 @@ private
   variable
     c c₁ c₂ c₃ p ℓ ℓ₁ ℓ₂ ℓ₃ : Level
 
+------------------------------------------------------------------------
+-- Basics
+
+module _ (S : Setoid c ℓ) where
+
+  open Membership S
+
+  ∉[] : ∀ {x} → x ∉ []
+  ∉[] ()
+
 ------------------------------------------------------------------------
 -- Equality properties
 

src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda

@@ -11,18 +11,18 @@ module Data.List.Relation.Binary.Subset.Propositional.Properties
 
 open import Data.Bool.Base using (Bool; true; false; T)
 open import Data.List.Base
-  using (List; map; _∷_; _++_; concat; concatMap; applyUpTo; any; filter)
+  using (List; []; map; _∷_; _++_; concat; concatMap; applyUpTo; any; filter)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.List.Relation.Unary.All using (All)
 import Data.List.Relation.Unary.Any.Properties as Any hiding (filter⁺)
 open import Data.List.Effectful using (monad)
 open import Data.List.Relation.Unary.Any using (Any)
-open import Data.List.Membership.Propositional using (_∈_; mapWith∈)
+open import Data.List.Membership.Propositional using (_∈_; _∉_; mapWith∈)
 open import Data.List.Membership.Propositional.Properties
   using (map-∈↔; concat-∈↔; >>=-∈↔; ⊛-∈↔; ⊗-∈↔)
 import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset
 open import Data.List.Relation.Binary.Subset.Propositional
-  using (_⊆_; _⊇_)
+  using (_⊆_; _⊇_; _⊈_)
 open import Data.List.Relation.Binary.Permutation.Propositional
   using (_↭_; ↭-sym; ↭-isEquivalence)
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation
@@ -52,8 +52,16 @@ private
     a b p q : Level
     A : Set a
     B : Set b
+    x y : A
     ws xs ys zs : List A
 
+------------------------------------------------------------------------
+-- Basics
+------------------------------------------------------------------------
+
+⊈[] : x ∷ xs ⊈ []
+⊈[] = Subset.⊈[] (setoid _)
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -150,6 +158,12 @@ xs⊆x∷xs = Subset.xs⊆x∷xs (setoid _)
 ∈-∷⁺ʳ : ∀ {x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
 ∈-∷⁺ʳ = Subset.∈-∷⁺ʳ (setoid _)
 
+⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+⊆∷∧∉⇒⊆ = Subset.⊆∷∧∉⇒⊆ (setoid _)
+
+∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
+∈∷∧⊆⇒∈ = Subset.∈∷∧⊆⇒∈ (setoid _)
+
 ------------------------------------------------------------------------
 -- _++_
 

src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda

@@ -9,6 +9,7 @@
 module Data.List.Relation.Binary.Subset.Setoid.Properties where
 
 open import Data.Bool.Base using (Bool; true; false)
+open import Data.Empty using (⊥-elim)
 open import Data.List.Base hiding (_∷ʳ_; find)
 import Data.List.Properties as List
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
@@ -22,7 +23,7 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality
 import Data.List.Relation.Binary.Permutation.Setoid as Permutation
 import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutationₚ
 open import Data.Product.Base using (_,_)
-open import Function.Base using (_∘_; _∘₂_; _$_)
+open import Function.Base using (_∘_; _∘₂_; _$_; case_of_)
 open import Level using (Level)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
@@ -41,6 +42,18 @@ private
   variable
     a b p q r ℓ : Level
 
+------------------------------------------------------------------------
+-- Basics
+------------------------------------------------------------------------
+
+module _ (S : Setoid a ℓ) where
+
+  open Setoid S using (refl)
+  open Subset S
+
+  ⊈[] : ∀ {x xs} → x ∷ xs ⊈ []
+  ⊈[] p = Membershipₚ.∉[] S $ p (here refl)
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -161,27 +174,43 @@ module _ (S : Setoid a ℓ) where
 
 ------------------------------------------------------------------------
 -- Properties of list functions
+------------------------------------------------------------------------
+
 ------------------------------------------------------------------------
 -- ∷
 
 module _ (S : Setoid a ℓ) where
 
-  open Setoid S
+  open Setoid S renaming (Carrier to A)
   open Subset S
   open Membership S
   open Membershipₚ
 
   xs⊆x∷xs : ∀ xs x → xs ⊆ x ∷ xs
   xs⊆x∷xs xs x = there
 
-  ∷⁺ʳ : ∀ {xs ys} x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
+  private variable
+    x y : A
+    xs ys : List A
+
+  ∷⁺ʳ : ∀ x → xs ⊆ ys → x ∷ xs ⊆ x ∷ ys
   ∷⁺ʳ x xs⊆ys (here  p) = here p
   ∷⁺ʳ x xs⊆ys (there p) = there (xs⊆ys p)
 
-  ∈-∷⁺ʳ : ∀ {xs ys x} → x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
+  ∈-∷⁺ʳ : x ∈ ys → xs ⊆ ys → x ∷ xs ⊆ ys
   ∈-∷⁺ʳ x∈ys _  (here  v≈x)  = ∈-resp-≈ S (sym v≈x) x∈ys
   ∈-∷⁺ʳ _ xs⊆ys (there x∈xs) = xs⊆ys x∈xs
 
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ⊆∷∧∉⇒⊆ xs⊆ y∉ x∈ = case xs⊆ x∈ of λ where
+    (here x≈) → ⊥-elim $ y∉ (∈-resp-≈ S x≈ x∈)
+    (there p) → p
+
+  ∈∷∧⊆⇒∈ : x ∈ y ∷ xs → xs ⊆ ys → x ∈ y ∷ ys
+  ∈∷∧⊆⇒∈ = λ where
+    (here x≡y) _   → here x≡y
+    (there x∈) xs⊆ → there $ xs⊆ x∈
+
 ------------------------------------------------------------------------
 -- ++