[ refactor ] proofs under Data.List.Membership.*.Properties

CHANGELOG.md

@@ -312,7 +312,7 @@ Additions to existing modules
   map∷⁻          : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × xs ≡ y ∷ ys
   map∷-decomp∈   : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss
   ∈-map∷⁻        : xs ∈ map (x ∷_) xss → x ∈ xs
-  ∉[]            : x ∉ []
+  _∉[]           : ∀ x → x ∉ []
   deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs
   ```
 
@@ -333,7 +333,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 ∉ []
+  _∉[]           : ∀ x → x ∉ []
   deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs
   ```
 

src/Data/List/Membership/Propositional.agda

@@ -10,7 +10,7 @@
 module Data.List.Membership.Propositional {a} {A : Set a} where
 
 open import Data.List.Relation.Unary.Any using (Any)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; resp; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; resp)
 open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 import Data.List.Membership.Setoid as SetoidMembership
@@ -26,7 +26,7 @@ open SetoidMembership (setoid A) public hiding (lose)
 infix 4 _≢∈_
 
 _≢∈_ : ∀ {x y : A} {xs} → x ∈ xs → y ∈ xs → Set _
-_≢∈_ x∈xs y∈xs = ∀ x≡y → subst (_∈ _) x≡y x∈xs ≢ y∈xs
+_≢∈_ x∈xs y∈xs = ∀ x≡y → resp (_∈ _) x≡y x∈xs ≢ y∈xs
 
 ------------------------------------------------------------------------
 -- Other operations

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

@@ -20,7 +20,7 @@ open import Function.Base using (flip; id; _∘_)
 open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; cong; resp)
+  using (_≡_; refl; trans; cong; resp)
 open import Relation.Unary using (Pred; _⊆_)
 
 private
@@ -42,7 +42,8 @@ private
 
 find-∈ : (x∈xs : x ∈ xs) → find x∈xs ≡ (x , x∈xs , refl)
 find-∈ (here refl)  = refl
-find-∈ (there x∈xs) rewrite find-∈ x∈xs = refl
+find-∈ (there x∈xs)
+  = cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find-∈ x∈xs)
 
 ------------------------------------------------------------------------
 -- Lemmas relating map and find.
@@ -59,22 +60,24 @@ module _ {P : Pred A p} where
              let x , x∈xs , px = find p in
              find (Any.map f p) ≡ (x , x∈xs , f px)
   find∘map (here  p) f = refl
-  find∘map (there p) f rewrite find∘map p f = refl
+  find∘map (there p) f
+    = cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find∘map p f)
 
 ------------------------------------------------------------------------
 -- Any can be expressed using _∈_
 
 module _ {P : Pred A p} where
 
   ∃∈-Any : (∃ λ x → x ∈ xs × P x) → Any P xs
-  ∃∈-Any (x , x∈xs , px) = lose {P = P} x∈xs px
+  ∃∈-Any (x , x∈xs , px) = lose x∈xs px
 
   ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p
   ∃∈-Any∘find p = map∘find p refl
 
   find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p
   find∘∃∈-Any p@(x , x∈xs , px)
-    rewrite find∘map x∈xs (flip (resp P) px) | find-∈ x∈xs = refl
+    = trans (find∘map x∈xs (flip (resp P) px))
+            (cong (λ (x , x∈xs , eq) → x , x∈xs , resp P eq px) (find-∈ x∈xs))
 
   Any↔ : (∃ λ x → x ∈ xs × P x) ↔ Any P xs
   Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any

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

@@ -49,8 +49,8 @@ module _ (S : Setoid c ℓ) where
 
   open Membership S
 
-  ∉[] : ∀ {x} → x ∉ []
-  ∉[] ()
+  _∉[] : ∀ x → x ∉ []
+  _ ∉[] = λ()
 
 ------------------------------------------------------------------------
 -- Equality properties

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

@@ -53,7 +53,7 @@ module _ (S : Setoid a ℓ) where
   open Subset S
 
   ∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ []
-  ∷⊈[] p = Membershipₚ.∉[] S $ p (here refl)
+  ∷⊈[] p = Membershipₚ._∉[] S _ $ p (here refl)
 
   ⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ [])
   ⊆[]⇒≡[] {x = []}    _ = ≡.refl