# "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`

.

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

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