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.
• 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, antisymm_of_irrefl_transGen, 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.

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.

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: a first step, then 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

The dual of Relation.ReflTransGen.total_of_right_unique: over a left-unique relation, positions reaching a common target are comparable.

theorem Relation.ReflTransGen.antisymm_of_irrefl_transGen {α : Type u} {r : α → α → Prop} (h : ∀ (a : α), ¬TransGen r a a) {a b : α} (hab : ReflTransGen r a b) (hba : ReflTransGen r b a) : a = b

The reflexive-transitive closure of a relation whose transitive closure is irreflexive is antisymmetric.

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.

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

@[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.