Vertex sequences: indexing and insertion

Positional access into a vertex sequence via the underlying list, and insertion of a vertex at a given index.

Main definitions

• GetElem (VertexSeq α) ℕ α — index into the visited vertices.
• VertexSeq.insert — insert a vertex at a position.

insert currently has no lemmas and no clients inside AlgoLib; it is kept as the one positional editing operation the carrier is expected to offer.

Indexing

@[implicit_reducible]

instance VertexSeq.instGetElemNatLtLengthToList {α : Type u_1} : GetElem (VertexSeq α) ℕ α fun (w : VertexSeq α) (i : ℕ) => i < w.toList.length

Equations

• VertexSeq.instGetElemNatLtLengthToList = { getElem := fun (w : VertexSeq α) (i : ℕ) (h : i < w.toList.length) => w.toList[i] }

theorem VertexSeq.getElem_zero_eq_head {α : Type u_1} (w : VertexSeq α) : w.toList[0] = w.head

Indexing position zero returns the head vertex.

theorem VertexSeq.head_dropHead_eq_getElem_one {α : Type u_1} (w : VertexSeq α) (h : w.length ≠ 0) : w.dropHead.head = w.toList[1]

For a nontrivial sequence, the head after dropHead is the vertex at index one.

theorem VertexSeq.head_dropHead_of_toList_eq_cons_cons {α : Type u_1} (w : VertexSeq α) (a b : α) (rest : List α) (h : w.toList = a :: b :: rest) : w.dropHead.head = b

If the vertex list starts a :: b :: _, then the head after dropHead is b. The index-free face of head_dropHead_eq_getElem_one.

insert

def VertexSeq.insert {α : Type u_1} : VertexSeq α → ℕ → α → VertexSeq α

Insert the vertex v at index i, shifting later vertices one position to the right. If i exceeds w.toList.length, v is appended at the end.

Equations

• (VertexSeq.singleton x_3).insert 0 x✝ = (VertexSeq.singleton x✝).cons x_3
• (VertexSeq.singleton x_3).insert n.succ x✝ = (VertexSeq.singleton x_3).cons x✝
• (q.cons x_3).insert x✝¹ x✝ = if x✝¹ ≤ q.length then (q.insert x✝¹ x✝).cons x_3 else if x✝¹ = q.length + 1 then (q.cons x✝).cons x_3 else (q.cons x_3).cons x✝