[ refactor ] Possible refactoring of #2509 / #2513 ?

[jamesmckinna]

This issue may be regarded (and hence instantly dismissed) as a status:duplicate of #2509... but posted for 'documentation'/alternative implementation purposes.

I'm happy with the merged #2513 , fixing #2509 , and so too is the author of the OP. Thanks to @MatthewDaggitt for the speedy turnround time!

That said, a brain-worm has been worrying away at me as to whether a pattern-matching-free solution was available (slightly better abstraction wrt presentation/implementation of the Sublist relation...?), and it seems there is: relative to the existing solution in Data.List.Relation.Unary.All.Properties, we can refactor as follows

all⊆concat : (xss : List (List A)) → All (Sublist._⊆ (concat xss)) xss
all⊆concat {A = A} xss = All.tabulate xs∈xss⇒xs⊆concat[xss] where
  xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs Sublist.⊆ concat xss
  xs∈xss⇒xs⊆concat[xss] {xs = xs} xs∈xss
    with prf ← Sublist.concat⁺ (Sublist.map Sublist.⊆-reflexive (Sublist.from∈ xs∈xss))
    rewrite List.++-identityʳ xs
    = prf

(and further simplification may be even be possible in the definition of prf itself? The ⊆-reflexive step is to pass from a rather simple relation via map to the more complex iterated Sublist (Sublist R) ... so this seems to have the flavour of the triangular identities for Sublist as a suitable 'monad' on relations... but I can't quite see the details yet)

This suggests that we might, instead, refactor by lifting out the above where-bound lemma into a self-standing one in Data.List.Relation.Binary.Sublist.Propositional.Properties (maybe even in Setoid? but then the proposed refactoring seems to stumble on the parameterisation on the Setoid, and the lemma shifts from A to List A... :-(, so perhaps the answer is to pull back all the way to Heterogeneous.Properties?) of the form

xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
xs∈xss⇒xs⊆concat[xss] {xs = xs} xs∈xss
  with prf ← concat⁺ (Sublist.map ⊆-reflexive (from∈ xs∈xss))
  rewrite List.++-identityʳ xs
  = prf

leaving the final implementation (under Data.List.Relation.Unary.All.Properties? or should this move as well?) simply as:

all⊆concat : (xss : List (List A)) → All (Sublist._⊆ (concat xss)) xss
all⊆concat {A = A} xss = All.tabulate Sublist.xs∈xss⇒xs⊆concat[xss]

[MatthewDaggitt]

If this can be done in a way compatible with the current module dependency graph then this seems like a nice refactoring.

[jamesmckinna]

If this can be done in a way compatible with the current module dependency graph then this seems like a nice refactoring.

#2513 added

• Data.List.Relation.Binary.Sublist.Propositional.
• Data.List.Relation.Binary.Sublist.Propositional.Properties

to the dependencies of Data.List.Relation.Unary.All.Properties, but before a v2.2 release we're free to migrate the code for all⊆concat, aren't we?.

So the question is: do we want Data.List.Relation.Binary.Sublist.* to depend on Data.List.Relation.Unary.All.*, or vice versa?

As for the proposed refactoring, I still need to figure out the best way to achieve it, but that is, I think, independent of the above question?

[MatthewDaggitt]

Data.List.Relation.Binary.Sublist.* to depend on Data.List.Relation.Unary.All.*

My feeling is definitely this way round. Binary relations should depend on unary relations.

[jamesmckinna]

OK. I think we were perhaps too hasty with #2513 !

[jamesmckinna]

Incoming PR #2524 refactors to put lemma under Sublist.Setoid.Properties, with (immediate) re-export to Sublist.Propositional.Properties.
I haven't managed to simplify the proof of the helper lemma, but that can follow later, if ever.