Odd-even transposition routes

An n-round sorting network gives the alternating permutation route used for complete flags.

Lean Pool port of wewantmoore commit d59bd80ea93fabb9faf769e790ab47692645e022. The port adds a namespace and adapts proofs to the current Mathlib APIs and repository style.

def MooreBound.OddEvenSorting.pairPhase {α : Type u_1} [LinearOrder α] : List α → List α

Sort each disjoint consecutive pair of list entries.

Equations

• MooreBound.OddEvenSorting.pairPhase (a :: b :: xs) = min a b :: max a b :: MooreBound.OddEvenSorting.pairPhase xs
• MooreBound.OddEvenSorting.pairPhase x✝ = x✝

def MooreBound.OddEvenSorting.phase {α : Type u_1} [LinearOrder α] (shifted : Bool) (xs : List α) : List α

Apply a comparator layer, optionally leaving the first entry fixed.

Equations

• MooreBound.OddEvenSorting.phase shifted [] = if shifted = true then [] else MooreBound.OddEvenSorting.pairPhase []
• MooreBound.OddEvenSorting.phase shifted (x :: xs_2) = if shifted = true then x :: MooreBound.OddEvenSorting.pairPhase xs_2 else MooreBound.OddEvenSorting.pairPhase (x :: xs_2)

@[simp]

theorem MooreBound.OddEvenSorting.pairPhase_nil {α : Type u_1} [LinearOrder α] : pairPhase [] = []

@[simp]

theorem MooreBound.OddEvenSorting.pairPhase_singleton {α : Type u_1} [LinearOrder α] (a : α) : pairPhase [a] = [a]

@[simp]

theorem MooreBound.OddEvenSorting.pairPhase_cons_cons {α : Type u_1} [LinearOrder α] (a b : α) (xs : List α) : pairPhase (a :: b :: xs) = min a b :: max a b :: pairPhase xs

@[simp]

theorem MooreBound.OddEvenSorting.phase_false {α : Type u_1} [LinearOrder α] (xs : List α) : phase false xs = pairPhase xs

@[simp]

theorem MooreBound.OddEvenSorting.phase_true_nil {α : Type u_1} [LinearOrder α] : phase true [] = []

@[simp]

theorem MooreBound.OddEvenSorting.phase_true_cons {α : Type u_1} [LinearOrder α] (a : α) (xs : List α) : phase true (a :: xs) = a :: pairPhase xs

@[simp]

theorem MooreBound.OddEvenSorting.length_pairPhase {α : Type u_1} [LinearOrder α] (xs : List α) : (pairPhase xs).length = xs.length

@[simp]

theorem MooreBound.OddEvenSorting.length_phase {α : Type u_1} [LinearOrder α] (p : Bool) (xs : List α) : (phase p xs).length = xs.length

def MooreBound.OddEvenSorting.pref (xs : List Bool) (i : ℕ) : ℤ

The integer count of true bits among the first i entries.

Equations

• MooreBound.OddEvenSorting.pref xs i = ↑(List.count true (List.take i xs))

def MooreBound.OddEvenSorting.bitInt (b : Bool) : ℤ

Interpret a Boolean bit as zero or one in the integers.

Equations

• MooreBound.OddEvenSorting.bitInt b = if b = true then 1 else 0

@[simp]

theorem MooreBound.OddEvenSorting.pref_nil (i : ℕ) : pref [] i = 0

@[simp]

theorem MooreBound.OddEvenSorting.pref_zero (xs : List Bool) : pref xs 0 = 0

@[simp]

theorem MooreBound.OddEvenSorting.pref_cons_succ (a : Bool) (xs : List Bool) (i : ℕ) : pref (a :: xs) (i + 1) = bitInt a + pref xs i

theorem MooreBound.OddEvenSorting.pref_cons_cons_add (a b : Bool) (xs : List Bool) (i : ℕ) : pref (a :: b :: xs) (i + 2) = bitInt a + bitInt b + pref xs i

theorem MooreBound.OddEvenSorting.bitInt_min_add_max (a b : Bool) : bitInt (min a b) + bitInt (max a b) = bitInt a + bitInt b

theorem MooreBound.OddEvenSorting.pref_pairPhase_even (xs : List Bool) (k : ℕ) : pref (pairPhase xs) (2 * k) = pref xs (2 * k)

theorem MooreBound.OddEvenSorting.pref_pairPhase_odd (xs : List Bool) (k : ℕ) (hk : 2 * k + 1 < xs.length) : pref (pairPhase xs) (2 * k + 1) = max (pref xs (2 * k)) (pref xs (2 * k + 2) - 1)

