Lists: porting several lemmas from other libraries #2479
Conversation
src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
CHANGELOG.md
Outdated
| * 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 |
There was a problem hiding this comment.
This PR introduces a lot of new names, some of which, like this one, are pretty hard to read to begin with... so maybe an alternative is preferable?
| Unique∷⇒head∉tail : Unique S (x ∷ xs) → x ∉ xs | |
| Unique[x∷xs]⇒x∉xs : Unique S (x ∷ xs) → x ∉ xs |
Etc. (my weakness for named variables vs. point-free/combinator-style naming?)
Shoutout to @MatthewDaggitt who is usually pretty good on coming up with good/better names for things...
There was a problem hiding this comment.
I've renamed to your suggestion for now, although I have to point out that I find this naming approach redundant: why would you want to repeat the type as-is? This is mere duplication, while names should provide "shortcuts" that are more intuitive/abstract/natural than the type that accompanies them (e.g. ⁺/⁻ for intro/elim).
There was a problem hiding this comment.
I take your point, just as I'm grateful you took my suggestion. I confess I don't think my position is necessarily 'correct' or (cognitively) 'optimal', but sometimes I think there is a place for redundancy...
... hence the call-out to a second reviewer.
omelkonian
force-pushed
the
orestis/list-additions
branch
from
b34bad7 to
0512041
Compare
omelkonian
force-pushed
the
orestis/list-additions
branch
from
0512041 to
d462216
Compare
omelkonian
force-pushed
the
orestis/list-additions
branch
from
d462216 to
75b4941
Compare
omelkonian
force-pushed
the
orestis/list-additions
branch
from
75b4941 to
53825a7
Compare
src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
omelkonian
force-pushed
the
orestis/list-additions
branch
from
53825a7 to
a50564e
Compare
omelkonian
force-pushed
the
orestis/list-additions
branch
from
a50564e to
49496df
Compare
CHANGELOG.md
Outdated
| ∈-map∘filter⁻ : y ∈₂ map f (filter P? xs) → ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x | ||
| ∈-map∘filter⁺ : f Preserves _≈₁_ ⟶ _≈₂_ → | ||
| ∃[ x ] x ∈₁ xs × y ≈₂ f x × P x → | ||
| y ∈₂ map f (filter P? xs) |
There was a problem hiding this comment.
These feel super ad-hoc. Why map and filter in particular?
Why not e.g. mapMaybe? Or unalignWith?
There was a problem hiding this comment.
Yep, I agree, and I was actually reluctant to include this in this PR for the same reason.
The only argument I find here is that these are operations that are so incredibly common, that if one user goes through the trouble of defining the composition to re-use it across their codebase/application, then probably it is worth including in the stdlib for other users. (It is, however, difficult to provide evidence for what is common and what is not.)
Of course, it is infeasible to be complete in any way, i.e. cover all possible combinations of list operations, but maybe a "the-more-the-merrier" strategy is better in this case, and we should encourage users to submit such combinations as they arise?
| @@ -123,10 +126,13 @@ module _ {v : A} where | |||
| ∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys) | |||
| ∈-++⁻ = Membership.∈-++⁻ (≡.setoid A) | |||
|
|
|||
| ∈-++ : v ∈ xs ++ ys ⇔ (v ∈ xs ⊎ v ∈ ys) | |||
There was a problem hiding this comment.
This should probably mention ⇔ in the name (cf. concat-∈↔ below)
There was a problem hiding this comment.
Wouldn't it be better to have a consistent naming convention for bundling introductions & eliminations?
Since intros are named <property_name>⁺ (modulo left/right qualifiers) and eliminators <property_name>⁻, my suggestion was to just drop the polarities (i.e. <property_name>) to communicate that this includes both intro & elim.
Another naming convention that I find intuitive is to explicitly include both polarities: <property_name>⁺⁻, e.g. ∈-++⁺⁻.
The things I don't like about the current naming of such bundles are the following:
- The exact arrow being used will change in each case (whether it's an equivalence
⇔, an inverse↔, a bi-inverse, etc...); isn't it preferable to have a universal convention that hides such differences (much like we do for intros/elims which might take different forms in each individual case but are always named with⁺and⁻. - names like
concat-∈↔are not immediately linked to the intros/elims that it contains (i.e. the<property_name>part is not retained)
So, if I follow the current practices, I would have to name this ++-∈⇔ :(
I can definitely do that, but I find it ugly and unintuitive.
src/Data/List/Relation/Binary/Permutation/Propositional/Properties/WithK.agda
Show resolved
Hide resolved
|
Thanks @JacquesCarette ! merging now... |
github-merge-queue
bot
removed this pull request from the merge queue due to failed status checks
|
So, the CI errors on the attempted merge are beyond my knowledge/understanding... can anyone (eg @gallais ) diagnose/fix? |
* Lists: irrelevance of membership (in unique lists) * Lists: the empty list is always a sublist of another * Lists: lookupMaybe (unsafe version of lookup) * List: `concatMap⁺` for the subset relation * Lists: memberhsip lemma for AllPairs * Lists: membership lemmas for map∘filter * Lists: lemmas about concatMap * Lists: lemmas about deduplicate * Lists: membership lemmas about nested lists * Lists: extra subset lemmas about _∷_ * Lists: extra lemmas about _∷_/Unique * Lists: incorporate feedback from James * Lists: incorporate feedback from Guillaume
github-merge-queue
bot
removed this pull request from the merge queue due to failed status checks
|
3rd time lucky? |
Porting useful list properties that we needed in the Cardano ledger project, several of which are themselves ported from my personal prelude.
I am totally fine with some of those not being merged due to the 'Fairbairn threshold' or just because it is too niche of a utility to be included in the standard library; I'll let the reviewer(s) decide.
NB: each commit is somewhat independent, so reviews can proceed in a per-commit fashion (unless a change is requested globally, e.g. cosmetic changes w.r.t. to the style guide).