List lemmas

theorem PhysLean.List.insertionSortMin_lt_length_succ {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) : ↑(insertionSortMinPos r i l) < (insertionSortDropMinPos r i l).length.succ

def PhysLean.List.insertionSortMinPosFin {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) : Fin (insertionSortDropMinPos r i l).length.succ

Given a list i :: l the left-most minimal position a of i :: l wrt r as an element of Fin (insertionSortDropMinPos r i l).length.succ.

Equations

• PhysLean.List.insertionSortMinPosFin r i l = ⟨↑(PhysLean.List.insertionSortMinPos r i l), ⋯⟩

theorem PhysLean.List.insertionSortMin_lt_mem_insertionSortDropMinPos {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a : α) (l : List α) (i : Fin (insertionSortDropMinPos r a l).length) : r (insertionSortMin r a l) (insertionSortDropMinPos r a l)[i]

theorem PhysLean.List.insertionSortMinPos_insertionSortEquiv {α : Type} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : (insertionSortEquiv r (a :: l)) (insertionSortMinPos r a l) = ⟨0, ⋯⟩

theorem PhysLean.List.insertionSortEquiv_gt_zero_of_ne_insertionSortMinPos {α : Type} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) (k : Fin (a :: l).length) (hk : k ≠ insertionSortMinPos r a l) : ⟨0, ⋯⟩ < (insertionSortEquiv r (a :: l)) k

theorem PhysLean.List.insertionSortMin_lt_mem_insertionSortDropMinPos_of_lt {α : Type} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) (i : Fin (insertionSortDropMinPos r a l).length) (h : (insertionSortMinPosFin r a l).succAbove i < insertionSortMinPosFin r a l) : ¬r (insertionSortDropMinPos r a l)[i] (insertionSortMin r a l)

theorem PhysLean.List.insertionSort_insertionSort {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l1 : List α) : List.insertionSort r (List.insertionSort r l1) = List.insertionSort r l1

theorem PhysLean.List.orderedInsert_commute {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a b : α) (hr : ¬r a b) (l : List α) : List.orderedInsert r a (List.orderedInsert r b l) = List.orderedInsert r b (List.orderedInsert r a l)

theorem PhysLean.List.insertionSort_orderedInsert_append {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a : α) (l1 l2 : List α) : List.insertionSort r (List.orderedInsert r a l1 ++ l2) = List.insertionSort r (a :: l1 ++ l2)

theorem PhysLean.List.insertionSort_insertionSort_append {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l1 l2 : List α) : List.insertionSort r (List.insertionSort r l1 ++ l2) = List.insertionSort r (l1 ++ l2)

