1 files changed, 152 insertions, 0 deletions

diff --git a/backend/Affinity_relation.v b/backend/Affinity_relation.v
new file mode 100755
index 00000000..7c4029c9
--- /dev/null
+++ b/backend/Affinity_relation.v
@@ -0,0 +1,152 @@
+Require Import FSets.
+Require Import InterfGraphMapImp.
+Require Import Delete_Preference_Edges_Degree.
+Require Import Edges.
+Require Import MyRegisters.
+
+Module Register := Regs.
+
+Import Edge RegFacts Props.
+
+Lemma compat_bool_move : forall g, 
+compat_bool Register.eq (move_related g).
+
+Proof.
+unfold move_related, compat_bool. intros.
+rewrite (compat_preference_adj _ _ _ H). reflexivity.
+Qed.
+
+(* Characterization of the move-relationship *)
+
+(* If a vertex x is move-related in g then there exists an affinity edge e
+    of g which is incident to x *)
+Lemma move_related_charac : forall x g,
+move_related g x = true ->
+exists e, aff_edge e /\ In_graph_edge e g /\ incident e x.
+
+Proof.
+intros. unfold move_related in H.
+destruct (set_induction2 (preference_adj x g)).
+rewrite Dec.F.is_empty_iff in H0. rewrite H0 in H. inversion H.
+destruct H0. destruct H0.
+rewrite Add_Equal in H0.
+assert (VertexSet.In x0 (preference_adj x g)).
+rewrite H0. apply VertexSet.add_1. intuition.
+rewrite in_pref in H1. destruct H1.
+exists (x0, x, Some x2). 
+split. unfold aff_edge. exists x2. auto.
+split. assumption.
+right. auto.
+Qed.
+
+(* The inversion characterization of move related *)
+Lemma move_related_charac2 : forall x g e,
+aff_edge e ->
+In_graph_edge e g ->
+incident e x ->
+move_related g x = true.
+
+Proof.
+intros. unfold move_related.
+case_eq (VertexSet.is_empty (preference_adj x g)); auto.
+intros. rewrite <-Dec.F.is_empty_iff in H2.
+generalize (empty_is_empty_1 H2). clear H2. intro.
+destruct H. destruct H1.
+assert (VertexSet.In (snd_ext e) (preference_adj x g)).
+rewrite in_pref. exists x0. rewrite edge_comm. rewrite <-H.
+assert (eq (x, snd_ext e, get_weight e) (fst_ext e, snd_ext e, get_weight e)) by Eq_eq.
+rewrite H3. rewrite <-(edge_eq e). assumption.
+rewrite H2 in H3. elim (VertexSet.empty_1 H3).
+assert (VertexSet.In (fst_ext e) (preference_adj x g)).
+rewrite in_pref. exists x0. rewrite <-H.
+assert (eq (fst_ext e, x, get_weight e) (fst_ext e, snd_ext e, get_weight e)) by Eq_eq.
+rewrite H3. rewrite <-(edge_eq e). assumption.
+rewrite H2 in H3. elim (VertexSet.empty_1 H3).
+Qed.
+
+(* Characterization of nonmove relation *)
+Lemma move_related_false_charac : forall e x g,
+aff_edge e ->
+In_graph_edge e g ->
+move_related g x = false ->
+~incident e x.
+
+Proof.
+intros e x g H H0 H1 H2.
+generalize (move_related_charac2 _ _ _ H H0 H2).
+intro H3;rewrite H1 in H3;inversion H3.
+Qed.
+
+Lemma move_related_false_charac2 : forall x g,
+(forall e, aff_edge e -> In_graph_edge e g -> ~incident e x) ->
+move_related g x = false.
+
+Proof.
+intros x g H.
+case_eq (move_related g x);intro H0.
+generalize (move_related_charac _ _ H0);intro H1.
+destruct H1 as [e H1];destruct H1 as [H1 H2];destruct H2 as [H2 H3].
+elim ((H e H1 H2) H3).
+reflexivity.
+Qed.
+
+(* A move-related vertex of the graph belongs to the graph *)
+Lemma move_related_in_graph : forall x g,
+move_related g x = true -> In_graph x g.
+
+Proof.
+intros x g H.
+generalize (move_related_charac x g H);intro H0.
+destruct H0 as [e H0];destruct H0 as [H0 H1];destruct H1 as [H1 H2].
+destruct H2;rewrite H2.
+apply (proj1 (In_graph_edge_in_ext _ _ H1)).
+apply (proj2 (In_graph_edge_in_ext _ _ H1)).
+Qed.
+
+(* The endpoints of any affinity edge of g are move-related in g *)
+Lemma Aff_edge_aff : forall e g,
+In_graph_edge e g ->
+aff_edge e ->
+move_related g (fst_ext e) = true /\ move_related g (snd_ext e) = true.
+
+Proof.
+intros. split.
+apply move_related_charac2 with (e:=e); [idtac|idtac|left]; auto.
+apply move_related_charac2 with (e:=e); [idtac|idtac|right]; auto.
+Qed.
+
+(* Any move-related vertex has a nonempty preference neighborhood *)
+Lemma move_related_not_empty_pref : forall x g,
+move_related g x = true ->
+~VertexSet.Equal (preference_adj x g) VertexSet.empty.
+
+Proof.
+unfold move_related. intros. intro.
+generalize (empty_is_empty_2 H0). intro.
+rewrite Dec.F.is_empty_iff in H1. rewrite H1 in H. inversion H.
+Qed.
+
+(* Any nonmove-related vertex has an empty preference neighborhood *)
+Lemma not_move_related_empty_pref : forall x g,
+move_related g x = false ->
+VertexSet.Equal (preference_adj x g) VertexSet.empty.
+
+Proof.
+unfold move_related. intros.
+apply empty_is_empty_1. rewrite Dec.F.is_empty_iff.
+case_eq (VertexSet.is_empty (preference_adj x g)); intros; auto.
+rewrite H0 in H. inversion H.
+Qed.
+
+(* Any vertex having a preference degree different than 0 is move-related *)
+Lemma move_related_card : forall x g,
+pref_degree g x  <> 0 ->
+move_related g x = true.
+
+Proof.
+unfold pref_degree. intros.
+case_eq (move_related g x); intros.
+reflexivity.
+generalize (not_move_related_empty_pref _ _ H0). intro.
+rewrite H1 in H. rewrite empty_cardinal in H. elim H. auto.
+Qed.