# "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} [] {f : Fin nα} {P : (Fin nα)Prop} (hf : P f) (h : ∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n), i < j(f σ) j < (f σ) iP (f σ)P (f σ ())) :
P (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} [] {f : Fin nα} {P : (Fin nα)Prop} (hf : P f) (h : ∀ (g : Fin nα) (i j : Fin n), i < jg j < g iP gP (g ())) :
P (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.