Grace/Cumulus/GraphTheory/Reachability.g17

Open in Workbench Download source

Imports

Complement · Set.Core

Declarations

• nextNeighbors def
• reachableWithin def
• reachableWithin.zero theorem derivation
• reachableWithin.successor theorem derivation
• reachableWithin.monotone theorem derivation
• reachableWithin.source theorem derivation
• reachableWithin.advance theorem derivation
• Reachable predicate
• Reachable.reflexive theorem derivation
• Reachable.of_edge theorem derivation

Source

1-- Bounded reachability as sets of vertices.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.GraphTheory.Reachability8import Complement9import Set.Core1011-- AtMost n contains vertices reachable in at most n edges.  The successor12-- set is bounded by V, so recursion stays within mainstream set theory.13def nextNeighbors (V E A : Set) : Set :=14  { y ∈ V | ∃ z ∈ A, Adjacent(E, z, y) }1516def reachableWithin (V E x : Set, n : Nat) → Set17  | V, E, x, zero => {x}18  | V, E, x, succ(n) =>19    reachableWithin(V, E, x, n) ∪ nextNeighbors(V, E, reachableWithin(V, E, x, n))2021theorem reachableWithin.zero (V E x : Set)22  shows reachableWithin(V, E, x, 0) = {x}23proof24  unfold reachableWithin25  rfl2627theorem reachableWithin.successor (V E x : Set, n : Nat)28  shows reachableWithin(V, E, x, succ(n)) =29    reachableWithin(V, E, x, n) ∪ nextNeighbors(V, E, reachableWithin(V, E, x, n))30proof31  unfold reachableWithin32  rfl3334theorem reachableWithin.monotone (V E x : Set, n : Nat)35  shows reachableWithin(V, E, x, n) ⊆ reachableWithin(V, E, x, succ(n))36proof37  rw reachableWithin.successor38  exact union2.subset_left3940theorem reachableWithin.source (V E x : Set, n : Nat)41  shows x ∈ reachableWithin(V, E, x, n)42proof43  induction n44  | zero =>45    rw reachableWithin.zero46    apply singleton.membership.backward47    rfl48  | succ(k) using ih =>49    rw reachableWithin.successor50    apply union2.membership.backward51    left52    exact ih5354theorem reachableWithin.advance (V E x y z : Set, n : Nat)55  requires reached : y ∈ reachableWithin(V, E, x, n)56  requires hz : z ∈ V57  requires edge : Adjacent(E, y, z)58  shows z ∈ reachableWithin(V, E, x, succ(n))59proof60  rw reachableWithin.successor61  apply union2.right62  exact nextNeighbors.membership.backward with ⟨hz, y, reached, edge⟩6364predicate Reachable (V E x y : Set) :=65  ∃ n ∈ ℕ, y ∈ reachableWithin(V, E, x, n)6667theorem Reachable.reflexive (V E x : Set)68  shows Reachable(V, E, x, x)69proof70  unfold Reachable71  have source := reachableWithin.source at V, E, x, 0 with Naturals.constructor.zero72  have zeroNat := nat.omega.forward with Naturals.constructor.zero73  refine ⟨0, zeroNat, source⟩7475theorem Reachable.of_edge (V E x y : Set)76  requires hy : y ∈ V77  requires edge : Adjacent(E, x, y)78  shows Reachable(V, E, x, y)79proof80  unfold Reachable81  have source := reachableWithin.source at V, E, x, 0 with Naturals.constructor.zero82  have reached := reachableWithin.advance with Naturals.constructor.zero, source, hy, edge83  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero84  have oneInOmega := nat.omega.forward with oneNat85  refine ⟨1, oneInOmega, reached⟩86