[ refactor ] Functoriality of `Data.List.Relation.Binary.Sublist|Subset` wrt `All` and `Any`

[jamesmckinna]

Should this be a corollary of something about All P xs implies All P ys whenever ys is a subset of xs?

Indeed, and this appears twice in the library:

• Data.List.Relation.Unary.All.Properties.anti-mono : xs Subset.⊆ ys → All P ys → All P xs (and Sublist is a stronger property than Subset)
• Data.List.Relation.Binary.Sublist.Propositional.Properties.All-resp-⊆ : {P : Pred A ℓ} → (All P) Respects _⊇_ and this should (added: perhaps?) be refactored to a proof in ...Sublist.Setoid.Properties, under assumptions that P respects the underlying Setoid equality?

Originally posted by @jamesmckinna in #2522 (comment)

[MatthewDaggitt]

Eek that's not ideal that it appears twice 😓

My instincts say that it should live under Sublist...

[jamesmckinna]

My instincts say that it should live under Sublist...

As would mine, except for the fact that the Sublist versions morally should delegate to the Subset versions via Sublist⇒Subset? But then we have the problem that this lemma is under ...Subset.Setoid.Properties... sigh!?

[MatthewDaggitt]

As would mine, except for the fact that the Sublist versions morally should delegate to the Subset versions via Sublist⇒Subset?

Err, that's not a principle that any of the existing code has been designed around. It might be possible to do but it would involve a wholesale refactoring of the Sublist modules I suspect.

[JacquesCarette]

(There's quite a bit of discussion in #2522 that is relevant.)

This is a much more general design issue: should we prove things directly or as special cases of more general results? That's probably the real discussion to be having. I'm fairly sure that has come up before! There are pros and cons, and my opinion on that has changed (evolved?) multiple times over the years.

[jamesmckinna]

@JacquesCarette 's deeper question

Are we able to distil, from the long history stdlib commits, any exemplary case studies to illustrate the pros and cons of each choice (wrt the general design question, rather than that of the OP)?

What would our criteria be for measuring 'pro' and 'con'?

[JacquesCarette]

One difficulty of using Agda for case studies is that it is hard to disentangle Agda-specific weaknesses from generic good/bad ideas for this kind of design.

Furthermore the pros and cons also depend hugely on the reader is (newcomer to the language, new learner of a topic, someone fairly comfortable, a bona fide mathematician expected to understand the general setting, a library maintainer, etc).

Lastly, it depends on what is being read. Is it the "original source code that was handwritten" or something derived? One definite possibility, which is currently a route not taken, is to generate human-readable, simplified proofs out of general/abstract proofs. Having multiple views on proofs could satisfy a broader audience than making a hard choice of having a single proof.

The only thing we can distill from the history of stdlib is a "feasible compromise path" that seemed reasonable based on technology of >> 12 months ago (both because of Agda itself and the slow deprecation cycle of stdlib).

[jamesmckinna]

Update, derived from my experiments in #2808 :

• the first definition, Data.List.Relation.Unary.All.Properties.anti-mono is based on the Propositional version of Subset.⊆ (so the lemma appears unnecessarily specialised), but is then required for all-anti-mono, in order to avoid having to additionally consider closure of boolean-valued predicate p closed under equality... NB. neither lemma is used anywhere else in stdlib... but attempting to deprecate them causes a dependency cycle :-(
• the second definition, based on Sublist, once refactored to avoid All.lookup in favour of the Setoid version of the lemma, then causes problems in Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables because no longer definitionally equal to All.lookup.

So: the overall refactoring strategy/pathway forward isn't completely clear... but perhaps suggests that my OP was... too hasty ;-)