"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.

source

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.

source

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.