Module AcyGraph

From Coq Require Import String.
From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.

From Coq Require Import RelationClasses.
Import Coq.Relations.Relation_Operators.
From Coq Require Import Arith.Arith.
From Coq Require Import Setoid.

From Velus Require Import Common.
From Velus Require Import Environment.

Vertices and arcs

Vertices

Definition V_set : Type := PS.t.

Arcs

Definition A_set : Type := Env.t PS.t.

Definition empty_arc_set : A_set := Env.empty _.

There is an arc between x and y in the arc set

Definition has_arc (a : A_set) (x y : ident) :=
exists s, Env.MapsTo x s a /\ PS.In y s.

Decision procedure to find if an arc exists

Definition has_arcb (a : A_set) (x y : ident) :=
  match (Env.find x a) with
  | Some s => PS.mem y s
  | None => false
  end.

Lemma has_arcb_spec : forall a x y,
    has_arcb a x y = true <-> has_arc a x y.

Proof.

Lemma nhas_arc_empty : forall x y,
~has_arc empty_arc_set x y.

Proof.

Add a single arc

Definition add_arc (x y : ident) (a : A_set) :=
  match (Env.find x a) with
  | Some s => Env.add x (PS.add y s) a
  | None => Env.add x (PS.singleton y) a
  end.

Lemma add_arc_spec : forall a x y x' y',
    has_arc (add_arc x y a) x' y' <->
    has_arc a x' y' \/
    (x = x' /\ y = y').

Proof.

Definition has_trans_arc a := clos_trans_n1 _ (has_arc a).

Global Hint Constructors clos_trans_n1 : acygraph.
Global Hint Unfold has_trans_arc : acygraph.

Global Instance has_trans_arc_Transitive : forall a,
Transitive (has_trans_arc a).

Proof.

Lemma nhas_trans_arc_empty : forall x y,
~has_trans_arc empty_arc_set x y.

Proof.

Fact add_arc_has_trans_arc1 : forall a x y,
has_trans_arc (add_arc x y a) x y.

Proof.

Fact add_arc_has_trans_arc2 : forall a x y x' y',
has_trans_arc a x' y' ->
has_trans_arc (add_arc x y a) x' y'.

Proof.

Global Hint Resolve add_arc_has_trans_arc1 add_arc_has_trans_arc2 : acygraph.

Lemma add_arc_spec2 : forall a x y x' y',
    has_trans_arc (add_arc x y a) x' y' <->
    has_trans_arc a x' y' \/
    (x = x' /\ y = y') \/
    (x = x' /\ has_trans_arc a y y') \/
    (has_trans_arc a x' x /\ y = y') \/
    (has_trans_arc a x' x /\ has_trans_arc a y y').

Proof.

Acyclic graph

Transitive, Directed Acyclic Graph

Inductive AcyGraph : V_set -> A_set -> Prop :=
| AGempty : AcyGraph PS.empty empty_arc_set
| AGaddv : forall v a x,
    AcyGraph v a ->
    AcyGraph (PS.add x v) a
| AGadda : forall v a x y,
    AcyGraph v a ->
    x <> y ->
    PS.In x v ->
    PS.In y v ->
    ~has_trans_arc a y x ->
    AcyGraph v (add_arc x y a).
Global Hint Constructors AcyGraph : acygraph.

Definition vertices {v a} (g : AcyGraph v a) : V_set := v.
Definition arcs {v a} (g : AcyGraph v a) : A_set := a.

Definition is_vertex {v a} (g : AcyGraph v a) (x : ident) : Prop :=
  PS.In x v.

Definition is_arc {v a} (g : AcyGraph v a) x y : Prop :=
  has_arc a x y.

Lemma nis_arc_Gempty : forall x y,
  ~is_arc AGempty x y.

Proof.

Definition is_trans_arc {v a} (g : AcyGraph v a) x y : Prop :=
has_trans_arc a x y.

Lemma nis_trans_arc_Gempty : forall x y,
~is_trans_arc AGempty x y.

Proof.

Major properties of is_arc : transitivity, irreflexivity, asymmetry

