Final overhaul of list membership and associated relations #271
Conversation
src/Data/List/All/Properties.agda
Outdated
| @@ -258,7 +260,7 @@ module _ {a p} {A : Set a} {P : A → Set p} where | |||
| ------------------------------------------------------------------------ | |||
| -- tabulate | |||
|
|
|||
| module _ {a p} {A : Set a} {P : A → Set p} where | |||
| module _ {a p} {A : Set a} {P : A → Set p} where | |||
| (x ∈ xs × y ∈ ys) ↔ (x , y) ∈ (xs ⊗ ys) | ||
| ⊗-∈↔ {xs} {ys} {x} {y} = | ||
| (x ∈ xs × y ∈ ys) ↔⟨ ⊗↔′ ⟩ | ||
| Any (x ≡_ ⟨×⟩ y ≡_) (xs ⊗ ys) ↔⟨ Any-cong helper (_ ∎) ⟩ |
|
|
||
| finite : ∀ {a} {A : Set a} (f : ℕ ↣ A) → | ||
| ∀ xs → ¬ (∀ i → Inj.Injection.to f ⟨$⟩ i ∈ xs) | ||
| finite inj [] ∈[] with ∈[] zero |
There was a problem hiding this comment.
Should we provide an inversion lemma ∈[]⁻ : x ∈ [] → ⊥ and use that here instead of a with + absurd pattern?
There was a problem hiding this comment.
This proof is not pretty and so far I've avoided touching it as it's really quite fragile. I'll see what I can do to tidy it up...
There was a problem hiding this comment.
A little tidier now.
| open Setoid S using (_≈_; sym) | ||
| open Membership S using (_∈_) | ||
|
|
||
| ∈-filter⁺ : (P? : Decidable P) → P Respects _≈_ → |
There was a problem hiding this comment.
These two parameters (P? : Decidable P) and P Respects _≈_ are common to both
∈-filter⁺ and ∈-filter⁻ and could be pushed in the anonymous module.
| ∈-filter⁻ P? resp {v} {x ∷ xs} v∈f[x∷xs] with P? x | ||
| ... | no _ = Prod.map there id (∈-filter⁻ P? resp v∈f[x∷xs]) | ||
| ... | yes Px with v∈f[x∷xs] | ||
| ... | here v≈x = here v≈x , resp (sym v≈x) Px |
| ∈-length {_} {_ ∷ xs} (here px) = s≤s z≤n | ||
| ∈-length {_} {_ ∷ xs} (there x∈xs) = | ||
| ≤-trans (∈-length x∈xs) (n≤1+n (length xs)) | ||
|
|
There was a problem hiding this comment.
Can't we have n≤1+n (length _) and drop the pattern matching on implicit arguments?
There was a problem hiding this comment.
Nope but we can have n≤1+n _!
src/Data/Product/Properties.agda
Outdated
| proj₂-injective refl = refl | ||
|
|
||
| proj-injective : ∀ (ab : Σ A B) → ab ≡ (proj₁ ab , proj₂ ab) | ||
| proj-injective (_ , _) = refl |
There was a problem hiding this comment.
Isn't this true by eta-equality (i.e. no need to pattern-match)?
There was a problem hiding this comment.
Yup, you're right. Removed.
It's obviously an afternoon for big PRs! This finally organises list membership in a sane, logical and easy-to-use way. As a happy consequence this solves issues #70, #155 and #220.
The major changes are:
Data/List.Any.BagAndSetEqualitytoData.List.Relation.BagAndSetEqualityData.List.Membershipinto it's own modulesData.List.Relation.Sublist.(Propositional/Setoid).Data.List.Membershipdirectory:Membership.Setoidparameterised by aSetoidMembership.DecSetoidparameterised by aDecSetoidMembership.Propositionalimplictly parameterised by a typeMembership.DecPropositionalparameterised by a proof of decidable equivalence for an implicit type.findandloseand are now in the correct membership property files instead of being confusingly misplaced inData.Any.Properties.This structure makes it easy to simply pick the type of membership you're interested in and get all the misfix notation working automatically upon module import at the top of the file.
I should also mention that I chose to prefix the introduction and elimination membership proofs with
∈as we may at some point want to have corresponding proofs with∉.