Lists: porting several lemmas from other libraries

[omelkonian]

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

[jamesmckinna]

Many thanks for a huge contribution!

Lots of nitpicky feedback, but I think quite a few changes (removing redundancy etc.) would make this a lot tighter.

[jamesmckinna]

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?

Suggested change

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

[omelkonian]

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

[jamesmckinna]

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.

[gallais]

These feel super ad-hoc. Why map and filter in particular?
Why not e.g. mapMaybe? Or unalignWith?

[omelkonian]

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?

[gallais]

This should probably mention ⇔ in the name (cf. concat-∈↔ below)

[omelkonian]

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.