1 files changed, 0 insertions, 191 deletions
diff --git a/backend/Graph_Facts.v b/backend/Graph_Facts.v
deleted file mode 100755
index 3919b1f..0000000
--- a/backend/Graph_Facts.v
+++ /dev/null
@@ -1,191 +0,0 @@
-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.