[ add ] Module ⊆-Reasoning for Data.List.Relation.Binary.Sublist.*

[jamesmckinna]

Fixes #2526

DRAFT until the following are sorted out:

• Propositional instantiation UPDATED: I think this does 'just' work by import from Setoid for the propositional equality setoid...?
• Refactor Setoid instantiation to delegate appropriately to Heterogeneous, but I can't quite figure out whether the relevant Preorder bundles match up (difference between Relation.Binary.Properties.Setoid.≈-isPreorder and Relation.Binary.Properties.Setoid.isPreorder ... hidden under Data.List.Relation.Binary.Equality.Setoid via Pointwise?)

Issues:

• A second set of eyes would be helpful re the second point above! (and even the first!?)

• Each implementation relies on an import of each of:

  • Relation.Binary.Reasoning.Preorder
  • Relation.Binary.Reasoning.Syntax

  Is there ever a reason not to have one without the other? (ie. should the specialised Relation.Binary.Reasoning.Preorder reexport the syntax directly?)

[JacquesCarette]

The code as is seems fine to me - so I'm not quite understanding what 'failure' the second point is about?

I'm pretty sure one can use Relation.Binary.Reasoning.Preorder without the Syntax part, if one is doing locally as opposed to building up externally-visible combinators.

[jamesmckinna]

Second things first:

I'm pretty sure one can use Relation.Binary.Reasoning.Preorder without the Syntax part, if one is doing locally as opposed to building up externally-visible combinators.

Fine. Happy to leave things as they are. My comment stems from the sense that the Relation.Binary.Reasoning.Base.* modules already handles the 'syntax-free' versions, and now that Preorder etc. introduced standardised syntax for the various relations via renaming directives, whether it made sense to also standardise on the corresponding syntax definitions for the generic Reasoning combinators, as part of that specialisation...

[jamesmckinna]

First thing second:

The code as is seems fine to me - so I'm not quite understanding what 'failure' the second point is about?

As I glimpse/see/understand it, there is a potential [ DRY ] opportunity to share the behaviour between Data.List.Relation.Binary.Sublist.Heterogeneous and ...Setoid by instantiating {R = _≈_} in the former to obtain the latter. But I wasn't sure whether that was actually correct, because there seems to be an impedance mismatch between the two (distinct?) proofs of ⊆-reflexive in play... and I had been wondering if there was a 'least common generalisation' available as a solution to the DRY 'problem'... but I couldn't see it.

[JacquesCarette]

Ahh, now I see it (the problem, that is). I'll try to circle back to this before I get swamped with term things.

[jamesmckinna]

While fixing the CHANGELOG merge conflict, I couldn't help noticing how broken (wrt alphabetical entries) that has become: fix in separate PR, or at release time?

[JacquesCarette]

While fixing the CHANGELOG merge conflict, I couldn't help noticing how broken (wrt alphabetical entries) that has become: fix in separate PR, or at release time?

Open a separate issue for that? I would think a separate PR - we don't want to push too many things to 'release time' otherwise it makes putting out a release too much work.

[JacquesCarette]

About DRY: as far as I can see, it's more than just instantiating the relation, a lot of the 'related' properties in the two files also differ in their uses of which equivalence relation is at play (Sublist vs containment). So that too would have to be factored out first - which would be quite a lot of work.

If anything's going to be done about this, it is for sure a non-trivial v3.0 job.

[jamesmckinna]

Thanks @JacquesCarette .

I'd be happy to leave things as they are, with distinct Reasoning modules for each of Heterogeneous and Setoid sublists, and postpone downstream further consideration of how we might unify these designs.

[JacquesCarette]

Were you just thinking about the reasoning modules? I was looking at the whole file.

[jamesmckinna]

Were you just thinking about the reasoning modules? I was looking at the whole file.

Ah!?

Because the PR at hand is only concerned with adding the new ⊆-Reasoning modules to Sublist, I was trying my utmost not to think about, or touch, anything else ;-) But might that mean you do know how to (diagnose and) fix the issue at the top relating the two kinds of Sublist reasoning?

[JacquesCarette]

Hmm, why doesn't

module ⊆-Reasoning where

  open HeteroProperties.⊆-Reasoning ⊆-preorder public

work? My tests make it feel like that accomplishes the same. Pushed to your branch.

[jamesmckinna]

HeteroProperties.⊆-Reasoning ⊆-preorder

Interesting! Thanks for the prompt to play around a bit more myself... and I think I disagree with you.

