From 307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 13 Jan 2010 09:53:07 +0000 Subject: Backtracking on commit 1220 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Interference_adjacency.v | 66 ---------------------------------------- 1 file changed, 66 deletions(-) delete mode 100755 backend/Interference_adjacency.v (limited to 'backend/Interference_adjacency.v') diff --git a/backend/Interference_adjacency.v b/backend/Interference_adjacency.v deleted file mode 100755 index 3d5d90dd..00000000 --- a/backend/Interference_adjacency.v +++ /dev/null @@ -1,66 +0,0 @@ -Require Import InterfGraphMapImp. -Require Import Graph_Facts. -Require Import FSets. -Require Import SetsFacts. -Require Import Edges. - -Import Edge RegFacts Props RegRegProps. - -(* Some properties about the interference adjacency - and the same about preference adjacency *) - -(* x is not in its own interference neighborhood *) -Lemma not_in_interf_self : forall x g, -~VertexSet.In x (interference_adj x g). - -Proof. -intros x g. rewrite in_interf. intro H. -elim (In_graph_edge_diff_ext _ _ H). auto. -Qed. - -(* x is not in its own preference neighborhood *) -Lemma not_in_pref_self : forall x g, -~VertexSet.In x (preference_adj x g). - -Proof. -intros x g. rewrite in_pref. intro H. destruct H. -elim (In_graph_edge_diff_ext _ _ H). auto. -Qed. - -(* If x is an interference neighbor of y in g - then y is an interference neighbor of x in g *) -Lemma interf_adj_comm : forall x y g, -VertexSet.In x (interference_adj y g) -> VertexSet.In y (interference_adj x g). - -Proof. -intros x y g H. rewrite in_interf. rewrite edge_comm. rewrite <-in_interf. auto. -Qed. - -(* If x is a preference neighbor of y in g - then y is a preference neighbor of x in g *) -Lemma pref_adj_comm : forall x y g, -VertexSet.In x (preference_adj y g) -> VertexSet.In y (preference_adj x g). - -Proof. -intros x y g H. -rewrite in_pref in H. destruct H. rewrite edge_comm in H. -rewrite in_pref. exists x0. assumption. -Qed. - -(* If x is an interference neighbor of any vertex of g then x is in g *) -Lemma in_interf_in : forall x r g, -VertexSet.In x (interference_adj r g) -> In_graph x g. - -Proof. -intros x r g H. rewrite in_interf in H. -apply (proj1 (In_graph_edge_in_ext _ _ H)). -Qed. - -(* If x is a preferenec neighbor of any vertex then x is in g *) -Lemma in_pref_in : forall x r g, -VertexSet.In x (preference_adj r g) -> In_graph x g. - -Proof. -intros x r g H. rewrite in_pref in H. destruct H. -apply (proj1 (In_graph_edge_in_ext _ _ H)). -Qed. -- cgit