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 Coq Require Import Omega.

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.

Get the successors of a vertex
Definition get_succ (x : ident) (a : A_set) :=
  match (Env.find x a) with
  | Some s => s
  | None => PS.empty
  end.

Lemma get_succ_spec : forall a x y,
    PS.In y (get_succ x a) <->
    has_arc a x y.
Proof.

Get the predecessors of a vertex
Definition get_pred (x : ident) (a : A_set) :=
  Env.fold (fun y s acc => if PS.mem x s then (PS.add y acc) else acc) a PS.empty.

Lemma get_pred_spec : forall a x y,
    PS.In x (get_pred y a) <->
    has_arc a x y.
Proof.

Definition has_trans_arc a := clos_trans_n1 _ (has_arc a).
Hint Constructors clos_trans_n1.
Hint Unfold has_trans_arc.

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.
Hint Resolve add_arc_has_trans_arc1 add_arc_has_trans_arc2.

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).
Hint Constructors 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.

Lemma is_vertex_spec {v a} : forall (g : AcyGraph v a) x,
    is_vertex g x <-> PS.In x (vertices g).
Proof.

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

Lemma is_arc_spec {v a} : forall (g : AcyGraph v a) x y,
    is_arc g x y <-> (has_arc (arcs g) x y).
Proof.

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


Lemma has_arc_trans : forall a x y z,
    has_arc a x y ->
    has_arc a y z ->
    has_trans_arc a x z.
Proof.

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.

Corollary has_arc_asym : forall v a,
    AcyGraph v a ->
    Asymmetric (has_arc a).
Proof.

Global Instance is_arc_Asymmetric {v a} (g : AcyGraph v a) :
    Asymmetric (is_arc g).
Proof.

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

Definition is_arcb {v a} (g : AcyGraph v a) x y : bool :=
  has_arcb a x y.

Lemma is_arcb_spec {v a} : forall (g : AcyGraph v a) x y,
    is_arcb g x y = true <-> is_arc g x y.
Proof.

Corollary is_arcb_false_iff {v a} : forall (g : AcyGraph v a) x y,
    is_arcb g x y = false <-> ~is_arc g x y.
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.