theorem MooreBound.OddEvenSorting.pref_phase_false_even (xs : List Bool) (k : ℕ) : pref (phase false xs) (2 * k) = pref xs (2 * k)

theorem MooreBound.OddEvenSorting.pref_phase_false_odd (xs : List Bool) (k : ℕ) (hk : 2 * k + 1 < xs.length) : pref (phase false xs) (2 * k + 1) = max (pref xs (2 * k)) (pref xs (2 * k + 2) - 1)

theorem MooreBound.OddEvenSorting.pref_phase_true_odd (xs : List Bool) (k : ℕ) : pref (phase true xs) (2 * k + 1) = pref xs (2 * k + 1)

theorem MooreBound.OddEvenSorting.pref_phase_true_even (xs : List Bool) (k : ℕ) (hk : 2 * k + 2 < xs.length) : pref (phase true xs) (2 * k + 2) = max (pref xs (2 * k + 1)) (pref xs (2 * k + 3) - 1)

def MooreBound.OddEvenSorting.active (q i : ℕ) : Bool

Whether a prefix boundary participates in comparator round q.

Equations

• MooreBound.OddEvenSorting.active q i = decide (i % 2 = (q + 1) % 2)

def MooreBound.OddEvenSorting.phaseN {α : Type u_1} [LinearOrder α] (q : ℕ) (xs : List α) : List α

The comparator layer whose offset alternates with the round number.

Equations

• MooreBound.OddEvenSorting.phaseN q xs = MooreBound.OddEvenSorting.phase (decide (q % 2 = 1)) xs

theorem MooreBound.OddEvenSorting.pref_phaseN (q : ℕ) (xs : List Bool) (i : ℕ) (hi0 : 0 < i) (hin : i < xs.length) : pref (phaseN q xs) i = if active q i = true then max (pref xs (i - 1)) (pref xs (i + 1) - 1) else pref xs i

def MooreBound.OddEvenSorting.countTrue (xs : List Bool) : ℕ

The total number of true bits in a Boolean list.

Equations

• MooreBound.OddEvenSorting.countTrue xs = List.count true xs

@[simp]

theorem MooreBound.OddEvenSorting.countTrue_pairPhase (xs : List Bool) : countTrue (pairPhase xs) = countTrue xs

@[simp]

theorem MooreBound.OddEvenSorting.countTrue_phase (p : Bool) (xs : List Bool) : countTrue (phase p xs) = countTrue xs

@[simp]

theorem MooreBound.OddEvenSorting.countTrue_phaseN (q : ℕ) (xs : List Bool) : countTrue (phaseN q xs) = countTrue xs

def MooreBound.OddEvenSorting.evolve {α : Type u_1} [LinearOrder α] (q : ℕ) (xs : List α) : ℕ → List α

Iterate alternating comparator layers starting with round q.

Equations

• MooreBound.OddEvenSorting.evolve q xs 0 = xs
• MooreBound.OddEvenSorting.evolve q xs t.succ = MooreBound.OddEvenSorting.phaseN (q + t) (MooreBound.OddEvenSorting.evolve q xs t)

@[simp]

theorem MooreBound.OddEvenSorting.evolve_zero {α : Type u_1} [LinearOrder α] (q : ℕ) (xs : List α) : evolve q xs 0 = xs

@[simp]

theorem MooreBound.OddEvenSorting.evolve_succ {α : Type u_1} [LinearOrder α] (q : ℕ) (xs : List α) (t : ℕ) : evolve q xs (t + 1) = phaseN (q + t) (evolve q xs t)

@[simp]

theorem MooreBound.OddEvenSorting.length_phaseN {α : Type u_1} [LinearOrder α] (q : ℕ) (xs : List α) : (phaseN q xs).length = xs.length

@[simp]

theorem MooreBound.OddEvenSorting.length_evolve {α : Type u_1} [LinearOrder α] (q : ℕ) (xs : List α) (t : ℕ) : (evolve q xs t).length = xs.length

@[simp]

theorem MooreBound.OddEvenSorting.countTrue_evolve (q : ℕ) (xs : List Bool) (t : ℕ) : countTrue (evolve q xs t) = countTrue xs

def MooreBound.OddEvenSorting.low (z i : ℕ) : ℤ

Prefix count in the sorted Boolean word with z zeroes.

Equations

• MooreBound.OddEvenSorting.low z i = max 0 (↑i - ↑z)

def MooreBound.OddEvenSorting.potential (z i : ℕ) (h : ℤ) : ℤ

