-- Bounded reachability as sets of vertices.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.GraphTheory.Reachability
import Complement
import Set.Core

-- AtMost n contains vertices reachable in at most n edges.  The successor
-- set is bounded by V, so recursion stays within mainstream set theory.
def nextNeighbors (V E A : Set) : Set :=
  { y ∈ V | ∃ z ∈ A, Adjacent(E, z, y) }

def reachableWithin (V E x : Set, n : Nat) → Set
  | V, E, x, zero => {x}
  | V, E, x, succ(n) =>
    reachableWithin(V, E, x, n) ∪ nextNeighbors(V, E, reachableWithin(V, E, x, n))

theorem reachableWithin.zero (V E x : Set)
  shows reachableWithin(V, E, x, 0) = {x}
proof
  unfold reachableWithin
  rfl

theorem reachableWithin.successor (V E x : Set, n : Nat)
  shows reachableWithin(V, E, x, succ(n)) =
    reachableWithin(V, E, x, n) ∪ nextNeighbors(V, E, reachableWithin(V, E, x, n))
proof
  unfold reachableWithin
  rfl

theorem reachableWithin.monotone (V E x : Set, n : Nat)
  shows reachableWithin(V, E, x, n) ⊆ reachableWithin(V, E, x, succ(n))
proof
  rw reachableWithin.successor
  exact union2.subset_left

theorem reachableWithin.source (V E x : Set, n : Nat)
  shows x ∈ reachableWithin(V, E, x, n)
proof
  induction n
  | zero =>
    rw reachableWithin.zero
    apply singleton.membership.backward
    rfl
  | succ(k) using ih =>
    rw reachableWithin.successor
    apply union2.membership.backward
    left
    exact ih

theorem reachableWithin.advance (V E x y z : Set, n : Nat)
  requires reached : y ∈ reachableWithin(V, E, x, n)
  requires hz : z ∈ V
  requires edge : Adjacent(E, y, z)
  shows z ∈ reachableWithin(V, E, x, succ(n))
proof
  rw reachableWithin.successor
  apply union2.right
  exact nextNeighbors.membership.backward with ⟨hz, y, reached, edge⟩

predicate Reachable (V E x y : Set) :=
  ∃ n ∈ ℕ, y ∈ reachableWithin(V, E, x, n)

theorem Reachable.reflexive (V E x : Set)
  shows Reachable(V, E, x, x)
proof
  unfold Reachable
  have source := reachableWithin.source at V, E, x, 0 with Naturals.constructor.zero
  have zeroNat := nat.omega.forward with Naturals.constructor.zero
  refine ⟨0, zeroNat, source⟩

theorem Reachable.of_edge (V E x y : Set)
  requires hy : y ∈ V
  requires edge : Adjacent(E, x, y)
  shows Reachable(V, E, x, y)
proof
  unfold Reachable
  have source := reachableWithin.source at V, E, x, 0 with Naturals.constructor.zero
  have reached := reachableWithin.advance with Naturals.constructor.zero, source, hy, edge
  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero
  have oneInOmega := nat.omega.forward with oneNat
  refine ⟨1, oneInOmega, reached⟩