Lists: incorporate feedback from James

CHANGELOG.md

@@ -123,11 +123,6 @@ Additions to existing modules
   Env = Vec Carrier
  ```
 
-* In `Data.List.Base`:
-  ```agda
-  lookupMaybe : List A → ℕ → Maybe A
-  ```
-
 * In `Data.List.Membership.Setoid.Properties`:
   ```agda
   Any-∈-swap    :  Any (_∈ ys) xs → Any (_∈ xs) ys
@@ -181,14 +176,12 @@ Additions to existing modules
 
 * In `Data.List.Relation.Unary.Unique.Setoid.Properties`:
   ```agda
-  Unique-dropSnd    : Unique S (x ∷ y ∷ xs) → Unique S (x ∷ xs)
-  Unique∷⇒head∉tail : Unique S (x ∷ xs) → x ∉ xs
+  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
   ```
 
 * In `Data.List.Relation.Unary.Unique.Propositional.Properties`:
   ```agda
-  Unique-dropSnd    : Unique (x ∷ y ∷ xs) → Unique (x ∷ xs)
-  Unique∷⇒head∉tail : Unique (x ∷ xs) → x ∉ xs
+  Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
   ```
 
 * In `Data.List.Relation.Binary.Equality.Setoid`:
@@ -203,6 +196,20 @@ Additions to existing modules
   ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
   ```
 
+* In `Data.List.Relation.Binary.Subset.Setoid.Properties`:
+  ```agda
+  ⊈[]    : x ∷ xs ⊈ []
+  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ```
+
+* In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+  ```agda
+  ⊈[]    : x ∷ xs ⊈ []
+  ⊆∷⇒∈∨⊆ : xs ⊆ y ∷ ys → y ∈ xs ⊎ xs ⊆ ys
+  ⊆∷∧∉⇒⊆ : xs ⊆ y ∷ ys → y ∉ xs → xs ⊆ ys
+  ```
+
 * In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
   ```agda
   concatMap⁺ : xs ⊆ ys → concatMap f xs ⊆ concatMap f ys
@@ -230,20 +237,6 @@ 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/Base.agda

@@ -229,12 +229,6 @@ lookup : ∀ (xs : List A) → Fin (length xs) → A
 lookup (x ∷ xs) zero    = x
 lookup (x ∷ xs) (suc i) = lookup xs i
 
-lookupMaybe : List A → ℕ → Maybe A
-lookupMaybe = λ where
-  []       _       → nothing
-  (x ∷ _)  zero    → just x
-  (_ ∷ xs) (suc n) → lookupMaybe xs n
-
 -- Numerical
 
 upTo : ℕ → List ℕ

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

@@ -41,7 +41,7 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality.Core as ≡
-  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_; subst)
+  using (_≡_; _≢_; refl; sym; trans; cong; cong₂; resp; _≗_)
 open import Relation.Binary.PropositionalEquality.Properties as ≡ using (setoid)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
 open import Relation.Nullary.Decidable.Core
@@ -463,7 +463,7 @@ map∷-decomp               {xss = _  ∷ _} (here refl) = -, here refl , refl
 map∷-decomp {xs = []}     {xss = _  ∷ _} (there xs∈) = ⊥-elim ([]∉map∷ xs∈)
 map∷-decomp {xs = x ∷ xs} {xss = _  ∷ _} (there xs∈) =
   let eq , p = map∷-decomp∈ xs∈
-  in -, there p , subst (λ ◆ → ◆ ∷ _ ≡ _) eq refl
+  in -, there p , cong (_∷ _) (sym eq)
 
 ∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs
 ∈-map∷⁻ {xss = _ ∷ _} = λ where

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

@@ -393,7 +393,7 @@ module _ (S : Setoid c ℓ) {P : Pred (Carrier S) p}
 
 module _
   (S₁ : Setoid c₁ ℓ₁) (S₂ : Setoid c₂ ℓ₂)