The HeteroProperties.⊆-Reasoning module takes a Preorder bundle on the carrier of R, and gives Preorder reasoning combinators for Sublist R. So HeteroProperties.⊆-Reasoning ⊆-preorder is going to yield Preorder reasoning for Sublist _⊆_, rather than Sublist _≈_.

But this did prompt me to investigate whether Sublist.Setoid.⊆-preorder is the same as Hetero.preorder instantiated at

Relation.Binary.Properties.Setoid.≈-isPreorder S : IsPreorder _≈_ _≈_

the (canonical!) Preorder based on _≈_... and it is, thankfully. Commit incoming.

UPDATED: I think this is the correct choice for reasoning wrt _⊆_, but some part of me is still niggling over whether it should instead be instantiated at

Relation.Binary.Properties.Setoid.isPreorder S : IsPreorder _≡_ _≈_

???
(This was the substantive issue at hand in the second point at the beginning of the PR)

[jamesmckinna]

Got my commits slightly out of order just now, but have now also refactored the proof of the lemma introduced in #2524 to use the new ⊆-Reasoning module...

  xs∈xss⇒xs⊆concat[xss] : xs ∈ xss → xs ⊆ concat xss
  xs∈xss⇒xs⊆concat[xss] {xs = xs} {xss = xss} xs∈xss = begin
    xs ⊆⟨ ⊆-reflexive (≋-reflexive (sym (++-identityʳ xs))) ⟩
    xs ++ [] ⊆⟨ concat⁺ (map-≋ ⊆-reflexive (from∈-≋ xs∈xss)) ⟩
    concat xss ∎
    where open ⊆-Reasoning

but there are clearly still some UX aspects to iron out, because the combinators for _≋⟨_⟩_ steps don't seem to work quite right:

• need for an explicit _⊆⟨ ≋-reflexive ... ⟩_ step ... neither of

    xs ≋⟨ ≋-reflexive (sym (++-identityʳ xs)) ⟩
    xs ++ []

  nor

    xs ≋⟨ sym (++-identityʳ xs) ⟩
    xs ++ []

  seem to be valid ⊆-Reasoning steps?
• need for explicit appeal to sym in the above:

    xs ≋⟨ ++-identityʳ xs ⟨
    xs ++ []

  isn't a valid step either?

[JacquesCarette]

Oops - thanks for spotting that. Subtle.

The other parts might be related to the Reasoning module not exporting enough?

[JacquesCarette]

The reason you can't do those steps is because in Data.List.Relation.Binary.Sublist.Heterogeneous.Properties those are explicitly hidden!!!

  open ≲-Reasoning (preorder ≲) public
    hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼)
    renaming (≲-go to ⊆-go; ≈-go to ≋-go)

After revealing that, then at least the proof could be simplified to

  xs∈xss⇒xs⊆concat[xss] {xs = xs} {xss = xss} xs∈xss = begin
    xs ≈⟨ ≋-reflexive (++-identityʳ xs) ⟨
    xs ++ [] ⊆⟨ concat⁺ (map-≋ ⊆-reflexive (from∈-≋ xs∈xss)) ⟩
    concat xss ∎
    where open ⊆-Reasoning

Then I tried the ≋ step. That gave very weird errors until I figured out that that particular module takes 4 arguments and not merely the 3 that it was given! Once I managed to fix that, the combinators worked, but I wasn't able to use them to simplify things.

My 'improvements' pushed.

[jamesmckinna]

The reason you can't do those steps is because in Data.List.Relation.Binary.Sublist.Heterogeneous.Properties those are explicitly hidden!!!

  open ≲-Reasoning (preorder ≲) public
    hiding (step-≈; step-≈˘; step-≈-⟩; step-≈-⟨; step-≲; step-∼)
    renaming (≲-go to ⊆-go; ≈-go to ≋-go)

See previous about being tired/making mistakes! I had been too quick to emulate the code for Subset without thinking through the consequences!

Thanks for pushing the changes, and paying more attention than I could manage to the structure of reasoning modules... ;-)

[JacquesCarette]

Thanks for pushing the changes, and paying more attention than I could manage to the structure of reasoning modules... ;-)

This wasn't "paying more attention", which would have been the case if I were writing the code. This was sleuthing, because I was in 'debugging mode'. Something that I rather enjoy (and, sadly, it seems few programmers like this kind of investigation).

[jamesmckinna]

Nice!

[jamesmckinna]

Hopefully that's now tidied things up enough after the merge conflict resolution and @JacquesCarette 's improvements.
Too cheeky to now ask @MatthewDaggitt to add this to the v2.2 milestone before v2.2-rc1?