Decidability of Relation.ReflTransGen on a finite carrier

Reachability along a relation whose successors lie in a finite set is decidable: close {a} under the successor function until it stops growing, and test membership. Mathlib has the analogue for finite simple graphs (SimpleGraph.Reachable), not for an arbitrary relation.

Main declarations

• Finset.isFixedPt_iterate_card: an inflationary operation on the subsets of a finite set u reaches a fixed point within u.card iterations.
• Function.exists_lt_card_iterate_eq: on a finite type, every point of a forward orbit is reached within card α iterations.
• Relation.ReflTransGen.reach, mem_reach_iff: the set reached from a node, and its characterization.
• decidable_of_finset_step and its wrappers for a list-valued successor function, a decidable relation with a bounding list, and a Fintype carrier; the TransGen siblings; and the two DecidableRel instances over a Fintype.
• total_of_left_unique, of_forall_exists, exists_boundary: order-theoretic facts about the closure.
• partialOrderOfCovers, linearOrderOfCovers, decidableLEOfCovers: the order generated by a relation of immediate subsumption whose edges decrease a rank, and its decidability.
• Relation.reflTransGen_iff_reachIn, decidableLEOfRank: along edges that decrease a natural-number rank, reachability is a search to the depth of the rank.
• Relation.transGen_iff_mem_iterate, decidable_TransGen_of_option: reachability along a partial function is decided by iterating it, with no closure computation.

Implementation notes

reach iterates one round of closure (insert a u).card times without testing for the fixed point, so that by decide evaluates a plain Nat.iterate. The bound comes from cardinality alone: a strictly growing chain of subsets of a finite set is no longer than the set.

theorem Finset.isFixedPt_iterate_card {α : Type u} {f : Finset α → Finset α} {u S : Finset α} (hf : ∀ (T : Finset α), T ⊆ f T) (hu : ∀ T ⊆ u, f T ⊆ u) (hS : S ⊆ u) : Function.IsFixedPt f (f^[u.card] S)

An inflationary operation on the subsets of a finite set reaches a fixed point after as many iterations as the set has elements.

theorem Function.exists_lt_card_iterate_eq {α : Type u} [Fintype α] {f : α → α} {a b : α} {n : ℕ} (h : f^[n] a = b) : ∃ m < Fintype.card α, f^[m] a = b

On a finite type, a point of the forward orbit of a is reached within card α iterations, since a longer path repeats a point and can be shortened.

def Relation.ReflTransGen.closeStep {α : Type u} [DecidableEq α] (step : α → Finset α) (S : Finset α) : Finset α

One round of closing a set under a successor function.

Equations

• Relation.ReflTransGen.closeStep step S = S ∪ S.biUnion step

def Relation.ReflTransGen.reach {α : Type u} [DecidableEq α] (step : α → Finset α) (s : Finset α) (a : α) : Finset α

The nodes reached from a along step, when every successor lies in the finite set s.

Equations

• Relation.ReflTransGen.reach step s a = (Relation.ReflTransGen.closeStep step)^[(insert a s).card] {a}

theorem Relation.ReflTransGen.of_mem_iterate_closeStep {α : Type u} [DecidableEq α] {step : α → Finset α} {a : α} (n : ℕ) {b : α} : b ∈ (closeStep step)^[n] {a} → ReflTransGen (fun (x y : α) => y ∈ step x) a b

theorem Relation.ReflTransGen.mem_reach_iff {α : Type u} [DecidableEq α] {step : α → Finset α} {s : Finset α} {a b : α} (hs : ∀ (x : α), step x ⊆ s) : b ∈ reach step s a ↔ ReflTransGen (fun (x y : α) => y ∈ step x) a b

Decidability

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)

Relation.ReflTransGen r is decidable when r has a finset-valued successor function whose values lie in a finite set.

Equations

• Relation.ReflTransGen.decidable_of_finset_step step s step_eq step_in_s a b = decidable_of_iff (b ∈ Relation.ReflTransGen.reach step s a) ⋯

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)

Relation.TransGen r is decidable under the hypotheses of decidable_of_finset_step, as a first step followed by reachability.

Equations

• Relation.ReflTransGen.decidable_TransGen_of_finset_step step s step_eq step_in_s a b = decidable_of_iff (∃ c ∈ step a, b ∈ Relation.ReflTransGen.reach step s c) ⋯

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)

The list-valued form of decidable_of_finset_step.

Equations

• Relation.ReflTransGen.decidable_of_finite_step step s step_eq step_in_s a b = Relation.ReflTransGen.decidable_of_finset_step (fun (a : α) => (step a).toFinset) s.toFinset ⋯ ⋯ a b

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)