-  {P : Pred (S₁ .Carrier) p} (P? : Decidable P) (resp : P Respects (S₁ .Setoid._≈_))
+  {P : Pred _ p} (P? : Decidable P) (resp : P Respects _)
   {f xs y} where
 
   open Setoid     S₁ renaming (_≈_ to _≈₁_)
@@ -513,4 +513,3 @@ module _ (S : Setoid c ℓ) where
 
   All-∉-swap :  ∀ {xs ys} → All (_∉ ys) xs → All (_∉ xs) ys
   All-∉-swap p = All.¬Any⇒All¬ _ ((All.All¬⇒¬Any p) ∘ Any-∈-swap)
-

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

@@ -26,7 +26,7 @@ open import Relation.Nullary.Negation using (¬_)
 
 module _ {c ℓ} (S : Setoid c ℓ) where
 
-  open Setoid S using (_≈_; reflexive) renaming (Carrier to A)
+  open Setoid S using (_≉_; reflexive) renaming (Carrier to A)
 
   ------------------------------------------------------------------------
   -- Relational properties
@@ -40,7 +40,7 @@ module _ {c ℓ} (S : Setoid c ℓ) where
   ------------------------------------------------------------------------
 
   Disjoint⇒AllAll : ∀ {xs ys} → Disjoint S xs ys →
-                    All (λ x → All (λ y → ¬ x ≈ y) ys) xs
+                    All (λ x → All (x ≉_) ys) xs
   Disjoint⇒AllAll xs#ys = All.map (¬Any⇒All¬ _)
     (All.tabulate (λ v∈xs v∈ys → xs#ys (Any.map reflexive v∈xs , v∈ys)))
 

src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda

@@ -33,7 +33,7 @@ open import Relation.Binary.Definitions using (DecidableEquality)
 ------------------------------------------------------------------------
 -- deduplicate
 
-module _ {a}{A : Set a} (_≟_ : DecidableEquality A) where
+module _ {a} {A : Set a} (_≟_ : DecidableEquality A) where
 
   private
     dedup≡   = deduplicate _≟_

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

@@ -28,7 +28,7 @@ open import Data.List.Relation.Binary.Permutation.Propositional
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation
 open import Data.Nat.Base using (ℕ; _≤_)
 import Data.Product.Base as Product
-import Data.Sum.Base as Sum
+open import Data.Sum.Base as Sum using (_⊎_)
 open import Effect.Monad
 open import Function.Base using (_∘_; _∘′_; id; _$_)
 open import Function.Bundles using (_↔_; Inverse; Equivalence)
@@ -62,6 +62,9 @@ private
 ⊈[] : x ∷ xs ⊈ []
 ⊈[] = Subset.⊈[] (setoid _)
 
+⊆[]⇒≡[] : ∀ {A : Set a} → (_⊆ []) ⋐ (_≡ [])
+⊆[]⇒≡[] {A = A} = Subset.⊆[]⇒≡[] (setoid A)
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -158,12 +161,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 _)
+
 ⊆∷∧∉⇒⊆ : 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,7 +9,6 @@
 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)
@@ -23,6 +22,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 Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘₂_; _$_; case_of_)
 open import Level using (Level)
 open import Relation.Nullary using (¬_; does; yes; no)
@@ -35,6 +35,7 @@ open import Relation.Binary.Bundles using (Setoid; Preorder)
 open import Relation.Binary.Structures using (IsPreorder)
 import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
 open import Relation.Binary.Reasoning.Syntax
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 open Setoid using (Carrier)
 
@@ -54,6 +55,10 @@ module _ (S : Setoid a ℓ) where
   ⊈[] : ∀ {x xs} → x ∷ xs ⊈ []
   ⊈[] p = Membershipₚ.∉[] S $ p (here refl)
 