Global Instance is_trans_arc_Transitive {v a} (g : AcyGraph v a) :
Transitive (is_trans_arc g).

Proof.

Lemma has_arc_irrefl : forall v a,
AcyGraph v a ->
Irreflexive (has_arc a).

Proof.

Global Instance is_arc_Irreflexive {v a} (g : AcyGraph v a) :
Irreflexive (is_arc g).

Proof.

Global Instance is_trans_arc_Asymmetric {v a} (g : AcyGraph v a) :
Asymmetric (is_trans_arc g).

Proof.

Global Instance is_trans_arc_Irreflexive {v a} (g : AcyGraph v a) :
Irreflexive (is_trans_arc g).

Proof.

Lemma is_arc_is_vertex : forall {v a} (g : AcyGraph v a) x y,
is_arc g x y ->
is_vertex g x /\ is_vertex g y.

Proof.

Corollary is_trans_arc_is_vertex : forall {v a} (g : AcyGraph v a) x y,
is_trans_arc g x y ->
is_vertex g x /\ is_vertex g y.

Proof.

Lemma is_trans_arc_neq : forall {v a} (g : AcyGraph v a) x y,
is_trans_arc g x y ->
x <> y.

Proof.

Local Ltac destruct_conj_disj :=
    match goal with
    | H : _ /\ _ |- _ => destruct H
    | H : _ \/ _ |- _ => destruct H
    end; subst.

is_trans_arc is decidable !

Lemma is_trans_arc_dec : forall {v a} (g : AcyGraph v a),
forall x y, (is_trans_arc g x y) \/ (~ is_trans_arc g x y).

Proof.

Building an acyclic graph

We can try to build an acyclic graph from any graph (defined as a mapping from vertices to their direct predecessors) We iterate through the list of vertices, trying to add some that are not already in the graph, and which predecessors are all already in the graph. This algorithm only succeeds if the graph is indeed acyclic, and produces a witness of that fact.

From compcert Require Import common.Errors.

Definition add_after (preds : PS.t) (x : ident) (a : A_set) : A_set :=
  PS.fold (fun p a => add_arc p x a) preds a.

Lemma add_after_spec : forall a preds y x' y',
    has_arc (add_after preds y a) x' y' <->
    has_arc a x' y' \/
    (PS.In x' preds /\ y = y').

Proof.