The potential used to rule out a bad prefix surviving all layers.

Equations

• MooreBound.OddEvenSorting.potential z i h = if i ≤ z then ↑i - 2 * h else 2 * ↑z - ↑i - 2 * h

def MooreBound.OddEvenSorting.Bad (z : ℕ) (xs : List Bool) (i : ℕ) (h : ℤ) : Prop

A positive excess of the prefix count above its sorted lower bound.

Equations

• MooreBound.OddEvenSorting.Bad z xs i h = (1 ≤ h ∧ MooreBound.OddEvenSorting.low z i + h ≤ MooreBound.OddEvenSorting.pref xs i)

theorem MooreBound.OddEvenSorting.pref_le_index (xs : List Bool) (i : ℕ) : pref xs i ≤ ↑i

theorem MooreBound.OddEvenSorting.pref_le_total (xs : List Bool) (i : ℕ) : pref xs i ≤ ↑(countTrue xs)

theorem MooreBound.OddEvenSorting.pref_at_length (xs : List Bool) : pref xs xs.length = ↑(countTrue xs)

theorem MooreBound.OddEvenSorting.pref_lower (xs : List Bool) (z r i : ℕ) (hlen : xs.length = r + z) (hcount : countTrue xs = r) (hi : i ≤ xs.length) : low z i ≤ pref xs i

theorem MooreBound.OddEvenSorting.potential_upper (z i : ℕ) (h : ℤ) (hh : 1 ≤ h) : potential z i h ≤ ↑z - 2

theorem MooreBound.OddEvenSorting.potential_lower_of_initial_bad (xs : List Bool) (z r i : ℕ) (h : ℤ) (hcount : countTrue xs = r) (hb : Bad z xs i h) : -↑r ≤ potential z i h

theorem MooreBound.OddEvenSorting.potential_left (z i : ℕ) (h : ℤ) (hi : 0 < i) : potential z (i - 1) (h + low z i - low z (i - 1)) = potential z i h - 1

theorem MooreBound.OddEvenSorting.potential_right (z i : ℕ) (h : ℤ) : potential z (i + 1) (h + 1 + low z i - low z (i + 1)) = potential z i h - 1

theorem MooreBound.OddEvenSorting.not_bad_zero (z : ℕ) (xs : List Bool) (h : ℤ) : ¬Bad z xs 0 h

theorem MooreBound.OddEvenSorting.not_bad_length (z r : ℕ) (xs : List Bool) (h : ℤ) (hlen : xs.length = r + z) (hcount : countTrue xs = r) : ¬Bad z xs xs.length h

