"Bubble sort" induction

We implement the following induction principle Tuple.bubble_sort_induction on tuples with values in a linear order α.

Let f : Fin n → α and let P be a predicate on Fin n → α. Then we can show that f ∘ sort f satisfies P if f satisfies P, and whenever some g : Fin n → α satisfies P and g i > g j for some i < j, then g ∘ swap i j also satisfies P.

We deduce it from a stronger variant Tuple.bubble_sort_induction', which requires the assumption only for g that are permutations of f.

The latter is proved by well-founded induction via WellFounded.induction_bot' with respect to the lexicographic ordering on the finite set of all permutations of f.

theorem Tuple.bubble_sort_induction' {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} {P : (Fin n → α) → Prop} (hf : P f) (h : ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n), i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))) : P (f ∘ ⇑(Tuple.sort f))

Bubble sort induction: Prove that the sorted version of f has some property P if f satisfies P and P is preserved on permutations of f when swapping two antitone values.

theorem Tuple.bubble_sort_induction {n : ℕ} {α : Type u_1} [LinearOrder α] {f : Fin n → α} {P : (Fin n → α) → Prop} (hf : P f) (h : ∀ (g : Fin n → α) (i j : Fin n), i < j → g j < g i → P g → P (g ∘ ⇑(Equiv.swap i j))) : P (f ∘ ⇑(Tuple.sort f))

Bubble sort induction: Prove that the sorted version of f has some property P if f satisfies P and P is preserved when swapping two antitone values.