diff options
Diffstat (limited to 'backend/Merge_Move.v')
| -rwxr-xr-x | backend/Merge_Move.v | 730 |
1 files changed, 0 insertions, 730 deletions
diff --git a/backend/Merge_Move.v b/backend/Merge_Move.v deleted file mode 100755 index 1e20d00..0000000 --- a/backend/Merge_Move.v +++ /dev/null @@ -1,730 +0,0 @@ -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. |