diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-13 09:53:07 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-01-13 09:53:07 +0000 |
commit | 307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac (patch) | |
tree | 1f8ce41f366bf19b777a1934ae0b1eb09be0a9f3 /backend/Delete_Preference_Edges_Move.v | |
parent | 33a4bcf3695d0ee2793b3bdd12f6ee787d152f36 (diff) | |
download | compcert-307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac.tar.gz compcert-307da4d1fb744bb3c66e5a43acd7702f0ce1b7ac.zip |
Backtracking on commit 1220v1.6
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1228 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Delete_Preference_Edges_Move.v')
-rwxr-xr-x | backend/Delete_Preference_Edges_Move.v | 138 |
1 files changed, 0 insertions, 138 deletions
diff --git a/backend/Delete_Preference_Edges_Move.v b/backend/Delete_Preference_Edges_Move.v deleted file mode 100755 index 66f9ab6a..00000000 --- a/backend/Delete_Preference_Edges_Move.v +++ /dev/null @@ -1,138 +0,0 @@ -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. |