From a8c744000247af207b489d3cdd4e3d3cf60f72e1 Mon Sep 17 00:00:00 2001 From: blazy Date: Fri, 8 Jan 2010 07:53:02 +0000 Subject: ajout branche allocation de registres git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Merge_Move.v | 730 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 730 insertions(+) create mode 100755 backend/Merge_Move.v (limited to 'backend/Merge_Move.v') diff --git a/backend/Merge_Move.v b/backend/Merge_Move.v new file mode 100755 index 00000000..1e20d001 --- /dev/null +++ b/backend/Merge_Move.v @@ -0,0 +1,730 @@ +Require Import FSetInterface. +Require Import InterfGraphMapImp. +Require Import Remove_Vertex_Move. +Require Import ZArith. +Require Import Edges. +Require Import MyRegisters. +Require Import Affinity_relation. +Require Import Interference_adjacency. +Require Import Graph_Facts. +Require Import Merge_Adjacency. + +Import Edge Props RegFacts. + +(* A nonmove-related vertex of g different from the first endpoint of e + is nonmove-related in (merge e g p q) *) +Lemma move_merge_false : forall x e g p q, +~Register.eq x (fst_ext e) -> +move_related g x = false -> +move_related (merge e g p q) x = false. + +Proof. +intros x e g p q Hfst H0. generalize I. intro H. +case_eq (move_related (merge e g p q) x); intros. +generalize (move_related_charac _ _ H1). intro. +destruct H2. destruct H2. destruct H3. +generalize (In_merge_edge_inv _ _ _ p q H3). intro. +destruct H5. destruct H5. +assert (move_related g x = true). +apply move_related_charac2 with (e := x1). +unfold weak_eq in H6. destruct H6. +unfold same_type in H7. destruct H7. destruct H7. assumption. +destruct H7. destruct H2. unfold interf_edge in H2. congruence. assumption. +destruct H6. +unfold redirect in H6. +destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); destruct H6; change_rewrite; destruct H6. +destruct H4. +elim Hfst. rewrite H4. auto. +right. rewrite H4. auto. +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. +destruct H4. +right. rewrite H4. auto. +elim Hfst. rewrite H4. auto. +destruct H4. +right. rewrite H4. auto. +elim Hfst. rewrite H4. auto. +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. +destruct H4. +left. rewrite H4. auto. +elim Hfst. rewrite H4. auto. +destruct H4. +left. rewrite H4. auto. +right. rewrite H4. auto. +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. +destruct H4. +elim Hfst. rewrite H4. auto. +left. rewrite H4. auto. +destruct H4. +right. rewrite H4. auto. +left. rewrite H4. auto. +rewrite H0 in H7. inversion H7. +auto. +Qed. + +(* Equivalently, a move-related vertex of (merge e g p q) is + move-related in g *) +Lemma move_related_merge_move_related : forall g e x H H0, +move_related (merge e g H H0) x = true -> +move_related g x = true. + +Proof. +intros. case_eq (move_related g x); auto. +intro. assert (~Register.eq x (fst_ext e)). +intro. rewrite (compat_bool_move _ _ _ H3) in H2. +rewrite (proj1 (Aff_edge_aff _ _ H H0)) in H2. inversion H2. +rewrite (move_merge_false _ _ _ H H0 H3 H2) in H1. inversion H1. +Qed. + +(* If x is neither a neighbor of (fst_ext e) nor (snd_ext e) and + if x is move-related in g, then x is move-related in (merge e g H Haff) *) +Lemma move_related_move_related_merge : forall g e x Haff H, +~VertexSet.In x (preference_adj (fst_ext e) g) -> +~VertexSet.In x (preference_adj (snd_ext e) g) -> +move_related g x = true -> +move_related (merge e g H Haff) x = true. + +Proof. +intros. +generalize (move_related_charac _ _ H2). intro. +destruct H3. destruct H3. destruct H4. +assert (~Register.eq x (fst_ext e)). +intro. elim H1. rewrite H6. +rewrite in_pref. destruct Haff. exists x1. rewrite <-H7. +rewrite (edge_eq e) in H. assumption. +assert (~Register.eq x (snd_ext e)). +intro. elim H0. rewrite H7. +rewrite in_pref. destruct Haff. exists x1. rewrite <-H8. +rewrite (edge_eq e) in H. rewrite edge_comm. assumption. + +assert (Prefere (fst_ext (redirect (snd_ext e) (fst_ext e) x0)) + (snd_ext (redirect (snd_ext e) (fst_ext e) x0)) + (merge e g H Haff)). +apply In_merge_pref_edge. assumption. +intro. destruct (eq_charac _ _ H8); destruct H9. +destruct H5. elim H6. rewrite H5. auto. +elim H7. rewrite H5. auto. +destruct H5. elim H7. rewrite H5. auto. +elim H6. rewrite H5. auto. +assumption. + +intro. unfold Interfere in H8. unfold redirect in H8. +destruct (OTFacts.eq_dec (fst_ext x0) (snd_ext e)); change_rewrite. +destruct H5. elim H7. rewrite H5. auto. +elim H1. rewrite in_pref. destruct H3. exists x1. +assert (eq (x, snd_ext e, Some x1) (snd_ext x0, fst_ext x0, Some x1)) by Eq_eq. +rewrite H9. rewrite <-H3. rewrite edge_comm. change Regs.registers with Regs.t. rewrite <-(edge_eq x0). auto. +destruct (OTFacts.eq_dec (snd_ext x0) (snd_ext e)); change_rewrite. +destruct H5. +elim H1. rewrite in_pref. destruct H3. exists x1. +assert (eq (x, snd_ext e, Some x1) (fst_ext x0, snd_ext x0, Some x1)) by Eq_eq. +rewrite H9. rewrite <-H3. rewrite <-(edge_eq x0). auto. +elim H7. rewrite H5. auto. +generalize (In_merge_edge_inv _ _ _ H Haff H8). intro. +destruct H9. destruct H9. destruct H10. +unfold redirect in H10. destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)). +unfold weak_eq in H10; destruct H10; destruct H10; change_rewrite. +destruct H5. elim H6. rewrite H5. auto. +elim H0. rewrite in_pref. destruct H3. exists x2. +assert (eq (x, fst_ext e, Some x2) (snd_ext x0, fst_ext x0, Some x2)) by Eq_eq. +rewrite H13. rewrite edge_comm. rewrite <-H3. change Regs.registers with Regs.t. rewrite <-(edge_eq x0). auto. +destruct H5. +elim H0. rewrite in_pref. destruct H3. exists x2. +assert (eq (x, fst_ext e, Some x2) (fst_ext x0, snd_ext x0, Some x2)) by Eq_eq. +rewrite H13. rewrite <-H3. rewrite <-(edge_eq x0). auto. +elim H6. rewrite H5. auto. +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)). +unfold weak_eq in H10; destruct H10; destruct H10; change_rewrite. +destruct H5. +elim H0. rewrite in_pref. destruct H3. exists x2. +assert (eq (x, fst_ext e, Some x2) (fst_ext x0, snd_ext x0, Some x2)) by Eq_eq. +rewrite H13. rewrite <-H3. rewrite <-(edge_eq x0). auto. +elim H6. rewrite H5. auto. +destruct H5. elim H6. rewrite H5. auto. +elim H0. rewrite in_pref. destruct H3. exists x2. +assert (eq (x, fst_ext e, Some x2) (snd_ext x0, fst_ext x0, Some x2)) by Eq_eq. +rewrite H13. rewrite <-H3. rewrite edge_comm. change Regs.registers with Regs.t. rewrite <-(edge_eq x0). auto. +elim (interf_pref_conflict (fst_ext x0) (snd_ext x0) g). +unfold Prefere, Interfere. split. +destruct H3. exists x2. rewrite <-H3. change Regs.registers with Regs.t. rewrite <-(edge_eq x0). auto. +assert (eq (fst_ext x0, snd_ext x0, None) (fst_ext x1, snd_ext x1, None)). +unfold weak_eq in H10; destruct H10; destruct H10; change_rewrite. +Eq_eq. Eq_comm_eq. rewrite H12. +unfold same_type in H11. destruct H11; destruct H11. +destruct H13. simpl in H13. congruence. +rewrite <-H11. rewrite <-(edge_eq x1). auto. + +unfold redirect in H8. destruct (OTFacts.eq_dec (fst_ext x0) (snd_ext e)); change_rewrite. +destruct H5. elim H7. rewrite H5. auto. +elim H1. rewrite in_pref. destruct H3. exists x1. +assert (eq (x, snd_ext e, Some x1) (fst_ext x0, snd_ext x0, Some x1)) by Eq_comm_eq. +rewrite H9. rewrite <-H3. rewrite <-(edge_eq x0). auto. +destruct (OTFacts.eq_dec (snd_ext x0) (snd_ext e)); change_rewrite. +destruct H5. +elim H1. rewrite in_pref. destruct H3. exists x1. +assert (eq (x, snd_ext e, Some x1) (fst_ext x0, snd_ext x0, Some x1)) by Eq_eq. +rewrite H9. rewrite <-H3. rewrite <-(edge_eq x0). auto. +elim H7. rewrite H5. auto. +unfold Prefere in H8. destruct H8. +apply (move_related_charac2 _ _ (fst_ext x0, snd_ext x0, Some x1)). +unfold aff_edge. exists x1. auto. +assumption. +destruct H5;[left|right]; auto. +Qed. + +Lemma interfere_dec : forall x y g, +Interfere x y g \/ ~Interfere x y g. + +Proof. +intros. unfold Interfere. +destruct (RegRegProps.In_dec (x,y,None) (IE g)). +left. right. assumption. +right. intro. elim n. +rewrite In_graph_interf_edge_in_IE. split. +unfold interf_edge. auto. +assumption. +Qed. + +(* A vertex x different from r which is move-related in g and nonmove-related + in (merge e g p q) is either + 1) interfering with the first endpoint of e and prefering with the second one + 2) interfering with the second endpoint of e and prefering with the first one *) +Lemma move_merge_not_move : forall x e g p q, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +move_related (merge e g p q) x = false -> +move_related g x = true -> +(VertexSet.In x (VertexSet.inter (interference_adj (fst_ext e) g) (preference_adj (snd_ext e) g))) \/ +(VertexSet.In x (VertexSet.inter (interference_adj (snd_ext e) g) (preference_adj (fst_ext e) g))). + +Proof. +intros x e g p q H0 H1 H2 H3. generalize I. intro H. +generalize (move_related_charac _ _ H3). intro. +destruct H4. destruct H4. destruct H5. +cut (Interfere (fst_ext (redirect (snd_ext e) (fst_ext e) x0)) + (snd_ext (redirect (snd_ext e) (fst_ext e) x0)) + (merge e g p q)). intro. +unfold Interfere in H7. unfold redirect in H7. +destruct (OTFacts.eq_dec (fst_ext x0) (snd_ext e)); change_rewrite. +destruct H6. +elim H1. rewrite H6. auto. +generalize (In_merge_edge_inv e _ g p q H7). intro. +destruct H8. destruct H8. destruct H9 as [H9 HH9]. +assert (eq (fst_ext e, snd_ext x0, None) (redirect (snd_ext e) (fst_ext e) x1)). +unfold weak_eq; destruct H9; destruct H9; change_rewrite. +apply eq_ordered_eq. split; intuition. change_rewrite. rewrite redirect_weight_eq. +unfold same_type in HH9. destruct HH9. destruct H11. +destruct H12. simpl in H12. congruence. +destruct H11. rewrite <-H11. apply OptionN_as_OT.eq_refl. +Eq_comm_eq. simpl. rewrite redirect_weight_eq. +unfold same_type in HH9. destruct HH9. destruct H11. +destruct H12. simpl in H12. congruence. +destruct H11. rewrite <-H11. apply OptionN_as_OT.eq_refl. +generalize H10. clear H9 HH9 H10. intro H9. +unfold redirect in H9. +destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)). +destruct (eq_charac _ _ H9); change_rewrite; destruct H10. +elim (interf_pref_conflict x (snd_ext e) g). +split. +destruct H4. +unfold Prefere. exists x2. +cut (eq (x, snd_ext e, Some x2) x0). intro. +rewrite H12. auto. +rewrite (edge_eq x0). +rewrite edge_comm. apply eq_ordered_eq. constructor; simpl. +split; intuition. +rewrite H4. apply OptionN_as_OT.eq_refl. +unfold Interfere. +cut (eq (x, snd_ext e, None) x1). intro. +rewrite H12. auto. +rewrite (edge_eq x1). +rewrite edge_comm. apply eq_ordered_eq. constructor;simpl. +split; intuition. rewrite H6. auto. +generalize (get_weight_m _ _ (eq_sym H9)). simpl. intro. +rewrite H12. apply OptionN_as_OT.eq_refl. + +elim H0. rewrite H6. auto. +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)). +destruct (eq_charac _ _ H9); change_rewrite. destruct H10. +elim H0. rewrite H6. auto. +destruct H10. + +elim (interf_pref_conflict x (snd_ext e) g). +split. +destruct H4. +unfold Prefere. exists x2. +cut (eq (x, snd_ext e, Some x2) x0). intro. +rewrite H12. auto. +rewrite (edge_eq x0). +rewrite edge_comm. apply eq_ordered_eq. constructor; simpl. +split; intuition. +rewrite H4. apply OptionN_as_OT.eq_refl. +unfold Interfere. +cut (eq (x, snd_ext e, None) x1). intro. +rewrite H12. auto. +rewrite (edge_eq x1). +apply eq_ordered_eq. constructor;simpl. +split; try rewrite H6; intuition. +generalize (get_weight_m _ _ (eq_sym H9)). simpl. intro. +rewrite H12. apply OptionN_as_OT.eq_refl. +left. apply VertexSet.inter_3. +rewrite in_interf. +cut (eq (x, fst_ext e, None) (fst_ext e, snd_ext x0, None)). intro. +rewrite H10. rewrite H9. auto. +rewrite edge_comm. apply eq_ordered_eq. +constructor; simpl. split; intuition. +apply OptionN_as_OT.eq_refl. +destruct H4. +rewrite in_pref. exists x2. +cut (eq (x,snd_ext e, Some x2) x0). intro. +rewrite H10. auto. +rewrite edge_comm. apply eq_ordered_eq. rewrite (edge_eq x0). +constructor; simpl. split; intuition. +auto. auto. rewrite H4. apply OptionN_as_OT.eq_refl. + +destruct (OTFacts.eq_dec (snd_ext x0) (snd_ext e)); change_rewrite. +destruct H6. +generalize (In_merge_edge_inv e _ g p q H7). intro. +destruct H8. destruct H8. destruct H9 as [H9 HH9]. +assert (eq (fst_ext x0, fst_ext e, None) (redirect (snd_ext e) (fst_ext e) x1)). +unfold weak_eq; destruct H9; destruct H9; change_rewrite. +Eq_eq. simpl. rewrite redirect_weight_eq. +unfold same_type in HH9. destruct HH9. destruct H11. +destruct H12. simpl in H12. congruence. +destruct H11. rewrite <-H11. apply OptionN_as_OT.eq_refl. +Eq_comm_eq. simpl. rewrite redirect_weight_eq. +unfold same_type in HH9. destruct HH9. destruct H11. +destruct H12. simpl in H12. congruence. +destruct H11. rewrite <-H11. apply OptionN_as_OT.eq_refl. +generalize H10. clear H9 HH9 H10. intro H9. +unfold redirect in H9. +destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)). +destruct (eq_charac _ _ H9); change_rewrite; destruct H10. +elim H0. rewrite H6. auto. +elim (interf_pref_conflict x (snd_ext e) g). +split. +destruct H4. +unfold Prefere. exists x2. +cut (eq (x, snd_ext e, Some x2) x0). intro. +rewrite H12. auto. +rewrite (edge_eq x0). +apply eq_ordered_eq. constructor; simpl. +split; intuition. +auto. +auto. +rewrite H4. apply OptionN_as_OT.eq_refl. +unfold Interfere. +cut (eq (x, snd_ext e, None) x1). intro. +rewrite H12. auto. +rewrite (edge_eq x1). +rewrite edge_comm. apply eq_ordered_eq. constructor;simpl. +split; try rewrite H6; intuition. +generalize (get_weight_m _ _ (eq_sym H9)). simpl. intro. +rewrite H12. apply OptionN_as_OT.eq_refl. + +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)). +destruct (eq_charac _ _ H9); change_rewrite. destruct H10. +elim (interf_pref_conflict x (snd_ext e) g). +split. +destruct H4. +unfold Prefere. exists x2. +cut (eq (x, snd_ext e, Some x2) x0). intro. +rewrite H12. auto. +rewrite (edge_eq x0). +apply eq_ordered_eq. constructor; simpl. +split; intuition. +rewrite H4. apply OptionN_as_OT.eq_refl. +unfold Interfere. +cut (eq (x, snd_ext e, None) x1). intro. +rewrite H12. auto. +rewrite (edge_eq x1). +apply eq_ordered_eq. constructor;simpl. +split; try rewrite H6; intuition. +generalize (get_weight_m _ _ (eq_sym H9)). simpl. intro. +rewrite H12. apply OptionN_as_OT.eq_refl. + +destruct H10. elim H0. rewrite H6. auto. + +left. apply VertexSet.inter_3. +rewrite in_interf. +cut (eq (x, fst_ext e, None) (fst_ext x0, fst_ext e, None)). intro. +rewrite H10. rewrite H9. auto. +apply eq_ordered_eq. +constructor; simpl. split; intuition. +apply OptionN_as_OT.eq_refl. +destruct H4. +rewrite in_pref. exists x2. +cut (eq (x,snd_ext e, Some x2) x0). intro. +rewrite H10. auto. +apply eq_ordered_eq. rewrite (edge_eq x0). +constructor; simpl. split; intuition. +rewrite H4. apply OptionN_as_OT.eq_refl. + +elim H1. rewrite H6. auto. +generalize (In_merge_edge_inv e _ g p q H7). intro. +destruct H8. destruct H8. destruct H9 as [H9 HH9]. +assert (eq (fst_ext x0, snd_ext x0, None) (redirect (snd_ext e) (fst_ext e) x1)). +unfold weak_eq; destruct H9; destruct H9; change_rewrite. +Eq_eq. simpl. rewrite redirect_weight_eq. +unfold same_type in HH9. destruct HH9. destruct H11. +destruct H12. simpl in H12. congruence. +destruct H11. rewrite <-H11. apply OptionN_as_OT.eq_refl. +Eq_comm_eq. simpl. rewrite redirect_weight_eq. +unfold same_type in HH9. destruct HH9. destruct H11. +destruct H12. simpl in H12. congruence. +destruct H11. rewrite <-H11. apply OptionN_as_OT.eq_refl. +generalize H10. clear H9 HH9 H10. intro H9. +unfold redirect in H9. +destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)). +destruct (eq_charac _ _ H9); change_rewrite; destruct H10. +destruct H6. elim H0. rewrite H6. auto. +right. apply VertexSet.inter_3. +rewrite in_interf. +cut (eq (x, snd_ext e, None) x1). intro. +rewrite H12. auto. +rewrite edge_comm. apply eq_ordered_eq. +constructor; simpl. split; intuition. +auto. rewrite H6. auto. +generalize (get_weight_m _ _ H9). simpl. intro. +rewrite H12. unfold get_weight. apply OptionN_as_OT.eq_refl. +destruct H4. +rewrite in_pref. exists x2. +cut (eq (x, fst_ext e, Some x2) x0). intro. +rewrite H12. auto. +rewrite edge_comm. apply eq_ordered_eq. rewrite (edge_eq x0). +constructor; simpl. split; intuition. +auto. auto. rewrite H4. apply OptionN_as_OT.eq_refl. + +destruct H6. +right. apply VertexSet.inter_3. +rewrite in_interf. +cut (eq (x, snd_ext e, None) x1). intro. +rewrite H12. auto. +rewrite edge_comm. apply eq_ordered_eq. +constructor; simpl. split; intuition. +auto. rewrite H6. auto. +generalize (get_weight_m _ _ H9). simpl. intro. +rewrite H12. unfold get_weight. apply OptionN_as_OT.eq_refl. +destruct H4. +rewrite in_pref. exists x2. +cut (eq (x, fst_ext e, Some x2) x0). intro. +rewrite H12. auto. +apply eq_ordered_eq. rewrite (edge_eq x0). +constructor; simpl. split; intuition. +auto. auto. rewrite H4. apply OptionN_as_OT.eq_refl. + +elim H0. rewrite H6. auto. +destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)). +destruct (eq_charac _ _ H9); change_rewrite; destruct H10. +destruct H6. +right. apply VertexSet.inter_3. +rewrite in_interf. +cut (eq (x, snd_ext e, None) x1). intro. +rewrite H12. auto. +apply eq_ordered_eq. +constructor; simpl. split; intuition. +rewrite H6. auto. auto. +generalize (get_weight_m _ _ H9). simpl. intro. +rewrite H12. unfold get_weight. apply OptionN_as_OT.eq_refl. +destruct H4. +rewrite in_pref. exists x2. +cut (eq (x, fst_ext e, Some x2) x0). intro. +rewrite H12. auto. +apply eq_ordered_eq. rewrite (edge_eq x0). +constructor; simpl. split; intuition. +auto. auto. rewrite H4. apply OptionN_as_OT.eq_refl. + +elim H0. rewrite H6. auto. + +destruct H6. +elim H0. rewrite H6. auto. +right. apply VertexSet.inter_3. +rewrite in_interf. +cut (eq (x, snd_ext e, None) x1). intro. +rewrite H12. auto. +apply eq_ordered_eq. +constructor; simpl. split; intuition. +rewrite H6. auto. auto. +generalize (get_weight_m _ _ H9). simpl. intro. +rewrite H12. unfold get_weight. apply OptionN_as_OT.eq_refl. +destruct H4. +rewrite in_pref. exists x2. +cut (eq (x, fst_ext e, Some x2) x0). intro. +rewrite H12. auto. +rewrite edge_comm. apply eq_ordered_eq. rewrite (edge_eq x0). +constructor; simpl. split; intuition. +auto. auto. rewrite H4. apply OptionN_as_OT.eq_refl. + +elim (interf_pref_conflict (fst_ext x0) (snd_ext x0) g). +split. +unfold Prefere. destruct H4. exists x2. +rewrite <-H4. change Regs.registers with Regs.t. rewrite <-(edge_eq x0). assumption. +unfold Interfere. rewrite H9. assumption. + +(* cut *) +destruct (interfere_dec (fst_ext (redirect (snd_ext e) (fst_ext e) x0)) + (snd_ext (redirect (snd_ext e) (fst_ext e) x0)) + (merge e g p q)). auto. +cut (~eq e x0). intro. +generalize (In_merge_pref_edge e x0 g p q H5 H8 H4 H7). intro. clear H7. +unfold Prefere in H9. destruct H9. unfold redirect in H7. +destruct (OTFacts.eq_dec (fst_ext x0) (snd_ext e)); change_rewrite. +destruct H6. +elim H1. rewrite H6. auto. +assert (move_related (merge e g p q) x = true). +apply move_related_charac2 with (e:= (fst_ext e, snd_ext x0, Some x1)). +exists x1. auto. +auto. +right. change_rewrite. auto. +rewrite H2 in H9. inversion H9. + +destruct (OTFacts.eq_dec (snd_ext x0) (snd_ext e)); change_rewrite. +destruct H6. +assert (move_related (merge e g p q) x = true). +apply move_related_charac2 with (e:= (fst_ext x0, fst_ext e, Some x1)). +exists x1. auto. +auto. +left. change_rewrite. auto. +rewrite H2 in H9. inversion H9. + +elim H1. rewrite H6. auto. + +assert (move_related (merge e g p q) x = true). +apply move_related_charac2 with (e:= (fst_ext x0, snd_ext x0, Some x1)). +exists x1. auto. +auto. +destruct H6;[left|right]; auto. +rewrite H2 in H9. inversion H9. + +intro. destruct (eq_charac _ _ H8); destruct H9. +destruct H6. +elim H0. rewrite H6. auto. +elim H1. rewrite H6. auto. +destruct H6. +elim H1. rewrite H6. auto. +elim H0. rewrite H6. auto. +Qed. + +(* A move-related vertex of g which does not interfere with an endpoint + of e and prefere with the other one is move-related in (merge e g p q) *) +Lemma move_related_merge_true : forall x e g p q, +move_related g x = true -> +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +~VertexSet.In x (VertexSet.inter (interference_adj (fst_ext e ) g) + (preference_adj (snd_ext e) g)) -> +~VertexSet.In x (VertexSet.inter (interference_adj (snd_ext e) g) + (preference_adj (fst_ext e) g)) -> +move_related (merge e g p q) x = true. + +Proof. +intros x e g p q H0 H1 H2 H3 H4. generalize I. intro H. +case_eq (move_related (merge e g p q) x); intros. +reflexivity. +generalize (move_merge_not_move _ _ _ p q H1 H2 H5 H0). intro. +destruct H6;[elim (H3 H6)|elim (H4 H6)]. +Qed. + +(* A vertex which interferes with an endpoint of e, preferes with + the other one and has a preference degree of one is + nonmove-related in (merge e g p q) *) +Lemma move_related_change_charac : forall x e g p q, +VertexSet.In x (VertexSet.union (VertexSet.inter (interference_adj (fst_ext e) g) + (preference_adj (snd_ext e) g)) + (VertexSet.inter (interference_adj (snd_ext e) g) + (preference_adj (fst_ext e) g))) -> +pref_degree g x = 1 -> +move_related (merge e g p q) x = false. + +Proof. +unfold pref_degree. intros x e g p q H1 H2. generalize I. intro H. +assert (move_related g x = true). +case_eq (move_related g x); auto. intro. +rewrite move_related_card in H0. inversion H0. +unfold pref_degree. congruence. +assert (~Register.eq x (fst_ext e)) as Hfst. +intro. rewrite H3 in H1. +destruct (VertexSet.union_1 H1). +elim (not_in_interf_self (fst_ext e) g). +apply (VertexSet.inter_1 H4). +elim (not_in_pref_self (fst_ext e) g). +apply (VertexSet.inter_2 H4). +assert (~Register.eq x (snd_ext e)) as Hsnd. +intro. rewrite H3 in H1. +destruct (VertexSet.union_1 H1). +elim (not_in_pref_self (snd_ext e) g). +apply (VertexSet.inter_2 H4). +elim (not_in_interf_self (snd_ext e) g). +apply (VertexSet.inter_1 H4). +destruct (VertexSet.union_1 H1). +assert (VertexSet.Equal (preference_adj x g) (VertexSet.singleton (snd_ext e))). +apply cardinal_1_singleton. +apply pref_adj_comm. apply (VertexSet.inter_2 H3). +assumption. + +assert (VertexSet.Equal (preference_adj x (merge e g p q)) VertexSet.empty). +split; intros. +assert (VertexSet.Subset (preference_adj x (merge e g p q)) + (VertexSet.add (fst_ext e) + (VertexSet.remove (snd_ext e) (preference_adj x g)))). +apply preference_adj_merge; assumption. +destruct (Register.eq_dec a (fst_ext e)). +elim (interf_pref_conflict (fst_ext e) x (merge e g p q)). +split. +rewrite in_pref in H5. destruct H5. +unfold Prefere. exists x0. +assert (eq (fst_ext e, x, Some x0) (a, x, Some x0)) by Eq_eq. +rewrite H7. assumption. +unfold Interfere. +assert (eq (fst_ext e, x,None) (redirect (snd_ext e) (fst_ext e) (fst_ext e, x,None))). +apply eq_ordered_eq. +split; simpl; try split; try apply Regs.eq_refl. +unfold redirect; change_rewrite. +destruct (OTFacts.eq_dec (fst_ext e) (snd_ext e)). apply Regs.eq_refl. +destruct (OTFacts.eq_dec x (snd_ext e)). apply Regs.eq_refl. apply Regs.eq_refl. +unfold redirect; change_rewrite; simpl. +destruct (OTFacts.eq_dec (fst_ext e) (snd_ext e)). apply Regs.eq_refl. +destruct (OTFacts.eq_dec x (snd_ext e)). simpl. +elim (not_in_pref_self (snd_ext e) g). +rewrite r in H3. apply (VertexSet.inter_2 H3). apply Regs.eq_refl. +auto. rewrite redirect_weight_eq. simpl. apply OptionN_as_OT.eq_refl. +rewrite H7. apply In_merge_interf_edge. +rewrite <-in_interf. apply interf_adj_comm. apply (VertexSet.inter_1 H3). +unfold interf_edge. auto. + +assert (VertexSet.In a (VertexSet.add (fst_ext e) (VertexSet.remove (snd_ext e) (preference_adj x g)))). +apply H6. assumption. +assert (VertexSet.In a (VertexSet.remove (snd_ext e) (preference_adj x g))). +apply VertexSet.add_3 with (x:=fst_ext e); auto. +rewrite H4 in H8. +assert (~Register.eq a (snd_ext e)). +intro. elim (VertexSet.remove_1 (Register.eq_sym _ _ H9) H8). +generalize (VertexSet.remove_3 H8). intro. +generalize (VertexSet.singleton_1 H10). intro. elim H9. auto. +elim (VertexSet.empty_1 H5). +case_eq (move_related (merge e g p q) x); intros. +elim (move_related_not_empty_pref _ _ H6). assumption. +reflexivity. + +(* symetric part *) +assert (VertexSet.Equal (preference_adj x g) (VertexSet.singleton (fst_ext e))). +apply cardinal_1_singleton. +apply pref_adj_comm. apply (VertexSet.inter_2 H3). +assumption. + +assert (VertexSet.Equal (preference_adj x (merge e g p q)) VertexSet.empty). +split; intros. +assert (VertexSet.Subset (preference_adj x (merge e g p q)) + (VertexSet.add (fst_ext e) + (VertexSet.remove (snd_ext e) (preference_adj x g)))). +apply preference_adj_merge; assumption. +destruct (Register.eq_dec a (fst_ext e)). +elim (interf_pref_conflict (fst_ext e) x (merge e g p q)). +split. +rewrite in_pref in H5. destruct H5. +unfold Prefere. exists x0. +assert (eq (fst_ext e, x, Some x0) (a, x, Some x0)) by Eq_eq. +rewrite H7. assumption. +unfold Interfere. +assert (eq (fst_ext e, x,None) (redirect (snd_ext e) (fst_ext e) (snd_ext e, x,None))). +apply eq_ordered_eq. +split; simpl; try split; auto. +unfold redirect; change_rewrite. +destruct (OTFacts.eq_dec (snd_ext e) (snd_ext e)). apply Regs.eq_refl. +elim n. apply Regs.eq_refl. +unfold redirect; change_rewrite. +destruct (OTFacts.eq_dec (snd_ext e) (snd_ext e)). apply Regs.eq_refl. +elim n. apply Regs.eq_refl. +rewrite redirect_weight_eq. simpl. apply OptionN_as_OT.eq_refl. +rewrite H7. apply In_merge_interf_edge. +rewrite <-in_interf. apply interf_adj_comm. apply (VertexSet.inter_1 H3). +unfold interf_edge. auto. + +assert (VertexSet.In a (VertexSet.add (fst_ext e) (VertexSet.remove (snd_ext e) (preference_adj x g)))). +apply H6. assumption. +assert (VertexSet.In a (VertexSet.remove (snd_ext e) (preference_adj x g))). +apply VertexSet.add_3 with (x:=fst_ext e); auto. +rewrite H4 in H8. +generalize (VertexSet.remove_3 H8). intro. +generalize (VertexSet.singleton_1 H9). intro. elim n. auto. +elim (VertexSet.empty_1 H5). +case_eq (move_related (merge e g p q) x); intros. +elim (move_related_not_empty_pref _ _ H6). assumption. +reflexivity. +Qed. + +(* A move-related vertex of g which is not move-related in + (merge e g p q) has a preference degree of 1 *) +Lemma move_related_dec_1 : forall x e g p q, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +move_related g x = true -> +move_related (merge e g p q) x = false -> +pref_degree g x = 1. + +Proof. +unfold pref_degree. intros x e g p q H0 H1 H2 H3. generalize I. intro H. +generalize (preference_adj_merge_2 x e g p q H0 H1). intro. +cut (VertexSet.cardinal (preference_adj x g) <= 1). intro. +cut (VertexSet.cardinal (preference_adj x g) > 0). intro. +intuition. +generalize (move_related_not_empty_pref x g H2). intro. +case_eq (VertexSet.cardinal (preference_adj x g)); intros. +elim H6. apply empty_is_empty_1. apply (cardinal_inv_1 H7). +intuition. +generalize (not_move_related_empty_pref x (merge e g p q) H3). intro. +generalize (move_merge_not_move _ _ _ p q H0 H1 H3 H2). intro. +destruct H6. +assert (VertexSet.cardinal (VertexSet.remove (fst_ext e) (VertexSet.remove (snd_ext e) (preference_adj x g))) <= + (VertexSet.cardinal (preference_adj x (merge e g p q)))). +apply subset_cardinal. assumption. +rewrite H5 in H7. rewrite empty_cardinal in H7. +rewrite remove_cardinal_2 in H7. +rewrite <-remove_cardinal_1 with (x:=snd_ext e). +apply le_n_S. assumption. +apply pref_adj_comm. apply (VertexSet.inter_2 H6). +intro. generalize (VertexSet.remove_3 H8). intro. +elim (interf_pref_conflict (fst_ext e) x g). +split. +rewrite in_pref in H9. destruct H9. +unfold Prefere. exists x0. assumption. +unfold Interfere. +rewrite edge_comm. generalize (VertexSet.inter_1 H6). intro. +rewrite in_interf in H10. assumption. +assert (VertexSet.cardinal (VertexSet.remove (fst_ext e) (VertexSet.remove (snd_ext e) (preference_adj x g))) <= + (VertexSet.cardinal (preference_adj x (merge e g p q)))). +apply subset_cardinal. assumption. +rewrite H5 in H7. rewrite empty_cardinal in H7. +rewrite <-remove_cardinal_2 with (x:=snd_ext e). +rewrite <-remove_cardinal_1 with (x:=fst_ext e). +apply le_n_S. assumption. +apply VertexSet.remove_2. +apply (In_graph_edge_diff_ext e g p). +apply pref_adj_comm. apply (VertexSet.inter_2 H6). +intro. elim (interf_pref_conflict (snd_ext e) x g). +split. +rewrite in_pref in H8. destruct H8. +unfold Prefere. exists x0. assumption. +generalize (VertexSet.inter_1 H6). intro. +unfold Interfere. rewrite edge_comm. rewrite <-in_interf. assumption. +Qed. + +(* Again, meaningful theorem *) +Theorem Merge_move_evolution : forall x e g p q, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +((move_related g x = true /\ move_related (merge e g p q) x = false) + <-> + (pref_degree g x = 1 /\ + (VertexSet.In x (VertexSet.inter (interference_adj (fst_ext e) g) (preference_adj (snd_ext e) g)) \/ + VertexSet.In x (VertexSet.inter (interference_adj (snd_ext e) g) (preference_adj (fst_ext e) g))))). + +Proof. +split; intros. +destruct H1. +split. apply (move_related_dec_1 x e g p q); auto. + apply (move_merge_not_move x e g p q); auto. +destruct H1. +split. case_eq (move_related g x); auto. intro. rewrite move_related_card in H3; congruence. + apply move_related_change_charac; auto. + destruct H2;[apply VertexSet.union_2|apply VertexSet.union_3]; auto. +Qed. -- cgit