[ refactor ] Move Data.List.Relation.Unary.All.Properties.all⊆concat to Data.List.Relation.Binary.Sublist.Setoid.Properties

[jamesmckinna]

Fixes #2517 following discussion there.
Re-exports to Data.List.Relation.Binary.Sublist.Propositional.Properties automatically, so this strictly generalises #2513 as a solution to #2509 .

[JacquesCarette]

Makes me wonder if we have equational proof combinators for ⊆ reasoning.

[jamesmckinna]

Makes me wonder if we have equational proof combinators for ⊆ reasoning.

We do, AFAIK, but would they help here?

Oh, I suppose you could eliminate my go-to pattern of with ... rewrite .... Hmm, I could try that... but I'm still thinking about your comments elsewhere about the fragility of rewrite, and would like to see some concrete examples of such fragility, ie of it working, then breaking. Plenty of examples of it not working, but they seem legitimately to arise from "I'm not sure there is a case for refl when attempting to unify..." diagnostics under cubical-compatible/without-K, which I guess we have to bite the bullet on...

[JacquesCarette]

Will try to collect examples of fragility. My memory is that it mostly arises in two cases: 1) Agda upgrades, 2) (what ought to be) minor refactorings. rewrite is extremely syntatic, and so prone to fail whenever any kind of minor disturbance happens. Of course, some equational proofs also fail in that way! The biggest difference is often rewrite is used to fix up a type, often enough an implicit one, and so why it's failing can be extremely hard to figure out.

[MatthewDaggitt]

I'm with @JacquesCarette on this one. It is also my experience that rewrite proofs tend to be very fragile, and refactoring proofs that use extensive rewriting is extremely painful. In particular, it's very non-obvious which and how many terms in the goal are being rewritten.

To be honest, I would be happy with a blanket policy of no rewrite proofs in the library, but I realise that might be a bit extreme.

[jamesmckinna]

I'll fix up the rewrite step... DONE.
(Turned out to be quite clunky, in lieu of developing ⊆-Reasoning to be able to fold in the equality proof... downstream PR?)

[jamesmckinna]

Makes me wonder if we have equational proof combinators for ⊆ reasoning.

It turns out I was wrong. There is a module ⊆-Reasoning for Subset, but not, it seems, for Sublist. Sigh.
UPDATED: #2527

[jamesmckinna]

I'm with @JacquesCarette on this one. It is also my experience that rewrite proofs tend to be very fragile, and refactoring proofs that use extensive rewriting is extremely painful. In particular, it's very non-obvious which and how many terms in the goal are being rewritten.

This perhaps is one of those rare situations where I envy the affordances in the Rocq prover, whereby you can localise a rewrite step to a specific term/hypothesis via rewrite eq in exp... and I think my idiomatic use of it here, precisely only to rewrite in a lemma/subterm introduced by with, is an attempt to simulate that... I won't attempt an argument to suggest that because such a thing is with-bound (and hence the goal is already abstracted) that this idiomatic usage is somehow more robust, because then we'll get into the robustness or otherwise, of with itself... but I suspect that I could enforce that locality further by having prf be defined in a where clause... but I have refactored to avoid all such considerations now, in the spirit of the subsequent:

To be honest, I would be happy with a blanket policy of no rewrite proofs in the library, but I realise that might be a bit extreme.

Well, it's a good yardstick to hold on to, I suppose, and have refactored accordingly. But I agree it might be 'too extreme'... except that we could put it in the style-guide and then not have to relitigate this every time... modulo all the legacy proofs. Sigh.

[jamesmckinna]

Given 2 approvals, are you each happy for me also to fold in tightening the imports as identified in #2533 ?

[JacquesCarette]

I'm always pro tighter imports.