Reachability in a finite type

To decide ◃⁺ we compute, for a decidable relation on a finite type, the set of all elements reachable in at least one step. Because reachStep only grows sets, after Fintype.card α iterations we must have reached a fixed point, which then is exactly the set of Relation.TransGen-successors.

def FinReach.reachStep {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (s : Finset α) : Finset α

One step of computing the set of elements reachable via r.

Equations

• FinReach.reachStep r s = s ∪ {b : α | ∃ a ∈ s, r a b}

def FinReach.reachSet {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (a : α) : Finset α

The set of all elements reachable from a in at least one r-step.

Equations

• FinReach.reachSet r a = (FinReach.reachStep r)^[Fintype.card α] {b : α | r a b}

theorem FinReach.subset_reachStep {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (s : Finset α) : s ⊆ reachStep r s

theorem FinReach.reachStep_iterate_mono {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (s : Finset α) {m n : ℕ} (h : m ≤ n) : (reachStep r)^[m] s ⊆ (reachStep r)^[n] s

theorem FinReach.reachStep_iterate_eq_of_eq {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (s : Finset α) {m : ℕ} (h : (reachStep r)^[m + 1] s = (reachStep r)^[m] s) (k : ℕ) : m ≤ k → (reachStep r)^[k] s = (reachStep r)^[m] s

As soon as the iteration stops growing it stays the same forever.

theorem FinReach.card_le_card_iterate {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (s : Finset α) (n : ℕ) : (∀ m < n, (reachStep r)^[m + 1] s ≠ (reachStep r)^[m] s) → n ≤ ((reachStep r)^[n] s).card

As long as the iteration is still growing it gains at least one element per step.

theorem FinReach.reachStep_iterate_card_fixed {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (s : Finset α) : reachStep r ((reachStep r)^[Fintype.card α] s) = (reachStep r)^[Fintype.card α] s

After Fintype.card α steps the iteration has reached a fixed point.

theorem FinReach.transGen_of_mem_iterate {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (a : α) (n : ℕ) (b : α) : b ∈ (reachStep r)^[n] {b : α | r a b} → Relation.TransGen r a b

theorem FinReach.mem_reachSet_iff {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (a b : α) : b ∈ reachSet r a ↔ Relation.TransGen r a b

The transitive closure of r is computed by reachSet.

def FinReach.decidableTransGen {α : Type u_1} [Fintype α] [DecidableEq α] (r : α → α → Prop) [DecidableRel r] (a b : α) : Decidable (Relation.TransGen r a b)

The transitive closure of a decidable relation on a finite type is decidable.

Equations

• FinReach.decidableTransGen r a b = decidable_of_iff (b ∈ FinReach.reachSet r a) ⋯