Relation.ReflTransGen r is decidable when r is decidable and its successors lie in a list.

Equations

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

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

Relation.ReflTransGen r is decidable on a Fintype given a finset-valued successor function.

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_TransGen_of_fintype_step {α : Type u} [DecidableEq α] {r : α → α → Prop} [Fintype α] (step : α → Finset α) (step_eq : ∀ (a b : α), r a b ↔ b ∈ step a) (a b : α) : Decidable (TransGen r a b)

Relation.TransGen r is decidable on a Fintype given a finset-valued successor function.

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_of_fintype {α : Type u} [DecidableEq α] {r : α → α → Prop} [Fintype α] [DecidableRel r] (a b : α) : Decidable (ReflTransGen r a b)

Relation.ReflTransGen r is decidable on a Fintype when r is.

Equations

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

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

Relation.TransGen r is decidable on a Fintype when r is.

Equations

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

@[instance_reducible]

instance Relation.ReflTransGen.instDecidableRel_linglib {α : Type u} [DecidableEq α] {r : α → α → Prop} [Fintype α] [DecidableRel r] : DecidableRel (ReflTransGen r)

Reachability on a Fintype is decidable, the analogue for a relation of mathlib's DecidableRel G.Reachable for finite simple graphs. Concrete decides over this instance may need +kernel.

Equations

• Relation.ReflTransGen.instDecidableRel_linglib = Relation.ReflTransGen.decidable_of_fintype

@[instance_reducible]

instance Relation.ReflTransGen.instDecidableRelTransGen_linglib {α : Type u} [DecidableEq α] {r : α → α → Prop} [Fintype α] [DecidableRel r] : DecidableRel (TransGen r)

Equations

• Relation.ReflTransGen.instDecidableRelTransGen_linglib = Relation.ReflTransGen.decidable_TransGen_of_fintype

The closure of an acyclic relation as an order

theorem Relation.ReflTransGen.total_of_left_unique {α : Type u} {r : α → α → Prop} (U : Relator.LeftUnique r) {a b c : α} (ac : ReflTransGen r a c) (bc : ReflTransGen r b c) : ReflTransGen r a b ∨ ReflTransGen r b a

Over a left-unique relation, positions reaching a common target are comparable, dually to Relation.ReflTransGen.total_of_right_unique.

theorem Relation.ReflTransGen.of_forall_exists {α : Type u} [Finite α] {r : α → α → Prop} (hirr : ∀ (v : α), ¬TransGen r v v) {a : α} (h : ∀ (v : α), v ≠ a → ∃ (u : α), r u v) (v : α) : ReflTransGen r a v

On a finite carrier, if the relation is acyclic and every element other than a has a predecessor, then a reaches everything.

Crossing a boundary

theorem Relation.ReflTransGen.exists_boundary {α : Type u} {r : α → α → Prop} {S : Set α} {a b : α} (h : ReflTransGen r a b) (ha : a ∈ S) (hb : b ∉ S) : ∃ (c : α) (d : α), r c d ∧ c ∈ S ∧ d ∉ S ∧ ReflTransGen r a c ∧ ReflTransGen r d b

A reflexive-transitive path from inside S to outside it crosses the boundary at a single step, the source reaching the exit and the entry reaching the target — the Relation.ReflTransGen analogue of SimpleGraph.Walk.exists_boundary_dart.

Reachability along a partial function

theorem Relation.transGen_iff_exists_iterate {α : Type u} {f : α → Option α} {a b : α} : TransGen (fun (a b : α) => b ∈ f a) a b ↔ ∃ (n : ℕ), (fun (x : Option α) => x.bind f)^[n] (f a) = some b

Reachability along a partial function is reachability by its iterates on Option α.

theorem Relation.transGen_iff_mem_iterate {α : Type u} {f : α → Option α} {a b : α} [Fintype α] : TransGen (fun (a b : α) => b ∈ f a) a b ↔ some b ∈ List.iterate (fun (x : Option α) => x.bind f) (f a) (Fintype.card (Option α))

On a finite carrier, reachability along a partial function is reachability within card (Option α) iterations.

def Relation.ReflTransGen.decidable_TransGen_of_option {α : Type u} [Fintype α] [DecidableEq α] (f : α → Option α) (a b : α) : Decidable (TransGen (fun (a b : α) => b ∈ f a) a b)

Reachability along a partial function on a Fintype is decidable by iterating the function, in time linear in the carrier, where decidable_TransGen_of_fintype closes a set.

Equations

