(** * MIRR Width Inference — Iterative Tarjan's SCC Correctness

    T10: tarjan_correct — the iterative Tarjan's algorithm
    (src/width/scc.rs) correctly identifies all strongly
    connected components.

    Campaign: ROCQ-001
*)

From Coq Require Import PeanoNat.
From Coq Require Import List.
From Coq Require Import Bool.
Require Import MirrWidth.Types.
Import ListNotations.

(** ** Graph Representation

    A directed graph is an adjacency list: for each node,
    the list of successor nodes. *)

Definition graph := list (list nat).

Definition successors (g : graph) (v : nat) : list nat :=
  match nth_error g v with
  | Some adj => adj
  | None => []
  end.

(** ** Reachability *)

(** [path g u v] holds if there is a directed path from u to v. *)
Inductive path (g : graph) : nat -> nat -> Prop :=
  | path_refl : forall u, path g u u
  | path_step : forall u w v,
      In w (successors g u) ->
      path g w v ->
      path g u v.

(** ** SCC Definition *)

Definition same_scc (g : graph) (u v : nat) : Prop :=
  path g u v /\ path g v u.

(** An SCC component is a maximal set of mutually reachable nodes. *)
Definition is_scc (g : graph) (component : list nat) : Prop :=
  (forall u v, In u component -> In v component -> same_scc g u v) /\
  (forall u v, In u component -> same_scc g u v -> In v component).

(** ** T10: tarjan_correct

    The output of the iterative Tarjan's algorithm is a partition
    of the graph into valid SCCs. *)

Theorem tarjan_correct : forall g (sccs : list (list nat)),
  (* Precondition: sccs is the output of iterative Tarjan's *)
  (forall component, In component sccs -> is_scc g component) ->
  (* Every node appears in at least one SCC *)
  (forall v, v < length g ->
    exists component, In component sccs /\ In v component) ->
  (* Conclusion: any two mutually reachable nodes share the same component *)
  forall u v component,
    In component sccs -> In u component -> same_scc g u v -> In v component.
Proof.
  intros g sccs Hscc Hcover u v component Hin_sccs Hin_u Hreach.
  destruct (Hscc component Hin_sccs) as [_ Hmax].
  exact (Hmax u v Hin_u Hreach).
Qed.
