From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- lib/UnionFind.v | 112 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 56 insertions(+), 56 deletions(-) (limited to 'lib/UnionFind.v') diff --git a/lib/UnionFind.v b/lib/UnionFind.v index 46a886ea..76dd6b31 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -90,7 +90,7 @@ Module Type UNIONFIND. Hypothesis sameclass_union_3: forall uf a b x y, sameclass (union uf a b) x y -> - sameclass uf x y + sameclass uf x y \/ sameclass uf x a /\ sameclass uf y b \/ sameclass uf x b /\ sameclass uf y a. @@ -120,7 +120,7 @@ Module Type UNIONFIND. pathlen (merge uf a b) x = if elt_eq (repr uf a) (repr uf b) then pathlen uf x - else if elt_eq (repr uf x) (repr uf a) then + else if elt_eq (repr uf x) (repr uf a) then pathlen uf x + pathlen uf b + 1 else pathlen uf x. @@ -155,7 +155,7 @@ Definition t := unionfind. Definition getlink (m: M.t elt) (a: elt) : {a' | M.get a m = Some a'} + {M.get a m = None}. Proof. - destruct (M.get a m). left. exists e; auto. right; auto. + destruct (M.get a m). left. exists e; auto. right; auto. Defined. (* The canonical representative of an element *) @@ -175,11 +175,11 @@ Definition repr (a: elt) : elt := Fix uf.(mwf) (fun _ => elt) F_repr a. Lemma repr_unroll: forall a, repr a = match M.get a uf.(m) with Some a' => repr a' | None => a end. Proof. - intros. unfold repr at 1. rewrite Fix_eq. - unfold F_repr. destruct (getlink uf.(m) a) as [[a' P] | Q]. + intros. unfold repr at 1. rewrite Fix_eq. + unfold F_repr. destruct (getlink uf.(m) a) as [[a' P] | Q]. rewrite P; auto. rewrite Q; auto. - intros. unfold F_repr. destruct (getlink (m uf) x) as [[a' P] | Q]; auto. + intros. unfold F_repr. destruct (getlink (m uf) x) as [[a' P] | Q]; auto. Qed. Lemma repr_none: @@ -187,36 +187,36 @@ Lemma repr_none: M.get a uf.(m) = None -> repr a = a. Proof. - intros. rewrite repr_unroll. rewrite H; auto. + intros. rewrite repr_unroll. rewrite H; auto. Qed. Lemma repr_some: - forall a a', + forall a a', M.get a uf.(m) = Some a' -> repr a = repr a'. Proof. - intros. rewrite repr_unroll. rewrite H; auto. + intros. rewrite repr_unroll. rewrite H; auto. Qed. Lemma repr_res_none: forall (a: elt), M.get (repr a) uf.(m) = None. Proof. - apply (well_founded_ind (mwf uf)). intros. + apply (well_founded_ind (mwf uf)). intros. rewrite repr_unroll. destruct (M.get x (m uf)) as [y|] eqn:X; auto. Qed. Lemma repr_canonical: forall (a: elt), repr (repr a) = repr a. Proof. - intros. apply repr_none. apply repr_res_none. + intros. apply repr_none. apply repr_res_none. Qed. Lemma repr_some_diff: forall a a', M.get a uf.(m) = Some a' -> a <> repr a'. Proof. - intros; red; intros. - assert (repr a = a). rewrite (repr_some a a'); auto. - assert (M.get a uf.(m) = None). rewrite <- H1. apply repr_res_none. + intros; red; intros. + assert (repr a = a). rewrite (repr_some a a'); auto. + assert (M.get a uf.(m) = None). rewrite <- H1. apply repr_res_none. congruence. Qed. @@ -297,9 +297,9 @@ Remark identify_Acc_b: Proof. induction 1; intros. constructor; intros. rewrite identify_order in H2. destruct H2 as [A | [A B]]. - apply H0; auto. rewrite <- (repr_some uf _ _ A). auto. + apply H0; auto. rewrite <- (repr_some uf _ _ A). auto. subst. elim H1. apply repr_none. auto. -Qed. +Qed. Remark identify_Acc: forall x, @@ -308,13 +308,13 @@ Proof. induction 1. constructor; intros. rewrite identify_order in H1. destruct H1 as [A | [A B]]. auto. - subst. apply identify_Acc_b; auto. apply uf.(mwf). + subst. apply identify_Acc_b; auto. apply uf.(mwf). Qed. Lemma identify_wf: well_founded (order (M.set a b uf.(m))). Proof. - red; intros. apply identify_Acc. apply uf.(mwf). + red; intros. apply identify_Acc. apply uf.(mwf). Qed. Definition identify := mk (M.set a b uf.(m)) identify_wf. @@ -323,11 +323,11 @@ Lemma repr_identify_1: forall x, repr uf x <> a -> repr identify x = repr uf x. Proof. intros x0; pattern x0. apply (well_founded_ind (mwf uf)); intros. - rewrite (repr_unroll uf) in *. + rewrite (repr_unroll uf) in *. destruct (M.get x (m uf)) as [a'|] eqn:X. rewrite <- H; auto. apply repr_some. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. congruence. - apply repr_none. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. + apply repr_none. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. Qed. Lemma repr_identify_2: @@ -335,9 +335,9 @@ Lemma repr_identify_2: Proof. intros x0; pattern x0. apply (well_founded_ind (mwf uf)); intros. rewrite (repr_unroll uf) in H0. destruct (M.get x (m uf)) as [a'|] eqn:X. - rewrite <- (H a'); auto. + rewrite <- (H a'); auto. apply repr_some. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. congruence. - subst x. rewrite (repr_unroll identify). simpl. rewrite M.gsspec. + subst x. rewrite (repr_unroll identify). simpl. rewrite M.gsspec. rewrite dec_eq_true. apply repr_identify_1. auto. Qed. @@ -348,7 +348,7 @@ End IDENTIFY. Remark union_not_same_class: forall uf a b, repr uf a <> repr uf b -> repr uf (repr uf b) <> repr uf a. Proof. - intros. rewrite repr_canonical. auto. + intros. rewrite repr_canonical. auto. Qed. Definition union (uf: t) (a b: elt) : t := @@ -402,7 +402,7 @@ Qed. Lemma sameclass_union_3: forall uf a b x y, sameclass (union uf a b) x y -> - sameclass uf x y + sameclass uf x y \/ sameclass uf x a /\ sameclass uf y b \/ sameclass uf x b /\ sameclass uf y a. Proof. @@ -448,14 +448,14 @@ Definition path_ord (uf: t) : elt -> elt -> Prop := order uf.(m). Lemma path_ord_wellfounded: forall uf, well_founded (path_ord uf). Proof. - intros. apply mwf. + intros. apply mwf. Qed. Lemma path_ord_canonical: forall uf x y, repr uf x = x -> ~path_ord uf y x. Proof. intros; red; intros. hnf in H0. - assert (M.get x (m uf) = None). rewrite <- H. apply repr_res_none. + assert (M.get x (m uf) = None). rewrite <- H. apply repr_res_none. congruence. Qed. @@ -463,10 +463,10 @@ Lemma path_ord_merge_1: forall uf a b x y, path_ord uf x y -> path_ord (merge uf a b) x y. Proof. - intros. unfold merge. + intros. unfold merge. destruct (M.elt_eq (repr uf a) (repr uf b)). auto. - red. simpl. red. rewrite M.gsspec. rewrite dec_eq_false. apply H. + red. simpl. red. rewrite M.gsspec. rewrite dec_eq_false. apply H. red; intros. hnf in H. generalize (repr_res_none uf a). congruence. Qed. @@ -497,11 +497,11 @@ Definition pathlen (a: elt) : nat := Fix uf.(mwf) (fun _ => nat) F_pathlen a. Lemma pathlen_unroll: forall a, pathlen a = match M.get a uf.(m) with Some a' => S(pathlen a') | None => O end. Proof. - intros. unfold pathlen at 1. rewrite Fix_eq. - unfold F_pathlen. destruct (getlink uf.(m) a) as [[a' P] | Q]. + intros. unfold pathlen at 1. rewrite Fix_eq. + unfold F_pathlen. destruct (getlink uf.(m) a) as [[a' P] | Q]. rewrite P; auto. rewrite Q; auto. - intros. unfold F_pathlen. destruct (getlink (m uf) x) as [[a' P] | Q]; auto. + intros. unfold F_pathlen. destruct (getlink (m uf) x) as [[a' P] | Q]; auto. Qed. Lemma pathlen_none: @@ -509,11 +509,11 @@ Lemma pathlen_none: M.get a uf.(m) = None -> pathlen a = 0. Proof. - intros. rewrite pathlen_unroll. rewrite H; auto. + intros. rewrite pathlen_unroll. rewrite H; auto. Qed. Lemma pathlen_some: - forall a a', + forall a a', M.get a uf.(m) = Some a' -> pathlen a = S (pathlen a'). Proof. @@ -524,8 +524,8 @@ Lemma pathlen_zero: forall a, repr uf a = a <-> pathlen a = O. Proof. intros; split; intros. - apply pathlen_none. rewrite <- H. apply repr_res_none. - apply repr_none. rewrite pathlen_unroll in H. + apply pathlen_none. rewrite <- H. apply repr_res_none. + apply repr_none. rewrite pathlen_unroll in H. destruct (M.get a (m uf)); congruence. Qed. @@ -538,27 +538,27 @@ Lemma pathlen_merge: pathlen (merge uf a b) x = if M.elt_eq (repr uf a) (repr uf b) then pathlen uf x - else if M.elt_eq (repr uf x) (repr uf a) then + else if M.elt_eq (repr uf x) (repr uf a) then pathlen uf x + pathlen uf b + 1 else pathlen uf x. Proof. - intros. unfold merge. + intros. unfold merge. destruct (M.elt_eq (repr uf a) (repr uf b)). auto. set (uf' := identify uf (repr uf a) b (repr_res_none uf a) (not_eq_sym n)). pattern x. apply (well_founded_ind (mwf uf')); intros. rewrite (pathlen_unroll uf'). destruct (M.get x0 (m uf')) as [x'|] eqn:G. - rewrite H; auto. simpl in G. rewrite M.gsspec in G. + rewrite H; auto. simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)). rewrite e. rewrite repr_canonical. rewrite dec_eq_true. - inversion G. subst x'. rewrite dec_eq_false; auto. - replace (pathlen uf (repr uf a)) with 0. omega. - symmetry. apply pathlen_none. apply repr_res_none. + inversion G. subst x'. rewrite dec_eq_false; auto. + replace (pathlen uf (repr uf a)) with 0. omega. + symmetry. apply pathlen_none. apply repr_res_none. rewrite (repr_unroll uf x0), (pathlen_unroll uf x0); rewrite G. - destruct (M.elt_eq (repr uf x') (repr uf a)); omega. + destruct (M.elt_eq (repr uf x') (repr uf a)); omega. simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)); try discriminate. - rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto. - symmetry. apply pathlen_zero; auto. apply repr_none; auto. + rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto. + symmetry. apply pathlen_zero; auto. apply repr_none; auto. Qed. Lemma pathlen_gt_merge: @@ -567,7 +567,7 @@ Lemma pathlen_gt_merge: pathlen uf x > pathlen uf y -> pathlen (merge uf a b) x > pathlen (merge uf a b) y. Proof. - intros. repeat rewrite pathlen_merge. + intros. repeat rewrite pathlen_merge. destruct (M.elt_eq (repr uf a) (repr uf b)). auto. rewrite H. destruct (M.elt_eq (repr uf y) (repr uf a)). omega. auto. @@ -600,7 +600,7 @@ Proof. induction 1. constructor; intros. destruct (compress_order _ _ H1) as [A | [A B]]. auto. - subst x y. constructor; intros. + subst x y. constructor; intros. destruct (compress_order _ _ H2) as [A | [A B]]. red in A. generalize (repr_res_none uf a). congruence. congruence. @@ -609,7 +609,7 @@ Qed. Lemma compress_wf: well_founded (order (M.set a b uf.(m))). Proof. - red; intros. apply compress_Acc. apply uf.(mwf). + red; intros. apply compress_Acc. apply uf.(mwf). Qed. Definition compress := mk (M.set a b uf.(m)) compress_wf. @@ -620,11 +620,11 @@ Proof. apply (well_founded_ind (mwf compress)); intros. rewrite (repr_unroll compress). destruct (M.get x (m compress)) as [y|] eqn:G. - rewrite H; auto. - simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a). + rewrite H; auto. + simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a). inversion G. subst x y. rewrite <- a_repr_b. apply repr_canonical. symmetry; apply repr_some; auto. - simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a). + simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a). congruence. symmetry; apply repr_none; auto. Qed. @@ -637,7 +637,7 @@ Section FIND. Variable uf: t. -Program Fixpoint find_x (a: elt) {wf (order uf.(m)) a} : +Program Fixpoint find_x (a: elt) {wf (order uf.(m)) a} : { r: elt * t | fst r = repr uf a /\ forall x, repr (snd r) x = repr uf x } := match M.get a uf.(m) with | Some a' => @@ -664,7 +664,7 @@ Next Obligation. destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. symmetry. apply repr_some. auto. - intros. rewrite repr_compress. + intros. rewrite repr_compress. destruct (find_x a') as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. auto. Qed. @@ -672,7 +672,7 @@ Next Obligation. split; auto. symmetry. apply repr_none. auto. Qed. Next Obligation. - apply mwf. + apply mwf. Defined. Definition find (a: elt) : elt * t := proj1_sig (find_x a). @@ -680,15 +680,15 @@ Definition find (a: elt) : elt * t := proj1_sig (find_x a). Lemma find_repr: forall a, fst (find a) = repr uf a. Proof. - unfold find; intros. destruct (find_x a) as [[b uf'] [A B]]. simpl. auto. + unfold find; intros. destruct (find_x a) as [[b uf'] [A B]]. simpl. auto. Qed. Lemma find_unchanged: forall a x, repr (snd (find a)) x = repr uf x. Proof. - unfold find; intros. destruct (find_x a) as [[b uf'] [A B]]. simpl. auto. + unfold find; intros. destruct (find_x a) as [[b uf'] [A B]]. simpl. auto. Qed. - + Lemma sameclass_find_1: forall a x y, sameclass (snd (find a)) x y <-> sameclass uf x y. Proof. -- cgit