theorem PhysLean.List.insertionSort_append_insertionSort_append {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (l1 l2 l3 : List α) : List.insertionSort r (l1 ++ List.insertionSort r l2 ++ l3) = List.insertionSort r (l1 ++ l2 ++ l3)

@[simp]

theorem PhysLean.List.orderedInsert_length {α : Type} (r : α → α → Prop) [DecidableRel r] (a : α) (l : List α) : (List.orderedInsert r a l).length = (a :: l).length

theorem PhysLean.List.takeWhile_orderedInsert {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a b : α) (hr : ¬r a b) (l : List α) : (List.takeWhile (fun (c : α) => !decide (r a c)) (List.orderedInsert r b l)).length = (List.takeWhile (fun (c : α) => !decide (r a c)) l).length + 1

theorem PhysLean.List.takeWhile_orderedInsert' {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a b : α) (hr : ¬r a b) (l : List α) : (List.takeWhile (fun (c : α) => !decide (r b c)) (List.orderedInsert r a l)).length = (List.takeWhile (fun (c : α) => !decide (r b c)) l).length

theorem PhysLean.List.insertionSortEquiv_commute {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a b : α) (hr : ¬r a b) (n : ℕ) (l : List α) (hn : n + 2 < (a :: b :: l).length) : (insertionSortEquiv r (a :: b :: l)) ⟨n + 2, hn⟩ = (finCongr ⋯) ((insertionSortEquiv r (b :: a :: l)) ⟨n + 2, hn⟩)

theorem PhysLean.List.insertionSortEquiv_orderedInsert_append {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a a2 : α) (l1 l2 : List α) : (insertionSortEquiv r (List.orderedInsert r a l1 ++ a2 :: l2)) ⟨l1.length + 1, ⋯⟩ = (finCongr ⋯) ((insertionSortEquiv r (a :: l1 ++ a2 :: l2)) ⟨l1.length + 1, ⋯⟩)

theorem PhysLean.List.insertionSortEquiv_insertionSort_append {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a : α) (l1 l2 : List α) : (insertionSortEquiv r (List.insertionSort r l1 ++ a :: l2)) ⟨l1.length, ⋯⟩ = (finCongr ⋯) ((insertionSortEquiv r (l1 ++ a :: l2)) ⟨l1.length, ⋯⟩)

Insertion sort with equal fields

theorem PhysLean.List.orderedInsert_filter_of_pos {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] (a : α) (p : α → Prop) [DecidablePred p] (h : p a) (l : List α) (hl : List.Sorted r l) : List.filter (fun (b : α) => decide (p b)) (List.orderedInsert r a l) = List.orderedInsert r a (List.filter (fun (b : α) => decide (p b)) l)

theorem PhysLean.List.orderedInsert_filter_of_neg {α : Type} (r : α → α → Prop) [DecidableRel r] (a : α) (p : α → Prop) [DecidablePred p] (h : ¬p a) (l : List α) : List.filter (fun (b : α) => decide (p b)) (List.orderedInsert r a l) = List.filter (fun (b : α) => decide (p b)) l

theorem PhysLean.List.insertionSort_filter {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (p : α → Prop) [DecidablePred p] (l : List α) : List.insertionSort r (List.filter (fun (b : α) => decide (p b)) l) = List.filter (fun (b : α) => decide (p b)) (List.insertionSort r l)

theorem PhysLean.List.takeWhile_sorted_eq_filter {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] (a : α) (l : List α) (hl : List.Sorted r l) : List.takeWhile (fun (c : α) => decide ¬r a c) l = List.filter (fun (c : α) => decide ¬r a c) l

theorem PhysLean.List.dropWhile_sorted_eq_filter {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] (a : α) (l : List α) (hl : List.Sorted r l) : List.dropWhile (fun (c : α) => decide ¬r a c) l = List.filter (fun (c : α) => decide (r a c)) l

theorem PhysLean.List.dropWhile_sorted_eq_filter_filter {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] (a : α) (l : List α) (hl : List.Sorted r l) : List.filter (fun (c : α) => decide (r a c)) l = List.filter (fun (c : α) => decide (r a c ∧ r c a)) l ++ List.filter (fun (c : α) => decide (r a c ∧ ¬r c a)) l

theorem PhysLean.List.filter_rel_eq_insertionSort {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a : α) (l : List α) : List.filter (fun (c : α) => decide (r a c ∧ r c a)) (List.insertionSort r l) = List.filter (fun (c : α) => decide (r a c ∧ r c a)) l

theorem PhysLean.List.insertionSort_of_eq_list {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a : α) (l1 l l2 : List α) (h : ∀ b ∈ l, r a b ∧ r b a) : List.insertionSort r (l1 ++ l ++ l2) = List.takeWhile (fun (c : α) => decide ¬r a c) (List.insertionSort r (l1 ++ l2)) ++ List.filter (fun (c : α) => decide (r a c ∧ r c a)) l1 ++ l ++ List.filter (fun (c : α) => decide (r a c ∧ r c a)) l2 ++ List.filter (fun (c : α) => decide (r a c ∧ ¬r c a)) (List.insertionSort r (l1 ++ l2))

theorem PhysLean.List.insertionSort_of_takeWhile_filter {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (a : α) (l1 l2 : List α) : List.insertionSort r (l1 ++ l2) = List.takeWhile (fun (c : α) => decide ¬r a c) (List.insertionSort r (l1 ++ l2)) ++ List.filter (fun (c : α) => decide (r a c ∧ r c a)) l1 ++ List.filter (fun (c : α) => decide (r a c ∧ r c a)) l2 ++ List.filter (fun (c : α) => decide (r a c ∧ ¬r c a)) (List.insertionSort r (l1 ++ l2))