Reimplement `Permutation.Propositional` in terms of `Permutation.Setoid`

[MatthewDaggitt]

Unlike other binary relations over lists, Data.List.Relation.Binary.Permutation.(Setoid/Propositional) are implemented separately which results in an awful lot of proof duplication. It also means that other modules (e.g. Subset) don't play nice when trying to transfer results from setoid equality to propositional equality. I've added the breaking tag as it remains to be seen if they can be unified in a backwards compatible manner.

[MatthewDaggitt]

Parameterise Homogeneous relation by extra relation Q with Pointwise R => Q then use it to instantiate with propositional equality.

[MatthewDaggitt]

Blocked by typed pattern synonyms: https://github.com/agda/agda/issues/2069.

[MatthewDaggitt]

I remember this causing me a huge amount of pain when working with these things. Maybe we only need typed pattern synonyms to do it in a backwards compatible manner. Going to look at it this afternoon as one possible last issue to sneak into v2.0.

[jamesmckinna]

I'm completely in sympathy with wanting to sneak more in to v2.0... ... but this one seems sufficiently specialised, that I might gingerly suggest taking a breath and sitting on your hands.

Your activity has been prodigious in the last few days alone, and it's hard not to think a moments pause might be worthwhile, before resuming with a planned v2.1 for say, sometime in the window Jan-Mar 2024.

That gives us, and users a window in which to upgrade, during which we move forward with issues/PRs like these, and others such as #2149 (which I might otherwise have lobbied harder for now, if I'd had time for the actual breaking changes which I intend to follow up with)

[MatthewDaggitt]

Yup fair enough. Re-exporting the constructors swap and prep seems to be blocked on https://github.com/agda/agda/issues/3210 anyway. Hmm but actually we could play the game that https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Relation/Ternary/Appending/Setoid.agda plays and define the general datatype in a parameterised module ourselves, and then re-open that.

[jamesmckinna]

Well... a lot has been merged since my (unironic, then; not sure so much, now) comment above.

I guess there might be time to revisit this for v2.0, but I'd once again counsel against that, not least because it's only recently come home to me that the 'modern' approach to Permutation on List seems quite far away from how it looked to us in the early 1990s. So I'd welcome some reconsideration of the basic API, not least because all of the discussion of the ability to reuse/reimport constructors from Setoid to Propositional seems to turn on (unintended) clash between the constructors (and their names!) and those of PropositionalEquality, at least if I understand the discussion of the closed #1761 ...

TL;DR: however you choose to represent the relation, consider carefully (the module-level API for) how you export access to it, and to 'doing induction over it'.

... so, with due apologies in advance if I have misunderstood (!?) the nature of the issue, please read on... for an old-timer's perspective:

Back in the Good Old Days (TM) (1990, to locate this personally for me; no real native inductive types in LEGO or Coq at this point, so things got defined impredicatively...), there were/semed to be two extremal versions of how to define the relation:

• (declarative) as the least congruence (for nil, cons; alternatively, and arguably better in terms of abstractness wrt the List API, for _++_) which makes `++` commutative; free commutative monoids as given/carried by List modulo permutation follows pretty immediately from this;
• (algorithmic) as the least relation _∼_ such that [] ∼ [] and if xs ∼ ys ++ zs, then x ∷ xs ∼ ys ++ x ∷ zs

NB

• this is the Propositional version, but I'm (reasonably!?) confident that it lifts up to Setoid with some more yoga...;
• no need for decidability equality! (compare count-based definitions of eg Bag-related notions)

Now, each of these choices (my PhD thesis chose the declarative one; the Coq developers the algorithmic) involves Lots (TM) of different amounts of work in showing equivalence (I forget if trans is admissible for the second, but reflexivity, symmetry, congruence and commutativity/swap follow easily, by induction on _∼_ and/with side induction on List, for example), but what is the case is that you can:

• choose 'better' constructor names (in either setting) to avoid name clashes (or even, to deliberately exploit it, eg re-using [] and _∷_ in the algorithmic case);
• take one or other definition as an abstract (module-level) API for the relation;
• (and, moreover, should) package it with a choice of induction principle for the abstract relation.

