Some preparatory proofs for proving sorting+permutation is equality #2724

[MatthewDaggitt]

I've been sniped by #2723. This is a preparatory PR for the full proof that sorting two lists that are permutations of each other result in equal lists.

[jamesmckinna]

Having looked at this, and its followup, in particular lemma ↗↭↗⇒≤, do I understand correctly that the gist of argument is (Cantor-Schroeder-Bernstein redux):

• Sorted O xs implies that lookup : Fin (length xs) → O.Carrier is an order monomorphism, so has a monotonic inverse on its range
• for Sorted O xs, Sorted O ys, xs ↭ ys via onIndices thus induces an order isomorphism between Fin n and itself, which is then necessarily the identity
• thus the O-monotone map from xs to ys induced via conjugation with lookup and its inverse, is also the identity (via faithfulness of the functor induced by onIndices?)
• hence xs ≋ ys...

If so, then I think this PR and its followup may be simplifiable via the already existing Data.Fin.Properties.injective⇒≤ (and/or pigeonhole/cantor-schroeder-bernstein)?

UPDATED: on closer examination, maybe this is what you have!

[jamesmckinna]

Some nitpicks.
Happy to approve, but I too have been sniped by this... would love to be able to simplify if at all possible!

[jamesmckinna]

Should we define these here, or have them created automatically by (defining and then) opening the corresponding bundle(s) in Data.Fin.Properties? cf. #2391 / #2490

[MatthewDaggitt]

Unsure. If we do so then we should do everywhere in all numeric data modules, consistently. Feel free to open an issue?

[MatthewDaggitt]

Having looked at this, and its followup, in particular lemma ↗↭↗⇒≤, do I understand correctly that the gist of argument is (Cantor-Schroeder-Bernstein redux):

Yes, I think so. If it can be simplified then I'm all for that 👍

[jamesmckinna]

I'll try to review properly this week, but for now, I've just fixed two things that slipped through the net...