Sequences

Sequences are an ordered collection of elements.

All sequences are isomorphic to [List], which is also the model used for sequence operations.

class LeanColls.Seq (C : Type u) (τ : outParam (Type v)) extends LeanColls.Fold , LeanColls.Insert , LeanColls.ToList , Membership , LeanColls.Size , Append : Type (max (u + 1) (v + 1))

A collection which is ordered (i.e. isomorphic to [List]).

• fold : {β : Type (max u v)} → C → (β → τ → β) → β → β
• foldM : {β : Type (max u v)} → {m : Type (max u v) → Type (max u v)} → [inst : Monad m] → C → (β → τ → m β) → β → m β
• empty : C
• insert : C → τ → C
• singleton : τ → C
• toList : C → List τ
• mem : τ → C → Prop
• size : C → ℕ
• append : C → C → C
• ofFn : {sz : ℕ} → (Fin sz → τ) → C
• get : (cont : C) → Fin (LeanColls.size cont) → τ
• set : (cont : C) → Fin (LeanColls.size cont) → τ → C
• update : (cont : C) → Fin (LeanColls.size cont) → (τ → τ) → C
• cons : τ → C → C
• getCons? : C → Option (τ × C)
• snoc : C → τ → C
• getSnoc? : C → Option (C × τ)

instance List.instSeqList {τ : Type u_1} : LeanColls.Seq (List τ) τ

Equations

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

@[simp]

theorem List.toList_eq {α : Type u_1} (L : List α) : LeanColls.toList L = L

@[simp]

theorem List.size_cons {α : Type u_1} (x : α) (xs : List α) : LeanColls.size (x :: xs) = LeanColls.size xs + 1

@[simp]

theorem List.size_nil {α : Type u_1} : LeanColls.size [] = 0

@[simp]

theorem List.toMultiset_eq {α : Type u_1} (L : List α) : LeanColls.ToMultiset.toMultiset L = ↑L

class LeanColls.LawfulSeq (C : Type u) (τ : outParam (Type v)) [LeanColls.Seq C τ] extends LeanColls.Mem.ToList , LeanColls.Append.ToList , LeanColls.Insert.ToMultiset , LeanColls.Fold.ToList : Prop

