Refactor Data.List.Relation.Binary.Permutation.*, part I

[jamesmckinna]

Part I of a project to fix #1354

Highlights of the refactoring, cf. #2317 :

• Definitions don't change, so this is a 'conservative' first go, non-breaking for v2.1
• Additions to each of Propositional and Setoid and their Properties reconcile, more or less, the shared parts of the API
• Remove appeals to 'buggy' PermutationReasoning additional syntax Parsing problems with the PermutationReasoning combinators in Data.List.Relation.Binary.Permutation.Propositional #2319
• General tidying up: variables etc.
• Equivalence in Propositional of the relation and the Setoid (setoid _) instance
• Refactor Propositional.product-↭ in that spirit
• Setoid changes the proof of ↭-trans in terms of new lemmas ↭-transˡ-≋ and ↭-transʳ-≋; with them a sharpening of the analysis in split via a new lemma ↭-split (purely structural; no WF-induction required)
• Move to Homogeneous, and deprecation in Setoid, of steps; towards removing legacy cruft now rendered obsolete by the above analysis
• (BUG?) steps is deprecated in Setoid, but doesn't trigger the WARNING_ON_USAGE when the qualified-imported module Permutation S is opened in Properties
• Final tidy up of BagAndSetEquality finishing off refactoring begun in Refactor Data.List.Relation.Binary.BagAndSetEquality #2321

Not done, but could be:

• refactor Setoid.Properties into Core and derived
• ditto. for Propositional, and then rederived via the Setoid (setoid _) instance (eg even the drop... properties can be derived from those in Setoid)

Won't do:

• move Setoid properties to Homogeneous (as in Refactor Data.List.Relation.Binary.Permutation.* #2317) and knock-on refactoring of the Core properties etc.

[MatthewDaggitt]

Generally looks good though! The drastic reduction in proof length is pretty great!

[jamesmckinna]

@MatthewDaggitt I think that's all of your review comments handled now! But leaving certain one of the conversations unresolved until you're happy... ;-)

[MatthewDaggitt]

Other than that looks great!

[gallais]

As always I am going to be annoying and complain that I don't like prefixed
names because users can either use the short names or import the module
qualified if they need to manually disambiguate.

The same goes for split being renamed to ↭-split (although in that case
the name split is already pretty poor IMO).

[jamesmckinna]

@gallais I don't find the comment annoying!
What I find annoying is the the abstraction failure when explicitly exporting constructors from an inductive definition which should remain (externally, to clients) abstract, IMHO (cf. z<s in Data.Nat.Base, and 0<1+n in Data.Nat.Properties, not that I/we are entirely consistent in enforcing this...)
Since this is also part of a greater project of refactoring Permutation towards completing #1761 / #1354 I wanted to make sure that in Properties, references to the constructors were abstracted on those lines before proceeding further.

As regards ↭-split, this is not a renaming of split, but a significant generalisation which permits a much improved proof of dropMiddleElement... so a cognate name change is needed to reflect the 'better' typing! As for giving it a better name, I'm open to suggestions!

[jamesmckinna]

Modulo @gallais 's comment, and my (attempted) rebuttal, I think that this is good to go @MatthewDaggitt unless there are review comments of yours that you are not happy have been dealt with...?

[jamesmckinna]

At some point, the merge conflict resolution (probably thanks to me) went wrong, so fixing things now...

[jamesmckinna]

Resolving latest round of merge conflicts exposed some issues with CHANGELOG (incl. a bug in that for #2418 ), which I've attempted to correctly rectify, but until this is merged, they'll probably go round and round in circles... sigh.

Meanwhile, there are still the (potentially) unresolved comments form @gallais about naming/synonyms for constructors, but I think these can be postponed until subsequent parts of this overall plan to revise/reform Permutation get implemented?

[jamesmckinna]

Hmmm.... fixing the merge conflict may need a bit more thought. UPDATED: I think that works now... Nope, something seems to have gone wrong somewhere. The product/All NonZero lemmas seem to have got bumped out of place? Hopefully fixed now!