List lemmas

theorem PhysLean.List.takeWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] (l : List I) (i : ℕ) (hi : ∀ (i j : Fin l.length), i < j → P (l.get j) → P (l.get i)) : List.takeWhile (fun (b : I) => decide (P b)) (l.eraseIdx i) = (List.takeWhile (fun (b : I) => decide (P b)) l).eraseIdx i

theorem PhysLean.List.dropWile_eraseIdx {I : Type} (P : I → Prop) [DecidablePred P] (l : List I) (i : ℕ) (hi : ∀ (i j : Fin l.length), i < j → P (l.get j) → P (l.get i)) : List.dropWhile (fun (b : I) => decide (P b)) (l.eraseIdx i) = if (List.takeWhile (fun (b : I) => decide (P b)) l).length ≤ i then (List.dropWhile (fun (b : I) => decide (P b)) l).eraseIdx (i - (List.takeWhile (fun (b : I) => decide (P b)) l).length) else List.dropWhile (fun (b : I) => decide (P b)) l

theorem PhysLean.List.insertionSort_length {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (l : List I) : (List.insertionSort le1 l).length = l.length

def PhysLean.List.orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : Fin (List.orderedInsert le1 r0 r).length

The position r0 ends up in r on adding it via List.orderedInsert _ r0 r.

Equations

• PhysLean.List.orderedInsertPos le1 r r0 = ⟨(List.takeWhile (fun (b : I) => decide ¬le1 r0 b) r).length, ⋯⟩

theorem PhysLean.List.orderedInsertPos_lt_length {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : ↑(orderedInsertPos le1 r r0) < (r0 :: r).length

@[simp]

theorem PhysLean.List.orderedInsert_get_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.orderedInsert le1 r0 r)[↑(orderedInsertPos le1 r r0)] = r0

@[simp]

theorem PhysLean.List.orderedInsert_eraseIdx_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.orderedInsert le1 r0 r).eraseIdx ↑(orderedInsertPos le1 r r0) = r

theorem PhysLean.List.orderedInsertPos_cons {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 r1 : I) : ↑(orderedInsertPos le1 (r1 :: r) r0) = ↑(if le1 r0 r1 then ⟨0, ⋯⟩ else (orderedInsertPos le1 r r0).succ)

theorem PhysLean.List.orderedInsertPos_sigma {I : Type} {f : I → Type} (le1 : I → I → Prop) [DecidableRel le1] (l : List ((i : I) × f i)) (k : I) (a : f k) : ↑(orderedInsertPos (fun (i j : (i : I) × f i) => le1 i.fst j.fst) l ⟨k, a⟩) = ↑(orderedInsertPos le1 (List.map (fun (i : (i : I) × f i) => i.fst) l) k)

theorem PhysLean.List.orderedInsert_get_lt {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (i : ℕ) (hi : i < ↑(orderedInsertPos le1 r r0)) : (List.orderedInsert le1 r0 r)[i] = r.get ⟨i, ⋯⟩

theorem PhysLean.List.orderedInsertPos_take_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r) = List.takeWhile (fun (b : I) => decide ¬le1 r0 b) r

theorem PhysLean.List.orderedInsertPos_take_eq_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : List.take (↑(orderedInsertPos le1 r r0)) r = List.take (↑(orderedInsertPos le1 r r0)) (List.orderedInsert le1 r0 r)

theorem PhysLean.List.orderedInsertPos_drop_eq_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : List.drop (↑(orderedInsertPos le1 r r0)) r = List.drop (↑(orderedInsertPos le1 r r0).succ) (List.orderedInsert le1 r0 r)

