-
Notifications
You must be signed in to change notification settings - Fork 235
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
More list properties about catMaybes/mapMaybe
#2389
Conversation
7c21ab4
to
bd4bd63
Compare
src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
bd4bd63
to
622c19b
Compare
@JacquesCarette To sum up, let's agree that there are both pros and cons to using old-school eliminators in contrast to immediately using (dependent) pattern matching:
Given that there is only one lemma about Feel free to push another commit on top of my branch to convert to eliminator-style proofs though... |
@omelkonian I'll comment on various of the details a bit later, but long story short: you make a very convincing case. I was overly optimistic. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great additions, but need to fix up layout and some of the with
-based proofs in favour of the (simpler!) originals, I think.
src/Data/List/Properties.agda
Outdated
Any-catMaybes⁺ : ∀ {P : Pred A ℓ} {xs : List (Maybe A)} | ||
→ Any (MAny P) xs → Any P (catMaybes xs) | ||
Any-catMaybes⁺ {xs = nothing ∷ xs} (there x∈) = Any-catMaybes⁺ x∈ | ||
Any-catMaybes⁺ {xs = just x ∷ xs} (here (just px)) = here px | ||
Any-catMaybes⁺ {xs = just x ∷ xs} (there x∈) = there $ Any-catMaybes⁺ x∈ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why here rather than added after L150 in the original?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And for the sake of juxtaposition, I'd swap L758 and L759, as well as suppressing x
and xs
:
Any-catMaybes⁺ : ∀ {P : Pred A ℓ} {xs : List (Maybe A)} | |
→ Any (MAny P) xs → Any P (catMaybes xs) | |
Any-catMaybes⁺ {xs = nothing ∷ xs} (there x∈) = Any-catMaybes⁺ x∈ | |
Any-catMaybes⁺ {xs = just x ∷ xs} (here (just px)) = here px | |
Any-catMaybes⁺ {xs = just x ∷ xs} (there x∈) = there $ Any-catMaybes⁺ x∈ | |
Any-catMaybes⁺ : ∀ {P : Pred A ℓ} {xs : List (Maybe A)} | |
→ Any (MAny P) xs → Any P (catMaybes xs) | |
Any-catMaybes⁺ {xs = nothing ∷ _} (there x∈) = Any-catMaybes⁺ x∈ | |
Any-catMaybes⁺ {xs = just _ ∷ _} (there x∈) = there $ Any-catMaybes⁺ x∈ | |
Any-catMaybes⁺ {xs = just _ ∷ _} (here (just px)) = here px |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why here rather than added after L150 in the original?
Grouped the properties of catMaybe
with the ones for mapMaybe
, as it seemed more intuitive.
Also, lemma catMaybes-concatMap
mentions concatMap
which comes just before in the file.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Well, perhaps there is no 'right' order for module contents, so the rule-of-thumb ends up being: try, where possible, to follow in Properties
the order in Base
... but even that seems hard to stick to.
src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
As I agree with @jamesmckinna 's comments, I won't approve this PR (yet), even though I'm not happy with the parts that I had commented on myself. |
8d831bf
to
8737650
Compare
src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda
Outdated
Show resolved
Hide resolved
8737650
to
6b8cbb2
Compare
src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
Outdated
Show resolved
Hide resolved
Thanks for the continued updates, but I won't re-review until you signal it's time to do so though! |
6b8cbb2
to
218d244
Compare
218d244
to
d2be656
Compare
@jamesmckinna ready for review |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good stuff.
d2be656
to
381299a
Compare
- Follow-up to PR #2361 - Ported from my [formal-prelude](https://github.com/omelkonian/formal-prelude/tree/c10fe94876a7378088f2e4cf68d9b18858dcc256)
381299a
to
e5fdf1c
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the update!
@JacquesCarette @jamesmckinna Ready to merge? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes from me.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think the new with
-based code (and the accompanying code motion) is an improvement over the existing pattern-matching based definitions, but you have two approvals from others, so I'm not going to stand in the way.
Requested changes haven't been made, and don't seem likely to be anytime soon.
Isn't the reuse of the inductive hypothesis ( [sorry, hit |
In this case, I (personally) actually think no, it's not, at least not enough to justify the rewriting of existing code. Funnily enough, I think that both you and @JacquesCarette have convinced me, in different ways, and from different starting points, to view such code style with... scepticism for the time being. And one reason I dismissed my review was to avoid going back over this ground...so: I stand aside, as previously. |
Mmh, I tend to agree with James @jamesmckinna that |
While I very much agree with @andreasabel 's general stance, especially for any definition that computes, I've gotten more relaxed about "pure proofs". Really what's we're sorely missing (and this is, I believe, what @omelkonian was using it for) is a proper pattern-matching |
See my comment above on "meta-properties", which nullifies the distinction between programs and "pure proofs".
Isn't the upcoming |
Yes, meta-properties, being proofs-about-proofs, do blur things. I've hated doing such proofs so much (in MLTT) that I block them out; when done 'properly', a la category theory where one adds higher-level cells, then these become sane again. I don't understand (yet!) enough of the details of |
Shall we close the discussion and merge? |
@omelkonian: Thanks, Orestis, for your patience and willingness to revert changes! |
Seconded! |
* More list properties about `catMaybes/mapMaybe` - Follow-up to PR #2361 - Ported from my [formal-prelude](https://github.com/omelkonian/formal-prelude/tree/c10fe94876a7378088f2e4cf68d9b18858dcc256) * Revert irrefutable `with`s for inductive hypotheses.
Data.List.Base.mapMaybe
(#2359; deprecate use ofwith
#2123) #2361