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