theorem PhysLean.List.orderedInsertPos_take {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : List.take (↑(orderedInsertPos le1 r r0)) r = List.takeWhile (fun (b : I) => decide ¬le1 r0 b) r

theorem PhysLean.List.orderedInsertPos_drop {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : List.drop (↑(orderedInsertPos le1 r r0)) r = List.dropWhile (fun (b : I) => decide ¬le1 r0 b) r

theorem PhysLean.List.orderedInsertPos_succ_take_orderedInsert {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : List.take (↑(orderedInsertPos le1 r r0).succ) (List.orderedInsert le1 r0 r) = List.takeWhile (fun (b : I) => decide ¬le1 r0 b) r ++ [r0]

theorem PhysLean.List.lt_orderedInsertPos_rel {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r0 : I) (r : List I) (n : Fin r.length) (hn : ↑n < ↑(orderedInsertPos le1 r r0)) : ¬le1 r0 (r.get n)

theorem PhysLean.List.lt_orderedInsertPos_rel_fin {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r0 : I) (r : List I) (n : Fin (List.orderedInsert le1 r0 r).length) (hn : n < orderedInsertPos le1 r r0) : ¬le1 r0 ((List.orderedInsert le1 r0 r).get n)

theorem PhysLean.List.gt_orderedInsertPos_rel {I : Type} (le1 : I → I → Prop) [DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) (hs : List.Sorted le1 r) (n : Fin r.length) (hn : ¬↑n < ↑(orderedInsertPos le1 r r0)) : le1 r0 (r.get n)

theorem PhysLean.List.orderedInsert_eraseIdx_lt_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (i : ℕ) (hi : i < ↑(orderedInsertPos le1 r r0)) (hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) : (List.orderedInsert le1 r0 r).eraseIdx i = List.orderedInsert le1 r0 (r.eraseIdx i)

theorem PhysLean.List.orderedInsert_eraseIdx_orderedInsertPos_le {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (i : ℕ) (hi : ↑(orderedInsertPos le1 r r0) ≤ i) (hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) : (List.orderedInsert le1 r0 r).eraseIdx i.succ = List.orderedInsert le1 r0 (r.eraseIdx i)

def PhysLean.List.orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : Fin (r.length + 1) ≃ Fin (List.orderedInsert le1 r0 r).length

The equivalence between Fin (r0 :: r).length and Fin (List.orderedInsert le1 r0 r).length according to where the elements map, i.e. 0 is taken to orderedInsertPos le1 r r0.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PhysLean.List.orderedInsertEquiv_zero {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (orderedInsertEquiv le1 r r0) 0 = orderedInsertPos le1 r r0

theorem PhysLean.List.orderedInsertEquiv_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : ℕ) (hn : n.succ < (r0 :: r).length) : (orderedInsertEquiv le1 r r0) ⟨n.succ, hn⟩ = Fin.cast ⋯ (⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨n, ⋯⟩)

theorem PhysLean.List.orderedInsertEquiv_fin_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : Fin r.length) : (orderedInsertEquiv le1 r r0) n.succ = Fin.cast ⋯ (⟨↑(orderedInsertPos le1 r r0), ⋯⟩.succAbove ⟨↑n, ⋯⟩)

theorem PhysLean.List.orderedInsertEquiv_monotone_fin_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n m : Fin r.length) (hx : (orderedInsertEquiv le1 r r0) n.succ < (orderedInsertEquiv le1 r r0) m.succ) : n < m

theorem PhysLean.List.orderedInsertEquiv_congr {α : Type} {r : α → α → Prop} [DecidableRel r] (a : α) (l l' : List α) (h : l = l') : orderedInsertEquiv r l a = (Fin.castOrderIso ⋯).trans ((orderedInsertEquiv r l' a).trans (Fin.castOrderIso ⋯).toEquiv)

theorem PhysLean.List.get_eq_orderedInsertEquiv {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (r0 :: r).get = (List.orderedInsert le1 r0 r).get ∘ ⇑(orderedInsertEquiv le1 r r0)

theorem PhysLean.List.orderedInsertEquiv_get {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (r0 :: r).get ∘ ⇑(orderedInsertEquiv le1 r r0).symm = (List.orderedInsert le1 r0 r).get

theorem PhysLean.List.orderedInsert_eraseIdx_orderedInsertEquiv_zero {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : (List.orderedInsert le1 r0 r).eraseIdx ↑((orderedInsertEquiv le1 r r0) ⟨0, ⋯⟩) = r

theorem PhysLean.List.orderedInsert_eraseIdx_orderedInsertEquiv_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : ℕ) (hn : n.succ < (r0 :: r).length) (hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) : (List.orderedInsert le1 r0 r).eraseIdx ↑((orderedInsertEquiv le1 r r0) ⟨n.succ, hn⟩) = List.orderedInsert le1 r0 (r.eraseIdx n)

theorem PhysLean.List.orderedInsert_eraseIdx_orderedInsertEquiv_fin_succ {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) (n : Fin r.length) (hr : ∀ (i j : Fin r.length), i < j → ¬le1 r0 (r.get j) → ¬le1 r0 (r.get i)) : (List.orderedInsert le1 r0 r).eraseIdx ↑((orderedInsertEquiv le1 r r0) n.succ) = List.orderedInsert le1 r0 (r.eraseIdx ↑n)

theorem PhysLean.List.orderedInsertEquiv_sigma {I : Type} {f : I → Type} (le1 : I → I → Prop) [DecidableRel le1] (l : List ((i : I) × f i)) (i : I) (a : f i) : orderedInsertEquiv (fun (i j : (i : I) × f i) => le1 i.fst j.fst) l ⟨i, a⟩ = (Fin.castOrderIso ⋯).trans ((orderedInsertEquiv le1 (List.map (fun (i : (i : I) × f i) => i.fst) l) i).trans (Fin.castOrderIso ⋯).toEquiv)

theorem PhysLean.List.orderedInsert_eq_insertIdx_orderedInsertPos {I : Type} (le1 : I → I → Prop) [DecidableRel le1] (r : List I) (r0 : I) : List.orderedInsert le1 r0 r = r.insertIdx (↑(orderedInsertPos le1 r r0)) r0

def PhysLean.List.insertionSortEquiv {α : Type} (r : α → α → Prop) [DecidableRel r] (l : List α) : Fin l.length ≃ Fin (List.insertionSort r l).length

The equivalence between Fin l.length ≃ Fin (List.insertionSort r l).length induced by the sorting algorithm.

Equations

• PhysLean.List.insertionSortEquiv r [] = Equiv.refl (Fin [].length)
• PhysLean.List.insertionSortEquiv r (a :: l) = (PhysLean.Fin.equivCons (PhysLean.List.insertionSortEquiv r l)).trans (PhysLean.List.orderedInsertEquiv r (List.insertionSort r l) a)

theorem PhysLean.List.insertionSortEquiv_get {α : Type} {r : α → α → Prop} [DecidableRel r] (l : List α) : l.get ∘ ⇑(insertionSortEquiv r l).symm = (List.insertionSort r l).get

theorem PhysLean.List.insertionSortEquiv_congr {α : Type} {r : α → α → Prop} [DecidableRel r] (l l' : List α) (h : l = l') : insertionSortEquiv r l = (Fin.castOrderIso ⋯).trans ((insertionSortEquiv r l').trans (Fin.castOrderIso ⋯).toEquiv)

theorem PhysLean.List.insertionSort_get_comp_insertionSortEquiv {α : Type} {r : α → α → Prop} [DecidableRel r] (l : List α) : (List.insertionSort r l).get ∘ ⇑(insertionSortEquiv r l) = l.get

theorem PhysLean.List.insertionSort_eq_ofFn {α : Type} {r : α → α → Prop} [DecidableRel r] (l : List α) : List.insertionSort r l = List.ofFn (l.get ∘ ⇑(insertionSortEquiv r l).symm)

theorem PhysLean.List.insertionSortEquiv_order {α : Type} {r : α → α → Prop} [DecidableRel r] (l : List α) (i j : Fin l.length) (hij : i < j) (hij' : (insertionSortEquiv r l) j < (insertionSortEquiv r l) i) : ¬r l[i] l[j]

def PhysLean.List.optionErase {I : Type} (l : List I) (i : Option (Fin l.length)) : List I

Optional erase of an element in a list. For none returns the list, for some i returns the list with the i'th element erased.

Equations

• PhysLean.List.optionErase l none = l
• PhysLean.List.optionErase l (some i_2) = l.eraseIdx ↑i_2

theorem PhysLean.List.eraseIdx_length' {I : Type} (l : List I) (i : Fin l.length) : (l.eraseIdx ↑i).length = l.length - 1

theorem PhysLean.List.eraseIdx_length {I : Type} (l : List I) (i : Fin l.length) : (l.eraseIdx ↑i).length + 1 = l.length

theorem PhysLean.List.eraseIdx_length_succ {I : Type} (l : List I) (i : Fin l.length) : (l.eraseIdx ↑i).length.succ = l.length

theorem PhysLean.List.eraseIdx_cons_length {I : Type} (a : I) (l : List I) (i : Fin (a :: l).length) : ((a :: l).eraseIdx ↑i).length = l.length

theorem PhysLean.List.eraseIdx_get {I : Type} (l : List I) (i : Fin l.length) : (l.eraseIdx ↑i).get = l.get ∘ Fin.cast ⋯ ∘ (Fin.cast ⋯ i).succAbove

theorem PhysLean.List.eraseIdx_insertionSort {I : Type} (le1 : I → I → Prop) [DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (n : ℕ) (r : List I) (hn : n < r.length) : (List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) ⟨n, hn⟩) = List.insertionSort le1 (r.eraseIdx n)

theorem PhysLean.List.eraseIdx_insertionSort_fin {I : Type} (le1 : I → I → Prop) [DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (r : List I) (n : Fin r.length) : (List.insertionSort le1 r).eraseIdx ↑((insertionSortEquiv le1 r) n) = List.insertionSort le1 (r.eraseIdx ↑n)

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

Given a list i :: l the left-most minimal position a of i :: l wrt r. That is the first position of l such that for every element (i :: l)[b] before that position r ((i :: l)[b]) ((i :: l)[a]) is not true. The use of i :: l here rather then just l is to ensure that such a position exists. .

Equations

• PhysLean.List.insertionSortMinPos r i l = (PhysLean.List.insertionSortEquiv r (i :: l)).symm ⟨0, ⋯⟩

def PhysLean.List.insertionSortMin {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) : α

The element of i :: l at insertionSortMinPos.

Equations

• PhysLean.List.insertionSortMin r i l = (i :: l).get (PhysLean.List.insertionSortMinPos r i l)

theorem PhysLean.List.insertionSortMin_eq_insertionSort_head {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) : insertionSortMin r i l = (List.insertionSort r (i :: l)).head ⋯

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

The list remaining after dropping the element at the position determined by insertionSortMinPos.

Equations

• PhysLean.List.insertionSortDropMinPos r i l = (i :: l).eraseIdx ↑(PhysLean.List.insertionSortMinPos r i l)

theorem PhysLean.List.insertionSort_eq_insertionSortMin_cons {α : Type} (r : α → α → Prop) [DecidableRel r] [IsTotal α r] [IsTrans α r] (i : α) (l : List α) : List.insertionSort r (i :: l) = insertionSortMin r i l :: List.insertionSort r (insertionSortDropMinPos r i l)

def PhysLean.List.optionEraseZ {I : Type} (l : List I) (a : I) (i : Option (Fin l.length)) : List I

Optional erase of an element in a list, with addition for none. For none adds a to the front of the list, for some i removes the ith element of the list (does not add a). E.g. optionEraseZ [0, 1, 2] 4 none = [4, 0, 1, 2] and optionEraseZ [0, 1, 2] 4 (some 1) = [0, 2].

Equations

• PhysLean.List.optionEraseZ l a none = a :: l
• PhysLean.List.optionEraseZ l a (some i_2) = l.eraseIdx ↑i_2

@[simp]

theorem PhysLean.List.optionEraseZ_some_length {I : Type} (l : List I) (a : I) (i : Fin l.length) : (optionEraseZ l a (some i)).length = l.length - 1

theorem PhysLean.List.optionEraseZ_ext {I : Type} {l l' : List I} {a a' : I} {i : Option (Fin l.length)} {i' : Option (Fin l'.length)} (hl : l = l') (ha : a = a') (hi : Option.map (Fin.cast ⋯) i = i') : optionEraseZ l a i = optionEraseZ l' a' i'

theorem PhysLean.List.mem_take_finrange (n m : ℕ) (a : Fin n) : a ∈ List.take m (List.finRange n) ↔ ↑a < m