1 files changed, 73 insertions, 0 deletions
diff --git a/backend/Remove_Vertex_Adjacency.v b/backend/Remove_Vertex_Adjacency.v
new file mode 100755
index 00000000..668063d1
--- /dev/null
+++ b/backend/Remove_Vertex_Adjacency.v
@@ -0,0 +1,73 @@
+Require Import FSets.
+Require Import InterfGraphMapImp.
+Require Import Interference_adjacency.
+Require Import Edges.
+Require Import MyRegisters.
+
+Import RegFacts Props.
+
+Module Register := Regs.
+
+(* For any vertex x different from r, the neighborhood of x in
+    (remove_vertex r g) is its one in g, minus r *)
+Lemma remove_interf_adj : forall x r g,
+~Register.eq x r ->
+VertexSet.Equal (interference_adj x (remove_vertex r g)) 
+                          (VertexSet.remove r (interference_adj x g)).
+
+Proof.
+intros.
+split; intros.
+apply VertexSet.remove_2. intro.
+rewrite <-H1 in H0. rewrite in_interf in H0.
+generalize (proj1 (In_graph_edge_in_ext _ _ H0)). change_rewrite. intro.
+rewrite In_remove_vertex in H2. destruct H2. elim (H3 (Register.eq_refl _)).
+rewrite in_interf in H0. rewrite In_remove_edge in H0. destruct H0.
+rewrite in_interf. assumption.
+
+rewrite in_interf. rewrite In_remove_edge.
+split.
+rewrite <-in_interf. apply (VertexSet.remove_3 H0).
+intro. destruct H1; change_rewrite.
+elim (VertexSet.remove_1 H1 H0).
+elim H. auto.
+Qed.
+
+(* If x is different from r and does not belong to the interference neighborhood
+   of r in g, then the interference neighborhood of x in (remove_vertex r g)
+   is equal to the interference neighborhood of x in g *)
+Lemma interf_adj_remove : forall x r g,
+~VertexSet.In x (interference_adj r g) ->
+~Register.eq x r ->
+VertexSet.Equal (interference_adj x g) (interference_adj x (remove_vertex r g)).
+
+Proof.
+intros x r g H H0.
+rewrite remove_interf_adj. rewrite remove_equal. apply VertexSet.eq_refl.
+intro. elim H. apply interf_adj_comm. assumption.
+auto.
+Qed.
+
+(* The interference neighborhood of x in (remove_vertex r g)
+    is a subset of the interference neighborhood of x in g *)
+Lemma sub_remove_interf : forall x r g,
+~Register.eq x r ->
+VertexSet.Subset (interference_adj x (remove_vertex r g))
+                            (interference_adj x g).
+
+Proof.
+intros x r g H. rewrite remove_interf_adj.
+unfold VertexSet.Subset. intros y H0.
+apply (VertexSet.remove_3 H0).
+assumption.
+Qed.
+
+(* If x is a neighbor of r in g, then x belongs to (remove_vertex r g) *)
+Lemma in_interf_adj_in_remove : forall x r g,
+VertexSet.In x (interference_adj r g) -> In_graph x (remove_vertex r g).
+
+Proof.
+intros x r g H. rewrite In_remove_vertex. split.
+rewrite in_interf in H. apply (proj1 (In_graph_edge_in_ext _ _ H)).
+intro H0. rewrite H0 in H. elim (not_in_interf_self _ _ H).
+Qed.