Refactor Data.List.Relation.Binary.Permutation.*

[jamesmckinna]

WORK IN PROGRESS: do not review!

Of independent interest to the various competing proposals in #2311 for the 'right' representation, as it attempts to decouple the main properties of the relation from any particular notion. In particular, the isolation of the dependencies (and improved implementation UPDATED can't seem to get the syntax declarations to work for the specialised Propositional version of PermutationReasoning!?) of the Reasoning module, together with a 'better' smart constructor for transitivity in the current implementation(s), as well as a lot of nitpicky streamlining.

NEW: have removed all dependency on well-founded induction on steps in favour of a (structurally inductive proof of) better ↭-split lemma which uses the fact that Permutation R absorbs Pointwise R steps provided R is Transitive.

Currently in DRAFT, but aims to, and is most of the way towards:

• redefining Propositional as the setoid instance of Setoid, ditto. Properties
• refactoring Setoid and Setoid.Properties to localise all uses of induction on the Homogeneous representation to properties proved in general in Homogeneous (thereby allowing alternative representations)
• back-porting lemmas and proofs from Propositional to Setoid or even Homogeneous, incl.
• I have managed to get hacky/kludge proofs to work, but there is something more systematic to investigate about the higher-dimensional structure of proofs about Pointwise and Permutation lurking offstage...!?

Outstanding issues:

• fix the syntax declarations for ↭-Reasoning (esp. for <<⟨_⟩? see Parsing problems with the PermutationReasoning combinators in Data.List.Relation.Binary.Permutation.Propositional #2319 )
• should the Properties module(s) automatically re-export the corresponding 'Base' module, to avoid having to explicitly import that separately?

TODO:

• CHANGELOG ;-)
• last missing implementations from Propositional (some fiddliness here, plus some deprecation opportunities once things have been suitably generalised) UPDATED only

 ↭-map-inv : List.map f xs ↭′ vs → ∃ λ ys → vs ≡ List.map f ys × xs ↭ ys

remains

• refactor Homogeneous into Core/Base and Properties (currently a total ⟪casino⟫, esp. wrt dependencies)
• refactor Setoid.Properties into Core (representation dependent; to be discussed as the best way to achieve such modularisation for (each of) the representation(s)) and Properties depending on that component
• exporting induction principles while keeping constructors hidden?

Etc. To be continued...

[jamesmckinna]

Note to self: typechecking appears not to terminate for Data.List.Relation.Binary.Permutation.Homogeneous.Properties!?

Refactored to lift out the lemmas as ...Homogeneous.Properties.HigherDimensional...

[jamesmckinna]

Stopping here as much of the refactoring of (the properties of Setoid as instances of those of) Homogeneous is fairly settled now. So I'll now attempt to retrofit that analysis back onto the old versions. See #2333 for a start.

[jamesmckinna]

Previously @MatthewDaggitt wrote

Before I review this, am I right in understanding there's really two changes here? Firstly moving lots of stuff from Setoid to Heterogeneous and secondly changing the implementation of Propositional to use Setoid.

If so then could we do this in two different PRs? In particular the second PR is big breaking change, and therefore there are questions about when it exactly it can be merged in.

Please now consider a possible roadmap as follows:

• (Part I) reconcile the APIs for Propositional and Setoid in their 'old' versions Refactor Data.List.Relation.Binary.Permutation.*, part I #2333 ; this is slightly more conservative, and doesn't even go as far as moving everything to Homogeneous as here
• (Part II) refactor via Homogeneous.Properties.* and Propositional.Properties and Setoid.Properties in terms of Core (based on Homogeneous) and 'derived' based on the respective Core properties (and refocus this PR on such work)
• (Part III) revisit [ fix #1354 ] Refactoring Permutation.Propositional #1761 to then reconcile the two definitions, and with minimised Cores via the pattern synonym tricks?

[MatthewDaggitt]

Stopping here

Does this mean the draft status should be removed and this PR reviewed?

[jamesmckinna]

Stopping here

Does this mean the draft status should be removed and this PR reviewed?

Thanks @MatthewDaggitt for the prompt to return to this. I think the short answer, for the time being, is/ought to be "No":

• merge conflicts ahead of of the v2.1 release are stymying various open PRs, including the first part of this, namely Refactor Data.List.Relation.Binary.Permutation.*, part I #2333 , which is badged as v2.2
• the above (re-)factorisation into three parts, the first of which above, I had hoped made clear that this PR would (eventually ;-)) get broken up, part-by-part, and I haven't had the brain space to return to the second and/or third parts given that they are (potentially) breaking, and moreover, somewhat depend on the eventual fate of the first...

Sound OK to you?

[MatthewDaggitt]

Yes, sounds reasonable.