• Relation.ReflTransGen.decidable_TransGen_of_option f a b = decidable_of_iff (some b ∈ List.iterate (fun (x : Option α) => x.bind f) (f a) (Fintype.card (Option α))) ⋯

theorem Finite.wellFounded_of_irrefl_transGen {α : Type u_1} [Finite α] {r : α → α → Prop} (h : ∀ (a : α), ¬Relation.TransGen r a a) : WellFounded r

On a finite carrier, a relation whose transitive closure is irreflexive is well founded.

The order generated by immediate subsumption

theorem Relation.ReflTransGen.rank_le {α : Type u_1} {β : Type u_2} [Preorder β] {covers : α → α → Prop} {rank : α → β} (hrank : ∀ (a b : α), covers a b → rank b < rank a) {a b : α} (hab : ReflTransGen covers a b) : rank b ≤ rank a

A path along edges that decrease a rank does not increase it.

theorem Relation.ReflTransGen.eq_of_rank_le {α : Type u_1} {β : Type u_2} [Preorder β] {covers : α → α → Prop} {rank : α → β} (hrank : ∀ (a b : α), covers a b → rank b < rank a) {a b : α} (hab : ReflTransGen covers a b) (h : rank a ≤ rank b) : a = b

A path along edges that decrease a rank, ending no lower than it starts, is trivial.

@[reducible]

def partialOrderOfCovers {α : Type u_1} {β : Type u_2} [Preorder β] (covers : α → α → Prop) (rank : α → β) (hrank : ∀ (a b : α), covers a b → rank b < rank a) : PartialOrder α

The partial order whose ≤ is the reflexive transitive closure of covers, given a rank that every covers edge strictly decreases.

Equations

• partialOrderOfCovers covers rank hrank = { le := Relation.ReflTransGen covers, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[reducible]

def decidableLEOfCovers {α : Type u_1} {covers : α → α → Prop} [DecidableEq α] [DecidableRel covers] (allSorts : List α) (complete : ∀ (a b : α), covers a b → b ∈ allSorts) (a b : α) : Decidable (Relation.ReflTransGen covers a b)

The order of partialOrderOfCovers is decidable when allSorts lists every target of a covers edge.

Equations

• decidableLEOfCovers allSorts complete a b = Relation.ReflTransGen.decidable_of_finite allSorts complete a b

def Relation.reachIn {α : Type u_1} [DecidableEq α] (step : α → List α) : ℕ → α → α → Bool

Whether b is reachable from a in at most n steps along the successor lists step.

Equations

• Relation.reachIn step 0 x✝¹ x✝ = (x✝¹ == x✝)
• Relation.reachIn step n.succ x✝¹ x✝ = (x✝¹ == x✝ || (step x✝¹).any fun (c : α) => Relation.reachIn step n c x✝)

theorem Relation.reflTransGen_iff_reachIn {α : Type u_1} {covers : α → α → Prop} [DecidableEq α] {step : α → List α} {rank : α → ℕ} (hstep : ∀ (a b : α), covers a b ↔ b ∈ step a) (hrank : ∀ (a b : α), covers a b → rank b < rank a) {n : ℕ} {a b : α} (h : rank a ≤ n) : ReflTransGen covers a b ↔ reachIn step n a b = true

Along edges that decrease a natural-number rank, b is reachable from a exactly when it is reachable within rank a steps.

@[reducible]

def decidableLEOfRank {α : Type u_1} {covers : α → α → Prop} [DecidableEq α] (step : α → List α) (rank : α → ℕ) (hstep : ∀ (a b : α), covers a b ↔ b ∈ step a) (hrank : ∀ (a b : α), covers a b → rank b < rank a) (a b : α) : Decidable (Relation.ReflTransGen covers a b)

The order of partialOrderOfCovers is decidable, for edges listed by step and a natural-number rank, by searching from a to the depth of its rank.

Equations

• decidableLEOfRank step rank hstep hrank a b = decidable_of_iff (Relation.reachIn step (rank a) a b = true) ⋯

@[reducible]

def linearOrderOfCovers {α : Type u_1} {β : Type u_2} [Preorder β] [Fintype α] [DecidableEq α] (covers : α → α → Prop) [DecidableRel covers] (rank : α → β) (hrank : ∀ (a b : α), covers a b → rank b < rank a) (htotal : ∀ (a b : α), Relation.ReflTransGen covers a b ∨ Relation.ReflTransGen covers b a) : LinearOrder α

The linear order whose ≤ is the reflexive transitive closure of covers, for a relation whose closure is total and which a rank strictly decreases along.

Equations

• One or more equations did not get rendered due to their size.