Proved sorted permutations are equal

[MatthewDaggitt]

The main result. Would like to try and sneak this into v2.3 for @onestruggler.

Have also added an explanation of the choice of propositional permutation in SortingAlgorithm and a lemma that proves the setoid version.

[jamesmckinna]

Downstream, after resolving the issues around #2744, I'd hope that these could be read off from a single appeal to min? to construct a suitable minimal counterexample (for existsPivot) or else rule out the Universal case branch by contradiction with nonStrictlyContractive. See also #2746 for the use of pigeonhole to prove injective⇒≤, so some simplification in the proof of nonStrictlyContractive might also be possible?

[jamesmckinna]

Voil`a:

Suggested change

	injective⇒nonStrictlyContractive : ∀ (f : Fin n → Fin m) → Injective _≡_ _≡_ f →
	∀ i → ¬ (∀ j → j ≤ i → f j < i)
	injective⇒nonStrictlyContractive f f-injective i j≤i⇒fj<i =
	ℕ.n≮n (toℕ i) (injective⇒≤ h-injective)
	where
	h : Fin′ (suc i) → Fin′ i
	h k = lower (f (inject! k)) (j≤i⇒fj<i _ (ℕ.s≤s⁻¹ (inject!-< k)))
	h-injective : Injective _≡_ _≡_ h
	h-injective = inject!-injective ∘ f-injective ∘ lower-injective _ _
	injective⇒existsPivot : ∀ (f : Fin n → Fin m) → Injective _≡_ _≡_ f →
	∀ (i : Fin n) → ∃ λ (j : Fin n) → j ≤ i × i ≤ f j
	injective⇒existsPivot {n = suc n} f f-injective i with any? (λ j → j ≤? i ×-dec i ≤? f j)
	... | yes result = result
	... | no ¬result = contradiction
	strictlyContractive
	(injective⇒nonStrictlyContractive f f-injective i)
	where
	strictlyContractive : ∀ j → j ≤ i → f j < i
	strictlyContractive j j≤i with i ≤? f j
	... | yes i≤fj = contradiction (j , j≤i , i≤fj) ¬result
	... | no i≰fj = ℕ.≰⇒> i≰fj
	injective⇒existsPivot : ∀ {f : Fin n → Fin m} → Injective _≡_ _≡_ f →
	∀ (i : Fin n) → ∃[ j ] j ≤ i × i ≤ f j
	injective⇒existsPivot {n = suc n} {f = f} f-injective i
	with any? (λ j → j ≤? i ×-dec i ≤? f j)
	... | yes result = result
	... | no ¬result = contradiction (injective⇒≤ h-injective) ℕ.1+n≰n
	where
	fj<i : (j : Fin′ (suc i)) → f (inject! j) < i
	fj<i j with f (inject! j) <? i
	... | yes fj<i = fj<i
	... | no fj≮i = contradiction (_ , ℕ.s≤s⁻¹ (inject!-< j) , ℕ.≮⇒≥ fj≮i) ¬result
	h : Fin′ (suc i) → Fin′ i
	h j = lower (f (inject! j)) (fj<i j)
	h-injective : Injective _≡_ _≡_ h
	h-injective = inject!-injective ∘ f-injective ∘ lower-injective _ _
	injective⇒nonStrictlyContractive : ∀ {f : Fin n → Fin m} → Injective _≡_ _≡_ f →
	∀ i → ¬ (∀ j → j ≤ i → f j < i)
	injective⇒nonStrictlyContractive f-injective i j≤i⇒fj<i =
	let j , j≤i , i≤fj = injective⇒existsPivot f-injective i
	in contradiction (j≤i⇒fj<i j j≤i) (ℕ.≤⇒≯ i≤fj)

I argue as follows:

• injective⇒nonStrictlyContractive, which I leave in here for API faithfulness, probably doesn't even need to be in the PR, as it now arises an 'easy' consequence by contradiction from the much more interesting (positive!) statement injective⇒existsPivot
• the proof that you do offer of this latter has some very weird contortions/convolutions via all kinds of contradictions, when the function h, and the proof that it is Injective, at the heart of the main argument, actually becomes considerably simpler once it suffices to define it, towards the eventual contradiction, only within the scope of ¬result... whence the fj<i lemma becomes provable outright.

NB. f can now be implicitly quantified? (and: is!)

[jamesmckinna]

As on previous iterations: suggest deprecating/redefining lower₁ in terms of this new definition, to avoid redundant duplication?

UPDATED: oh, I see... it would involve importing Data.Nat.Properties in order to fix up the precondition, and that might be considered A Bad Thing...

[jamesmckinna]

Accordingly, we should perhaps instead consider (an issue about) refactoring to deprecate it, and rewrite (a lot of!?) code which uses it...

[jamesmckinna]

Suggested change

	with Fin.injective⇒existsPivot _ (inverseʳ⇒injective _ (Inverse.inverseʳ (toFin xs↭ys))) i
	with Fin.injective⇒existsPivot _ (inverseʳ⇒injective _ (Inverse.inverseʳ (onIndices xs↭ys))) i

???

[jamesmckinna]

Also, there's no need for with here: the pattern is irrefutable, and computable with a pattern-matching let, so...

[jamesmckinna]

Ditto.

Suggested change

	lookup ys (toFin xs↭ys ⟨$⟩ʳ k) ≈⟨ toFin-lookup xs↭ys k ⟨
	lookup ys (onIndices xs↭ys ⟨$⟩ʳ k) ≈⟨ onIndices-lookup xs↭ys k ⟨

[jamesmckinna]

Various nitpicks and bugfixes suggested, but otherwise: good to go!

[jamesmckinna]

Suggested change

	lower {suc _} {suc n} zero leq = zero
	lower {suc _} {suc n} (suc i) leq = suc (lower i (ℕ.s≤s⁻¹ leq))
	lower {n = suc _} zero leq = zero
	lower {n = suc _} (suc i) leq = suc (lower i (ℕ.s≤s⁻¹ leq))

I don't think there's any need to involve the m binding in the definition, and named telescopes are (typically) more robust in the face of modifications to variable declarations etc.

[jamesmckinna]

Ditto re: avoiding the m binding

Suggested change

	lower-injective {suc _} {suc n} zero zero eq = refl
	lower-injective {suc _} {suc n} (suc i) (suc j) eq =
	lower-injective {n = suc n} zero zero eq = refl
	lower-injective {n = suc n} (suc i) (suc j) eq =

[jamesmckinna]

What happened here?

[JacquesCarette]

As an entirely separate thing: 2+ ?

[JacquesCarette]

I have no comments beyond James'.

[JacquesCarette]

As an entirely separate thing: 2+ ?

[jamesmckinna]

Suggested change

	lower-injective : ∀ {m n} (i j : Fin m)
	lower-injective : ∀ (i j : Fin m)

m and n are already governed by the top-level variable declarations.

[jamesmckinna]

Sorry to go back on my original approval, but I think the new proof structure is... better!?

[jamesmckinna]

Voil`a:

