[ fix #1354 ] Refactoring Permutation.Propositional

[gallais]

Still missing: CHANGELOG entries

[MatthewDaggitt]

Closing as we've decided that its better to wait for typed pattern synonyms to finally make an appearance.

[jamesmckinna]

Suggest re-opening this, as I seem to have got it to work with the pattern synonyms... using some ideas from #2317 and #2321 towards further unification, if someone can help me unify the two Permutation.*.Properties modules along the lines considered in #2317 ... incoming revised/streamlined/refactored/rebased commits shortly.

UPDATED: as with that more recent PR, will convert to DRAFT for now until ready to review.

[JacquesCarette]

Other than that one odd name (which seems to actually be something pre-existing), this is looking quite good.

[jamesmckinna]

So far all the heavy lifting was done years ago by @gallais so props to him.

But I think that my recent work on #2317 hopefully points the way to getting the Properties unified as well. If that succeeds, then most of the guff in Propositional disappears entirely, and with it, all/most of the angst about qualified import of refl... I hope. Fingers crossed!

UPDATED Lots of refactoring work on #2317 ahead of bringing it to bear on this PR. But first see #2333 as a more manageable first part of a roadmap detailed there.

[jamesmckinna]

Removing the milestone marker from this for the time being...

[JacquesCarette]

So what needs to be done to push this to the finish line? [Other than a likely rather nasty merge!]

[JacquesCarette]

I might have a student who could push this to the finishing line, if it was clear what needed to be done - @jamesmckinna ?

[jamesmckinna]

I might have a student who could push this to the finishing line, if it was clear what needed to be done - @jamesmckinna ?

See my comment on #2317

[MatthewDaggitt]

My understanding of the argument was that we wanted to eventually deprecate Permutation in favour of the two new definitions. Which would mean re-proving all the existing results for both variants. This probably would be a good student project.

[jamesmckinna]

My understanding of the argument was that we wanted to eventually deprecate Permutation in favour of the two new definitions. Which would mean re-proving all the existing results for both variants. This probably would be a good student project.

Happy to consult/supervise/review if there is a willing candidate. There may well be more we can usefully do, esp. eg. wrt names of lemmas, as well as the overall structure. The factorisation out of Homogeneous properties may still be useful, but less so now than before? I suspect any end result will also end up being v3.0 because breaking...

[MatthewDaggitt]

I suspect any end result will also end up being v3.0 because breaking...

Yes, the big switch over will be, but we extend the API for the two new modules in a non-breaking way in 2.4.