Decidability of Relation.ReflTransGen on a finite carrier

Generic substrate: given a relation r : α → α → Prop whose successors lie in some finite list s : List α, derive Decidable (Relation.ReflTransGen r a b) via path compression.

Construction

A Path r a chain b is a list of intermediates [c₁, …, cₖ] with r a c₁ ∧ r c₁ c₂ ∧ … ∧ r cₖ b. The empty chain [] witnesses a direct edge r a b. Then:

1. ReflTransGen r a b is equivalent to a = b or the existence of some Path r a chain b (ReflTransGen.eq_or_path).
2. Any Path reduces to one whose intermediates are pairwise distinct and contain neither a nor b (Path.compress).
3. A compressed Path has length < s.length by List.Subperm.
4. Hence reachability is decidable via bounded BFS at fuel s.length.

Naming

Path is named to match Quiver.Path / SimpleGraph.Walk-style naming. It is distinct from List.Chain' (which is a relation between consecutive list elements without fixed endpoints).

Provenance

Lifted from Core/Inheritance/Basic.lean where it was first proved for Hudson's Word Grammar IsA relation. Generalised to be reusable across Network.IsA, CausalGraph.IsAncestor, SDRT.availableViaChain.

def Relation.ReflTransGen.Path {α : Type u} (r : α → α → Prop) (a : α) : List α → α → Prop

A chain of intermediate nodes [c₁, c₂, …, cₖ] witnesses a → c₁ → c₂ → … → cₖ → b via r-steps. The empty chain [] witnesses a direct edge r a b.

Distinct from List.Chain': Path r a chain b pins the source a and target b; List.Chain' r l does not.

Equations

• Relation.ReflTransGen.Path r a [] x✝ = r a x✝
• Relation.ReflTransGen.Path r a (x_2 :: xs) x✝ = (r a x_2 ∧ Relation.ReflTransGen.Path r x_2 xs x✝)

@[simp]

theorem Relation.ReflTransGen.Path.cons_iff {α : Type u} {r : α → α → Prop} (a x b : α) (xs : List α) : Path r a (x :: xs) b ↔ r a x ∧ Path r x xs b

@[simp]

theorem Relation.ReflTransGen.Path.nil_iff {α : Type u} {r : α → α → Prop} (a b : α) : Path r a [] b ↔ r a b

theorem Relation.ReflTransGen.Path.toReflTransGen {α : Type u} {r : α → α → Prop} {a b : α} {chain : List α} : Path r a chain b → ReflTransGen r a b

A path realises ReflTransGen.

theorem Relation.ReflTransGen.Path.congr {α : Type u} {r r' : α → α → Prop} (h : ∀ (x y : α), r x y ↔ r' x y) {a b : α} {chain : List α} : Path r a chain b ↔ Path r' a chain b

Path is monotonic in the relation: pointwise iff lifts to path iff.

theorem Relation.ReflTransGen.Path.snoc {α : Type u} {r : α → α → Prop} {a b c : α} {chain : List α} : Path r a chain b → r b c → Path r a (chain ++ [b]) c

Extend a path by one edge at the END.

theorem Relation.ReflTransGen.eq_or_path {α : Type u} {r : α → α → Prop} {a b : α} (h : ReflTransGen r a b) : a = b ∨ ∃ (chain : List α), Path r a chain b

ReflTransGen r a b decomposes either as a = b or as a Path.

