diff options
Diffstat (limited to 'backend/Merge_Adjacency.v')
| -rwxr-xr-x | backend/Merge_Adjacency.v | 347 |
1 files changed, 0 insertions, 347 deletions
diff --git a/backend/Merge_Adjacency.v b/backend/Merge_Adjacency.v deleted file mode 100755 index d6d879a..0000000 --- a/backend/Merge_Adjacency.v +++ /dev/null @@ -1,347 +0,0 @@ -Require Import FSets. -Require Import InterfGraphMapImp. -Require Import Remove_Vertex_Degree. -Require Import Edges. -Require Import MyRegisters. -Require Import Interference_adjacency. -Require Import Graph_Facts. - -Module Register := Regs. - -Import Edge RegFacts Props. - -(* The following lemmas define the interference adjacency - of the first endpoint of e after the merge of e *) - -Lemma merge_interf_adj_fst_1 : forall e g H0 Haff, -VertexSet.Subset (interference_adj (fst_ext e) (merge e g H0 Haff)) - (VertexSet.union (interference_adj (fst_ext e) g) - (interference_adj (snd_ext e) g)). - -Proof. -unfold VertexSet.Subset. intros e g H Haff a H1. -rewrite in_interf in H1. generalize (In_merge_edge_inv _ _ _ H Haff H1); intro. -destruct H0 as [x H0]. destruct H0 as [H3 H4]. -destruct x as [ex wx]. destruct ex as [x1 x2]. -assert (interf_edge (x1,x2,wx)) as Hinterf. -destruct H4. unfold same_type in H2. destruct H2; destruct H2. -unfold aff_edge in H4. destruct H4. simpl in H4. congruence. -assumption. -destruct H4 as [H4 HH4]. -assert (eq (a, fst_ext e, None) (redirect (snd_ext e) (fst_ext e) (x1,x2,wx))). -apply weak_eq_interf_eq. assumption. unfold interf_edge. auto. -unfold interf_edge. rewrite redirect_weight_eq. auto. clear H4. -generalize (redirect_charac (x1,x2,wx) (snd_ext e) (fst_ext e)); intros. -destruct H2. destruct H2. destruct H4. rewrite <-H2 in H0. -apply VertexSet.union_2. rewrite in_interf. rewrite H0. assumption. -destruct H2. destruct H2. rewrite <-H2 in H0. change_rewrite. -apply VertexSet.union_3. rewrite in_interf. -destruct (eq_charac _ _ H0); destruct H5; change_rewrite. -assert (eq (a, snd_ext e, None) (x1, x2, wx)). -Eq_comm_eq. apply (Register.eq_trans _ _ _ H5 H6). -generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl. -rewrite H7. assumption. -assert (eq (a,snd_ext e, None) (x1,x2,wx)). -Eq_comm_eq. -generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl. -rewrite H7. assumption. -destruct H2; change_rewrite. rewrite <-H2 in H0. -destruct (eq_charac _ _ H0); destruct H5; change_rewrite. -apply VertexSet.union_3. rewrite in_interf. -assert (eq (a, snd_ext e, None) (x1,x2,wx)). -Eq_eq. -generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl. -rewrite H7. assumption. -apply VertexSet.union_3. rewrite in_interf. -assert (eq (a, snd_ext e, None) (x1,x2,wx)). -Eq_eq. -apply (Register.eq_trans _ _ _ H5 H6). -generalize (get_weight_m _ _ H0). simpl. intro. rewrite H7. apply OptionN_as_OT.eq_refl. -rewrite H7. assumption. -Qed. - -Lemma merge_interf_adj_fst_2 : forall e g H0 Haff, -VertexSet.Subset (interference_adj (fst_ext e) g) - (interference_adj (fst_ext e) (merge e g H0 Haff)). - -Proof. -unfold VertexSet.Subset. intros. -rewrite in_interf in H. rewrite in_interf. -destruct (redirect_charac (a, fst_ext e, None) (snd_ext e) (fst_ext e)); intros. -change_rewrite. destruct H1. destruct H2. -rewrite H1. apply In_merge_interf_edge. assumption. -unfold interf_edge. auto. -change_rewrite. destruct H1. destruct H1. -elim (interf_pref_conflict (snd_ext e) (fst_ext e) g). -split. unfold Prefere. destruct Haff. exists x. -rewrite edge_comm. rewrite <-H3. rewrite (edge_eq e) in H0. assumption. -unfold Interfere. -assert (eq (snd_ext e, fst_ext e, None) (a, fst_ext e, None)) by Eq_eq. -rewrite H3. assumption. -destruct H1. rewrite H1. apply In_merge_interf_edge. assumption. -unfold interf_edge. auto. -Qed. - -Lemma merge_interf_adj_fst_3 : forall e g H0 Haff, -VertexSet.Subset (interference_adj (snd_ext e) g) - (interference_adj (fst_ext e) (merge e g H0 Haff)). - -Proof. -unfold VertexSet.Subset. intros. -rewrite in_interf in H. rewrite in_interf. -destruct (redirect_charac (a, snd_ext e, None) (snd_ext e) (fst_ext e)); intros. -change_rewrite. destruct H1. destruct H2. elim H3. auto. -change_rewrite. destruct H1. destruct H1. -elim (In_graph_edge_diff_ext _ _ H). change_rewrite. auto. -destruct H1. rewrite H1. apply In_merge_interf_edge. assumption. -unfold interf_edge. auto. -Qed. - -Lemma merge_interf_adj_fst : forall e g H0 Haff, -VertexSet.Equal (interference_adj (fst_ext e) (merge e g H0 Haff)) - (VertexSet.union (interference_adj (fst_ext e) g) - (interference_adj (snd_ext e) g)). - -Proof. -intros. split; intros. -apply (merge_interf_adj_fst_1 _ _ H0 Haff _ H). -destruct (VertexSet.union_1 H). - apply (merge_interf_adj_fst_2 _ _ H0 Haff _ H1). - apply (merge_interf_adj_fst_3 _ _ H0 Haff _ H1). -Qed. - -(* The following lemmas define the equality of the interference adjacency - of any vertex which is not an endpoint of e after the merge of e *) - -Lemma merge_interf_adj_1 : forall x e g Hin Haff, -~Register.eq x (fst_ext e) -> -~Register.eq x (snd_ext e) -> -VertexSet.Subset (VertexSet.remove (snd_ext e) (interference_adj x g)) - (interference_adj x (merge e g Hin Haff)). - -Proof. -unfold VertexSet.Subset. intros. -rewrite in_interf. rewrite Dec.F.remove_iff in H1. destruct H1. -destruct (redirect_charac (a,x,None) (snd_ext e) (fst_ext e)); change_rewrite. -destruct H3. destruct H4. rewrite H3. -apply In_merge_interf_edge. rewrite <-in_interf. assumption. -unfold interf_edge. auto. -destruct H3. destruct H3. elim H2. auto. -destruct H3. elim H0. auto. -Qed. - -Lemma merge_interf_adj_2 : forall x e g Hin Haff, -~Register.eq x (fst_ext e) -> -~Register.eq x (snd_ext e) -> -VertexSet.Subset (interference_adj x (merge e g Hin Haff)) - (VertexSet.add (fst_ext e) (interference_adj x g)). - -Proof. -unfold VertexSet.Subset. intros. -destruct (Register.eq_dec a (fst_ext e)); [apply VertexSet.add_1|apply VertexSet.add_2]; intuition. -rewrite in_interf in H1. generalize (In_merge_edge_inv _ _ _ Hin Haff H1). intro. -destruct H2. destruct H2. destruct H3. -assert (eq (a,x,None) (redirect (snd_ext e) (fst_ext e) x0)). -apply weak_eq_interf_eq. assumption. unfold interf_edge. auto. -unfold interf_edge. rewrite redirect_weight_eq. -unfold same_type in H4. destruct H4; destruct H4. -unfold aff_edge in H5. destruct H5. simpl in H5. congruence. -auto. intuition. -rewrite in_interf. rewrite H5. -destruct (redirect_charac x0 (snd_ext e) (fst_ext e)). -destruct H6. destruct H7. rewrite <-H6. assumption. -destruct H6. destruct H6. rewrite <-H6 in H5. -destruct (eq_charac _ _ H5); destruct H8; change_rewrite. -elim n. auto. elim H. auto. -destruct H6. rewrite <-H6 in H5. -destruct (eq_charac _ _ H5); destruct H8; change_rewrite. -elim H. auto. elim n. auto. -Qed. - -Lemma merge_interf_adj_not_in : forall x e g Hin Haff, -~Register.eq x (fst_ext e) -> -~Register.eq x (snd_ext e) -> -~VertexSet.In x (interference_adj (snd_ext e) g) -> -VertexSet.Equal (interference_adj x (merge e g Hin Haff)) - (interference_adj x g). - -Proof. -intros. split; intros. -generalize (merge_interf_adj_2 x e g Hin Haff H H0 a H2). intro. -rewrite Dec.F.add_iff in H3. destruct H3. -rewrite <-H3 in H2. generalize (interf_adj_comm _ _ _ H2). intro. -rewrite merge_interf_adj_fst in H4. destruct (VertexSet.union_1 H4). -rewrite <-H3. apply interf_adj_comm. assumption. -elim H1. auto. -assumption. -apply merge_interf_adj_1; auto. -apply VertexSet.remove_2; auto. -intro. elim H1. apply interf_adj_comm. rewrite H3. assumption. -Qed. - -Lemma merge_interf_adj_in_snd : forall x e g Hin Haff, -~Register.eq x (fst_ext e) -> -~Register.eq x (snd_ext e) -> -VertexSet.In x (interference_adj (snd_ext e) g) -> -VertexSet.Equal (interference_adj x (merge e g Hin Haff)) - (VertexSet.add (fst_ext e) (VertexSet.remove (snd_ext e) - (interference_adj x g))). - -Proof. -intros. split; intros. -generalize (merge_interf_adj_2 _ _ _ Hin Haff H H0 _ H2). intro. -rewrite Dec.F.add_iff in H3. destruct H3. -apply VertexSet.add_1. assumption. -apply VertexSet.add_2. apply VertexSet.remove_2. -intro. rewrite <-H4 in H2. rewrite in_interf in H2. -generalize (proj1 (In_graph_edge_in_ext _ _ H2)). change_rewrite. intro. -rewrite In_merge_vertex in H5. destruct H5. elim H6. auto. assumption. - -rewrite Dec.F.add_iff in H2. destruct H2. -rewrite <-H2. apply interf_adj_comm. rewrite merge_interf_adj_fst. -apply VertexSet.union_3. auto. -apply merge_interf_adj_1; auto. -Qed. - -Lemma merge_interf_adj_in_both : forall x e g Hin Haff, -VertexSet.In x (interference_adj (snd_ext e) g) -> -VertexSet.In x (interference_adj (fst_ext e) g) -> -VertexSet.Equal (interference_adj x (merge e g Hin Haff)) - (VertexSet.remove (snd_ext e) (interference_adj x g)). - -Proof. -intros. -assert (~Register.eq x (fst_ext e)). -intro. rewrite H1 in H0. elim (not_in_interf_self _ _ H0). -assert (~Register.eq x (snd_ext e)). -intro. rewrite H2 in H. elim (not_in_interf_self _ _ H). -rewrite merge_interf_adj_in_snd; auto. -split; intros. -rewrite Dec.F.add_iff in H3. destruct H3. -apply VertexSet.remove_2. intro. -elim (In_graph_edge_diff_ext _ _ Hin). rewrite H3. auto. -rewrite <-H3. apply interf_adj_comm. assumption. -assumption. -apply VertexSet.add_2. auto. -Qed. - -Lemma preference_adj_merge : forall x e g p q, -~Register.eq x (fst_ext e) -> -~Register.eq x (snd_ext e) -> -VertexSet.Subset (preference_adj x (merge e g p q)) - (VertexSet.add (fst_ext e) - (VertexSet.remove (snd_ext e) (preference_adj x g))). - -Proof. -intros x e g p q H0 H1. generalize I. intro H. -unfold VertexSet.Subset; intros. -rewrite in_pref in H2. destruct H2. -generalize (In_merge_edge_inv e _ g p q H2). intro. -destruct H3. destruct H3. destruct H4 as [H4 HH4]. -unfold weak_eq in H4. change_rewrite. destruct H4. -unfold redirect in H4; change_rewrite. -destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite. -destruct H4. apply VertexSet.add_1. intuition. -destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. -destruct H4. elim H0. intuition. -destruct H4. apply VertexSet.add_2. apply VertexSet.remove_2. -intro. elim n. rewrite H6. intuition. -rewrite in_pref. unfold same_type in HH4. -destruct HH4. destruct H6. -destruct H6. exists x2. -assert (eq (a,x,Some x2) x1). -apply eq_ordered_eq. split; try split; simpl; auto. -unfold get_weight in H6. rewrite H6. apply OptionN_as_OT.eq_refl. -rewrite H8. assumption. -destruct H6. unfold interf_edge in H7. simpl in H7. congruence. -unfold redirect in H4; change_rewrite. -destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite. -destruct H4. elim H0. auto. -destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. -destruct H4. apply VertexSet.add_1. intuition. -destruct H4. apply VertexSet.add_2. apply VertexSet.remove_2. -intro. elim n0. rewrite H6. intuition. -rewrite in_pref. unfold same_type in HH4. -destruct HH4. destruct H6. -destruct H6. exists x2. -assert (eq (a,x,Some x2) x1). -rewrite edge_comm. apply eq_ordered_eq. split; try split; simpl; auto. -unfold get_weight in H6. rewrite H6. apply OptionN_as_OT.eq_refl. -rewrite H8. assumption. -destruct H6. unfold interf_edge in H7. simpl in H7. congruence. -Qed. - -Lemma preference_adj_merge_2 : forall x e g p q, -~Register.eq x (fst_ext e) -> -~Register.eq x (snd_ext e) -> -VertexSet.Subset (VertexSet.remove (fst_ext e) (VertexSet.remove (snd_ext e) (preference_adj x g))) - (preference_adj x (merge e g p q)). - -Proof. -unfold VertexSet.Subset; intros x e g p q H0 H1 a H2. generalize I. intro H. -assert (~Register.eq a (fst_ext e)). intro. -rewrite H3 in H2. elim (VertexSet.remove_1 (Register.eq_refl _) H2). -generalize (VertexSet.remove_3 H2). clear H2. intro H2. -assert (~Register.eq a (snd_ext e)). intro. -rewrite H4 in H2. elim (VertexSet.remove_1 (Register.eq_refl _) H2). -generalize (VertexSet.remove_3 H2). clear H2. intro. -rewrite in_pref in H2. destruct H2. -assert (exists w, In_graph_edge (a,x,Some w) (merge e g p q)). -cut (Prefere (fst_ext (redirect (snd_ext e) (fst_ext e) (a,x,Some x0))) - (snd_ext (redirect (snd_ext e) (fst_ext e) (a,x,Some x0))) - (merge e g p q)). intro. -unfold redirect in H5; change_rewrite. -destruct (OTFacts.eq_dec a (snd_ext e)); change_rewrite. -elim (H4 r). -destruct (OTFacts.eq_dec x (snd_ext e)); change_rewrite. -elim (H1 r). -unfold Prefere in H5. assumption. -apply In_merge_pref_edge. assumption. -intro. destruct (eq_charac _ _ H5); change_rewrite; destruct H6. -elim H1. auto. -elim H0. auto. -unfold aff_edge. exists x0. auto. -intro. unfold redirect in H5;change_rewrite. -destruct (OTFacts.eq_dec a (snd_ext e)); change_rewrite. -elim (H4 r). -destruct (OTFacts.eq_dec x (snd_ext e)); change_rewrite. -elim (H1 r). -unfold Interfere in H5. generalize (In_merge_edge_inv e _ g p q H5). intro H8. -generalize I. intro H7. -destruct H8. destruct H6. destruct H8. -unfold weak_eq in H8. change_rewrite. destruct H8. -unfold redirect in H8; change_rewrite. -destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite; destruct H8. -elim (H3 H8). -destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. -elim (H0 H10). -elim (interf_pref_conflict a x g). -split. -unfold Prefere. exists x0. assumption. -unfold Interfere. -assert (eq (a,x,None) x1). -apply weak_eq_interf_eq. unfold weak_eq. change_rewrite. -left. split; auto. unfold interf_edge. auto. -unfold same_type in H9. destruct H9. destruct H9. -unfold aff_edge in H11. destruct H11. simpl in H11. congruence. -destruct H9. assumption. -rewrite H11. assumption. - -unfold redirect in H8; change_rewrite. -destruct (OTFacts.eq_dec (fst_ext x1) (snd_ext e)); change_rewrite. -destruct H8. elim (H0 H10). -destruct (OTFacts.eq_dec (snd_ext x1) (snd_ext e)); change_rewrite. -destruct H8. elim (H3 H8). -elim (interf_pref_conflict a x g). -split. -unfold Prefere. exists x0. assumption. -unfold Interfere. destruct H8. -assert (eq (a,x,None) x1). -apply weak_eq_interf_eq. unfold weak_eq. change_rewrite. -right. split; auto. unfold interf_edge. auto. -unfold same_type in H9. destruct H9. destruct H9. -unfold aff_edge in H11. destruct H11. simpl in H11. congruence. -destruct H9. assumption. -rewrite H11. assumption. -rewrite in_pref. assumption. -Qed. |