More list properties about catMaybes/mapMaybe

[omelkonian]

• Follow-up to PR Improve Data.List.Base.mapMaybe (#2359; deprecate use of with #2123) #2361
• Ported from my formal-prelude

[omelkonian]

@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:

• PRO: reusability! e.g. if we have some lemmas about maybe we could reuse them for deriving other proofs
• CONS:
  • type inference (e.g. explicitly giving the motives in the examples above)
  • someone wanting to prove something about these definitions can immediately see what they have to do case analysis on, while with maybe that have to perform one additional mental step

Given that there is only one lemma about maybe 😞 (maybe-map) and that the inductive hypotheses in the proofs above can easily be shared using with IH ← ..., I have not followed your suggestion to use eliminators and stuck with matching on the maybes and so forth.

Feel free to push another commit on top of my branch to convert to eliminator-style proofs though...

[JacquesCarette]

@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.

[jamesmckinna]

Great additions, but need to fix up layout and some of the with-based proofs in favour of the (simpler!) originals, I think.

[jamesmckinna]

Why here rather than added after L150 in the original?

[jamesmckinna]

And for the sake of juxtaposition, I'd swap L758 and L759, as well as suppressing x and xs:

Suggested change

	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

[omelkonian]

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.

[jamesmckinna]

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.

[JacquesCarette]

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.

[jamesmckinna]

Thanks for the continued updates, but I won't re-review until you signal it's time to do so though!

[omelkonian]

@jamesmckinna ready for review

[andreasabel]

Good stuff.

[andreasabel]

Thanks for the update!

[omelkonian]

@JacquesCarette @jamesmckinna Ready to merge?

[JacquesCarette]

Yes from me.

[jamesmckinna]

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.

[omelkonian]

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.

Isn't the reuse of the inductive hypothesis (ih) clearly an improvement?

[sorry, hit edit instead of quote reply]

[jamesmckinna]

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.

Isn't the reuse of the inductive hypothesis (ih) clearly an improvement?

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.

[andreasabel]

Mmh, I tend to agree with James @jamesmckinna that with should be avoided where possible. The reason is that it internally generates a helper function which Agda might sometimes leak in printing. Also, it bears some hazards in proving things about the parent function as the name of the auxiliary function is not available to the user.
So, I think the general thrust should be to get rid of with where possible rather than introducing more withs.

[JacquesCarette]

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 let that doesn't unfold eagerly. This is a real wart in the current Agda language (along with the same issue wrt module parameters).

[omelkonian]

While I very much agree with @andreasabel 's general stance, especially for any definition that computes, I've gotten more relaxed about "pure proofs".

See my comment above on "meta-properties", which nullifies the distinction between programs and "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 let that doesn't unfold eagerly. This is a real wart in the current Agda language (along with the same issue wrt module parameters).

Isn't the upcoming using syntax that I mentioned above already what you wish for (although I'm not sure about its unfolding behaviour, but the opaque feature should cover that).

[JacquesCarette]

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. subst hell is really the worst hell of them all.

I don't understand (yet!) enough of the details of using to know if it really going to be 'the' feature needed. I suspect that as long as there isn't some kind of let-like construct in the internal AST, it won't be, it'll merely be pleasant syntactic sugar.

[jamesmckinna]

Shall we close the discussion and merge?

[andreasabel]

@omelkonian: Thanks, Orestis, for your patience and willingness to revert changes!
(with is gone again)

[jamesmckinna]

@omelkonian: Thanks, Orestis, for your patience and willingness to revert changes! (with is gone again)

Seconded!