Tuple.bubble_sort_induction'
theorem Tuple.bubble_sort_induction' :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {P : (Fin n → α) → Prop},
P f →
(∀ (σ : 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))
This theorem, called "Bubble sort induction", states that for a sequence `f` from `Fin n` to some type `α` ordered by a linear order, and a property `P` that is a predicate on such sequences, if `f` satisfies `P` and `P` is preserved under permutations of `f` that swap two values in `f` that are in reverse order, then the sorted version of `f` also satisfies `P`. In more concrete terms, this theorem confirms that if a property holds for a sequence and remains true when two out-of-order elements are swapped, then this property holds for the sequence after it has been sorted using bubble sort.
More concisely: If a sequence ordered by a linear order and a property on the sequence are invariant under swapping adjacent out-of-order elements during bubble sort, then the sorted sequence satisfies the property.
|
Tuple.bubble_sort_induction
theorem Tuple.bubble_sort_induction :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {P : (Fin n → α) → Prop},
P f →
(∀ (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))
This theorem, termed as "Bubble Sort Induction", states that if a function `f` from `Fin n` to some type `α` satisfies a certain property `P`, and this property `P` is preserved when two values of `f` that are in reverse order are swapped, then the sorted version of `f` (obtained using an ordering defined by `f`) also satisfies the property `P`. Here, `Fin n` represents the finite set of natural numbers from 0 to `n-1` and `α` is a type equipped with a linear order. This theorem essentially provides an inductive principle for proving properties about the bubble sort algorithm.
More concisely: If `f : Fin n → α` satisfies property `P` and swapping `f(i)` and `f(i+1)` when `i < n-1` preserves `P`, then the sorted `f` satisfies property `P`.
|