has_arc is decidable !
Lemma has_arc_dec : forall a,
    forall x y, (has_arc a x y) \/ (~has_arc a 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.

Fact add_after_has_trans_arc2 : forall a preds y x' y',
    has_trans_arc a x' y' ->
    has_trans_arc (add_after preds y a) x' y'.
Proof.

Lemma add_after_spec2 : forall a preds y x' y',
    has_trans_arc (add_after preds y a) x' y' <->
    has_trans_arc a x' y' \/
    (PS.In x' preds /\ y = y') \/
    (PS.In x' preds /\ has_trans_arc a y y') \/
    (PS.Exists (fun p => has_trans_arc a x' p) preds /\ y = y') \/
    (PS.Exists (fun p => has_trans_arc a x' p) preds /\ has_trans_arc a y y').
Proof.

Corollary add_after_has_trans_arc1 : forall a preds x' y',
    PS.In x' preds ->
    has_trans_arc (add_after preds y' a) x' y'.
Proof.

Corollary add_after_has_trans_arc3 : forall {v a} x y preds,
    AcyGraph v a ->
    ~PS.In y v ->
    has_trans_arc (add_after preds y a) x y ->
    PS.In x preds \/ PS.Exists (fun x' => has_trans_arc a x x') preds.
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.

Corollary 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 ->
    AcyGraph v a ->
    AcyGraph (PS.add x v) (add_after preds x a).
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).

  Record dfs_state : Type :=
    mk_dfs_state {
        in_progress : PS.t;
        progress_in_graph : forall x, PS.In x in_progress -> Env.In x graph
      }.

  Extraction Inline in_progress.

  Definition empty_dfs_state :=
    {| in_progress := PS.empty;
       progress_in_graph := fun x Hin =>
                              False_ind (Env.In x graph) (not_In_empty x Hin) |}.
  Extraction Inline empty_dfs_state.

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

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

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

  Lemma wf_deeper: well_founded deeper.
Proof.

  Lemma add_deeper:
    forall x s P,
      ~ PS.In x (in_progress s) ->
      deeper {| in_progress := PS.add x (in_progress s);
                progress_in_graph := 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 dfs'_loop
             (inp : PS.t)
             (dfs' : forall x (v : { v | visited inp v }),
                 option { v' | visited inp v'
                               & (In_ps [x] v'
                                  /\ PS.Subset (proj1_sig v) v') })
             (zs : list positive)
             (v : {v | visited inp v })
    : option { v' | visited inp v' & (In_ps zs v' /\ PS.Subset (proj1_sig v) v') }.
Proof.
  Extraction Inline dfs'_loop.

  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.

  Definition dfs'
     (s : dfs_state)
     (dfs'' : forall s', deeper s' s ->
                forall x (v : { v | visited s'.(in_progress) v }),
                  option { v' | visited s'.(in_progress) v'
                                & In_ps [x] v' /\ PS.Subset (proj1_sig v) v' })
     (x : positive)
     (v : { v | visited s.(in_progress) v })
    : option { v' | visited s.(in_progress) v'
                    & In_ps [x] v' /\ PS.Subset (proj1_sig v) v' }.
Proof.

  Definition dfs
    : forall x (v : { v | visited PS.empty v }),
      option { v' | visited PS.empty v' &
                    (In_ps [x] v'
                     /\ PS.Subset (proj1_sig v) v') }
    := Fix wf_deeper _ dfs' empty_dfs_state.

End Dfs.

Program Definition build_acyclic_graph (graph : Env.t (list positive)) : res PS.t :=
  bind (Env.fold (fun x _ vo =>
                    bind vo
                         (fun v => match dfs graph x v with
                                | None => Error (msg "Couldn't build acyclic graph")
                                | Some v => OK (sig_of_sig2 v)
                                end))
                         graph (OK (none_visited graph)))
                 (fun v => OK _).

Lemma build_acyclic_graph_spec : forall graph v,
    build_acyclic_graph graph = 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) :=
  ForallTail (fun x xs => ~In x xs
                       /\ is_vertex g x
                       /\ (forall y, is_trans_arc g y x -> In y xs)) xs.
Hint Unfold TopoOrder.

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_nIn : forall {v a} (g : AcyGraph v a) x xs,
    ~In x xs ->
    TopoOrder g xs ->
    ~Exists (fun y => is_trans_arc g x y) 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 :=
  ForallTail (fun x' xs => 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.

Inserting into the graph

When we compile the program, what we do is often add some intermediate vertices between a set of predecessors and an existing vertex.

Definition add_between preds x y a :=
  add_arc x y (add_after preds x a).

Lemma add_between_AcyGraph : forall {v a} (g : AcyGraph v a) x preds succ,
    PS.For_all (is_vertex g) preds ->
    is_vertex g succ ->
    PS.For_all (fun p => is_arc g p succ) preds ->
    ~is_vertex g x ->
    AcyGraph (PS.add x v) (add_between preds x succ a).
Proof.

Lemma add_between_spec : forall v a preds x y x' y',
    ~PS.In y preds ->
    ~PS.Exists (fun p => has_arc a y p) preds ->
    AcyGraph v a ->
    has_arc (add_between preds x y a) x' y' <->
    has_arc a x' y' \/
    PS.In x' preds /\ x = y' \/
    x = x' /\ y = y'.
Proof.

Fact add_between_has_trans_arc2 : forall v a preds x y x' y',
    ~PS.In y preds ->
    ~PS.Exists (fun p => has_arc a y p) preds ->
    AcyGraph v a ->
    has_trans_arc a x' y' ->
    has_trans_arc (add_between preds x y a) x' y'.
Proof.

Lemma add_between_spec2 : forall v a preds x y x' y',
    ~PS.In y preds ->
    ~PS.Exists (fun p => has_trans_arc a y p) preds ->
    AcyGraph v a ->
    has_trans_arc (add_between preds x y a) x' y' <->
    has_trans_arc a x' y' \/
    PS.In x' preds /\ x = y' \/
    PS.In x' preds /\ y = y' \/
    x = x' /\ y = y' \/
    PS.Exists (fun p => has_trans_arc a x' p) preds /\ x = y' \/
    PS.Exists (fun p => has_trans_arc a x' p) preds /\ y = y' \/
    has_trans_arc a x' x /\ y = y' \/
    PS.In x' preds /\ has_trans_arc a x y' \/
    PS.In x' preds /\ has_trans_arc a y y' \/
    x = x' /\ has_trans_arc a y y' \/
    PS.Exists (fun p => has_trans_arc a x' p) preds /\ has_trans_arc a x y' \/
    PS.Exists (fun p => has_trans_arc a x' p) preds /\ has_trans_arc a y y' \/
    has_trans_arc a x' x /\ has_trans_arc a y y'.
Proof.