+  ⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ [])
+  ⊆[]⇒≡[] {x = []}    _ = ≡.refl
+  ⊆[]⇒≡[] {x = _ ∷ _} p with () ← ⊈[] p
+
 ------------------------------------------------------------------------
 -- Relational properties with _≋_ (pointwise equality)
 ------------------------------------------------------------------------
@@ -201,15 +206,18 @@ module _ (S : Setoid a ℓ) where
   ∈-∷⁺ʳ 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∷ys = inj₂ λ ()
+  ⊆∷⇒∈∨⊆ {xs = _ ∷ _} x∷xs⊆y∷ys with ⊆∷⇒∈∨⊆ $ x∷xs⊆y∷ys ∘ there
+  ... | inj₁ y∈xs  = inj₁ $ there y∈xs
+  ... | inj₂ xs⊆ys with x∷xs⊆y∷ys (here refl)
+  ...   | here x≈y = inj₁ $ here (sym x≈y)
+  ...   | there x∈ys = inj₂ (∈-∷⁺ʳ x∈ys xs⊆ys)
+
   ⊆∷∧∉⇒⊆ : 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∈
+  ⊆∷∧∉⇒⊆ xs⊆y∷ys y∉xs with ⊆∷⇒∈∨⊆ xs⊆y∷ys
+  ... | inj₁ y∈xs  = contradiction y∈xs y∉xs
+  ... | inj₂ xs⊆ys = xs⊆ys
 
 ------------------------------------------------------------------------
 -- ++

src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda

@@ -164,8 +164,5 @@ module _ {A : Set a} {P : Pred _ p} (P? : Decidable P) where
 ------------------------------------------------------------------------
 -- ∷
 
-Unique-dropSnd : Unique (x ∷ y ∷ xs) → Unique (x ∷ xs)
-Unique-dropSnd = Setoid.Unique-dropSnd (setoid _)
-
-Unique∷⇒head∉tail : Unique (x ∷ xs) → x ∉ xs
-Unique∷⇒head∉tail = Setoid.Unique∷⇒head∉tail (setoid _)
+Unique[x∷xs]⇒x∉xs : Unique (x ∷ xs) → x ∉ xs
+Unique[x∷xs]⇒x∉xs = Setoid.Unique[x∷xs]⇒x∉xs (setoid _)

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

@@ -16,7 +16,7 @@ open import Data.List.Relation.Binary.Disjoint.Setoid.Properties
 open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.All.Properties using (All¬⇒¬Any)
-open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; _∷_)
+open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
 open import Data.List.Relation.Unary.Unique.Setoid
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
@@ -165,14 +165,14 @@ module _ (S : Setoid a ℓ) {P : Pred _ p} (P? : Decidable P) where
 module _ (S : Setoid a ℓ) where
 
   open Setoid S renaming (Carrier to A)
-  open Membership S using (_∈_; _∉_)
+  open Membership S using (_∉_)
 
-  private variable x y : A; xs : List A
+  private
+    variable
+      x y : A
+      xs : List A
 
-  Unique-dropSnd : Unique S (x ∷ y ∷ xs) → Unique S (x ∷ xs)
-  Unique-dropSnd ((_ ∷ x∉) ∷ uniq) = x∉ AllPairs.∷ drop⁺ S 1 uniq
-
-  Unique∷⇒head∉tail : Unique S (x ∷ xs) → x ∉ xs
-  Unique∷⇒head∉tail uniq@((x∉ ∷ _) ∷ _) = λ where
-    (here x≈)  → x∉ x≈
-    (there x∈) → Unique∷⇒head∉tail (Unique-dropSnd uniq) x∈
+  Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs
+  Unique[x∷xs]⇒x∉xs ((x≉ ∷ x∉) ∷ _ ∷ uniq) = λ where
+    (here x≈)  → x≉ x≈
+    (there x∈) → Unique[x∷xs]⇒x∉xs (x∉ AllPairs.∷ uniq) x∈