mathlib3 documentation

data.fin.tuple.bubble_sort_induction

"Bubble sort" induction #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 well_founded.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} [linear_order α] {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 satsifies P and P is preserved on permutations of f when swapping two antitone values.

theorem tuple.bubble_sort_induction {n : } {α : Type u_1} [linear_order α] {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 satsifies P and P is preserved when swapping two antitone values.