Add "Complete" predicate for lists that contain every element of a type (#1482)

Author: MatthewDaggitt

CHANGELOG.md

@@ -33,6 +33,12 @@ New modules
   Function.Metric.Rational.Bundles
   ```
 
+* Lists that contain every element of a type:
+  ```
+  Data.List.Relation.Unary.Complete.Setoid
+  Data.List.Relation.Unary.Complete.Setoid.Properties
+  ```
+
 Other minor additions
 ---------------------
 
@@ -49,3 +55,9 @@ Other minor additions
   <-weakInduction : P zero      → (∀ i → P (inject₁ i) → P (suc i)) → ∀ i → P i
   >-weakInduction : P (fromℕ n) → (∀ i → P (suc i) → P (inject₁ i)) → ∀ i → P i
   ```
+
+* Added new proofs to `Relation.Binary.Properties.Setoid`:
+  ```agda
+  respʳ-flip : _≈_ Respectsʳ (flip _≈_)
+  respˡ-flip : _≈_ Respectsˡ (flip _≈_)
+  ```

src/Data/List/Relation/Unary/Complete/Setoid.agda

@@ -0,0 +1,23 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Lists which contain every element of a given type
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.List
+open import Level
+open import Relation.Binary
+
+module Data.List.Relation.Unary.Complete.Setoid
+  {a ℓ} (S : Setoid a ℓ) where
+
+open Setoid S renaming (Carrier to A)
+open import Data.List.Membership.Setoid S
+
+------------------------------------------------------------------------
+-- Definition
+
+Complete : List A → Set (a ⊔ ℓ)
+Complete xs = ∀ x → x ∈ xs

src/Data/List/Relation/Unary/Complete/Setoid/Properties.agda

@@ -0,0 +1,90 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of lists which contain every element of a given type
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Fin hiding (_≟_)
+open import Data.List.Base
+open import Data.List.Membership.Setoid.Properties as Membership
+open import Data.List.Relation.Unary.Any using (index)
+open import Data.List.Relation.Unary.Any.Properties using (lookup-index)
+open import Data.List.Relation.Unary.Complete.Setoid
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Sum.Relation.Binary.Pointwise
+  using (_⊎ₛ_; inj₁; inj₂)
+open import Data.Product using (_,_; proj₁; proj₂)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent
+  using (_×ₛ_)
+open import Function
+open import Level
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.Properties.Setoid using (respʳ-flip)
+
+module Data.List.Relation.Unary.Complete.Setoid.Properties where
+
+open Setoid
+
+private
+  variable
+    a b ℓ₁ ℓ₂ : Level
+
+------------------------------------------------------------------------
+-- map
+
+module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂)
+         {f} (surj : IsSurjection (_≈_ S) (_≈_ T) f)
+         where
+  open IsSurjection surj
+
+  map⁺ : ∀ {xs} → Complete S xs → Complete T (map f xs)
+  map⁺ _∈xs y with surjective y
+  ... | (x , fx≈y) = ∈-resp-≈ T fx≈y (∈-map⁺ S T cong (x ∈xs))
+
+------------------------------------------------------------------------
+-- _++_
+
+module _ (S : Setoid a ℓ₁) where
+
+  ++⁺ˡ : ∀ {xs} ys → Complete S xs → Complete S (xs ++ ys)
+  ++⁺ˡ _ _∈xs v = Membership.∈-++⁺ˡ S (v ∈xs)
+
+  ++⁺ʳ : ∀ xs {ys} → Complete S ys → Complete S (xs ++ ys)
+  ++⁺ʳ _ _∈ys v = Membership.∈-++⁺ʳ S _ (v ∈ys)
+
+module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where
+
+  ++⁺ : ∀ {xs ys} → Complete S xs → Complete T ys →
+        Complete (S ⊎ₛ T) (map inj₁ xs ++ map inj₂ ys)
+  ++⁺ _∈xs _ (inj₁ x) = ∈-++⁺ˡ (S ⊎ₛ T)   (∈-map⁺ S (S ⊎ₛ T) inj₁ (x ∈xs))
+  ++⁺ _ _∈ys (inj₂ y) = ∈-++⁺ʳ (S ⊎ₛ T) _ (∈-map⁺ T (S ⊎ₛ T) inj₂ (y ∈ys))
+
+------------------------------------------------------------------------
+-- cartesianProduct
+
+module _ (S : Setoid a ℓ₁) (T : Setoid b ℓ₂) where
+
+  cartesianProduct⁺ : ∀ {xs ys} → Complete S xs → Complete T ys →
+                      Complete (S ×ₛ T) (cartesianProduct xs ys)
+  cartesianProduct⁺ _∈xs _∈ys (x , y) = ∈-cartesianProduct⁺ S T (x ∈xs) (y ∈ys)
+
+------------------------------------------------------------------------
+-- deduplicate
+
+module _ (S? : DecSetoid a ℓ₁) where
+  open DecSetoid S? renaming (setoid to S)
+
+  deduplicate⁺ : ∀ {xs} → Complete S xs → Complete S (deduplicate _≟_ xs)
+  deduplicate⁺ = ∈-deduplicate⁺ S _≟_ (respʳ-flip S) ∘_
+
+------------------------------------------------------------------------
+-- lookup
+
+module _ (S : Setoid a ℓ₁) where
+
+  lookup-surjective : ∀ {xs} → Complete S xs →
+                      Surjective {A = Fin (length xs)} _≡_ (_≈_ S) (lookup xs)
+  lookup-surjective _∈xs y = index (y ∈xs) , sym S (lookup-index (y ∈xs))

src/Relation/Binary/Properties/Setoid.agda

@@ -6,16 +6,16 @@
 
 {-# OPTIONS --without-K --safe #-}
 
+open import Data.Product using (_,_)
+open import Function.Base using (_∘_; _$_; flip)
+open import Relation.Nullary using (¬_)
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Binary
 
 module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where
 
 open Setoid S
 
-open import Data.Product using (_,_)
-open import Function.Base using (_∘_; _$_)
-open import Relation.Nullary using (¬_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 ------------------------------------------------------------------------------
 -- Every setoid is a preorder with respect to propositional equality
@@ -46,3 +46,12 @@ preorder = record
 
 ≉-resp₂ : _≉_ Respects₂ _≈_
 ≉-resp₂ = ≉-respʳ , ≉-respˡ
+
+------------------------------------------------------------------------------
+-- Other properties
+
+respʳ-flip : _≈_ Respectsʳ (flip _≈_)
+respʳ-flip y≈z x≈z = trans x≈z (sym y≈z)
+
+respˡ-flip : _≈_ Respectsˡ (flip _≈_)
+respˡ-flip = trans