NB Fans of views may note that the latter move (and indeed the former!) may be accomplished by defining a suitable view of either relation (or any other representation, for that matter). Is that the content of @MatthewDaggitt 's Appending observation?

The current choices of a version of the relation intermediate between the above two extremes seems (with the 'benefit' (!?) of 30+years' hindsight... ;-)) ... worth revisiting, at least, before proceeding.

[jamesmckinna]

So, my memory is clearly not what it was, at least locally... revisiting this now after #2317 and #2311 which I developed entirely oblivious to the discussion here (including my own contributions!), and perhaps more defensibly, the closed #1761 ... sigh.

[jamesmckinna]

So... there is probably a lot more to discuss (ahead of any eventual PR for review; I was probably premature in filing #2317 but my experience so far has led me to some of the things I'll propose below), but here goes, with a big pinch of IMNSVHO, a possible route-map (breaking/refactoring) for how to take this forward:

(BREAKING) The thing, heartbreaking for me at least, about the legacy implementations is the missed opportunity from the ground up to unify the two presentations by choosing [] and _∷_ as constructors (in place of refl and prep; [] is 'refl specialised at []'; prep is 'just' _∷_, exactly by analogy with Pointwise), in order to make Reflexivity wrt Pointwise equality an admissible rule, and not a constructor.

This would permit a number of things:

• prep for Propositional permutation could then be given as a pattern synonym (I don't believe this requires typed pattern synonyms to be effective, unblocking the objections noted above) so that Setoid and Propositional could then otherwise share constructors/pattern-matching in the various (inductive) proofs of their properties;
• having refl only defined as a constructor at xs = [] = ys gives a tighter definition of the Homogeneous/Setoidrelation, and makes properties of it easier to prove (design pattern for inductive definitions: 'Atomic Axioms' discussed extensively in McKinna and Pollack (1992/1999) in the context of the proof theory of formalised type theory, but the remarks/insights apply mutatis mutandis here in spades, too);
• the 'smart constructor' for Transitive reduces to a much simpler instance of inversion wrt assumptions of the form Permutation R [] ys/Permutation R xs [], and can be introduced (and used!) before having to prove that Permutation R is stable under LeftTrans/RightTrans wrt Pointwise R ; this is provable already, but the point being made is that one Pointwise reflexivity is merely an admissible rule, we can focus on what properties Pointwise R needs to satisfy for desirable properties of Permutation R without getting caught up in the inductive definition of the latter... and the basic idea, akin to that of the(old) smart constructor(s) for transitivity is that refl steps should be absorbed without disturbing the ambient 'shape' of a derivation of 'permutation R', because Pointwise equalities get pushed to the leaves via prep/_∷_ (using Transitive R), at which point they disappear, because we only have Permutation R [] [] at those leaves, by construction...
• the focus on the above analysis means that, with refl only at [], or in the 'full' case, the proof of split can be improved as far as eliminating well-founded induction on steps entirely (IIUC, this was the only proof that used that observer function, together with its fiddly 'transitivity-wrt-Pointwise-preserves-steps' arguments, which are merely proxies for the 'real' 'transitivity-wrt-Pointwise-preserves-Permutation' proofs...)
• against @gallais 's comments on #1761 I think it is essential to insist on the use of smart constructors on the RHS of definitions (even the ones inductively defined, and in any case for the Reasoning modules etc.) as this better supports abstraction wrt the underlying choice of representation, as well as avoiding direct appeal to trans etc. (known to be inefficient in its 'unoptimised' form) /systematically building in the 'optimising' versions...

(NON-BREAKING)

• all of the above, but retaining 'full' refl as a constructor, and having to work around the pattern synonym problem for the Propositional case, but I believe at no point does that require the inductive definition of Permutation.Propositional to be exposed to clients, except to show equivalence with the Setoid definition instantiated at setoid A... (to be further discussed? certainly not yet implemented, but the path is now clear, I think, to me at least)
• more of the factorisation of Setoid/Propositional properties by delegation to a set of Core properties of Homogeneous, with inductive proofs, and most (all, if we accept the breaking change above, I think) available by specialisation of a set of Homogenous.Properties derivable from the Core; most of the germ of such factorisation is already done in #2317 , if not the actual modular organisation
• the main non-trivial appeal to the inductive character of Permutation.Propositional, in the library at least, is in the proof of equivalence with Bag equality in BagAndSetEquality, but that is also tidied up/refactored by #2317 in favour of Core properties of Homogeneous; but as @MatthewDaggitt points out, the interaction with other definitions such as Any/Membership in the Propositional case would, as already noted, benefit greatly from a rationalisation of the representations (but that's out-of-scope for the time being, unless insights from those problems feed into a critique of the proposed design here)

(DOWNSTREAM)

• (DEPRECATION) those 'non-Core properties of Homogeneous are really properties of any plausible definition of Permutation, so should be factored out as a parametrised module, to support new/alternative definitions (cf. #2311 and its competing proposals)
• etc. To Be Continued...

[MatthewDaggitt]

Okay so there's a few ways to proceed:

1. We can wait until 3.0 rolls around in a few years time and fix it all then.
2. We can make what backwards compatible changes we can now, and then make the major changes in 3.0.
3. We can add a new implementation to the library that lives alongside the current one. Maybe deprecate the current one, and then do a switcheroo in 3.0.

Thoughts?

[jamesmckinna]

Well, I had understood your critique of #2317 to amount to "do 2, then do 3, and then loop back to 1 eventually if necessary", and that's what I am slowly proceeding towards in refactoring that PR into more manageable pieces.

But I still thought it worth arguing for one possible design for a breaking change which is sufficiently 'small' (specialise refl to []) that it might fly now if it were given enough support after due consideration. Sorry now that we didn't manage to do this before 2.0 ;-) Big mouth strikes again!

[MatthewDaggitt]

Well, I had understood your critique of https://github.com/agda/agda-stdlib/pull/2317 to amount to "do 2, then do 3, and then loop back to 1 eventually if necessary", and that's what I am slowly proceeding towards in refactoring that PR into more manageable pieces.

Yes that sounds reasonable.

But I still thought it worth arguing for one possible design for a breaking change which is sufficiently 'small' (specialise refl to []) that it might fly now if it were given enough support after due consideration.

The problem is although it's a small change semantically, refl is used a lot in code that actually uses permutations so it's still a big breaking change for users, one that we've promised not to do unless absolutely necessary. Unfortunately I think we'd struggle to justify that it's absolutely necessary to change it immediately...

I do sympathise with the urge to fix things immediately! I find it quite frustrating that we can't!

[jamesmckinna]

So I thought I could knock-up a version of the (BREAKING) proposal, but it foundered on not getting sharing to work between an import of

• Propositional {A = A} and
• Setoid.Properties (setoid A)

Any idea how to achieve such sharing in general?

(Also the arithmetic of stepsand its properties: all proofs of [] ↭ [] need to be collapsed during the computation)

[jamesmckinna]

As for client code/users making use of refl as a constructor... that does surprise me. or perhaps: shocks me, but doesn't surprise me.

It feels as though that;s not something to use on the RHS ever (in favour of a definitional proof of reflexivity) and as I've attempted to argue already, the exposure of the patterns in the various definitions is most of the source of the problem in the first place! You can just about get away with using it on the LHS during pattern-matching, if prep and swap can be given as pattern synonyms, but you shouldn't really want to!

[jamesmckinna]

Yup fair enough. Re-exporting the constructors swap and prep seems to be blocked on agda/agda#3210 anyway. Hmm but actually we could play the game that https://github.com/agda/agda-stdlib/blob/master/src/Data/List/Relation/Ternary/Appending/Setoid.agda plays and define the general datatype in a parameterised module ourselves, and then re-open that.

Looping back to this point, the significance of which I missed the first time around: is this not a/the suitable role for the Homogeneous module, to be the (analogue of the) General module, and then be reimported in each of Setoid and Propositional? For sure, there's more machinery to define in such a module (but I think I've successfully isolated most of the pieces, essentially to do with factoring out the dependencies on refl/↭-pointwise and trans/-trans in #2317 ) together with how we parametrise the eventual Properties modules on properties of Homogeneous cf. my question about sharing above, I think. Food for thought!