Corollary add_after_has_arc1 : forall a x y x' preds,
has_arc a x y ->
has_arc (add_after preds x' a) x y.

Proof.

Corollary add_after_has_arc2 : forall a x y preds,
PS.In y preds ->
has_arc (add_after preds x a) y x.

Proof.

Lemma add_after_AcyGraph : forall v a x preds,
    PS.In x v ->
    ~PS.In x preds ->
    PS.For_all (fun x => PS.In x v) preds ->
    PS.For_all (fun p => ~has_trans_arc a x p) preds ->
    AcyGraph v a ->
    AcyGraph v (add_after preds x a) /\
    PS.For_all (fun p => ~has_trans_arc (add_after preds x a) x p) preds.

Proof.

Definition acgraph_of_graph g v a :=
  (forall x, Env.In x g <-> PS.In x v) /\
  (forall x y, (exists xs, Env.find y g = Some xs /\ In x xs) -> has_arc a x y).

Section Dfs.

  Variable graph : Env.t (list positive).

  Definition dfs_state := { p | forall x, PS.In x p -> Env.In x graph }.
  Definition proj1_dfs_state (s : dfs_state) := proj1_sig s.
  Coercion proj1_dfs_state : dfs_state >-> PS.t.
  Extraction Inline proj1_dfs_state.

  Program Definition empty_dfs_state : dfs_state :=
    exist _ PS.empty _.
  Extraction Inline empty_dfs_state.

  Lemma cardinals_in_progress_le_graph:
    forall (a : dfs_state),
      PS.cardinal a <= Env.cardinal graph.

Proof.

  Definition num_remaining (s : dfs_state) : nat :=
    Env.cardinal graph - PS.cardinal s.

  Definition deeper : dfs_state -> dfs_state -> Prop :=
    ltof _ num_remaining.

  Lemma add_deeper:
    forall x (s : dfs_state) P,
      ~ PS.In x s ->
      deeper (exist _ (PS.add x s) P) s.

Proof.

  Definition visited (p : PS.t) (v : PS.t) : Prop :=
    (forall x, PS.In x p -> ~PS.In x v)
    /\ exists a, AcyGraph v a
           /\ (forall x, PS.In x v ->
                   exists zs, Env.find x graph = Some zs
                         /\ (forall y, In y zs -> has_arc a y x)).

  Definition none_visited : { v | visited PS.empty v }.

Proof.

  Extraction Inline none_visited.

  Definition pre_visited_add:
    forall {inp} x
      (v : { v | visited inp v }),
      ~PS.In x (proj1_sig v) ->
      { v' | visited (PS.add x inp) v' & v' = (proj1_sig v) }.

Proof.

  Extraction Inline pre_visited_add.

  Fact fold_dfs_props : forall zs p (v: {v | visited p v}) v'
      (dfs : forall (x : positive) (v : {v | visited p v}), res {v' | visited p v' & In_ps [x] v' /\ PS.Subset (proj1_sig v) v'}),
      fold_left (fun v w => Errors.bind v (fun v => Errors.bind (dfs w v) (fun v' => OK (sig_of_sig2 v')))) zs (OK v) = OK v' ->
      In_ps zs (proj1_sig v') /\ PS.Subset (proj1_sig v) (proj1_sig v').

Proof.

  Section msg_of.
    Variable msgs : Env.t errmsg.

    Definition msg_of_label (x : ident) :=
      match Env.find x msgs with
      | Some msg => msg
      | None => msg "?"
      end.

    Fixpoint msg_of_cycle' (stop: ident) (s : list ident) :=
      match s with
      | [] => []
      | x::tl =>
          if ident_eq_dec x stop then msg_of_label x
          else (msg_of_label x ++ MSG " -> " :: msg_of_cycle' stop tl)
      end.
    Definition msg_of_cycle (s : list ident) :=
      match s with
      | [] => []
      | x::tl => msg_of_label x ++ MSG " -> " :: msg_of_cycle' x tl
      end.
  End msg_of.

  Variable get_msgs : unit -> Env.t errmsg.

  Program Fixpoint dfs' (s : dfs_state) (stack : list positive) (x : positive) (v : { v | visited s v })
    {measure (num_remaining s)} :
    res { v' | visited s v' & In_ps [x] v' /\ PS.Subset (proj1_sig v) v' } :=
      match PS.mem x s with
      | true => Error (MSG "dependency cycle : " :: msg_of_cycle (get_msgs tt) stack)
      | false =>
          match PS.mem x (proj1_sig v) with
          | true => OK (sig2_of_sig v _)
          | false =>
              match (Env.find x graph) with
              | None => Error (CTX x :: msg " not found")
              | Some zs =>
                  let s' := exist _ (PS.add x s) _ in
                  match fold_left (fun v w => Errors.bind v (fun v => Errors.bind (dfs' s' (w::stack) w v) (fun v' => OK (sig_of_sig2 v')))) zs (OK v) with
                  | Error msg => Error msg
                  | OK (exist _ v' (conj P1 _)) => OK (exist2 _ _ (PS.add x v') _ _)
                  end
              end
          end
      end.

