1 files changed, 60 insertions, 0 deletions
diff --git a/backend/Delete_Preference_Edges_Adjacency.v b/backend/Delete_Preference_Edges_Adjacency.v
new file mode 100755
index 00000000..64ace15a
--- /dev/null
+++ b/backend/Delete_Preference_Edges_Adjacency.v
@@ -0,0 +1,60 @@
+Require Import FSets.
+Require Import InterfGraphMapImp.
+Require Import Merge_Degree.
+Require Import Interference_adjacency.
+Require Import Edges.
+Require Import MyRegisters.
+
+Module Register := Regs.
+
+Import Edge RegFacts Props.
+
+(* The interference neighborhood of any vertex is left
+    unchanged when x is frozen *)
+Lemma interf_adj_delete_preference : forall x r g H,
+VertexSet.Equal (interference_adj x g) 
+                          (interference_adj x (delete_preference_edges r g H)).
+
+Proof.
+split;intros.
+rewrite in_interf. rewrite In_delete_preference_edges_edge.
+rewrite in_interf in H0. split. assumption.
+intro. destruct H1.
+unfold aff_edge in H1. destruct H1. simpl in H1. congruence.
+
+rewrite in_interf in H0. rewrite In_delete_preference_edges_edge in H0. destruct H0.
+rewrite in_interf. assumption.
+Qed.
+
+(* The preference neighborhood of any vertex different from r
+    is obtained by removing r from its preference neighborhood in g *)
+Lemma delete_preference_preference_adj : forall x r g H,
+~Register.eq x r ->
+VertexSet.Equal (preference_adj x (delete_preference_edges r g H))
+                          (VertexSet.remove r (preference_adj x g)).
+
+Proof.
+intros.
+split; intros.
+apply VertexSet.remove_2.
+intro. rewrite <-H2 in H1.
+generalize (pref_adj_comm _ _ _ H1). intro.
+rewrite in_pref in H3. destruct H3.
+rewrite In_delete_preference_edges_edge in H3.
+destruct H3. elim H4. split.
+unfold aff_edge. exists x0. auto.
+right. auto.
+rewrite in_pref in H1.
+destruct H1. rewrite In_delete_preference_edges_edge in H1.
+destruct H1. rewrite in_pref. exists x0. assumption.
+
+(* <= *)
+assert (~Register.eq r a).
+intro. elim (VertexSet.remove_1 H2 H1).
+generalize (VertexSet.remove_3 H1). clear H1. intro.
+rewrite in_pref in H1. destruct H1.
+rewrite in_pref. exists x0.
+rewrite In_delete_preference_edges_edge. split. assumption.
+intro. destruct H3.
+destruct H4; change_rewrite. elim (H2 H4). elim H0; auto.
+Qed.