ajout branche allocation de registres

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 730 insertions, 0 deletions

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.