From f8d59bccd57fd53b55de5e9dd96fbc1af150951a Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Aug 2009 12:43:08 +0000 Subject: Unionfind data structure, used in new implementation of backend/Tunneling git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1122 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/UnionFind.v | 702 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 702 insertions(+) create mode 100644 lib/UnionFind.v (limited to 'lib/UnionFind.v') diff --git a/lib/UnionFind.v b/lib/UnionFind.v new file mode 100644 index 00000000..d74a20a7 --- /dev/null +++ b/lib/UnionFind.v @@ -0,0 +1,702 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** A persistent union-find data structure. *) + +Require Import Wf. +Require Recdef. +Require Setoid. +Require Coq.Program.Wf. +Require Import Coqlib. + +Open Scope nat_scope. +Set Implicit Arguments. + +Module Type MAP. + Variable elt: Type. + Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}. + Variable t: Type -> Type. + Variable empty: forall (A: Type), t A. + Variable get: forall (A: Type), elt -> t A -> option A. + Variable set: forall (A: Type), elt -> A -> t A -> t A. + Hypothesis gempty: forall (A: Type) (x: elt), get x (empty A) = None. + Hypothesis gsspec: forall (A: Type) (x y: elt) (v: A) (m: t A), + get x (set y v m) = if elt_eq x y then Some v else get x m. +End MAP. + +Unset Implicit Arguments. + +Module Type UNIONFIND. + Variable elt: Type. + Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}. + Variable t: Type. + + Variable repr: t -> elt -> elt. + Hypothesis repr_canonical: forall uf a, repr uf (repr uf a) = repr uf a. + + Definition sameclass (uf: t) (a b: elt) : Prop := repr uf a = repr uf b. + Hypothesis sameclass_refl: + forall uf a, sameclass uf a a. + Hypothesis sameclass_sym: + forall uf a b, sameclass uf a b -> sameclass uf b a. + Hypothesis sameclass_trans: + forall uf a b c, + sameclass uf a b -> sameclass uf b c -> sameclass uf a c. + Hypothesis sameclass_repr: + forall uf a, sameclass uf a (repr uf a). + + Variable empty: t. + Hypothesis repr_empty: + forall a, repr empty a = a. + Hypothesis sameclass_empty: + forall a b, sameclass empty a b -> a = b. + + Variable find: t -> elt -> elt * t. + Hypothesis find_repr: + forall uf a, fst (find uf a) = repr uf a. + Hypothesis find_unchanged: + forall uf a x, repr (snd (find uf a)) x = repr uf x. + Hypothesis sameclass_find_1: + forall uf a x y, sameclass (snd (find uf a)) x y <-> sameclass uf x y. + Hypothesis sameclass_find_2: + forall uf a, sameclass uf a (fst (find uf a)). + Hypothesis sameclass_find_3: + forall uf a, sameclass (snd (find uf a)) a (fst (find uf a)). + + Variable union: t -> elt -> elt -> t. + Hypothesis repr_union_1: + forall uf a b x, repr uf x <> repr uf a -> repr (union uf a b) x = repr uf x. + Hypothesis repr_union_2: + forall uf a b x, repr uf x = repr uf a -> repr (union uf a b) x = repr uf b. + Hypothesis repr_union_3: + forall uf a b, repr (union uf a b) b = repr uf b. + Hypothesis sameclass_union_1: + forall uf a b, sameclass (union uf a b) a b. + Hypothesis sameclass_union_2: + forall uf a b x y, sameclass uf x y -> sameclass (union uf a b) x y. + Hypothesis sameclass_union_3: + forall uf a b x y, + sameclass (union uf a b) x y -> + sameclass uf x y + \/ sameclass uf x a /\ sameclass uf y b + \/ sameclass uf x b /\ sameclass uf y a. + + Variable merge: t -> elt -> elt -> t. + Hypothesis repr_merge: + forall uf a b x, repr (merge uf a b) x = repr (union uf a b) x. + Hypothesis sameclass_merge: + forall uf a b x y, sameclass (merge uf a b) x y <-> sameclass (union uf a b) x y. + + Variable path_ord: t -> elt -> elt -> Prop. + Hypothesis path_ord_wellfounded: + forall uf, well_founded (path_ord uf). + Hypothesis path_ord_canonical: + forall uf x y, repr uf x = x -> ~path_ord uf y x. + Hypothesis path_ord_merge_1: + forall uf a b x y, + path_ord uf x y -> path_ord (merge uf a b) x y. + Hypothesis path_ord_merge_2: + forall uf a b, + repr uf a <> repr uf b -> path_ord (merge uf a b) b (repr uf a). + + Variable pathlen: t -> elt -> nat. + Hypothesis pathlen_zero: + forall uf a, repr uf a = a <-> pathlen uf a = O. + Hypothesis pathlen_merge: + forall uf a b x, + 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 + pathlen uf x + pathlen uf b + 1 + else + pathlen uf x. + Hypothesis pathlen_gt_merge: + forall uf a b x y, + repr uf x = repr uf y -> + pathlen uf x > pathlen uf y -> + pathlen (merge uf a b) x > pathlen (merge uf a b) y. + +End UNIONFIND. + +Module UF (M: MAP) : UNIONFIND with Definition elt := M.elt. + +Definition elt := M.elt. +Definition elt_eq := M.elt_eq. + +(* A set of equivalence classes over elt is represented by a map m. + M.get a m = Some a' means that a is in the same class as a'. + M.get a m = None means that a is the canonical representative + for its equivalence class. *) + +(* The ordering over elt induced by such a map. + repr_order m a a' iff M.get a' m = Some a. + This ordering must be well founded. *) + +Definition order (m: M.t elt) (a a': elt) : Prop := + M.get a' m = Some a. + +Record unionfind : Type := mk { m: M.t elt; mwf: well_founded (order m) }. + +Definition t := unionfind. + +(* The canonical representative of an element *) + +Section REPR. + +Variable uf: t. + +Function repr (a: elt) {wf (order uf.(m)) a} : elt := + match M.get a uf.(m) with + | Some a' => repr a' + | None => a + end. +Proof. + intros. auto. + apply mwf. +Qed. + +Lemma repr_none: + forall a, + M.get a uf.(m) = None -> + repr a = a. +Proof. + intros. + functional induction (repr a). congruence. auto. +Qed. + +Lemma repr_some: + forall a a', + M.get a uf.(m) = Some a' -> + repr a = repr a'. +Proof. + intros. + functional induction (repr a). congruence. congruence. +Qed. + +Lemma repr_res_none: + forall (a: elt), M.get (repr a) uf.(m) = None. +Proof. + intros. functional induction (repr a). auto. auto. +Qed. + +Lemma repr_canonical: + forall (a: elt), repr (repr a) = repr a. +Proof. + 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. + congruence. +Qed. + +End REPR. + +Definition sameclass (uf: t) (a b: elt) : Prop := + repr uf a = repr uf b. + +Lemma sameclass_refl: + forall uf a, sameclass uf a a. +Proof. + intros. red. auto. +Qed. + +Lemma sameclass_sym: + forall uf a b, sameclass uf a b -> sameclass uf b a. +Proof. + intros. red. symmetry. exact H. +Qed. + +Lemma sameclass_trans: + forall uf a b c, + sameclass uf a b -> sameclass uf b c -> sameclass uf a c. +Proof. + intros. red. transitivity (repr uf b). exact H. exact H0. +Qed. + +Lemma sameclass_repr: + forall uf a, sameclass uf a (repr uf a). +Proof. + intros. red. symmetry. rewrite repr_canonical. auto. +Qed. + +(* The empty unionfind structure (each element in its own class) *) + +Lemma wf_empty: + well_founded (order (M.empty elt)). +Proof. + red. intros. apply Acc_intro. intros b RO. red in RO. + rewrite M.gempty in RO. discriminate. +Qed. + +Definition empty : t := mk (M.empty elt) wf_empty. + +Lemma repr_empty: + forall a, repr empty a = a. +Proof. + intros. apply repr_none. simpl. apply M.gempty. +Qed. + +Lemma sameclass_empty: + forall a b, sameclass empty a b -> a = b. +Proof. + intros. red in H. repeat rewrite repr_empty in H. auto. +Qed. + +(* Merging two equivalence classes *) + +Section IDENTIFY. + +Variable uf: t. +Variables a b: elt. +Hypothesis a_canon: M.get a uf.(m) = None. +Hypothesis not_same_class: repr uf b <> a. + +Lemma identify_order: + forall x y, + order (M.set a b uf.(m)) y x <-> + order uf.(m) y x \/ (x = a /\ y = b). +Proof. + intros until y. unfold order. rewrite M.gsspec. + destruct (M.elt_eq x a). intuition congruence. intuition congruence. +Qed. + +Remark identify_Acc_b: + forall x, + Acc (order uf.(m)) x -> repr uf x <> a -> Acc (order (M.set a b uf.(m))) x. +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. + subst. elim H1. apply repr_none. auto. +Qed. + +Remark identify_Acc: + forall x, + Acc (order uf.(m)) x -> Acc (order (M.set a b uf.(m))) x. +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). +Qed. + +Lemma identify_wf: + well_founded (order (M.set a b uf.(m))). +Proof. + red; intros. apply identify_Acc. apply uf.(mwf). +Qed. + +Definition identify := mk (M.set a b uf.(m)) identify_wf. + +Lemma repr_identify_1: + forall x, repr uf x <> a -> repr identify x = repr uf x. +Proof. + intros. functional induction (repr uf x). + + rewrite <- IHe; auto. apply repr_some. simpl. rewrite M.gsspec. + destruct (M.elt_eq a0 a). congruence. auto. + + apply repr_none. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. +Qed. + +Lemma repr_identify_2: + forall x, repr uf x = a -> repr identify x = repr uf b. +Proof. + intros. functional induction (repr uf x). + + rewrite <- IHe; auto. apply repr_some. simpl. rewrite M.gsspec. + rewrite dec_eq_false; auto. congruence. + + transitivity (repr identify b). apply repr_some. simpl. + rewrite M.gsspec. apply dec_eq_true. + apply repr_identify_1. auto. +Qed. + +End IDENTIFY. + +(* Union *) + +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. +Qed. + +Definition union (uf: t) (a b: elt) : t := + let a' := repr uf a in + let b' := repr uf b in + match M.elt_eq a' b' with + | left EQ => uf + | right NEQ => identify uf a' b' (repr_res_none uf a) (union_not_same_class uf a b NEQ) + end. + +Lemma repr_union_1: + forall uf a b x, repr uf x <> repr uf a -> repr (union uf a b) x = repr uf x. +Proof. + intros. unfold union. destruct (M.elt_eq (repr uf a) (repr uf b)). + auto. + apply repr_identify_1. auto. +Qed. + +Lemma repr_union_2: + forall uf a b x, repr uf x = repr uf a -> repr (union uf a b) x = repr uf b. +Proof. + intros. unfold union. destruct (M.elt_eq (repr uf a) (repr uf b)). + congruence. + rewrite <- (repr_canonical uf b). apply repr_identify_2. auto. +Qed. + +Lemma repr_union_3: + forall uf a b, repr (union uf a b) b = repr uf b. +Proof. + intros. unfold union. destruct (M.elt_eq (repr uf a) (repr uf b)). + auto. apply repr_identify_1. auto. +Qed. + +Lemma sameclass_union_1: + forall uf a b, sameclass (union uf a b) a b. +Proof. + intros; red. rewrite repr_union_2; auto. rewrite repr_union_3. auto. +Qed. + +Lemma sameclass_union_2: + forall uf a b x y, sameclass uf x y -> sameclass (union uf a b) x y. +Proof. + unfold sameclass; intros. + destruct (M.elt_eq (repr uf x) (repr uf a)); + destruct (M.elt_eq (repr uf y) (repr uf a)). + repeat rewrite repr_union_2; auto. + congruence. congruence. + repeat rewrite repr_union_1; auto. +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 a /\ sameclass uf y b + \/ sameclass uf x b /\ sameclass uf y a. +Proof. + intros until y. unfold sameclass. + destruct (M.elt_eq (repr uf x) (repr uf a)); + destruct (M.elt_eq (repr uf y) (repr uf a)). + intro. left. congruence. + rewrite repr_union_2; auto. rewrite repr_union_1; auto. + rewrite repr_union_1; auto. rewrite repr_union_2; auto. + repeat rewrite repr_union_1; auto. +Qed. + +(* Merge *) + +Definition merge (uf: t) (a b: elt) : t := + let a' := repr uf a in + let b' := repr uf b in + match M.elt_eq a' b' with + | left EQ => uf + | right NEQ => identify uf a' b (repr_res_none uf a) (sym_not_equal NEQ) + end. + +Lemma repr_merge: + forall uf a b x, repr (merge uf a b) x = repr (union uf a b) x. +Proof. + intros. unfold merge, union. destruct (M.elt_eq (repr uf a) (repr uf b)). + auto. + destruct (M.elt_eq (repr uf x) (repr uf a)). + repeat rewrite repr_identify_2; auto. rewrite repr_canonical; auto. + repeat rewrite repr_identify_1; auto. +Qed. + +Lemma sameclass_merge: + forall uf a b x y, sameclass (merge uf a b) x y <-> sameclass (union uf a b) x y. +Proof. + unfold sameclass; intros. repeat rewrite repr_merge. tauto. +Qed. + +(* Path order and merge *) + +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. +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. + congruence. +Qed. + +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. + destruct (M.elt_eq (repr uf a) (repr uf b)). + auto. + 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. + +Lemma path_ord_merge_2: + forall uf a b, + repr uf a <> repr uf b -> path_ord (merge uf a b) b (repr uf a). +Proof. + intros. unfold merge. + destruct (M.elt_eq (repr uf a) (repr uf b)). + congruence. + red. simpl. red. rewrite M.gsspec. rewrite dec_eq_true; auto. +Qed. + +(* Path length and merge *) + +Section PATHLEN. + +Variable uf: t. + +Function pathlen (a: elt) {wf (order uf.(m)) a} : nat := + match M.get a uf.(m) with + | Some a' => S (pathlen a') + | None => O + end. +Proof. + intros. auto. + apply mwf. +Qed. + +Lemma pathlen_none: + forall a, + M.get a uf.(m) = None -> + pathlen a = 0. +Proof. + intros. + functional induction (pathlen a). congruence. auto. +Qed. + +Lemma pathlen_some: + forall a a', + M.get a uf.(m) = Some a' -> + pathlen a = S (pathlen a'). +Proof. + intros. + functional induction (pathlen a). congruence. congruence. +Qed. + +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. + functional induction (pathlen a). + congruence. + apply repr_none. auto. +Qed. + +End PATHLEN. + +(* Path length and merge *) + +Lemma pathlen_merge: + forall uf a b x, + 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 + pathlen uf x + pathlen uf b + 1 + else + pathlen uf x. +Proof. + intros. unfold merge. + destruct (M.elt_eq (repr uf a) (repr uf b)). + auto. + functional induction (pathlen (identify uf (repr uf a) b (repr_res_none uf a) (sym_not_equal n)) x). + simpl in e. rewrite M.gsspec in e. + destruct (M.elt_eq a0 (repr uf a)). + inversion e; subst a'; clear e. + replace (repr uf a0) with (repr uf a). rewrite dec_eq_true. + rewrite IHn0. rewrite dec_eq_false; auto. + rewrite (pathlen_none uf a0). omega. subst a0. apply repr_res_none. + subst a0. rewrite repr_canonical; auto. + rewrite (pathlen_some uf a0 a'); auto. + rewrite IHn0. + replace (repr uf a0) with (repr uf a'). + destruct (M.elt_eq (repr uf a') (repr uf a)); omega. + symmetry. apply repr_some; auto. + + simpl in e. rewrite M.gsspec in e. destruct (M.elt_eq a0 (repr uf a)). + congruence. rewrite (repr_none uf a0); auto. + rewrite dec_eq_false; auto. symmetry. apply pathlen_none; auto. +Qed. + +Lemma pathlen_gt_merge: + forall uf a b x y, + repr uf x = repr uf y -> + pathlen uf x > pathlen uf y -> + pathlen (merge uf a b) x > pathlen (merge uf a b) y. +Proof. + 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. +Qed. + +(* Path compression *) + +Section COMPRESS. + +Variable uf: t. +Variable a b: elt. +Hypothesis a_diff_b: a <> b. +Hypothesis a_repr_b: repr uf a = b. + +Lemma compress_order: + forall x y, + order (M.set a b uf.(m)) y x -> + order uf.(m) y x \/ (x = a /\ y = b). +Proof. + intros until y. unfold order. rewrite M.gsspec. + destruct (M.elt_eq x a). + intuition congruence. + auto. +Qed. + +Remark compress_Acc: + forall x, + Acc (order uf.(m)) x -> Acc (order (M.set a b uf.(m))) x. +Proof. + induction 1. constructor; intros. + destruct (compress_order _ _ H1) as [A | [A B]]. + auto. + subst x y. constructor; intros. + destruct (compress_order _ _ H2) as [A | [A B]]. + red in A. generalize (repr_res_none uf a). congruence. + congruence. +Qed. + +Lemma compress_wf: + well_founded (order (M.set a b uf.(m))). +Proof. + red; intros. apply compress_Acc. apply uf.(mwf). +Qed. + +Definition compress := mk (M.set a b uf.(m)) compress_wf. + +Lemma repr_compress: + forall x, repr compress x = repr uf x. +Proof. + intros. functional induction (repr compress x). + simpl in e. rewrite M.gsspec in e. destruct (M.elt_eq a0 a). + subst a0. injection e; intros. subst a'. rewrite IHe. rewrite <- a_repr_b. + apply repr_canonical. + rewrite IHe. symmetry. apply repr_some; auto. + simpl in e. rewrite M.gsspec in e. destruct (M.elt_eq a0 a). + congruence. symmetry. apply repr_none. auto. +Qed. + +End COMPRESS. + +(* Find with path compression *) + +Section FIND. + +Variable uf: t. + +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' => + match find_x a' with + | pair b uf' => (b, compress uf' a b _ _) + end + | None => (a, uf) + end. +Next Obligation. + red. auto. +Qed. +Next Obligation. + destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a' + (find_x_obligation_1 a find_x a' Heq_anonymous))) + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + apply repr_some_diff. auto. +Qed. +Next Obligation. + destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a' + (find_x_obligation_1 a find_x a' Heq_anonymous))) + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + rewrite B. apply repr_some. auto. +Qed. +Next Obligation. + split. + destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a' + (find_x_obligation_1 a find_x a' Heq_anonymous))) + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. + symmetry. apply repr_some. auto. + intros. rewrite repr_compress. + destruct (find_x (exist (fun a' : elt => order (m uf) a' a) a' + (find_x_obligation_1 a find_x a' Heq_anonymous))) + as [[b' uf''] [A B]]. simpl in *. inv Heq_anonymous0. auto. +Qed. +Next Obligation. + split; auto. symmetry. apply repr_none. auto. +Qed. +Next Obligation. + apply mwf. +Defined. + +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. +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. +Qed. + +Lemma sameclass_find_1: + forall a x y, sameclass (snd (find a)) x y <-> sameclass uf x y. +Proof. + unfold sameclass; intros. repeat rewrite find_unchanged. tauto. +Qed. + +Lemma sameclass_find_2: + forall a, sameclass uf a (fst (find a)). +Proof. + intros. rewrite find_repr. apply sameclass_repr. +Qed. + +Lemma sameclass_find_3: + forall a, sameclass (snd (find a)) a (fst (find a)). +Proof. + intros. rewrite sameclass_find_1. apply sameclass_find_2. +Qed. + +End FIND. + +End UF. + -- cgit