theorem MooreBound.OddEvenSorting.bad_predecessor (z r q i : ℕ) (xs : List Bool) (h : ℤ) (hlen : xs.length = r + z) (hcount : countTrue xs = r) (hi0 : 0 < i) (hin : i < xs.length) (hact : active q i = true) (hb : Bad z (phaseN q xs) i h) : ∃ (j : ℕ) (h' : ℤ), (j = i - 1 ∨ j = i + 1) ∧ 0 < j ∧ j < xs.length ∧ Bad z xs j h' ∧ potential z j h' = potential z i h - 1

theorem MooreBound.OddEvenSorting.active_previous_neighbor (q i j : ℕ) (hq : 0 < q) (hi0 : 0 < i) (hi : active q i = true) (hj : j = i - 1 ∨ j = i + 1) : active (q - 1) j = true

theorem MooreBound.OddEvenSorting.active_previous_same (q i : ℕ) (hq : 0 < q) (hi : active q i = false) : active (q - 1) i = true

theorem MooreBound.OddEvenSorting.trace_bad_active (z r q : ℕ) (xs : List Bool) (t i : ℕ) (h : ℤ) (hlen : xs.length = r + z) (hcount : countTrue xs = r) (ht : 0 < t) (hact : active (q + t - 1) i = true) (hb : Bad z (evolve q xs t) i h) : ∃ (j : ℕ) (h' : ℤ), 0 < j ∧ j < xs.length ∧ Bad z xs j h' ∧ potential z j h' = potential z i h - ↑t

theorem MooreBound.OddEvenSorting.pref_evolve_full (z r q : ℕ) (xs : List Bool) (hlen : xs.length = r + z) (hcount : countTrue xs = r) (i : ℕ) (hi : i ≤ xs.length) : pref (evolve q xs (r + z)) i = low z i

def MooreBound.OddEvenSorting.threshold {α : Type u_1} [LinearOrder α] (a x : α) : Bool

The monotone Boolean threshold used in the zero-one sorting argument.

Equations

• MooreBound.OddEvenSorting.threshold a x = decide (a ≤ x)

theorem MooreBound.OddEvenSorting.threshold_min {α : Type u_1} [LinearOrder α] (a x y : α) : threshold a (min x y) = min (threshold a x) (threshold a y)

theorem MooreBound.OddEvenSorting.threshold_max {α : Type u_1} [LinearOrder α] (a x y : α) : threshold a (max x y) = max (threshold a x) (threshold a y)

theorem MooreBound.OddEvenSorting.map_threshold_pairPhase {α : Type u_1} [LinearOrder α] (a : α) (xs : List α) : List.map (threshold a) (pairPhase xs) = pairPhase (List.map (threshold a) xs)

theorem MooreBound.OddEvenSorting.map_threshold_phase {α : Type u_1} [LinearOrder α] (a : α) (p : Bool) (xs : List α) : List.map (threshold a) (phase p xs) = phase p (List.map (threshold a) xs)

theorem MooreBound.OddEvenSorting.map_threshold_phaseN {α : Type u_1} [LinearOrder α] (a : α) (q : ℕ) (xs : List α) : List.map (threshold a) (phaseN q xs) = phaseN q (List.map (threshold a) xs)

theorem MooreBound.OddEvenSorting.map_threshold_evolve {α : Type u_1} [LinearOrder α] (a : α) (q t : ℕ) (xs : List α) : List.map (threshold a) (evolve q xs t) = evolve q (List.map (threshold a) xs) t

theorem MooreBound.OddEvenSorting.pref_succ (xs : List Bool) (i : ℕ) (hi : i < xs.length) : pref xs (i + 1) = pref xs i + bitInt xs[i]

theorem MooreBound.OddEvenSorting.bool_getElem_of_pref_full (z r q : ℕ) (xs : List Bool) (hlen : xs.length = r + z) (hcount : countTrue xs = r) (i : ℕ) (hi : i < xs.length) : (evolve q xs (r + z))[i] = decide (z ≤ i)

theorem MooreBound.OddEvenSorting.countTrue_map_threshold {α : Type u_1} [LinearOrder α] (a : α) (xs : List α) : countTrue (List.map (threshold a) xs) = (List.filter (threshold a) xs).length

theorem MooreBound.OddEvenSorting.countTrue_map_threshold_finRange {n : ℕ} (a : Fin n) : countTrue (List.map (threshold a) (List.finRange n)) = n - ↑a

theorem MooreBound.OddEvenSorting.countTrue_map_threshold_of_perm_finRange {n : ℕ} (a : Fin n) (xs : List (Fin n)) (hp : xs.Perm (List.finRange n)) : countTrue (List.map (threshold a) xs) = n - ↑a

theorem MooreBound.OddEvenSorting.threshold_evolve_perm_finRange {n : ℕ} (xs : List (Fin n)) (hp : xs.Perm (List.finRange n)) (q : ℕ) (a : Fin n) (i : ℕ) (hi : i < n) : threshold a (evolve q xs n)[i] = decide (↑a ≤ i)

theorem MooreBound.OddEvenSorting.evolve_perm_finRange_eq {n : ℕ} (xs : List (Fin n)) (hp : xs.Perm (List.finRange n)) (q : ℕ) : evolve q xs n = List.finRange n

theorem MooreBound.OddEvenSorting.pair_minmax_perm {α : Type u_1} [LinearOrder α] (a b : α) (xs : List α) : (min a b :: max a b :: xs).Perm (a :: b :: xs)

@[simp]

theorem MooreBound.OddEvenSorting.pairPhase_perm {α : Type u_1} [LinearOrder α] (xs : List α) : (pairPhase xs).Perm xs

@[simp]

theorem MooreBound.OddEvenSorting.phase_perm {α : Type u_1} [LinearOrder α] (p : Bool) (xs : List α) : (phase p xs).Perm xs

@[simp]

theorem MooreBound.OddEvenSorting.phaseN_perm {α : Type u_1} [LinearOrder α] (q : ℕ) (xs : List α) : (phaseN q xs).Perm xs

@[simp]

theorem MooreBound.OddEvenSorting.evolve_perm {α : Type u_1} [LinearOrder α] (q t : ℕ) (xs : List α) : (evolve q xs t).Perm xs

theorem MooreBound.OddEvenSorting.take_pairPhase_even_perm {α : Type u_1} [LinearOrder α] (xs : List α) (k : ℕ) : (List.take (2 * k) (pairPhase xs)).Perm (List.take (2 * k) xs)

theorem MooreBound.OddEvenSorting.take_phase_false_even_perm {α : Type u_1} [LinearOrder α] (xs : List α) (k : ℕ) : (List.take (2 * k) (phase false xs)).Perm (List.take (2 * k) xs)

theorem MooreBound.OddEvenSorting.take_phase_true_odd_perm {α : Type u_1} [LinearOrder α] (xs : List α) (k : ℕ) : (List.take (2 * k + 1) (phase true xs)).Perm (List.take (2 * k + 1) xs)

theorem MooreBound.OddEvenSorting.take_phaseN_perm_of_inactive {α : Type u_1} [LinearOrder α] (q : ℕ) (xs : List α) (i : ℕ) (hact : active q i = false) : (List.take i (phaseN q xs)).Perm (List.take i xs)

noncomputable def MooreBound.OddEvenSorting.permOfList {n : ℕ} (l : List (Fin n)) (hp : l.Perm (List.finRange n)) : Equiv.Perm (Fin n)

The permutation whose one-line notation is l.

Equations

• MooreBound.OddEvenSorting.permOfList l hp = (finCongr ⋯).trans (List.Nodup.getEquivOfForallMemList l ⋯ ⋯)

theorem MooreBound.OddEvenSorting.permOfList_apply {n : ℕ} (l : List (Fin n)) (hp : l.Perm (List.finRange n)) (i : Fin n) : (permOfList l hp) i = l[↑i]

theorem MooreBound.OddEvenSorting.permOfList_map_finRange {n : ℕ} (σ : Equiv.Perm (Fin n)) : permOfList (List.map (⇑σ) (List.finRange n)) ⋯ = σ

theorem MooreBound.OddEvenSorting.permOfList_finRange {n : ℕ} : permOfList (List.finRange n) ⋯ = Equiv.refl (Fin n)

def MooreBound.OddEvenSorting.PrefixSet2 {n : ℕ} (σ : Equiv.Perm (Fin n)) (i : Fin (n + 1)) : Set (Fin n)

The image of an initial rank segment under a permutation.

Equations

• MooreBound.OddEvenSorting.PrefixSet2 σ i = ⇑σ '' {j : Fin n | j.castSucc < i}

def MooreBound.OddEvenSorting.OrderingStep2 {n : ℕ} (s : Fin n) (σ τ : Equiv.Perm (Fin n)) : Prop

A layer preserves prefix sets at every inactive rank.

Equations

• MooreBound.OddEvenSorting.OrderingStep2 s σ τ = ∀ (i : Fin (n + 1)), ↑i % 2 ≠ (↑s + 1) % 2 → MooreBound.OddEvenSorting.PrefixSet2 σ i = MooreBound.OddEvenSorting.PrefixSet2 τ i

theorem MooreBound.OddEvenSorting.mem_PrefixSet2_permOfList_iff {n : ℕ} (l : List (Fin n)) (hp : l.Perm (List.finRange n)) (i : Fin (n + 1)) (x : Fin n) : x ∈ PrefixSet2 (permOfList l hp) i ↔ x ∈ List.take (↑i) l

theorem MooreBound.OddEvenSorting.mem_PrefixSet2_trans_permOfList_iff {n : ℕ} (l : List (Fin n)) (hp : l.Perm (List.finRange n)) (π : Equiv.Perm (Fin n)) (i : Fin (n + 1)) (x : Fin n) : x ∈ PrefixSet2 (Equiv.trans (permOfList l hp) π) i ↔ (Equiv.symm π) x ∈ List.take (↑i) l

theorem MooreBound.OddEvenSorting.prefixSet2_trans_eq_of_take_perm {n : ℕ} (l m : List (Fin n)) (hl : l.Perm (List.finRange n)) (hm : m.Perm (List.finRange n)) (π : Equiv.Perm (Fin n)) (i : Fin (n + 1)) (htake : (List.take (↑i) l).Perm (List.take (↑i) m)) : PrefixSet2 (Equiv.trans (permOfList l hl) π) i = PrefixSet2 (Equiv.trans (permOfList m hm) π) i

theorem MooreBound.OddEvenSorting.oddEvenRoute2 {n : ℕ} (π : Equiv.Perm (Fin n)) : ∃ (route : Fin (n + 1) → Equiv.Perm (Fin n)), route 0 = Equiv.refl (Fin n) ∧ route (Fin.last n) = π ∧ ∀ (s : Fin n), OrderingStep2 s (route s.castSucc) (route s.succ)

Odd--even transposition routing, in the exact combinatorial form needed for Lemma 2.1.