diff options
Diffstat (limited to 'backend/Merge_Degree.v')
-rwxr-xr-x | backend/Merge_Degree.v | 205 |
1 files changed, 205 insertions, 0 deletions
diff --git a/backend/Merge_Degree.v b/backend/Merge_Degree.v new file mode 100755 index 00000000..15849794 --- /dev/null +++ b/backend/Merge_Degree.v @@ -0,0 +1,205 @@ +Require Import FSets. +Require Import InterfGraphMapImp. +Require Import Merge_Adjacency. +Require Import ZArith. +Require Import Edges. +Require Import MyRegisters. +Require Import Merge_Adjacency. +Require Import Interference_adjacency. +Require Import Remove_Vertex_Degree. + +Module Register := Regs. + +Import Edge Props RegFacts. + +(* If x interferes with both (fst_ext e) and (snd_ext e), then + its degree decreases of one when e is coalesced *) +Lemma merge_degree_dec_inter : forall x e g Hin Haff, +VertexSet.In x (interference_adj (fst_ext e) g) -> +VertexSet.In x (interference_adj (snd_ext e) g) -> +interf_degree g x = S (interf_degree (merge e g Hin Haff) x). + +Proof. +intros. unfold interf_degree. +rewrite (cardinal_m (merge_interf_adj_in_both _ _ _ Hin Haff H0 H)). +rewrite remove_cardinal_1. reflexivity. apply interf_adj_comm. auto. +Qed. + +(* If x does not interfere with both (fst_ext e) and (snd_ext e) + then its degree is unchanged when e is coalesced *) +Lemma merge_dec_eq : forall x e g Hin Haff, +~VertexSet.In x (interference_adj (fst_ext e) g) \/ +~VertexSet.In x (interference_adj (snd_ext e) g) -> +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +interf_degree g x = interf_degree (merge e g Hin Haff) x. + +Proof. +intros. unfold interf_degree. destruct H. +destruct (In_dec x (interference_adj (snd_ext e) g)). +rewrite (cardinal_m (merge_interf_adj_in_snd _ _ _ Hin Haff H0 H1 i)). +rewrite add_cardinal_2. rewrite remove_cardinal_1. reflexivity. +apply interf_adj_comm. auto. +intro. elim H. apply interf_adj_comm. apply (VertexSet.remove_3 H2). +rewrite (cardinal_m (merge_interf_adj_not_in _ _ _ Hin Haff H0 H1 n)). reflexivity. +rewrite (cardinal_m (merge_interf_adj_not_in _ _ _ Hin Haff H0 H1 H)). reflexivity. +Qed. + +(* The interference degree of any vertex which is not an endpoint + of e decreases when e is coalesced *) +Lemma merge_degree_dec : forall x e g Hin Haff, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +interf_degree (merge e g Hin Haff) x <= interf_degree g x. + +Proof. +intros. destruct (In_dec x (interference_adj (fst_ext e) g)). +destruct (In_dec x (interference_adj (snd_ext e) g)). +rewrite (merge_degree_dec_inter x e g Hin Haff i i0). auto. +rewrite (merge_dec_eq x e g Hin Haff (or_intror _ n)); auto. +rewrite (merge_dec_eq x e g Hin Haff (or_introl _ n)); auto. +Qed. + +(* If x does not interfere with the first endpoint of e then + x is of low-degree in (merge e g Hin Haff) iff it is in g *) +Lemma low_merge_low_fst : forall x e g K Hin Haff, +~VertexSet.In x (interference_adj (fst_ext e) g) -> +~Register.eq x (snd_ext e) -> +~Register.eq x (fst_ext e) -> +has_low_degree (merge e g Hin Haff) K x = has_low_degree g K x. + +Proof. +intros x e g palette Hin Haff H H0 H1. unfold has_low_degree. +rewrite (merge_dec_eq x e g Hin Haff); auto. +Qed. + +(* If x does not interfere with the second endpoint of e then + x is of low-degree in (merge e g Hin Haff) iff it is in g *) +Lemma low_merge_low_snd : forall x e g K Hin Haff, +~VertexSet.In x (interference_adj (snd_ext e) g) -> +~Register.eq x (snd_ext e) -> +~Register.eq x (fst_ext e) -> +has_low_degree (merge e g Hin Haff) K x = has_low_degree g K x. + +Proof. +intros x e g palette Hin Haff H H0 H1. unfold has_low_degree. +rewrite (merge_dec_eq x e g Hin Haff); auto. +Qed. + +(* A high-degree vertex of (merge e g Hin Haff) is of high-degree in g *) +Lemma merge_low_1 : forall g e x K Haff Hin, +has_low_degree (merge e g Hin Haff) K x = false -> +~Register.eq x (snd_ext e) -> +~Register.eq x (fst_ext e) -> +has_low_degree g K x = false. + +Proof. +intros g e x K Haff Hin Hpre H0 H1. unfold has_low_degree in *. +destruct (le_lt_dec K (interf_degree (merge e g Hin Haff) x)); +destruct (le_lt_dec K (interf_degree g x )); inversion Hpre. +reflexivity. +generalize (merge_degree_dec x e g Hin Haff H1 H0). intro. +apply False_ind. intuition. +Qed. + +(* A low-degree vertex of g is of low-degree in (merge e g Haff Hin) *) +Lemma low_dec : forall x e g Hin Haff K, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +has_low_degree g K x = true -> +has_low_degree (merge e g Hin Haff) K x = true. + +Proof. +intros. +case_eq (has_low_degree (merge e g Hin Haff) K x);[auto|intros]. +rewrite (merge_low_1 g e x K Haff Hin H2 H0 H) in H1. inversion H1. +Qed. + +(* A vertex high-degree vertex of g (which is not an endpoint of e) + which is of low-degree in (merge e g p q) belongs to the interference + neighborhood of the two endpoints of e in g *) +Lemma merge_dec_interf : forall x e k g p q, +has_low_degree g k x = false -> +has_low_degree (merge e g p q) k x = true -> +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +VertexSet.In x (interference_adj (fst_ext e) g) /\ +VertexSet.In x (interference_adj (snd_ext e) g). + +Proof. +intros. +destruct (In_dec x (interference_adj (fst_ext e) g)). +split. assumption. +destruct (In_dec x (interference_adj (snd_ext e) g)). +assumption. +rewrite (low_merge_low_snd _ _ _ _ p q n H2 H1) in H0. rewrite H0 in H. inversion H. +rewrite (low_merge_low_fst _ _ _ _ p q n H2 H1) in H0. rewrite H0 in H. inversion H. +Qed. + +(* A vertex high-degree vertex of g (which is not an endpoint of e) + which is of low-degree in (merge e g p q) is of degree k in g *) +Lemma merge_dec_K : forall x e k g p q, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +has_low_degree g k x = false -> +has_low_degree (merge e g p q) k x = true -> +interf_degree g x = k. + +Proof. +intros x e k g p q H0 H1 H2 H3. generalize I. intro H. unfold interf_degree. +assert (VertexSet.In x (interference_adj (fst_ext e) g) /\ + VertexSet.In x (interference_adj (snd_ext e) g)). +apply (merge_dec_interf x e k g p q); auto. +destruct H4. +generalize (merge_degree_dec_inter x e g p q H4 H5). intro. +unfold has_low_degree, interf_degree in *. +destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x (merge e g p q)))). +inversion H3. +destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x g))). +rewrite H6 in l0. rewrite (lt_le_S_eq _ _ l l0). assumption. +inversion H2. +Qed. + +(* Reciprocally, a vertex of degree k interfering with + the two endpoints of g is of low-degree in (merge e g p q) *) +Lemma merge_dec_low : forall x e k g p q, +interf_degree g x = k -> +VertexSet.In x (interference_adj (fst_ext e) g) -> +VertexSet.In x (interference_adj (snd_ext e) g) -> +has_low_degree (merge e g p q) k x = true. + +Proof. +unfold interf_degree. intros x e k g p q H0 H1 H2. generalize I. intro H. +assert (~Register.eq x (fst_ext e)). +intro. elim (not_in_interf_self (fst_ext e) g). rewrite H3 in H1. assumption. +assert (~Register.eq x (snd_ext e)). +intro. elim (not_in_interf_self (snd_ext e) g). rewrite H4 in H2. assumption. +generalize (merge_degree_dec_inter x e g p q H1 H2). intro. +unfold has_low_degree, interf_degree in *. +destruct (le_lt_dec k (VertexSet.cardinal (interference_adj x (merge e g p q)))). +rewrite H5 in H0. rewrite <-H0 in l. elim (le_S_irrefl _ l). +reflexivity. +Qed. + +(* Again, unused but meaningful theorem, summarizing evolution of degree + when an edge e is coalesced *) + +Theorem merge_degree_evolution : forall x e k g p q, +~Register.eq x (fst_ext e) -> +~Register.eq x (snd_ext e) -> +((has_low_degree g k x = false /\ has_low_degree (merge e g p q) k x = true) + <-> +(interf_degree g x = k /\ + VertexSet.In x (interference_adj (fst_ext e) g) /\ + VertexSet.In x (interference_adj (snd_ext e) g))). + +Proof. +split; intros. +destruct H1. +split. apply (merge_dec_K x e k g p q); auto. +apply (merge_dec_interf x e k g p q); auto. +destruct H1. destruct H2. +split. unfold has_low_degree. rewrite H1. +destruct (le_lt_dec k k). reflexivity. elim (lt_irrefl _ l). +apply merge_dec_low; auto. +Qed. |