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.
intros a x y.
unfold has_arcb,
has_arc.
split; [
intros H|
intros (?&
Hmap&
Hin)];
destruct (
Env.find _ _)
eqn:
Hfind.
-
eauto.
-
inv H.
-
rewrite Hmap in Hfind.
inv Hfind.
apply PSF.mem_1;
auto.
-
rewrite Hmap in Hfind.
inv Hfind.
Qed.
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.
intros ? ??? Ha1 Ha2.
induction Ha2; eauto.
Qed.
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.
intros *;
split;
intros Ha.
-
induction Ha;
try rewrite add_arc_spec in *.
+
destruct H as [?|(?&?)];
subst;
auto.
+
destruct H as [?|(?&?)];
destruct IHHa as [?|[(?&?)|[(?&?)|[(?&?)|(?&?)]]]];
subst;
eauto 10.
-
destruct Ha as [?|[(?&?)|[(?&?)|[(?&?)|(?&?)]]]];
subst;
eauto.
+
etransitivity;
eauto.
+
etransitivity;
eauto.
+
etransitivity;
eauto.
etransitivity;
eauto.
Qed.
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.
reflexivity. Qed.
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.
reflexivity. Qed.
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.
intros * Ha1 Ha2; eauto.
Qed.
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.
fix irrefl 3.
intros *
g.
destruct g.
-
intros ?
Ha.
apply nis_arc_Gempty in Ha;
auto.
-
specialize (
irrefl _ _ g);
auto.
-
specialize (
irrefl _ _ g).
intros x'
Harc.
apply add_arc_spec in Harc as [?|(?&?)];
subst.
+
eapply irrefl;
eauto.
+
congruence.
Qed.
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.
revert v a g.
fix trans 3.
intros *.
destruct g.
-
intros ? ? ?
Ha1.
exfalso.
eapply nhas_trans_arc_empty;
eauto.
-
specialize (
trans _ _ g);
auto.
-
specialize (
trans _ _ g).
intros x'
y'
Harc1 Harc2.
apply add_arc_spec2 in Harc1;
apply add_arc_spec2 in Harc2.
destruct Harc1 as [?|[(?&?)|[(?&?)|[(?&?)|(?&?)]]]];
destruct Harc2 as [?|[(?&?)|[(?&?)|[(?&?)|(?&?)]]]];
subst;
eauto 10.
1-7:
eapply n0.
1-7:
etransitivity;
eauto.
1,2:
etransitivity;
eauto.
Qed.
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.
revert v a g.
fix irrefl 3.
intros *
x.
destruct g.
-
apply nis_trans_arc_Gempty.
-
eapply (
irrefl _ _ g).
-
intros contra.
specialize (
irrefl _ _ g).
apply add_arc_spec2 in contra as [?|[(?&?)|[(?&?)|[(?&?)|(?&?)]]]];
subst;
eauto.
+
eapply irrefl;
eauto.
+
eapply n0.
etransitivity;
eauto.
Qed.
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.
fix is_arc_is_vertex 3.
intros *
Hisarc.
destruct g;
simpl in *.
-
exfalso.
destruct Hisarc as (?&
contra&
_).
rewrite Env.Props.P.F.empty_mapsto_iff in contra;
auto.
-
specialize (
is_arc_is_vertex _ _ g).
apply is_arc_is_vertex in Hisarc as (
Hvx&
Hvy).
split;
apply PSF.add_2;
auto.
-
specialize (
is_arc_is_vertex _ _ g).
unfold is_arc in Hisarc.
apply add_arc_spec in Hisarc as [?|(?&?)];
subst;
auto.
apply is_arc_is_vertex in H;
auto.
Qed.
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.
intros *.
unfold has_arc.
destruct (
Env.find x a)
eqn:
Hfind.
-
destruct (
PS.mem y t)
eqn:
Hmem; [
left|
right].
+
apply PSF.mem_2 in Hmem.
exists t;
split;
auto.
+
intros (?&
Hmap&
Hin).
unfold Env.MapsTo in *.
rewrite Hfind in Hmap.
inv Hmap.
apply PSF.mem_1 in Hin.
congruence.
-
right.
intros (?&
Hmap&
_).
unfold Env.MapsTo in *.
rewrite Hfind in Hmap.
inv Hmap.
Qed.
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.
fix is_trans_arc_dec 3.
intros *.
destruct g.
-
right.
eapply nis_trans_arc_Gempty.
-
specialize (
is_trans_arc_dec _ _ g x y)
as [?|?];
auto.
-
specialize (
is_trans_arc_dec _ _ g).
destruct (
is_trans_arc_dec x y), (
is_trans_arc_dec x x0), (
is_trans_arc_dec y0 y),
(
ident_eq_dec y y0), (
ident_eq_dec x x0);
subst.
1-32:
try solve [
left;
apply add_arc_spec2;
auto 10].
1-7:(
right;
intro contra;
apply add_arc_spec2 in contra;
repeat destruct_conj_disj;
auto).
Qed.
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.
Local Ltac simpl_ps_add :=
unfold PSP.Add in *;
match goal with
|
Hadd: (
forall y,
PS.In y ?
s2 <-> ?
p =
y \/
PS.In y ?
s1),
Hin:
PS.In ?
x ?
s1 |-
_ =>
eapply or_intror in Hin;
erewrite <-
Hadd in Hin
|
Hadd: (
forall y,
PS.In y ?
s2 <-> ?
x =
y \/
PS.In y ?
s1) |-
_ =>
specialize (
Hadd x)
as (
_&?)
|
_ =>
idtac
end.
intros preds a y.
unfold add_after.
apply PSP.fold_rec.
-
intros *
Hemp.
split;
auto.
intros [?|(
Hin&?)];
subst;
auto.
destruct (
Hemp _ Hin).
-
intros p *
Hin Hnin Hadd Hrec *.
rewrite add_arc_spec.
split;
intros [?|(?&?)];
subst;
auto.
+
apply Hrec in H as [?|(?&?)];
subst;
auto;
unfold PS.Exists.
repeat simpl_ps_add;
eauto 10.
+
repeat simpl_ps_add;
eauto 10.
+
rewrite Hrec;
auto.
+
destruct (
ident_eq_dec p x');
subst;
auto.
specialize (
Hrec x'
y').
left.
rewrite Hrec;
auto.
right.
split;
auto.
apply Hadd in H as [?|?];
auto.
congruence.
Qed.
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.
intros *
Hin1 Hnin2 Hpreds Hna Hacy.
revert Hacy.
unfold add_after.
eapply PSP.fold_rec_nodep.
-
intros *
Hacy;
split;
auto.
-
intros *
Hin'
Hrec Hacy.
specialize (
Hrec Hacy)
as (
Hacy'&
Hna').
split; [
apply AGadda|];
auto.
+
intro contra;
subst;
auto.
+
intros ?
Hin contra.
apply Hna'
in Hin.
apply Hin.
rewrite add_arc_spec2 in contra.
repeat destruct_conj_disj;
auto.
*
exfalso;
auto.
*
exfalso;
auto.
apply Hna'
in Hin';
auto.
Qed.
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.
revert zs v.
fix dfs'
_loop 1.
intros zs v.
destruct zs as [|
w ws].
-
refine (
Some (
sig2_of_sig v _)).
split.
now apply In_ps_nil.
reflexivity.
-
destruct (
dfs'
w v)
as [(
v',
Pv', (
Hinv',
Hsubv'))|]; [|
exact None].
destruct (
dfs'
_loop ws (
exist _ v'
Pv'))
as [
v''|]; [|
exact None].
refine (
Some (
sig2_weaken2 _ v'')).
intros S (
Hin,
Hsub).
split.
+
apply Forall_cons;
auto.
rewrite <-
Hsub.
now inv Hinv'.
+
rewrite <-
Hsub.
simpl.
rewrite <-
Hsubv'.
reflexivity.
Defined.
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.
intros inp x (
v, (
Pv1 &
Pv2))
Hnxp.
simpl in *.
exists v;
split;
auto.
intros y Hyp.
apply PS.add_spec in Hyp as [
HH|
HH];
subst;
auto.
Defined.
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.
unfold build_acyclic_graph.
intros graph v Hcheck.
monadInv Hcheck.
rename EQ into Hfold.
rename x into v'.
rewrite Env.fold_1 in Hfold.
assert (
PS.Equal (
proj1_sig v')
(
ps_adds (
map fst (
Env.elements graph))
(
proj1_sig (
none_visited graph))))
as Hveq;
[
apply PSP.double_inclusion;
split|].
-
destruct v'
as (
v' &
Pv'1 &
a &
Pv'2 &
Pv'3).
simpl.
intros x Hx.
apply Pv'3
in Hx as (
zs &
Hx &
Hsuc).
apply Env.elements_correct in Hx.
apply ps_adds_spec;
left.
apply in_map_iff.
exists (
x,
zs);
auto.
-
revert Hfold.
revert v'.
generalize (
none_visited graph)
as acc.
generalize (
Env.elements graph)
as xs.
induction xs as [|
x xs IH]; [
inversion 1;
reflexivity|].
simpl.
intros acc v'
Hfold.
destruct (
dfs graph (
fst x)
acc)
as [
acc'|]
eqn:
Hacc';
simpl in *.
+
apply IH in Hfold.
rewrite <-
Hfold.
apply Subset_ps_adds.
destruct acc'
as (
acc',
Vacc', (
H1acc' &
H2acc'));
simpl in *.
apply PSP.subset_add_3;
auto.
now apply In_ps_singleton.
+
clear -
Hfold.
exfalso.
induction xs;
simpl in *;
try congruence.
-
clear Hfold.
destruct v'
as (
v &
Pv1 &
a &
Pv2 &
Pv3).
simpl in *.
exists a.
split;
auto.
constructor;
auto.
+
intros x.
rewrite Hveq,
ps_adds_of_list,
ps_of_list_In,
Env.In_Members,
fst_InMembers.
reflexivity.
+
intros ?? (?&
Find&
In).
specialize (
Pv3 y).
rewrite Hveq,
ps_adds_of_list,
ps_of_list_In in Pv3.
assert (
Find':=
Find).
apply Env.elements_correct in Find'.
eapply in_map with (
f:=
fst),
Pv3 in Find'
as (?&
Find'&?).
setoid_rewrite Find in Find';
inv Find';
eauto.
Qed.
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.
intros *
Hpref.
induction Hpref;
auto.
destruct H as (
Hnin&
Hv&
Ha).
constructor;
intuition.
eapply Forall_impl; [|
eauto].
intros * ? ? ?.
right;
auto.
Qed.
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.
intros * Hpref.
induction Hpref; constructor; auto.
destruct H; auto.
Qed.
Fact TopoOrder_AGaddv :
forall {
v a} (
g :
AcyGraph v a)
x xs,
TopoOrder g xs ->
TopoOrder (
AGaddv v a x g)
xs.
Proof.
induction xs;
intros *
Hpre;
inv Hpre;
auto.
destruct H1 as (?&?&?).
specialize (
IHxs H2).
repeat constructor;
auto.
apply PSF.add_2;
auto.
Qed.
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.
induction xs1;
intros *
Hver Hnin Ha Hpre;
simpl in *.
-
constructor;
repeat split;
auto.
-
inversion_clear Hpre as [|?? (
Hnin'&
Hver'&
Ha')
Hpre'].
apply not_or'
in Hnin as (
Hneq&
Hnin).
apply not_In_app in Hnin'
as (
Hnin1&
Hnin2).
constructor;
repeat split;
auto.
+
rewrite not_In_app;
simpl;
rewrite not_or';
auto.
+
intros *
Ha''.
specialize (
Ha'
_ Ha'').
rewrite in_app_iff in *;
simpl.
destruct Ha';
auto.
+
apply IHxs1;
auto.
Qed.
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.
induction xs1;
intros *
Hneq Hnin1 Hnin2;
simpl.
-
constructor; [|
constructor].
+
intros _.
left;
auto.
+
intros contra;
subst.
congruence.
+
induction xs2;
auto.
apply not_in_cons in Hnin2 as (
Hneq'&
Hnin2).
constructor;
auto.
intros contra;
subst.
congruence.
-
apply not_in_cons in Hnin1 as (
Hneq'&
Hnin1).
constructor;
auto.
+
intros contra;
subst.
congruence.
+
apply IHxs1;
auto.
Qed.
Lemma Before_In :
forall xs x y,
Before x y xs ->
In y xs ->
In x xs.
Proof.
induction xs; intros * Hbef Hin; inv Hbef; inv Hin.
1,2:right; eauto.
Qed.
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.
induction xs1;
intros *
Hpart Hpre;
inv Hpart;
simpl in *.
-
assumption.
-
inversion_clear Hpre as [|?? (
Hnin&
Hver&
Ha)
Hf].
constructor;
repeat split;
auto.
+
erewrite (
Partition_Permutation _ xs1), <-
app_assoc, <-
Permutation_middle in Hnin;
eauto.
+
intros *
Ha'.
specialize (
Ha _ Ha').
erewrite (
Partition_Permutation _ xs1), <-
app_assoc, <-
Permutation_middle in Ha;
eauto.
+
apply IHxs1;
auto.
-
inversion_clear Hpre as [|?? (
Hnin&
Hver&
Ha)
Hf].
rewrite cons_is_app,
app_assoc.
apply TopoOrder_insert;
auto;
try rewrite <-
app_assoc, <-
cons_is_app.
+
erewrite (
Partition_Permutation _ xs1), <-
app_assoc, <-
Permutation_middle in Hnin;
eauto.
+
intros *
Ha'.
specialize (
Ha _ Ha').
erewrite (
Partition_Permutation _ xs1), <-
app_assoc in Ha;
eauto.
repeat (
rewrite in_app_iff in *;
simpl in *;
idtac).
destruct Ha as [
Hin|[?|[?|?]]];
subst;
auto. 2:
congruence.
exfalso.
eapply Partition_Forall1,
Forall_forall in H1; [|
eauto].
eapply H4;
eauto.
etransitivity;
eauto.
+
apply IHxs1;
auto.
Qed.
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.
induction xs;
intros *
Hneq Hin1 Hin2 Hpref Hna;
inv Hin1;
inv Hin2;
inversion_clear Hpref as [|?? (
Hnin&
Hv&
Ha)];
subst.
-
contradiction.
-
clear IHxs.
apply in_split in H as (
xs1&
xs2&?);
subst.
assert (
exists xs1l xs1r,
Partition (
fun z =>
is_trans_arc g y z)
xs1 xs1l xs1r)
as (
xs1l&
xs1r&
Hpart).
{
eapply dec_Partition,
is_trans_arc_dec. }
exists (
xs1l ++
y ::
x ::
xs1r ++
xs2).
assert (
Permutation xs1 (
xs1l ++
xs1r))
as Hperm.
{
eapply Partition_Permutation;
eauto. }
repeat split.
+
repeat rewrite <-
Permutation_middle.
rewrite app_assoc, <-
Hperm.
apply perm_swap.
+
eapply TopoOrder_Partition_split in H0;
eauto.
rewrite cons_is_app,
app_assoc.
apply TopoOrder_insert;
try rewrite <-
app_assoc, <-
cons_is_app;
auto.
*
rewrite Hperm, <-
app_assoc, <-
Permutation_middle in Hnin;
auto.
*
intros ?
Ha'.
specialize (
Ha _ Ha').
rewrite Hperm, <-
app_assoc in Ha.
repeat (
rewrite in_app_iff in *;
simpl in *;
idtac).
destruct Ha as [?|[?|[?|?]]];
subst;
auto. 2:
congruence.
exfalso.
eapply Partition_Forall1,
Forall_forall in Hpart; [|
eauto].
eapply Hna.
etransitivity;
eauto.
+
assert (~
In y (
xs1 ++
xs2)).
{
apply TopoOrder_NoDup in H0.
rewrite <-
Permutation_middle in H0.
inv H0;
auto. }
rewrite Hperm, <-
app_assoc in H.
apply not_In_app in H as (?&?).
apply Before_middle;
auto.
-
exists (
y::
xs).
repeat split;
auto.
constructor;
auto.
clear -
Hnin.
induction xs; [
constructor|].
apply not_in_cons in Hnin as (
Hneq&
Hnin).
constructor;
eauto.
intro contra;
subst;
congruence.
-
specialize (
IHxs _ _ Hneq H H0 H1 Hna)
as (
xs'&
Hperm&
Hpre&
Hbef).
exists (
a0::
xs');
repeat split;
auto.
+
repeat constructor;
auto.
2:
intros ?
Ha'.
1,2:
rewrite Hperm;
auto.
+
constructor;
auto.
intros ?;
subst.
rewrite Hperm;
auto.
Qed.
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.
induction xs;
intros *
Hbef Hpre;
auto.
inv Hbef.
inversion_clear Hpre as [|?? (?&?&?)
Hf].
constructor. 2:
eapply IHxs;
eauto.
repeat split;
auto.
intros ?
Ha.
apply add_arc_spec2 in Ha as [?|[(?&?)|[(?&?)|[(?&?)|(?&?)]]]];
subst;
auto.
-
apply H3 in H5;
auto.
eapply Before_In in H2;
eauto.
-
specialize (
H1 eq_refl).
eapply TopoOrder_weaken,
Forall_forall in Hf;
eauto.
-
specialize (
H3 _ H5).
eapply Before_In in H2;
eauto.
eapply TopoOrder_weaken,
Forall_forall in Hf;
eauto.
Qed.
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.