1 files changed, 191 insertions, 0 deletions
diff --git a/backend/Graph_Facts.v b/backend/Graph_Facts.v
new file mode 100755
index 00000000..3919b1f3
--- /dev/null
+++ b/backend/Graph_Facts.v
@@ -0,0 +1,191 @@
+Require Import FSets.
+Require Import InterfGraphMapImp.
+Require Import ZArith.
+Require Import Edges.
+Require Import MyRegisters.
+
+Import  Edge OTFacts.
+Module Import RegFacts := Facts VertexSet.
+Module Import RegRegFacts := Facts EdgeSet.
+
+(* Definition of useful morphisms *)
+
+Add Morphism In_graph : In_graph_m.
+
+Proof.
+unfold In_graph;intros x y H g.
+split;intro H0;[rewrite <-H|rewrite H];assumption.
+Qed.
+
+Add Morphism In_graph_edge : In_graph_edge_m.
+
+Proof.
+unfold In_graph_edge; intros x y H g. fold (eq x y) in H.
+split;intro H0;[rewrite <-H|rewrite H];assumption.
+Qed.
+
+Add Morphism move_related : move_related_m.
+
+Proof.
+unfold move_related. intros. rewrite (compat_preference_adj _ _ _ H). reflexivity.
+Qed.
+
+Add Morphism get_weight : get_weight_m.
+
+Proof.
+intros x y H.
+rewrite (weight_ordered_weight x);rewrite (weight_ordered_weight y).
+unfold get_weight;unfold E.eq in H.
+destruct H as [_ H];inversion H;[|rewrite H2];reflexivity.
+Qed.
+
+(* Useful rewriting lemmas *)
+
+Lemma rewrite_fst : forall x y z,
+fst_ext (x,y,z) = x.
+
+Proof.
+auto.
+Qed.
+
+Lemma rewrite_snd : forall x y z,
+snd_ext (x,y,z) = y.
+
+Proof.
+auto.
+Qed.
+
+Lemma rewrite_weight : forall x y z,
+get_weight (x,y,z) = z.
+
+Proof.
+auto.
+Qed.
+
+(* A rewriting tactic *)
+
+Ltac change_rewrite := 
+repeat (try rewrite rewrite_fst in *;
+             try rewrite rewrite_snd in *;
+             try rewrite rewrite_weight in *).
+
+(* Two tactics for proving equality of edges *)
+Ltac Eq_eq :=
+apply eq_ordered_eq;unfold E.eq;
+split;[simpl;split;auto; intuition |try apply OptionN_as_OT.eq_refl; intuition].
+
+Ltac Eq_comm_eq := rewrite edge_comm; Eq_eq.
+
+(* Extensionnality of redirect *)
+Lemma redirect_ext : forall e e' x y,
+eq e e' ->
+eq (redirect x y e) (redirect x y e').
+
+Proof.
+intros e e' x y H.
+destruct e as [xe we];destruct xe as [ex1 ex2];
+destruct e' as [xe' we'];destruct xe' as [e'x1 e'x2];simpl in *.
+generalize (get_weight_m _ _ H);simpl;intro Heq;subst.
+destruct (eq_charac _  _ H);destruct H0 as [H0 H1];unfold redirect;change_rewrite.
+destruct (OTFacts.eq_dec ex1 x).
+destruct (OTFacts.eq_dec e'x1 x).
+Eq_eq. intuition.
+elim (n (Regs.eq_trans (Regs.eq_sym H0) r)).
+destruct (OTFacts.eq_dec e'x1 x).
+elim (n (Regs.eq_trans H0 r)).
+destruct (OTFacts.eq_dec ex2 x).
+destruct (OTFacts.eq_dec e'x2 x).
+Eq_eq. intuition.
+elim (n1 (Regs.eq_trans (Regs.eq_sym H1) r)).
+destruct (OTFacts.eq_dec e'x2 x).
+elim (n1 (Regs.eq_trans H1 r)).
+Eq_eq.
+destruct (OTFacts.eq_dec ex1 x).
+destruct (OTFacts.eq_dec e'x1 x).
+Eq_eq. intuition.
+apply (Regs.eq_trans H1 (Regs.eq_trans r0 (Regs.eq_trans (Regs.eq_sym r) H0))).
+destruct (OTFacts.eq_dec e'x2 x).
+Eq_comm_eq. intuition.
+elim (n0 (Regs.eq_trans (Regs.eq_sym H0) r)).
+destruct (OTFacts.eq_dec e'x2 x).
+elim (n (Regs.eq_trans H0 r)).
+destruct (OTFacts.eq_dec ex2 x). 
+destruct (OTFacts.eq_dec e'x1 x).
+Eq_comm_eq.
+elim (n1 (Regs.eq_trans (Regs.eq_sym H1) r)).
+destruct (OTFacts.eq_dec e'x1 x).
+elim (n1 (Regs.eq_trans H1 r)).
+Eq_comm_eq.
+Qed.
+
+(* The weight is left unchanged while applying redirect *)
+Lemma redirect_weight_eq : forall e x y,
+Edge.get_weight (redirect x y e) = Edge.get_weight e.
+
+Proof.
+unfold redirect;intros e x y;destruct e as [e w];destruct e as [ex1 ex2];change_rewrite.
+destruct (OTFacts.eq_dec ex1 x);destruct (OTFacts.eq_dec ex2 x);reflexivity.
+Qed.
+
+(* Specification of redirect *)
+Lemma redirect_charac : forall e x y,
+(eq e (redirect x y e) /\ (~Regs.eq x (fst_ext e) /\ ~Regs.eq x (snd_ext e))) \/
+(eq (y, snd_ext e, get_weight e) (redirect x y e) /\ Regs.eq x (fst_ext e)) \/
+(eq (fst_ext e, y, get_weight e) (redirect x y e) /\ Regs.eq x (snd_ext e)).
+
+Proof.
+intros e x y.
+unfold redirect. change_rewrite.
+destruct (OTFacts.eq_dec (fst_ext e) x).
+right. left. split. apply eq_refl. auto.
+destruct (OTFacts.eq_dec (snd_ext e) x).
+right. right. split. apply eq_refl. auto.
+left. split. apply eq_refl. split; intuition.
+Qed.
+
+(* Weak equality implies equality for interference edges *)
+Lemma weak_eq_interf_eq : forall x y,
+weak_eq x y ->
+interf_edge x ->
+interf_edge y ->
+eq x y.
+
+Proof.
+unfold weak_eq, interf_edge, get_weight. intros. destruct H; destruct H. 
+Eq_eq. rewrite H0. rewrite H1. apply OptionN_as_OT.eq_refl.
+rewrite (edge_eq x). rewrite (edge_eq y).
+Eq_comm_eq. simpl. unfold get_weight.
+rewrite H0. rewrite H1. apply OptionN_as_OT.eq_refl.
+Qed.
+
+(* The second endpoint of e does not belongs to (merge e g H H0) *)
+Lemma not_in_merge_snd : forall e g H H0,
+~In_graph (snd_ext e) (merge e g H H0).
+
+Proof.
+intros. intro.
+rewrite In_merge_vertex in H1. destruct H1.
+elim (H2 (Regs.eq_refl _)).
+Qed.
+
+(* Extensionnality of the low-degree function *)
+Lemma compat_bool_low : forall g K,
+compat_bool Regs.eq (has_low_degree g K).
+
+Proof.
+unfold compat_bool, has_low_degree, interf_degree. intros.
+rewrite (compat_interference_adj _ _ _ H). reflexivity.
+Qed.
+
+(* There cannot exist both an interference and 
+    a preference between two vertices *)
+Lemma interf_pref_conflict : forall x y g,
+Prefere x y g /\ Interfere x y g -> False.
+
+Proof.
+unfold Prefere, Interfere. intros. destruct H. destruct H.
+assert (eq (x,y,Some x0) (x,y,None)).
+apply is_simple_graph with (g:=g); auto.
+unfold weak_eq. left. change_rewrite. split; auto.
+generalize (get_weight_m _ _ H1). simpl. congruence.
+Qed.