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.

[JacquesCarette]

This is a special case of \oplus of two permutations.

[MatthewDaggitt]

I agree (lift0 should be as well!), but we don't have such an operation in the library. I have added a note that we should refactor it when we add that operator.

[JacquesCarette]

I have it buried in my Rig Categories repo. I need to port the basic operations on permutations over. I've got the full semiring defined there.

[jamesmckinna]

But also: Function.Related.TypeIsomorphisms etc. as per #2489 ?

[jamesmckinna]

Plus, of course: we only need this operation because Permutation.Setoid stipulates swap as a constructor... ;-)

[JacquesCarette]

Yes, absolutely, there is some great stuff in Function.Related.TypeIsomorphism. And a rather apt 'of course'.

[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

[jamesmckinna]

How about

Suggested change

	xs↭ys⇒|xs|≡|ys| (swap eq₁ eq₂ xs↭ys) = ≡.cong (λ x → suc (suc x)) (xs↭ys⇒|xs|≡|ys| xs↭ys)
	xs↭ys⇒|xs|≡|ys| (swap eq₁ eq₂ xs↭ys) = ≡.cong 2+_ (xs↭ys⇒|xs|≡|ys| xs↭ys)

(possibly at the cost of an additional import from Data.Nat.Base)?

[jamesmckinna]

Can we, by convention, avoid writing the ∀ {n} → prefix here?

[jamesmckinna]

I think this should be:

Suggested change

	toFin-lookup : ∀ i → lookup xs i ≈ lookup ys (Inverse.to (toFin xs↭ys) i)
	onIndices-lookup : ∀ i → lookup xs i ≈ lookup ys (Inverse.to (onIndices xs↭ys) i)

and again, do we need the ∀ i → prefix in CHANGELOG?

[Taneb]

(explicit arguments should definitely be in the changelog - but does i need to be explicit?)

[jamesmckinna]

@Taneb I'm surprised to learn that (is it documented?): given that CHANGELOG isn't machine-checked, I use it to get (a sense of) the high-level gist of what's been added, and then look at the module for the exact details of the quantification/parametrisation etc.

As for whether i needs to be explicit in this lemma, I expect so, if only by analogy with (all the) lemmas about lookup in Data.List.Properties...?

[jamesmckinna]

Suggested change

	open import Data.Fin using (zero; suc)
	open import Data.Fin.Base using (zero; suc)

[jamesmckinna]

Is this definition easier to describe/define indirectly, via the composition of

• eval ((0F , 1F) ∷ (1F , 0F)) using Data.Fin.Permutation.Transposition.List
• lift₀ {suc m} {suc n} (lift₀ {m} {n} π)

or indeed (more) directly, as transpose 0F 1F ∘ₚ lift₀ {suc m} {suc n} (lift₀ {m} {n} π)?