• mem_iff_mem_toList : ∀ (x : τ) (cont : C), x ∈ cont ↔ x ∈ LeanColls.toList cont
• toList_append : ∀ (c1 c2 : C), LeanColls.toList (c1 ++ c2) = LeanColls.toList c1 ++ LeanColls.toList c2
• toMultiset_empty : LeanColls.ToMultiset.toMultiset LeanColls.empty = ∅
• toMultiset_insert : ∀ (cont : C) (x : τ), LeanColls.ToMultiset.toMultiset (LeanColls.insert cont x) = x ::ₘ LeanColls.ToMultiset.toMultiset cont
• toMultiset_singleton : ∀ (x : τ), LeanColls.ToMultiset.toMultiset (LeanColls.singleton x) = {x}
• fold_eq_fold_toList : ∀ (c : C), ∃ (L : List τ), L.Perm (LeanColls.toList c) ∧ ∀ {β : Type (max u v)} (f : β → τ → β) (init : β), LeanColls.fold c f init = List.foldl f init L
• foldM_eq_fold : ∀ {m : Type (max u v) → Type (max u v)} {β : Type (max u v)} [inst : Monad m] [inst_1 : LawfulMonad m] (c : C) (f : β → τ → m β) (init : β), LeanColls.foldM c f init = LeanColls.fold c (fun (acc : m β) (x : τ) => do let x_1 ← acc f x_1 x) (pure init)
• size_def : ∀ (cont : C), LeanColls.size cont = (LeanColls.toList cont).length
• toList_ofFn : ∀ {n : ℕ} (f : Fin n → τ), LeanColls.toList (LeanColls.Seq.ofFn f) = LeanColls.Seq.ofFn f
• get_def : ∀ (cont : C) (i : Fin (LeanColls.size cont)), LeanColls.Seq.get cont i = LeanColls.Seq.get (LeanColls.toList cont) (Fin.cast ⋯ i)
• toList_set : ∀ (cont : C) (i : Fin (LeanColls.size cont)) (x : τ), LeanColls.toList (LeanColls.Seq.set cont i x) = LeanColls.Seq.set (LeanColls.toList cont) (Fin.cast ⋯ i) x
• toList_update : ∀ (cont : C) (i : Fin (LeanColls.size cont)) (f : τ → τ), LeanColls.toList (LeanColls.Seq.update cont i f) = LeanColls.Seq.update (LeanColls.toList cont) (Fin.cast ⋯ i) f
• toList_cons : ∀ (x : τ) (cont : C), LeanColls.toList (LeanColls.Seq.cons x cont) = LeanColls.Seq.cons x (LeanColls.toList cont)
• getCons?_eq_none : ∀ (cont : C), LeanColls.Seq.getCons? cont = none ↔ LeanColls.toList cont = []
• getCons?_eq_some : ∀ (cont : C) (x : τ) (c' : C), LeanColls.Seq.getCons? cont = some (x, c') ↔ LeanColls.toList cont = x :: LeanColls.toList c'
• toList_snoc : ∀ (cont : C) (x : τ), LeanColls.toList (LeanColls.Seq.snoc cont x) = LeanColls.Seq.snoc (LeanColls.toList cont) x
• getSnoc?_eq_none : ∀ (cont : C), LeanColls.Seq.getSnoc? cont = none ↔ LeanColls.toList cont = []
• getSnoc?_eq_some : ∀ (cont : C) (x : τ) (c' : C), LeanColls.Seq.getSnoc? cont = some (c', x) ↔ LeanColls.toList cont = (LeanColls.toList c').snoc x

theorem LeanColls.LawfulSeq.size_def {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (cont : C) : LeanColls.size cont = (LeanColls.toList cont).length

@[simp]

theorem LeanColls.LawfulSeq.toList_ofFn {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] {n : ℕ} (f : Fin n → τ) : LeanColls.toList (LeanColls.Seq.ofFn f) = LeanColls.Seq.ofFn f

theorem LeanColls.LawfulSeq.get_def {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) : LeanColls.Seq.get cont i = LeanColls.Seq.get (LeanColls.toList cont) (Fin.cast ⋯ i)

@[simp]

theorem LeanColls.LawfulSeq.toList_set {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (x : τ) : LeanColls.toList (LeanColls.Seq.set cont i x) = LeanColls.Seq.set (LeanColls.toList cont) (Fin.cast ⋯ i) x

@[simp]

theorem LeanColls.LawfulSeq.toList_update {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (f : τ → τ) : LeanColls.toList (LeanColls.Seq.update cont i f) = LeanColls.Seq.update (LeanColls.toList cont) (Fin.cast ⋯ i) f

@[simp]

theorem LeanColls.LawfulSeq.toList_cons {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (x : τ) (cont : C) : LeanColls.toList (LeanColls.Seq.cons x cont) = LeanColls.Seq.cons x (LeanColls.toList cont)

theorem LeanColls.LawfulSeq.getCons?_eq_none {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (cont : C) : LeanColls.Seq.getCons? cont = none ↔ LeanColls.toList cont = []

theorem LeanColls.LawfulSeq.getCons?_eq_some {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (cont : C) (x : τ) (c' : C) : LeanColls.Seq.getCons? cont = some (x, c') ↔ LeanColls.toList cont = x :: LeanColls.toList c'

@[simp]

theorem LeanColls.LawfulSeq.toList_snoc {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (cont : C) (x : τ) : LeanColls.toList (LeanColls.Seq.snoc cont x) = LeanColls.Seq.snoc (LeanColls.toList cont) x

theorem LeanColls.LawfulSeq.getSnoc?_eq_none {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (cont : C) : LeanColls.Seq.getSnoc? cont = none ↔ LeanColls.toList cont = []

theorem LeanColls.LawfulSeq.getSnoc?_eq_some {C : Type u} {τ : outParam (Type v)} [LeanColls.Seq C τ] [self : LeanColls.LawfulSeq C τ] (cont : C) (x : τ) (c' : C) : LeanColls.Seq.getSnoc? cont = some (c', x) ↔ LeanColls.toList cont = (LeanColls.toList c').snoc x

instance List.instLawfulSeq {τ : Type u_1} : LeanColls.LawfulSeq (List τ) τ

Equations

• ⋯ = ⋯

@[simp]

theorem LeanColls.Seq.size_set {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (x : τ) : LeanColls.size (LeanColls.Seq.set cont i x) = LeanColls.size cont

@[simp]

theorem LeanColls.Seq.size_update {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (f : τ → τ) : LeanColls.size (LeanColls.Seq.update cont i f) = LeanColls.size cont

@[simp]

theorem LeanColls.Seq.size_cons {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (x : τ) : LeanColls.size (LeanColls.Seq.cons x cont) = LeanColls.size cont + 1

@[simp]

theorem LeanColls.Seq.size_snoc {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (x : τ) : LeanColls.size (LeanColls.Seq.snoc cont x) = LeanColls.size cont + 1

@[simp]

theorem LeanColls.Seq.size_append {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (c1 : C) (c2 : C) : LeanColls.size (c1 ++ c2) = LeanColls.size c1 + LeanColls.size c2

@[simp]

theorem LeanColls.Seq.size_singleton {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (x : τ) : LeanColls.size (LeanColls.singleton x) = 1

@[simp]

theorem LeanColls.Seq.size_ofFn {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] {n : ℕ} (f : Fin n → τ) : LeanColls.size (LeanColls.Seq.ofFn f) = n

@[simp]

theorem LeanColls.Seq.get_ofFn {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] {n : ℕ} (f : Fin n → τ) (i : Fin (LeanColls.size (LeanColls.Seq.ofFn f))) : LeanColls.Seq.get (LeanColls.Seq.ofFn f) i = f (Fin.cast ⋯ i)

@[simp]

theorem LeanColls.Seq.get_set_eq {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (x : τ) (j : Fin (LeanColls.size (LeanColls.Seq.set cont i x))) : ↑i = ↑j → LeanColls.Seq.get (LeanColls.Seq.set cont i x) j = x

@[simp]

theorem LeanColls.Seq.get_set_ne {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (x : τ) (j : Fin (LeanColls.size (LeanColls.Seq.set cont i x))) : ↑i ≠ ↑j → LeanColls.Seq.get (LeanColls.Seq.set cont i x) j = LeanColls.Seq.get cont (Fin.cast ⋯ j)

theorem LeanColls.Seq.get_set {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (x : τ) (j : Fin (LeanColls.size (LeanColls.Seq.set cont i x))) : LeanColls.Seq.get (LeanColls.Seq.set cont i x) j = if ↑i = ↑j then x else LeanColls.Seq.get cont (Fin.cast ⋯ j)

@[simp]

theorem LeanColls.Seq.get_update_eq {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (f : τ → τ) (j : Fin (LeanColls.size (LeanColls.Seq.update cont i f))) : ↑i = ↑j → LeanColls.Seq.get (LeanColls.Seq.update cont i f) j = f (LeanColls.Seq.get cont i)

@[simp]

theorem LeanColls.Seq.get_update_ne {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (f : τ → τ) (j : Fin (LeanColls.size (LeanColls.Seq.update cont i f))) : ↑i ≠ ↑j → LeanColls.Seq.get (LeanColls.Seq.update cont i f) j = LeanColls.Seq.get cont (Fin.cast ⋯ j)

theorem LeanColls.Seq.get_update {C : Type u_1} {τ : Type u_2} [LeanColls.Seq C τ] [LeanColls.LawfulSeq C τ] (cont : C) (i : Fin (LeanColls.size cont)) (f : τ → τ) (j : Fin (LeanColls.size (LeanColls.Seq.update cont i f))) : LeanColls.Seq.get (LeanColls.Seq.update cont i f) j = if ↑i = ↑j then f (LeanColls.Seq.get cont (Fin.cast ⋯ j)) else LeanColls.Seq.get cont (Fin.cast ⋯ j)