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 (r0 :: r).length ≃ 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.

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.length_insertIdx' {α✝ : Type u_1} {a : α✝} (n : ℕ) (as : List α✝) : (List.insertIdx n a as).length = if n ≤ as.length then as.length + 1 else as.length

This result is taken from: https://github.com/leanprover/lean4/blob/master/src/Init/Data/List/Nat/InsertIdx.lean with simple modification here to make it run. The file it was taken from is licensed under the Apache License, Version 2.0. and written by Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro.

Once PhysLean is updated to a more recent version of Lean this result will be removed.

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 = List.insertIdx (↑(orderedInsertPos le1 r r0)) r0 r

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