bubble_sort_induction' — Mathlib

English

Bubble sort induction: if a property P holds for a sequence f: Fin n → α and is preserved under swapping adjacent elements in permutations, then P holds for the sorted version of f.

Русский

Индукция пузырьковой сортировки: если свойство P выполняется для последовательности f и сохраняется при обмене соседних элементов в перестановках, то верно и для отсортированной версии f.

LaTeX

$$$\\text{bubble_sort_induction'}\\; : \\; P f \\rightarrow \\Big(\\forall (\\sigma : Perm(\\mathrm{Fin} n)) (i,j), i

Lean4

/-- *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 bubble_sort_induction' {n : ℕ} {α : Type*} [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 ∘ sort f) :=
  by
  letI := @Preorder.lift _ (Lex (Fin n → α)) _ fun σ : Equiv.Perm (Fin n) => toLex (f ∘ σ)
  refine
    @WellFounded.induction_bot' _ _ _ (IsWellFounded.wf : WellFounded (· < ·)) (Equiv.refl _) (sort f) P
      (fun σ => f ∘ σ) (fun σ hσ hfσ => ?_) hf
  obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ
  exact ⟨σ * Equiv.swap i j, Pi.lex_desc hij₁.le hij₂, h σ i j hij₁ hij₂ hfσ⟩

Похожие утверждения