Suggested change

	injective⇒nonStrictlyContractive : ∀ (f : Fin n → Fin m) → Injective _≡_ _≡_ f →
	∀ i → ¬ (∀ j → j ≤ i → f j < i)
	injective⇒nonStrictlyContractive f f-injective i j≤i⇒fj<i =
	ℕ.n≮n (toℕ i) (injective⇒≤ h-injective)
	where
	h : Fin′ (suc i) → Fin′ i
	h k = lower (f (inject! k)) (j≤i⇒fj<i _ (ℕ.s≤s⁻¹ (inject!-< k)))
	h-injective : Injective _≡_ _≡_ h
	h-injective = inject!-injective ∘ f-injective ∘ lower-injective _ _
	injective⇒existsPivot : ∀ (f : Fin n → Fin m) → Injective _≡_ _≡_ f →
	∀ (i : Fin n) → ∃ λ (j : Fin n) → j ≤ i × i ≤ f j
	injective⇒existsPivot {n = suc n} f f-injective i with any? (λ j → j ≤? i ×-dec i ≤? f j)
	... | yes result = result
	... | no ¬result = contradiction
	strictlyContractive
	(injective⇒nonStrictlyContractive f f-injective i)
	where
	strictlyContractive : ∀ j → j ≤ i → f j < i
	strictlyContractive j j≤i with i ≤? f j
	... | yes i≤fj = contradiction (j , j≤i , i≤fj) ¬result
	... | no i≰fj = ℕ.≰⇒> i≰fj
	injective⇒existsPivot : ∀ {f : Fin n → Fin m} → Injective _≡_ _≡_ f →
	∀ (i : Fin n) → ∃[ j ] j ≤ i × i ≤ f j
	injective⇒existsPivot {n = suc n} {f = f} f-injective i
	with any? (λ j → j ≤? i ×-dec i ≤? f j)
	... | yes result = result
	... | no ¬result = contradiction (injective⇒≤ h-injective) ℕ.1+n≰n
	where
	fj<i : (j : Fin′ (suc i)) → f (inject! j) < i
	fj<i j with f (inject! j) <? i
	... | yes fj<i = fj<i
	... | no fj≮i = contradiction (_ , ℕ.s≤s⁻¹ (inject!-< j) , ℕ.≮⇒≥ fj≮i) ¬result
	h : Fin′ (suc i) → Fin′ i
	h j = lower (f (inject! j)) (fj<i j)
	h-injective : Injective _≡_ _≡_ h
	h-injective = inject!-injective ∘ f-injective ∘ lower-injective _ _
	injective⇒nonStrictlyContractive : ∀ {f : Fin n → Fin m} → Injective _≡_ _≡_ f →
	∀ i → ¬ (∀ j → j ≤ i → f j < i)
	injective⇒nonStrictlyContractive f-injective i j≤i⇒fj<i =
	let j , j≤i , i≤fj = injective⇒existsPivot f-injective i
	in contradiction (j≤i⇒fj<i j j≤i) (ℕ.≤⇒≯ i≤fj)

I argue as follows:

• injective⇒nonStrictlyContractive, which I leave in here for API faithfulness, probably doesn't even need to be in the PR, as it now arises an 'easy' consequence by contradiction from the much more interesting (positive!) statement injective⇒existsPivot
• the proof that you do offer of this latter has some very weird contortions/convolutions via all kinds of contradictions, when the function h, and the proof that it is Injective, at the heart of the main argument, actually becomes considerably simpler once it suffices to define it, towards the eventual contradiction, only within the scope of ¬result... whence the fj<i lemma becomes provable outright.

NB. f can now be implicitly quantified? (and: is!)

[jamesmckinna]

Suggest leaving this out of the PR: as below, it's an easy corollary of injective⇒existsPivot after re-ordering.