Cutting wLists Off

def WList.prefixUntil {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : WList α β

Take the prefix ending at the first vertex satisfying a predicate P (or the entire wList if nothing satisfies P).

Equations

• (WList.nil x).prefixUntil P = WList.nil x
• (WList.cons x e w_2).prefixUntil P = if P x then WList.nil x else WList.cons x e (w_2.prefixUntil P)

@[simp]

theorem WList.prefixUntil_nil {α : Type u_1} {β : Type u_2} {u : α} {P : α → Prop} [DecidablePred P] : (nil u).prefixUntil P = nil u

@[simp]

theorem WList.prefixUntil_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {P : α → Prop} [DecidablePred P] (w : WList α β) : (cons x e w).prefixUntil P = if P x then nil x else cons x e (w.prefixUntil P)

def WList.prefixUntilVertex {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (x : α) : WList α β

The prefix of w ending at a vertex x. Equal to w if x ∉ w.

Equations

• w.prefixUntilVertex x = w.prefixUntil fun (x_1 : α) => x_1 = x

@[simp]

theorem WList.prefixUntilVertex_nil {α : Type u_1} {β : Type u_2} {u x : α} [DecidableEq α] : (nil u).prefixUntilVertex x = nil u

@[simp]

theorem WList.prefixUntilVertex_cons_eq_nil {α : Type u_1} {β : Type u_2} [DecidableEq α] (u : α) (e : β) (w : WList α β) : (cons u e w).prefixUntilVertex u = nil u

theorem WList.prefixUntilVertex_cons {α : Type u_1} {β : Type u_2} {x : α} [DecidableEq α] (u : α) (e : β) (w : WList α β) : (cons u e w).prefixUntilVertex x = if u = x then nil u else cons u e (w.prefixUntilVertex x)

def WList.suffixFrom {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : WList α β

Take the suffix starting at the first vertex satisfying a predicate P, (or the Nil wList on the last vertex if nothing satisfies P)

Equations

• (WList.nil x).suffixFrom P = WList.nil x
• (WList.cons x e w_2).suffixFrom P = if P x then WList.cons x e w_2 else w_2.suffixFrom P

@[simp]

theorem WList.suffixFrom_nil {α : Type u_1} {β : Type u_2} {u : α} {P : α → Prop} [DecidablePred P] : (nil u).suffixFrom P = nil u

@[simp]

theorem WList.suffixFrom_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {P : α → Prop} [DecidablePred P] (w : WList α β) : (cons x e w).suffixFrom P = if P x then cons x e w else w.suffixFrom P

theorem WList.suffixFrom_isSuffix {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : (w.suffixFrom P).IsSuffix w

def WList.suffixFromVertex {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (x : α) : WList α β

The suffix of w starting at the first occurence of a vertex x. Equal to [w.last] if x ∉ w.

Equations

• w.suffixFromVertex x = w.suffixFrom fun (x_1 : α) => x_1 = x

@[simp]

theorem WList.suffixFromVertex_nil {α : Type u_1} {β : Type u_2} {u x : α} [DecidableEq α] : (nil u).suffixFromVertex x = nil u

theorem WList.suffixFromVertex_isSuffix {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) (x : α) : (w.suffixFromVertex x).IsSuffix w

def WList.prefixUntilEdge {α : Type u_1} {β : Type u_2} (w : WList α β) (Q : β → Prop) [DecidablePred Q] : WList α β

Take the prefix ending at the tail of the first edge satisfying Q. Equal to w if no edge satisfies Q.

Equations

• (WList.nil x).prefixUntilEdge Q = WList.nil x
• (WList.cons x e w_2).prefixUntilEdge Q = if Q e then WList.nil x else WList.cons x e (w_2.prefixUntilEdge Q)

@[simp]

theorem WList.prefixUntilEdge_nil {α : Type u_1} {β : Type u_2} {u : α} {Q : β → Prop} [DecidablePred Q] : (nil u).prefixUntilEdge Q = nil u

theorem WList.prefixUntilEdge_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {Q : β → Prop} [DecidablePred Q] (w : WList α β) : (cons x e w).prefixUntilEdge Q = if Q e then nil x else cons x e (w.prefixUntilEdge Q)

@[simp]

theorem WList.prefixUntilEdge_cons_true {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} {Q : β → Prop} [DecidablePred Q] (he : Q e) : (cons x e w).prefixUntilEdge Q = nil x

@[simp]

theorem WList.prefixUntilEdge_cons_false {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} {Q : β → Prop} [DecidablePred Q] (he : ¬Q e) : (cons x e w).prefixUntilEdge Q = cons x e (w.prefixUntilEdge Q)

theorem WList.prefixUntilEdge_isPrefix {α : Type u_1} {β : Type u_2} (w : WList α β) (Q : β → Prop) [DecidablePred Q] : (w.prefixUntilEdge Q).IsPrefix w

theorem WList.prefixUntilEdge_length_lt {α : Type u_1} {β : Type u_2} {w : WList α β} {Q : β → Prop} [DecidablePred Q] (hQ : ∃ e ∈ w.edgeSet, Q e) : (w.prefixUntilEdge Q).length < w.length

def WList.suffixFromEdge {α : Type u_1} {β : Type u_2} (w : WList α β) (Q : β → Prop) [DecidablePred Q] : WList α β

Take the suffix starting at the head of the first edge satisfying Q. Equal to nil w.last if no edge satisfies Q.

Equations

• (WList.nil x).suffixFromEdge Q = WList.nil x
• (WList.cons x e w_2).suffixFromEdge Q = if Q e then w_2 else w_2.suffixFromEdge Q

@[simp]

theorem WList.suffixFromEdge_nil {α : Type u_1} {β : Type u_2} {u : α} {Q : β → Prop} [DecidablePred Q] : (nil u).suffixFromEdge Q = nil u

theorem WList.suffixFromEdge_cons {α : Type u_1} {β : Type u_2} {x : α} {e : β} {Q : β → Prop} [DecidablePred Q] (w : WList α β) : (cons x e w).suffixFromEdge Q = if Q e then w else w.suffixFromEdge Q

@[simp]

theorem WList.suffixFromEdge_cons_true {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} {Q : β → Prop} [DecidablePred Q] (he : Q e) : (cons x e w).suffixFromEdge Q = w

@[simp]

theorem WList.suffixFromEdge_cons_false {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} {Q : β → Prop} [DecidablePred Q] (he : ¬Q e) : (cons x e w).suffixFromEdge Q = w.suffixFromEdge Q

theorem WList.suffixFromEdge_isSuffix {α : Type u_1} {β : Type u_2} (w : WList α β) (Q : β → Prop) [DecidablePred Q] : (w.suffixFromEdge Q).IsSuffix w

theorem WList.suffixFromEdge_length_lt {α : Type u_1} {β : Type u_2} {w : WList α β} {Q : β → Prop} [DecidablePred Q] (hQ : ∃ e ∈ w.edgeSet, Q e) : (w.suffixFromEdge Q).length < w.length

def WList.prefixUntilEdgeLabel {α : Type u_1} {β : Type u_2} [DecidableEq β] (w : WList α β) (e : β) : WList α β

The prefix of w ending just before the first occurrence of edge e. Equal to w if e ∉ w.edge.

Equations

• w.prefixUntilEdgeLabel e = w.prefixUntilEdge fun (x : β) => x = e

def WList.suffixFromEdgeLabel {α : Type u_1} {β : Type u_2} [DecidableEq β] (w : WList α β) (e : β) : WList α β

The suffix of w starting just after the first occurrence of edge e. Equal to nil w.last if e ∉ w.edge.

Equations

• w.suffixFromEdgeLabel e = w.suffixFromEdge fun (x : β) => x = e

def WList.prefixUntilLast {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : WList α β

Take the prefix of w ending at the last occurence of x in w. Equal to w if x ∉ w.

Equations

• w.prefixUntilLast P = (w.reverse.suffixFrom P).reverse

def WList.suffixFromLast {α : Type u_1} {β : Type u_2} (w : WList α β) (P : α → Prop) [DecidablePred P] : WList α β

Take the suffix of w starting at the last occurence of P in w. If P never occurs, this is all of w.

Equations

• w.suffixFromLast P = (w.reverse.prefixUntil P).reverse

def WList.tail {α : Type u_1} {β : Type u_2} : WList α β → WList α β

Remove the first vertex and edge from a wList

Equations

• (WList.nil x).tail = WList.nil x
• (WList.cons x e w_1).tail = w_1

@[simp]

theorem WList.tail_nil {α : Type u_1} {β : Type u_2} (x : α) : (nil x).tail = nil x

@[simp]

theorem WList.tail_cons {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) : (cons x e w).tail = w

theorem WList.edgeMap_tail {α : Type u_1} {β : Type u_2} {β' : Type u_3} (w : WList α β) (σ : β → β') : (edgeMap σ w).tail = edgeMap σ w.tail

theorem WList.map_tail {α : Type u_1} {β : Type u_2} {α' : Type u_3} (w : WList α β) (f : α → α') : (map f w).tail = map f w.tail

def WList.dropLast {α : Type u_1} {β : Type u_2} : WList α β → WList α β

Remove the last edge and vertex from a wList. This is the reverse of the reversed tail.

Equations

• (WList.nil x_1).dropLast = WList.nil x_1
• (WList.cons x_1 e (WList.nil u)).dropLast = WList.nil x_1
• (WList.cons x_1 e (WList.cons y e' w)).dropLast = WList.cons x_1 e (WList.cons y e' w).dropLast

@[simp]

theorem WList.dropLast_nil {α : Type u_1} {β : Type u_2} {x : α} : (nil x).dropLast = nil x

@[simp]

theorem WList.dropLast_cons_nil {α : Type u_1} {β : Type u_2} {x y : α} {e : β} : (cons x e (nil y)).dropLast = nil x

@[simp]

theorem WList.dropLast_cons_cons {α : Type u_1} {β : Type u_2} {x y : α} {e e' : β} {w : WList α β} : (cons x e (cons y e' w)).dropLast = cons x e (cons y e' w).dropLast

def WList.take {α : Type u_1} {β : Type u_2} : WList α β → ℕ → WList α β

Take the first n vertices from a WList. Returns the entire list if n ≥ w.length + 1.

Equations

• (WList.nil x_2).take x✝ = WList.nil x_2
• (WList.cons x_2 e w).take 0 = WList.nil x_2
• (WList.cons x_2 e w).take n.succ = WList.cons x_2 e (w.take n)

@[simp]

theorem WList.take_nil {α : Type u_1} {β : Type u_2} (x : α) (n : ℕ) : (nil x).take n = nil x

@[simp]

theorem WList.take_zero {α : Type u_1} {β : Type u_2} (w : WList α β) : w.take 0 = nil w.first

@[simp]

theorem WList.take_cons_succ {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) (n : ℕ) : (cons x e w).take (n + 1) = cons x e (w.take n)

def WList.drop {α : Type u_1} {β : Type u_2} : WList α β → ℕ → WList α β

Drop the first n vertices from a WList. Returns nil w.last if n ≥ w.length + 1.

Equations

• x✝.drop 0 = x✝
• (WList.nil x_2).drop x✝ = WList.nil x_2
• (WList.cons u e w).drop n.succ = w.drop n

@[simp]

theorem WList.drop_zero {α : Type u_1} {β : Type u_2} (w : WList α β) : w.drop 0 = w

@[simp]

theorem WList.drop_nil {α : Type u_1} {β : Type u_2} (x : α) (n : ℕ) : (nil x).drop n = nil x

@[simp]

theorem WList.drop_cons_succ {α : Type u_1} {β : Type u_2} (x : α) (e : β) (w : WList α β) (n : ℕ) : (cons x e w).drop (n + 1) = w.drop n

@[irreducible]

def WList.dedup {α : Type u_1} {β : Type u_2} [DecidableEq α] : WList α β → WList α β

Remove duplicate vertices from a WList to give a duplicate-free sublist.

Equations

• (WList.nil x).dedup = WList.nil x
• (WList.cons x e w_1).dedup = if x ∈ w_1 then (w_1.suffixFromVertex x).dedup else WList.cons x e w_1.dedup

@[simp]

theorem WList.dedup_nil {α : Type u_1} {β : Type u_2} [DecidableEq α] (x : α) : (nil x).dedup = nil x