Paths along a relation

Facts about Relation.TransGen, and about walks: paths that record the vertex each of their edges leaves from.

They live in Cedar.Relation rather than Relation, like the Mathlib copies in Cedar.List, so that a file can import both Cedar and Mathlib.

theorem Cedar.Relation.transGen_head {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : Relation.TransGen r a b) : ∃ (c : α), r a c

A path starts with an edge.

theorem Cedar.Relation.transGen_tail {α : Sort u_1} {r : α → α → Prop} {a b : α} (h : Relation.TransGen r a b) : ∃ (c : α), r c b

A path ends with an edge.

theorem Cedar.Relation.transGen_mono {α : Sort u_1} {r s : α → α → Prop} (hrs : ∀ (a b : α), r a b → s a b) {a b : α} (h : Relation.TransGen r a b) : Relation.TransGen s a b

A path stays a path along a larger relation.

inductive Cedar.Relation.Walk {α : Type u_1} (edge : α → α → Prop) : α → α → List α → Prop

A path along edge from x to y whose edges leave from srcs, in order.

• single {α : Type u_1} {edge : α → α → Prop} {x y : α} : edge x y → Walk edge x y [x]
• cons {α : Type u_1} {edge : α → α → Prop} {x z y : α} {srcs : List α} : edge x z → Walk edge z y srcs → Walk edge x y (x :: srcs)

theorem Cedar.Relation.Walk.append {α : Type u_1} {edge : α → α → Prop} {x y z : α} {s₁ s₂ : List α} (h₁ : Walk edge x y s₁) (h₂ : Walk edge y z s₂) : Walk edge x z (s₁ ++ s₂)

Walks compose.

theorem Cedar.Relation.Walk.of_transGen {α : Type u_1} {edge : α → α → Prop} {x y : α} (h : Relation.TransGen edge x y) : ∃ (srcs : List α), Walk edge x y srcs

Every path is a walk.

theorem Cedar.Relation.Walk.source_edge {α : Type u_1} {edge : α → α → Prop} {x y : α} {srcs : List α} (h : Walk edge x y srcs) (v : α) : v ∈ srcs → ∃ (w : α), edge v w

Every vertex a walk leaves from has an edge.

theorem Cedar.Relation.Walk.suffix {α : Type u_1} {edge : α → α → Prop} {x y v : α} {srcs : List α} (h : Walk edge x y srcs) (hv : v ∈ srcs) : ∃ (srcs' : List α), srcs' <:+ srcs ∧ Walk edge v y srcs'

A walk through v continues from v along a suffix of its sources.

theorem Cedar.Relation.Walk.nodup {α : Type u_1} {edge : α → α → Prop} {x y : α} {srcs : List α} (h : Walk edge x y srcs) : ∃ (srcs' : List α), srcs'.Nodup ∧ srcs' ⊆ srcs ∧ Walk edge x y srcs'

Every walk can be shortened to one that leaves from each vertex at most once.