Next Obligation.

  Definition dfs
    : forall x (v : { v | visited PS.empty v }),
      res { v' | visited PS.empty v' &
                    (In_ps [x] v'
                     /\ PS.Subset (proj1_sig v) v') }
    := fun x => dfs' empty_dfs_state [x] x.

End Dfs.

Program Definition build_acyclic_graph (graph : Env.t (list positive)) (get_msgs : unit -> Env.t errmsg) : res PS.t :=
  bind (Env.fold (fun x _ vo =>
                    bind vo
                         (fun v => match dfs graph get_msgs x v with
                                | Error msg => Error msg
                                | OK v => OK (sig_of_sig2 v)
                                end))
                         graph (OK (none_visited graph)))
                 (fun v => OK _).

Lemma build_acyclic_graph_spec : forall graph msgs v,
    build_acyclic_graph graph msgs = OK v ->
    exists a, acgraph_of_graph graph v a /\ AcyGraph v a.

Proof.

Extracting a prefix

In order to build an induction principle over the graph, we need to linearize it. We want to extract a Topological Order (TopoOrder) from the graph, which is simply encoded as a list, with the head variable only depending on the tail ones.

Definition TopoOrder {v a} (g : AcyGraph v a) (xs : list ident) :=
  Forall' (fun xs x => ~In x xs
                    /\ is_vertex g x
                    /\ (forall y, is_trans_arc g y x -> In y xs)) xs.

Definition TopoOrder' {v a} (g : AcyGraph v a) (xs : list ident) :=
  Forall' (fun xs x => ~In x xs
                    /\ is_vertex g x
                    /\ (forall y, is_arc g y x -> In y xs)) xs.
Global Hint Unfold TopoOrder : acygraph.

Lemma TopoOrder_weaken : forall {v a} (g : AcyGraph v a) xs,
    TopoOrder g xs ->
    Forall (fun x => forall y, is_trans_arc g y x -> In y xs) xs.

Proof.

Lemma TopoOrder_equiv {v a} (g : AcyGraph v a) : forall xs,
TopoOrder g xs <-> TopoOrder' g xs.

Proof.

Lemma TopoOrder_NoDup : forall {v a} (g : AcyGraph v a) xs,
TopoOrder g xs ->
NoDup xs.

Proof.

Fact TopoOrder_AGaddv : forall {v a} (g : AcyGraph v a) x xs,
TopoOrder g xs ->
TopoOrder (AGaddv v a x g) xs.

Proof.

Lemma TopoOrder_insert : forall {v a} (g : AcyGraph v a) xs1 xs2 x,
    is_vertex g x ->
    ~In x (xs1++xs2) ->
    (forall y, is_trans_arc g y x -> In y xs2) ->
    TopoOrder g (xs1 ++ xs2) ->
    TopoOrder g (xs1 ++ x :: xs2).

Proof.

x is located before y in l

Definition Before (x y : ident) l :=
  Forall' (fun xs x' => x' = y -> In x xs) l.

Lemma Before_middle : forall xs1 xs2 x y,
    x <> y ->
    ~In y xs1 ->
    ~In y xs2 ->
    Before x y (xs1 ++ y :: x :: xs2).

Proof.

Lemma Before_In : forall xs x y,
    Before x y xs ->
    In y xs ->
    In x xs.

Proof.

Import Permutation.

Given a prefix of the form xs1 ++ y :: xs2, we can split xs1 into two list: xs1l depends on y and xs1r doesnt

Fact TopoOrder_Partition_split : forall {v a} (g : AcyGraph v a) xs1 xs2 xs1l xs1r y,
    Partition (fun z => is_trans_arc g y z) xs1 xs1l xs1r ->
    TopoOrder g (xs1 ++ y :: xs2) ->
    TopoOrder g (xs1l ++ y :: xs1r ++ xs2).

Proof.

Lemma TopoOrder_reorganize : forall {v a} (g : AcyGraph v a) xs x y,
    x <> y ->
    In x xs ->
    In y xs ->
    TopoOrder g xs ->
    ~is_trans_arc g y x ->
    exists xs', Permutation.Permutation xs' xs /\
           TopoOrder g xs' /\
           Before x y xs'.

Proof.

Lemma TopoOrder_AGadda : forall {v a} (g : AcyGraph v a) xs x y Hneq Hin1 Hin2 Hna,
    Before x y xs ->
    TopoOrder g xs ->
    TopoOrder (AGadda _ _ x y g Hneq Hin1 Hin2 Hna) xs.

Proof.

Every Directed Acyclic Graph has at least one complete TopoOrder

Lemma has_TopoOrder {v a} :
  forall g : AcyGraph v a,
  exists xs,
    PS.Equal (vertices g) (PSP.of_list xs)
    /\ TopoOrder g xs.

Proof.