theorem Relation.ReflTransGen.Path.truncate_at_target {α : Type u} {r : α → α → Prop} {a b : α} {chain : List α} : Path r a chain b → b ∈ chain → ∃ (chain' : List α), chain'.length < chain.length ∧ Path r a chain' b

Compression (right-truncation): if b appears in the chain, take the prefix ending at its first occurrence.

theorem Relation.ReflTransGen.Path.suffix_from {α : Type u} {r : α → α → Prop} {x b : α} (y : α) {chain : List α} : Path r x chain b → y ∈ chain → ∃ (tail : List α), tail.length < chain.length ∧ Path r y tail b

Helper: if a chain Path r x chain b contains y, the suffix from y's first occurrence is itself a chain Path r y _ b.

theorem Relation.ReflTransGen.Path.skip_to_self {α : Type u} {r : α → α → Prop} {a b : α} {chain : List α} (h : Path r a chain b) (ha_in : a ∈ chain) : ∃ (chain' : List α), chain'.length < chain.length ∧ Path r a chain' b

Compression (skip-to-self): if a appears in the chain, take the suffix from its reappearance.

theorem Relation.ReflTransGen.Path.dedup_interior {α : Type u} {r : α → α → Prop} {a b : α} {chain : List α} : Path r a chain b → ¬chain.Nodup → ∃ (chain' : List α), chain'.length < chain.length ∧ Path r a chain' b

Compression (interior duplication): if some node appears twice in the chain, splice out the cycle.

theorem Relation.ReflTransGen.Path.compress_aux {α : Type u} [DecidableEq α] {r : α → α → Prop} {a b : α} (n : ℕ) (chain : List α) : chain.length = n → Path r a chain b → ∃ (chain' : List α), Path r a chain' b ∧ chain'.Nodup ∧ a ∉ chain' ∧ b ∉ chain'

Strong-induction helper for Path.compress. The explicit length parameter threads chain-length through Nat.strongRecOn. Public so external callers that already have a Nat-bound on the chain in hand can avoid Path.compress's implicit chain.length evaluation; in practice all uses go through compress.

theorem Relation.ReflTransGen.Path.compress {α : Type u} [DecidableEq α] {r : α → α → Prop} {a b : α} {chain : List α} (h : Path r a chain b) : ∃ (chain' : List α), Path r a chain' b ∧ chain'.Nodup ∧ a ∉ chain' ∧ b ∉ chain'

Chain compression: any path reduces to one with no repeats whose intermediates are disjoint from {a, b}.

theorem Relation.ReflTransGen.Path.intermediates_satisfy {α : Type u} {r : α → α → Prop} {a b : α} {P : α → Prop} (succ_satisfies : ∀ (x y : α), r x y → P y) {chain : List α} : Path r a chain b → ∀ y ∈ chain, P y

All intermediates of a path satisfy any predicate that holds of r-successors. Stated abstractly so it specialises to both List and Finset universes.

theorem Relation.ReflTransGen.Path.endpoint_satisfies {α : Type u} {r : α → α → Prop} {a b : α} {P : α → Prop} (succ_satisfies : ∀ (x y : α), r x y → P y) {chain : List α} : Path r a chain b → P b

The endpoint of a path satisfies any predicate that holds of r-successors.

theorem Relation.ReflTransGen.Path.intermediates_subset {α : Type u} {r : α → α → Prop} {a b : α} {s : List α} (succ_in_s : ∀ (x y : α), r x y → y ∈ s) {chain : List α} (h : Path r a chain b) (y : α) (hy : y ∈ chain) : y ∈ s

List specialisation of Path.intermediates_satisfy with P := (· ∈ s).

theorem Relation.ReflTransGen.Path.endpoint_mem {α : Type u} {r : α → α → Prop} {a b : α} {s : List α} (succ_in_s : ∀ (x y : α), r x y → y ∈ s) {chain : List α} (h : Path r a chain b) : b ∈ s

List specialisation of Path.endpoint_satisfies with P := (· ∈ s).

theorem Relation.ReflTransGen.Path.length_lt_of_nodup {α : Type u} [DecidableEq α] {r : α → α → Prop} {a b : α} {s : List α} (succ_in_s : ∀ (x y : α), r x y → y ∈ s) {chain : List α} (h : Path r a chain b) (hnodup : chain.Nodup) (hb_notin : b ∉ chain) : chain.length < s.length

Length bound: a Nodup path with b not in the chain is bounded by the size of any successor-closed list.

def Relation.ReflTransGen.decidable_of_finite_step {α : Type u} [DecidableEq α] {r : α → α → Prop} (step : α → List α) (s : List α) (step_eq : ∀ (a b : α), r a b ↔ b ∈ step a) (step_in_s : ∀ (a b : α), b ∈ step a → b ∈ s) (a b : α) : Decidable (ReflTransGen r a b)

Decidability of Relation.ReflTransGen on a finite carrier, given an explicit step function and a successor-bound list s.

Equations

• Relation.ReflTransGen.decidable_of_finite_step step s step_eq step_in_s a b = decidable_of_iff (a = b ∨ b ∈ Relation.ReflTransGen.stepBFS✝ step a s.length) ⋯

def Relation.ReflTransGen.decidable_of_finite {α : Type u} [DecidableEq α] {r : α → α → Prop} [DecidableRel r] (s : List α) (succ_in_s : ∀ (a b : α), r a b → b ∈ s) (a b : α) : Decidable (ReflTransGen r a b)

Decidability of Relation.ReflTransGen on a finite carrier, derived from a [DecidableRel r] instance and a successor-bound list. A convenience wrapper around decidable_of_finite_step for callers that have r decidable but no natural step function.

Equations

• Relation.ReflTransGen.decidable_of_finite s succ_in_s a b = Relation.ReflTransGen.decidable_of_finite_step (fun (a : α) => List.filter (fun (b : α) => decide (r a b)) s) s ⋯ ⋯ a b

The List-based API above suits callers whose universe is naturally a List α (e.g., Network.nodeUniverse derived from links via .dedup). The Finset variants below suit callers whose universe is a Finset α (e.g., CausalGraph.parents : V → Finset V with [Fintype V]). The shared mathematical content (Path, compression, length_lt_of_nodup) applies to both — only the BFS engine and the headline iff differ.

theorem Relation.ReflTransGen.Path.length_lt_of_nodup_finset {α : Type u} [DecidableEq α] {r : α → α → Prop} {a b : α} {s : Finset α} (succ_in_s : ∀ (x y : α), r x y → y ∈ s) {chain : List α} (h : Path r a chain b) (hnodup : chain.Nodup) (hb_notin : b ∉ chain) : chain.length < s.card

Finset length-bound variant. Goes through List.toFinset (computable since List.dedup is computable) and Finset.card_le_card.

def Relation.ReflTransGen.decidable_of_finset_step {α : Type u} [DecidableEq α] {r : α → α → Prop} (step : α → Finset α) (s : Finset α) (step_eq : ∀ (a b : α), r a b ↔ b ∈ step a) (step_in_s : ∀ (a b : α), b ∈ step a → b ∈ s) (a b : α) : Decidable (ReflTransGen r a b)

Decidability of Relation.ReflTransGen on a Finset-bounded carrier, given an explicit Finset-valued step function.

Equations

• Relation.ReflTransGen.decidable_of_finset_step step s step_eq step_in_s a b = decidable_of_iff (a = b ∨ b ∈ Relation.ReflTransGen.finsetBFS✝ step a s.card) ⋯

def Relation.ReflTransGen.decidable_of_fintype_step {α : Type u} [Fintype α] [DecidableEq α] {r : α → α → Prop} (step : α → Finset α) (step_eq : ∀ (a b : α), r a b ↔ b ∈ step a) (a b : α) : Decidable (ReflTransGen r a b)

Decidability of Relation.ReflTransGen on a [Fintype] carrier — the convenience headline most callers want. Takes no explicit universe; uses Finset.univ as the bound.

Equations

• Relation.ReflTransGen.decidable_of_fintype_step step step_eq a b = Relation.ReflTransGen.decidable_of_finset_step step Finset.univ step_eq ⋯ a b

def Relation.ReflTransGen.decidable_of_fintype {α : Type u} [Fintype α] [DecidableEq α] {r : α → α → Prop} [DecidableRel r] (a b : α) : Decidable (ReflTransGen r a b)

Decidability of Relation.ReflTransGen on a [Fintype] carrier given only a [DecidableRel r] instance. The convenience parallel to mathlib's SimpleGraph.Reachable.decidable.

Equations

• Relation.ReflTransGen.decidable_of_fintype a b = Relation.ReflTransGen.decidable_of_fintype_step (fun (a : α) => {b : α | decide (r a b) = true}) ⋯ a b

theorem Relation.TransGen.exists_path {α : Type u} {r : α → α → Prop} {a b : α} (h : TransGen r a b) : ∃ (chain : List α), ReflTransGen.Path r a chain b

TransGen r a b decomposes as a Path (one or more edges).

theorem Relation.ReflTransGen.Path.toTransGen {α : Type u} {r : α → α → Prop} {a b : α} {chain : List α} : Path r a chain b → TransGen r a b

A Path realises TransGen (always at least one edge).

def Relation.ReflTransGen.decidable_TransGen_of_finset_step {α : Type u} [DecidableEq α] {r : α → α → Prop} (step : α → Finset α) (s : Finset α) (step_eq : ∀ (a b : α), r a b ↔ b ∈ step a) (step_in_s : ∀ (a b : α), b ∈ step a → b ∈ s) (a b : α) : Decidable (TransGen r a b)

Decidability of Relation.TransGen on a Finset-bounded carrier.

Equations

• Relation.ReflTransGen.decidable_TransGen_of_finset_step step s step_eq step_in_s a b = decidable_of_iff (b ∈ Relation.ReflTransGen.finsetBFS✝ step a s.card) ⋯

def Relation.ReflTransGen.decidable_TransGen_of_fintype_step {α : Type u} [Fintype α] [DecidableEq α] {r : α → α → Prop} (step : α → Finset α) (step_eq : ∀ (a b : α), r a b ↔ b ∈ step a) (a b : α) : Decidable (TransGen r a b)

Decidability of Relation.TransGen on a [Fintype] carrier.

Equations

• Relation.ReflTransGen.decidable_TransGen_of_fintype_step step step_eq a b = Relation.ReflTransGen.decidable_TransGen_of_finset_step step Finset.univ step_eq ⋯ a b

def Relation.ReflTransGen.decidable_TransGen_of_fintype {α : Type u} [Fintype α] [DecidableEq α] {r : α → α → Prop} [DecidableRel r] (a b : α) : Decidable (TransGen r a b)

Decidability of Relation.TransGen on a [Fintype] carrier given [DecidableRel r].

Equations

• Relation.ReflTransGen.decidable_TransGen_of_fintype a b = Relation.ReflTransGen.decidable_TransGen_of_fintype_step (fun (a : α) => {b : α | decide (r a b) = true}) ⋯ a b