def WList.IsClosed {α : Type u_1} {β : Type u_2} (w : WList α β) : Prop

A WList is closed if its first and last entries are equal.

Equations

• w.IsClosed = (w.first = w.last)

theorem WList.IsClosed.eq {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.IsClosed) : w.first = w.last

@[simp]

theorem WList.nil_isClosed {α : Type u_1} {β : Type u_2} (x : α) : (nil x).IsClosed

@[simp]

theorem WList.cons_isClosed_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).IsClosed ↔ x = w.last

@[simp]

theorem WList.concat_isClosed_iff {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (w.concat e x).IsClosed ↔ x = w.first

theorem WList.IsClosed.vertexSet_tail {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.IsClosed) : w.tail.vertexSet = w.vertexSet

theorem WList.IsClosed.reverse {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.IsClosed) : w.reverse.IsClosed

@[simp]

theorem WList.reverse_isClosed_iff {α : Type u_1} {β : Type u_2} {w : WList α β} : w.reverse.IsClosed ↔ w.IsClosed

theorem WList.IsClosed.vertexSet_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (h : w.IsClosed) : w.dropLast.vertexSet = w.vertexSet

theorem WList.IsClosed.mem_tail_iff {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (h : w.IsClosed) : x ∈ w.tail ↔ x ∈ w

theorem WList.IsClosed.mem_dropLast {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (h : w.IsClosed) : x ∈ w.dropLast ↔ x ∈ w

theorem WList.IsClosed.tail_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) : w.tail.dropLast = w.dropLast.tail

theorem WList.IsClosed.length_eq_one_iff {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) : w.length = 1 ↔ ∃ (x : α) (e : β), w = cons x e (nil x)

theorem WList.IsClosed.dropLast_vertex_nodup {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) (hw₁ : w.tail.vertex.Nodup) : w.dropLast.vertex.Nodup

theorem WList.IsClosed.idxOf_get {α : Type u_1} {β : Type u_2} {w : WList α β} [DecidableEq α] (hw : w.IsClosed) (hw₁ : w.tail.vertex.Nodup) {n : ℕ} (hn : n < w.length) : w.idxOf (w.get n) = n

theorem WList.IsClosed.idxOf_lt_length {α : Type u_1} {β : Type u_2} {x : α} {C : WList α β} [DecidableEq α] (hC : C.IsClosed) (hx : x ∈ C) (hne : C.Nonempty) : C.idxOf x < C.length

Rotations

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

Rotate a WList n vertices to the left. This behaves badly (forgets the first vertex) if the list isn't closed.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem WList.cons_rotate_one {α : Type u_1} {β : Type u_2} {x : α} {e : β} {w : WList α β} : (cons x e w).rotate 1 = w.concat e w.first

@[simp]

theorem WList.rotate_cons_succ {α : Type u_1} {β : Type u_2} (w : WList α β) (x : α) (e : β) (n : ℕ) : (cons x e w).rotate (n + 1) = (w.concat e w.first).rotate n

theorem WList.rotate_eq_append {α : Type u_1} {β : Type u_2} {w₁ w₂ : WList α β} (h : w₁.first = w₂.last) (h' : w₁.last = w₂.first) : (w₁ ++ w₂).rotate w₁.length = w₂ ++ w₁

@[simp]

theorem WList.rotate_rotate {α : Type u_1} {β : Type u_2} (w : WList α β) (m n : ℕ) : (w.rotate m).rotate n = w.rotate (m + n)

theorem WList.rotate_succ {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : w.rotate (n + 1) = (w.rotate 1).rotate n

@[simp]

theorem WList.length_rotate {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.rotate n).length = w.length

@[simp]

theorem WList.rotate_nonempty_iff {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} : (w.rotate n).Nonempty ↔ w.Nonempty

theorem WList.Nonempty.rotate {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nonempty) (n : ℕ) : (w.rotate n).Nonempty

@[simp]

theorem WList.rotate_nontrivial_iff {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} : (w.rotate n).Nontrivial ↔ w.Nontrivial

theorem WList.Nontrivial.rotate {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) (n : ℕ) : (w.rotate n).Nontrivial

theorem WList.rotate_firstEdge {α : Type u_1} {β : Type u_2} {w : WList α β} (n : ℕ) (hn : n < w.length) : have hne := ⋯; have hn := ⋯; Nonempty.firstEdge (w.rotate n) ⋯ = w.edge[n]

@[simp]

theorem WList.rotate_first {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) (hn : n ≤ w.length) : (w.rotate n).first = w.get n

theorem WList.rotate_induction {α : Type u_1} {β : Type u_2} {w : WList α β} {motive : WList α β → Prop} (h0 : motive w) (rotate : ∀ ⦃w : WList α β⦄, motive w → motive (w.rotate 1)) (n : ℕ) : motive (w.rotate n)

theorem WList.IsClosed.rotate {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) (n : ℕ) : (w.rotate n).IsClosed

@[simp]

theorem WList.rotate_edge {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.rotate n).edge = w.edge.rotate n

@[simp]

theorem WList.rotate_vertex_tail {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.rotate n).tail.vertex = w.tail.vertex.rotate n

theorem WList.Nonempty.rotate_one {α : Type u_1} {β : Type u_2} {C : WList α β} (hCne : C.Nonempty) : ∃ (e : β), C.rotate 1 = C.tail.concat e C.tail.first

theorem WList.Nonempty.idxOf_rotate_one {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hw : w.Nonempty) (h1 : w.first ≠ x) (hx : x ∈ w) : (w.rotate 1).idxOf x + 1 = w.idxOf x

theorem WList.mem_rotate_of_le_idxOf {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} {n : ℕ} [DecidableEq α] (hx : x ∈ w) (hle : n ≤ w.idxOf x) : x ∈ w.rotate n

theorem WList.idxOf_rotate_add_of_le_idxOf {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} {n : ℕ} [DecidableEq α] (hx : x ∈ w) (hle : n ≤ w.idxOf x) : (w.rotate n).idxOf x + n = w.idxOf x

theorem WList.idxOf_rotate_first_ne_of_lt {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} {n : ℕ} [DecidableEq α] (hlt : n < w.idxOf x) : (w.rotate n).first ≠ x

theorem WList.get_rotate {α : Type u_1} {β : Type u_2} [DecidableEq α] (w : WList α β) {a b : ℕ} (hab : a + b ≤ w.length) : (w.rotate a).get b = w.get (a + b)

theorem WList.IsClosed.rotate_vertexSet {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) (n : ℕ) : (w.rotate n).vertexSet = w.vertexSet

theorem WList.IsClosed.mem_rotate {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hw : w.IsClosed) {n : ℕ} : x ∈ w.rotate n ↔ x ∈ w

theorem WList.IsClosed.dInc_rotate {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (hw : w.IsClosed) (h : w.DInc e x y) (n : ℕ) : (w.rotate n).DInc e x y

theorem WList.IsClosed.isLink_rotate {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (hw : w.IsClosed) (h : w.IsLink e x y) (n : ℕ) : (w.rotate n).IsLink e x y

@[simp]

theorem WList.rotate_edgeSet {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℕ) : (w.rotate n).edgeSet = w.edgeSet

@[simp]

theorem WList.IsClosed.rotate_length {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) : w.rotate w.length = w

theorem WList.IsClosed.rotate_eq_mod {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) (n : ℕ) : w.rotate n = w.rotate (n % w.length)

theorem WList.IsClosed.rotate_first_mod {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) (n : ℕ) : (w.rotate n).first = w.get (n % w.length)

@[simp]

theorem WList.rotate_idxOf_first {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} [DecidableEq α] (hx : x ∈ w) : (w.rotate (w.idxOf x)).first = x

theorem WList.exists_rotate_first_eq {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hx : x ∈ w) : ∃ n ≤ w.length, (w.rotate n).first = x

theorem WList.IsClosed.exists_rotate_first_eq {α : Type u_1} {β : Type u_2} {x : α} {w : WList α β} (hw : w.IsClosed) (hw' : w.Nonempty) (hx : x ∈ w) : ∃ n < w.length, (w.rotate n).first = x

theorem WList.exists_rotate_firstEdge_eq {α : Type u_1} {β : Type u_2} {e : β} {w : WList α β} (hx : e ∈ w.edge) : ∃ n < w.length, ∃ (hw : w.Nonempty), Nonempty.firstEdge (w.rotate n) ⋯ = e

theorem WList.firstEdge_rotate_one {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.Nontrivial) : Nonempty.firstEdge (w.rotate 1) ⋯ = Nonempty.firstEdge w.tail ⋯

theorem WList.IsClosed.rotate_one_dropLast {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) : (w.rotate 1).dropLast = w.tail

Relationships with take and drop

theorem WList.rotate_first_eq_drop_first {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} (hn : n ≤ w.length) : (w.rotate n).first = (w.drop n).first

theorem WList.IsClosed.rotate_take_drop {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} (hw : w.IsClosed) (hn : n ≤ w.length) : w.rotate n = w.drop n ++ w.take n

theorem WList.IsClosed.rotate_eq_drop_append_take_mod {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) (n : ℕ) : w.rotate n = w.drop (n % w.length) ++ w.take (n % w.length)

theorem WList.IsClosed.exists_first_of_dInc {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (hC : w.IsClosed) (he : w.DInc e x y) : ∃ (w' : WList α β) (n : ℕ), w.rotate n = cons x e w' ∧ w'.first = y

theorem WList.IsClosed.exists_first_of_isLink {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (hC : w.IsClosed) (he : w.IsLink e x y) : ∃ (w' : WList α β), w.edgeSet = (cons x e w').edgeSet ∧ w'.first = y

def WList.intRotate {α : Type u_1} {β : Type u_2} (w : WList α β) (n : ℤ) : WList α β

Rotate by an integer amount.

Equations

• w.intRotate n = w.rotate (n.natMod ↑w.length)

@[simp]

theorem WList.length_intRotate {α : Type u_1} {β : Type u_2} (w : WList α β) (m : ℤ) : (w.intRotate m).length = w.length

@[simp]

theorem WList.intRotate_zero {α : Type u_1} {β : Type u_2} {w : WList α β} : w.intRotate 0 = w

@[simp]

theorem WList.nil_intRotate {α : Type u_1} {β : Type u_2} (x : α) (n : ℤ) : (nil x).intRotate n = nil x

theorem WList.IsClosed.intRotate_eq_rotate {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) (n : ℕ) : w.intRotate ↑n = w.rotate n

theorem WList.IsClosed.intRotate_intRotate {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) (m n : ℤ) : (w.intRotate m).intRotate n = w.intRotate (m + n)

Nasty proof.

theorem WList.IsClosed.rotate_intRotate_neg {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.IsClosed) (n : ℕ) : (w.rotate n).intRotate (-↑n) = w

theorem WList.IsClosed.dInc_intRotate {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} (hw : w.IsClosed) (n : ℤ) (h : w.DInc e x y) : (w.intRotate n).DInc e x y

@[simp]

theorem WList.IsClosed.dInc_rotate_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} {n : ℕ} (hw : w.IsClosed) : (w.rotate n).DInc e x y ↔ w.DInc e x y

@[simp]

theorem WList.IsClosed.isLink_rotate_iff {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {w : WList α β} {n : ℕ} (hw : w.IsClosed) : (w.rotate n).IsLink e x y ↔ w.IsLink e x y

theorem WList.WellFormed.rotate {α : Type u_1} {β : Type u_2} {w : WList α β} (hw : w.WellFormed) (h_closed : w.IsClosed) (n : ℕ) : (w.rotate n).WellFormed

@[simp]

theorem WList.IsClosed.wellFormed_rotate_iff {α : Type u_1} {β : Type u_2} {w : WList α β} {n : ℕ} (h_closed : w.IsClosed) : (w.rotate n).WellFormed ↔ w.WellFormed