1 files changed, 138 insertions, 0 deletions
diff --git a/backend/Delete_Preference_Edges_Move.v b/backend/Delete_Preference_Edges_Move.v
new file mode 100755
index 00000000..66f9ab6a
--- /dev/null
+++ b/backend/Delete_Preference_Edges_Move.v
@@ -0,0 +1,138 @@
+Require Import FSets.
+Require Import InterfGraphMapImp.
+Require Import Merge_Move.
+Require Import Edges.
+Require Import MyRegisters.
+Require Import Affinity_relation.
+Require Import Interference_adjacency.
+Require Import Delete_Preference_Edges_Adjacency.
+Require Import Remove_Vertex_Move.
+
+Import Edge Props RegFacts.
+
+(* The frozen vertex is nonmove-related in the resulting graph *)
+Lemma not_aff_related_delete_preference_edges : forall r g p,
+move_related (delete_preference_edges r g p) r = false.
+
+Proof.
+intros. apply move_related_false_charac2.
+intros.
+rewrite In_delete_preference_edges_edge in H0. destruct H0.
+intro. elim H1. split; assumption.
+Qed.
+
+(* A vertex which is move-related after a freeze is move-related before it *)
+Lemma move_related_delete_move_related : forall x r g p,
+move_related (delete_preference_edges r g p) x = true ->
+move_related g x = true.
+
+Proof.
+intros x r g p H.
+generalize (move_related_charac _ _ H);intro H0.
+destruct H0 as [y H0].
+destruct H0 as [H0 H1];destruct H1 as [H1 H2].
+rewrite In_delete_preference_edges_edge in H1. destruct H1.
+apply (move_related_charac2 _ _ _ H0 H1 H2).
+Qed.
+
+(* A vertex which is move-related in g and not in (delete_preference_edges r g H)
+    is a preference neighbor of r in g *)
+Lemma delete_preference_edges_move_1 : forall x r g H,
+~Register.eq r x ->
+move_related g x = true ->
+move_related (delete_preference_edges r g H) x = false ->
+VertexSet.In x (preference_adj r g).
+
+Proof.
+intros. generalize (not_move_related_empty_pref _ _ H2). intro.
+rewrite delete_preference_preference_adj in H3.
+destruct (In_dec r (preference_adj x g)).
+apply pref_adj_comm. assumption.
+assert (VertexSet.Equal (preference_adj x g) VertexSet.empty).
+split; intros.
+rewrite <-H3. apply VertexSet.remove_2.
+intro. rewrite <-H5 in H4. elim n. auto.
+assumption.
+elim (VertexSet.empty_1 H4).
+elim (move_related_not_empty_pref _ _ H1 H4).
+auto.
+Qed.
+
+(* A vertex which is move-related in g and nonmove-related in 
+   (delete_preference_edges r g H) has a preference degree of 1 *)
+Lemma delete_preference_edges_move_2 : forall x r g H,
+~Register.eq r x ->
+move_related g x = true ->
+move_related (delete_preference_edges r g H) x = false ->
+VertexSet.cardinal (preference_adj x g) = 1.
+
+Proof.
+intros. generalize (not_move_related_empty_pref _ _ H2). intro.
+rewrite delete_preference_preference_adj in H3.
+destruct (In_dec r (preference_adj x g)).
+cut (VertexSet.Equal (preference_adj x g) (VertexSet.singleton r)). intros.
+rewrite H4. apply singleton_cardinal.
+split; intros.
+destruct (Register.eq_dec a r).
+apply VertexSet.singleton_2. intuition.
+assert (VertexSet.In a VertexSet.empty).
+rewrite <-H3. apply VertexSet.remove_2; auto.
+elim (VertexSet.empty_1 H5).
+generalize (VertexSet.singleton_1 H4). intro.
+rewrite <-H5. auto.
+elim (move_related_not_empty_pref _ _ H1).
+rewrite <-H3.
+
+split; intros. 
+rewrite Dec.F.remove_neq_iff.
+assumption.
+intro. rewrite <-H5 in H4. elim n. auto.
+apply (VertexSet.remove_3 H4).
+auto.
+Qed.
+
+(* Reciprocally, a vertex which is move-related in g,
+    has a preference degree of 1 and is a preference neighbor of r
+    is nonmove-related in (delete_preference_edges r g H) *)
+Lemma delete_preference_edges_move_inv : forall x r g H,
+~Register.eq r x ->
+move_related g x = true ->
+VertexSet.In x (preference_adj r g) ->
+VertexSet.cardinal (preference_adj x g) = 1 ->
+move_related (delete_preference_edges r g H) x = false.
+
+Proof.
+intros.
+apply move_related_false_charac2. intros.
+rewrite In_delete_preference_edges_edge in H5.
+destruct H5.
+intro. elim H6.
+split. assumption.
+cut (VertexSet.Equal (preference_adj x g) (VertexSet.singleton r)). intros.
+destruct H7;[right|left].
+rewrite (edge_eq e) in H5.
+assert (eq (x, snd_ext e, get_weight e) (fst_ext e, snd_ext e, get_weight e)).
+Eq_eq. rewrite <-H9 in H5.
+destruct H4. rewrite H4 in H5.
+apply VertexSet.singleton_1. rewrite <-H8. 
+rewrite in_pref. exists x0. rewrite edge_comm. auto.
+rewrite (edge_eq e) in H5.
+assert (eq (fst_ext e, x, get_weight e) (fst_ext e, snd_ext e, get_weight e)).
+Eq_eq. rewrite <-H9 in H5.
+destruct H4. rewrite H4 in H5.
+apply VertexSet.singleton_1. rewrite <-H8.
+rewrite in_pref. exists x0. rewrite edge_comm. auto.
+rewrite edge_comm. assumption.
+apply cardinal_1_singleton. apply pref_adj_comm. assumption. assumption.
+Qed.
+
+Lemma delete_preference_edges_move_false_false : forall x r g H,
+move_related g x = false ->
+move_related (delete_preference_edges r g H) x = false.
+
+Proof.
+intros.
+case_eq (move_related (delete_preference_edges r g H) x); intros.
+rewrite (move_related_delete_move_related _ _ _ _ H1) in H0. inversion H0.
+reflexivity.
+Qed.