diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Lattice.v | 199 | ||||
-rw-r--r-- | lib/Maps.v | 82 | ||||
-rw-r--r-- | lib/Sets.v | 189 | ||||
-rw-r--r-- | lib/union_find.v | 484 |
4 files changed, 248 insertions, 706 deletions
diff --git a/lib/Lattice.v b/lib/Lattice.v index 7adcffba..7ef1b9e1 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -2,6 +2,7 @@ Require Import Coqlib. Require Import Maps. +Require Import FSets. (** * Signatures of semi-lattices *) @@ -13,14 +14,20 @@ Require Import Maps. Module Type SEMILATTICE. Variable t: Set. - Variable eq: forall (x y: t), {x=y} + {x<>y}. + Variable eq: t -> t -> Prop. + Hypothesis eq_refl: forall x, eq x x. + Hypothesis eq_sym: forall x y, eq x y -> eq y x. + Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Variable beq: t -> t -> bool. + Hypothesis beq_correct: forall x y, beq x y = true -> eq x y. Variable ge: t -> t -> Prop. - Hypothesis ge_refl: forall x, ge x x. + Hypothesis ge_refl: forall x y, eq x y -> ge x y. Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. Variable bot: t. Hypothesis ge_bot: forall x, ge x bot. Variable lub: t -> t -> t. - Hypothesis lub_commut: forall x y, lub x y = lub y x. + Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x). Hypothesis ge_lub_left: forall x y, ge (lub x y) x. End SEMILATTICE. @@ -31,16 +38,22 @@ End SEMILATTICE. Module Type SEMILATTICE_WITH_TOP. Variable t: Set. - Variable eq: forall (x y: t), {x=y} + {x<>y}. + Variable eq: t -> t -> Prop. + Hypothesis eq_refl: forall x, eq x x. + Hypothesis eq_sym: forall x y, eq x y -> eq y x. + Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Variable beq: t -> t -> bool. + Hypothesis beq_correct: forall x y, beq x y = true -> eq x y. Variable ge: t -> t -> Prop. - Hypothesis ge_refl: forall x, ge x x. + Hypothesis ge_refl: forall x y, eq x y -> ge x y. Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. Variable bot: t. Hypothesis ge_bot: forall x, ge x bot. Variable top: t. Hypothesis ge_top: forall x, ge top x. Variable lub: t -> t -> t. - Hypothesis lub_commut: forall x y, lub x y = lub y x. + Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x). Hypothesis ge_lub_left: forall x y, ge (lub x y) x. End SEMILATTICE_WITH_TOP. @@ -59,13 +72,6 @@ Inductive t_ : Set := Definition t: Set := t_. -Lemma eq: forall (x y: t), {x=y} + {x<>y}. -Proof. - assert (forall m1 m2: PTree.t L.t, {m1=m2} + {m1<>m2}). - apply PTree.eq. exact L.eq. - decide equality. -Qed. - Definition get (p: positive) (x: t) : L.t := match x with | Bot_except m => @@ -96,12 +102,48 @@ Proof. intros. destruct x; simpl; rewrite PTree.gso; auto. Qed. +Definition eq (x y: t) : Prop := + forall p, L.eq (get p x) (get p y). + +Lemma eq_refl: forall x, eq x x. +Proof. + unfold eq; intros. apply L.eq_refl. +Qed. + +Lemma eq_sym: forall x y, eq x y -> eq y x. +Proof. + unfold eq; intros. apply L.eq_sym; auto. +Qed. + +Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. +Proof. + unfold eq; intros. eapply L.eq_trans; eauto. +Qed. + +Definition beq (x y: t) : bool := + match x, y with + | Bot_except m, Bot_except n => PTree.beq L.beq m n + | Top_except m, Top_except n => PTree.beq L.beq m n + | _, _ => false + end. + +Lemma beq_correct: forall x y, beq x y = true -> eq x y. +Proof. + destruct x; destruct y; simpl; intro; try congruence. + red; intro; simpl. + generalize (PTree.beq_correct L.eq L.beq L.beq_correct t0 t1 H p). + destruct (t0!p); destruct (t1!p); intuition. apply L.eq_refl. + red; intro; simpl. + generalize (PTree.beq_correct L.eq L.beq L.beq_correct t0 t1 H p). + destruct (t0!p); destruct (t1!p); intuition. apply L.eq_refl. +Qed. + Definition ge (x y: t) : Prop := forall p, L.ge (get p x) (get p y). -Lemma ge_refl: forall x, ge x x. +Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. - unfold ge; intros. apply L.ge_refl. + unfold ge, eq; intros. apply L.ge_refl. auto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. @@ -109,6 +151,11 @@ Proof. unfold ge; intros. apply L.ge_trans with (get p y); auto. Qed. +Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. +Proof. + unfold eq,ge; intros. eapply L.ge_compat; eauto. +Qed. + Definition bot := Bot_except (PTree.empty L.t). Lemma get_bot: forall p, get p bot = L.bot. @@ -177,11 +224,13 @@ Definition lub (x y: t) : t := end. Lemma lub_commut: - forall x y, lub x y = lub y x. + forall x y, eq (lub x y) (lub y x). Proof. - destruct x; destruct y; unfold lub; decEq; - apply PTree.combine_commut; intros; - (destruct i; destruct j; auto; decEq; apply L.lub_commut). + intros x y p. + destruct x; destruct y; simpl; + repeat rewrite PTree.gcombine; auto; + destruct t0!p; destruct t1!p; + try apply L.eq_refl; try apply L.lub_commut. Qed. Lemma ge_lub_left: @@ -191,7 +240,8 @@ Proof. rewrite PTree.gcombine. destruct t0!p. destruct t1!p. apply L.ge_lub_left. - apply L.ge_refl. destruct t1!p. apply L.ge_bot. apply L.ge_refl. + apply L.ge_refl. apply L.eq_refl. + destruct t1!p. apply L.ge_bot. apply L.ge_refl. apply L.eq_refl. auto. rewrite PTree.gcombine. @@ -201,16 +251,67 @@ Proof. rewrite PTree.gcombine. destruct t0!p. destruct t1!p. apply L.ge_lub_left. - apply L.ge_refl. apply L.ge_refl. auto. + apply L.ge_refl. apply L.eq_refl. apply L.ge_refl. apply L.eq_refl. auto. rewrite PTree.gcombine. destruct t0!p. destruct t1!p. apply L.ge_lub_left. - apply L.ge_top. apply L.ge_refl. + apply L.ge_top. apply L.ge_refl. apply L.eq_refl. auto. Qed. End LPMap. +(** * Semi-lattice over a set. *) + +(** Given a set [S: FSetInterface.S], the following functor + implements a semi-lattice over these sets, ordered by inclusion. *) + +Module LFSet (S: FSetInterface.S) <: SEMILATTICE. + + Definition t := S.t. + + Definition eq (x y: t) := S.Equal x y. + Definition eq_refl: forall x, eq x x := S.eq_refl. + Definition eq_sym: forall x y, eq x y -> eq y x := S.eq_sym. + Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := S.eq_trans. + Definition beq: t -> t -> bool := S.equal. + Definition beq_correct: forall x y, beq x y = true -> eq x y := S.equal_2. + + Definition ge (x y: t) := S.Subset y x. + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge, S.Equal, S.Subset; intros. firstorder. + Qed. + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge, S.Subset; intros. eauto. + Qed. + Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. + Proof. + unfold ge, eq, S.Subset, S.Equal; intros. firstorder. + Qed. + + Definition bot: t := S.empty. + Lemma ge_bot: forall x, ge x bot. + Proof. + unfold ge, bot, S.Subset; intros. elim (S.empty_1 H). + Qed. + + Definition lub: t -> t -> t := S.union. + Lemma lub_commut: forall x y, eq (lub x y) (lub y x). + Proof. + unfold lub, eq, S.Equal; intros. split; intro. + destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto. + destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto. + Qed. + + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold lub, ge, S.Subset; intros. apply S.union_2; auto. + Qed. + +End LFSet. + (** * Flat semi-lattice *) (** Given a type with decidable equality [X], the following functor @@ -227,9 +328,23 @@ Inductive t_ : Set := Definition t : Set := t_. -Lemma eq: forall (x y: t), {x=y} + {x<>y}. +Definition eq (x y: t) := (x = y). +Definition eq_refl: forall x, eq x x := (@refl_equal t). +Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). +Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + +Definition beq (x y: t) : bool := + match x, y with + | Bot, Bot => true + | Inj u, Inj v => if X.eq u v then true else false + | Top, Top => true + | _, _ => false + end. + +Lemma beq_correct: forall x y, beq x y = true -> eq x y. Proof. - decide equality. apply X.eq. + unfold eq; destruct x; destruct y; simpl; try congruence; intro. + destruct (X.eq t0 t1); congruence. Qed. Definition ge (x y: t) : Prop := @@ -240,9 +355,9 @@ Definition ge (x y: t) : Prop := | _, _ => False end. -Lemma ge_refl: forall x, ge x x. +Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. - unfold ge; destruct x; auto. + unfold eq, ge; intros; subst y; destruct x; auto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. @@ -251,6 +366,11 @@ Proof. transitivity t1; auto. Qed. +Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. +Proof. + unfold eq; intros; congruence. +Qed. + Definition bot: t := Bot. Lemma ge_bot: forall x, ge x bot. @@ -274,9 +394,9 @@ Definition lub (x y: t) : t := | Inj a, Inj b => if X.eq a b then Inj a else Top end. -Lemma lub_commut: forall x y, lub x y = lub y x. +Lemma lub_commut: forall x y, eq (lub x y) (lub y x). Proof. - destruct x; destruct y; simpl; auto. + unfold eq; destruct x; destruct y; simpl; auto. case (X.eq t0 t1); case (X.eq t1 t0); intros; congruence. Qed. @@ -297,17 +417,29 @@ Module LBoolean <: SEMILATTICE_WITH_TOP. Definition t := bool. -Lemma eq: forall (x y: t), {x=y} + {x<>y}. -Proof. decide equality. Qed. +Definition eq (x y: t) := (x = y). +Definition eq_refl: forall x, eq x x := (@refl_equal t). +Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t). +Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t). + +Definition beq : t -> t -> bool := eqb. + +Lemma beq_correct: forall x y, beq x y = true -> eq x y. +Proof eqb_prop. Definition ge (x y: t) : Prop := x = y \/ x = true. -Lemma ge_refl: forall x, ge x x. +Lemma ge_refl: forall x y, eq x y -> ge x y. Proof. unfold ge; tauto. Qed. Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. Proof. unfold ge; intuition congruence. Qed. +Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'. +Proof. + unfold eq; intros; congruence. +Qed. + Definition bot := false. Lemma ge_bot: forall x, ge x bot. @@ -320,8 +452,8 @@ Proof. unfold ge, top; tauto. Qed. Definition lub (x y: t) := x || y. -Lemma lub_commut: forall x y, lub x y = lub y x. -Proof. intros; unfold lub. apply orb_comm. Qed. +Lemma lub_commut: forall x y, eq (lub x y) (lub y x). +Proof. intros; unfold eq, lub. apply orb_comm. Qed. Lemma ge_lub_left: forall x y, ge (lub x y) x. Proof. destruct x; destruct y; compute; tauto. Qed. @@ -329,3 +461,4 @@ Proof. destruct x; destruct y; compute; tauto. Qed. End LBoolean. + @@ -60,6 +60,19 @@ Module Type TREE. forall (A: Set) (i j: elt) (m: t A), i <> j -> get i (remove j m) = get i m. + (** Extensional equality between trees. *) + Variable beq: forall (A: Set), (A -> A -> bool) -> t A -> t A -> bool. + Hypothesis beq_correct: + forall (A: Set) (P: A -> A -> Prop) (cmp: A -> A -> bool), + (forall (x y: A), cmp x y = true -> P x y) -> + forall (t1 t2: t A), beq cmp t1 t2 = true -> + forall (x: elt), + match get x t1, get x t2 with + | None, None => True + | Some y1, Some y2 => P y1 y2 + | _, _ => False + end. + (** Applying a function to all data of a tree. *) Variable map: forall (A B: Set), (elt -> A -> B) -> t A -> t B. @@ -305,6 +318,75 @@ Module PTree <: TREE. auto. Qed. + Section EXTENSIONAL_EQUALITY. + + Variable A: Set. + Variable eqA: A -> A -> Prop. + Variable beqA: A -> A -> bool. + Hypothesis beqA_correct: forall x y, beqA x y = true -> eqA x y. + + Definition exteq (m1 m2: t A) : Prop := + forall (x: elt), + match get x m1, get x m2 with + | None, None => True + | Some y1, Some y2 => eqA y1 y2 + | _, _ => False + end. + + Fixpoint bempty (m: t A) : bool := + match m with + | Leaf => true + | Node l None r => bempty l && bempty r + | Node l (Some _) r => false + end. + + Lemma bempty_correct: + forall m, bempty m = true -> forall x, get x m = None. + Proof. + induction m; simpl; intros. + change (@Leaf A) with (empty A). apply gempty. + destruct o. congruence. destruct (andb_prop _ _ H). + destruct x; simpl; auto. + Qed. + + Fixpoint beq (m1 m2: t A) {struct m1} : bool := + match m1, m2 with + | Leaf, _ => bempty m2 + | _, Leaf => bempty m1 + | Node l1 o1 r1, Node l2 o2 r2 => + match o1, o2 with + | None, None => true + | Some y1, Some y2 => beqA y1 y2 + | _, _ => false + end + && beq l1 l2 && beq r1 r2 + end. + + Lemma beq_correct: + forall m1 m2, beq m1 m2 = true -> exteq m1 m2. + Proof. + induction m1; destruct m2; simpl. + intros; red; intros. change (@Leaf A) with (empty A). + repeat rewrite gempty. auto. + destruct o; intro. congruence. + red; intros. change (@Leaf A) with (empty A). rewrite gempty. + rewrite bempty_correct. auto. assumption. + destruct o; intro. congruence. + red; intros. change (@Leaf A) with (empty A). rewrite gempty. + rewrite bempty_correct. auto. assumption. + destruct o; destruct o0; simpl; intro; try congruence. + destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). + red; intros. destruct x; simpl. + apply IHm1_2; auto. apply IHm1_1; auto. + apply beqA_correct; auto. + destruct (andb_prop _ _ H). + red; intros. destruct x; simpl. + apply IHm1_2; auto. apply IHm1_1; auto. + auto. + Qed. + + End EXTENSIONAL_EQUALITY. + Fixpoint append (i j : positive) {struct i} : positive := match i with | xH => j diff --git a/lib/Sets.v b/lib/Sets.v deleted file mode 100644 index 0a809fcd..00000000 --- a/lib/Sets.v +++ /dev/null @@ -1,189 +0,0 @@ -(** Finite sets. This module implements finite sets over any type - that is equipped with a tree (partial finite mapping) structure. - The set structure forms a semi-lattice, ordered by set inclusion. - - It would have been better to use the [FSet] library, which provides - sets over any totally ordered type. However, there are technical - mismatches between the [FSet] export signature and our signature for - semi-lattices. For now, we keep this somewhat redundant - implementation of sets. -*) - -Require Import Coqlib. -Require Import Maps. -Require Import Lattice. - -Set Implicit Arguments. - -Module MakeSet (P: TREE) <: SEMILATTICE. - -(** Sets of elements of type [P.elt] are implemented as a partial mapping - from [P.elt] to the one-element type [unit]. *) - - Definition elt := P.elt. - - Definition t := P.t unit. - - Lemma eq: forall (a b: t), {a=b} + {a<>b}. - Proof. - unfold t; intros. apply P.eq. - intros. left. destruct x; destruct y; auto. - Qed. - - Definition empty := P.empty unit. - - Definition mem (r: elt) (s: t) := - match P.get r s with None => false | Some _ => true end. - - Definition add (r: elt) (s: t) := P.set r tt s. - - Definition remove (r: elt) (s: t) := P.remove r s. - - Definition union (s1 s2: t) := - P.combine - (fun e1 e2 => - match e1, e2 with - | None, None => None - | _, _ => Some tt - end) - s1 s2. - - Lemma mem_empty: - forall r, mem r empty = false. - Proof. - intro; unfold mem, empty. rewrite P.gempty. auto. - Qed. - - Lemma mem_add_same: - forall r s, mem r (add r s) = true. - Proof. - intros; unfold mem, add. rewrite P.gss. auto. - Qed. - - Lemma mem_add_other: - forall r r' s, r <> r' -> mem r' (add r s) = mem r' s. - Proof. - intros; unfold mem, add. rewrite P.gso; auto. - Qed. - - Lemma mem_remove_same: - forall r s, mem r (remove r s) = false. - Proof. - intros; unfold mem, remove. rewrite P.grs; auto. - Qed. - - Lemma mem_remove_other: - forall r r' s, r <> r' -> mem r' (remove r s) = mem r' s. - Proof. - intros; unfold mem, remove. rewrite P.gro; auto. - Qed. - - Lemma mem_union: - forall r s1 s2, mem r (union s1 s2) = (mem r s1 || mem r s2). - Proof. - intros; unfold union, mem. rewrite P.gcombine. - case (P.get r s1); case (P.get r s2); auto. - auto. - Qed. - - Definition elements (s: t) := - List.map (@fst elt unit) (P.elements s). - - Lemma elements_correct: - forall r s, mem r s = true -> In r (elements s). - Proof. - intros until s. unfold mem, elements. caseEq (P.get r s). - intros. change r with (fst (r, u)). apply in_map. - apply P.elements_correct. auto. - intros; discriminate. - Qed. - - Lemma elements_complete: - forall r s, In r (elements s) -> mem r s = true. - Proof. - unfold mem, elements. intros. - generalize (list_in_map_inv _ _ _ H). - intros [p [EQ IN]]. - destruct p. simpl in EQ. subst r. - rewrite (P.elements_complete _ _ _ IN). auto. - Qed. - - Definition fold (A: Set) (f: A -> elt -> A) (s: t) (x: A) := - P.fold (fun (x: A) (r: elt) (z: unit) => f x r) s x. - - Lemma fold_spec: - forall (A: Set) (f: A -> elt -> A) (s: t) (x: A), - fold f s x = List.fold_left f (elements s) x. - Proof. - intros. unfold fold. rewrite P.fold_spec. - unfold elements. generalize x; generalize (P.elements s). - induction l; simpl; auto. - Qed. - - Definition for_all (f: elt -> bool) (s: t) := - fold (fun b x => andb b (f x)) s true. - - Lemma for_all_spec: - forall f s x, - for_all f s = true -> mem x s = true -> f x = true. - Proof. - intros until x. unfold for_all. rewrite fold_spec. - assert (forall l b0, - fold_left (fun (b : bool) (x : elt) => b && f x) l b0 = true -> - b0 = true). - induction l; simpl; intros. - auto. - generalize (IHl _ H). intro. - elim (andb_prop _ _ H0); intros. auto. - assert (forall l, - fold_left (fun (b : bool) (x : elt) => b && f x) l true = true -> - In x l -> f x = true). - induction l; simpl; intros. - elim H1. - generalize (H _ _ H0); intro. - elim H1; intros. - subst x. auto. - apply IHl. rewrite H2 in H0; auto. auto. - intros. eapply H0; eauto. - apply elements_correct. auto. - Qed. - - Definition ge (s1 s2: t) : Prop := - forall r, mem r s2 = true -> mem r s1 = true. - - Lemma ge_refl: forall x, ge x x. - Proof. - unfold ge; intros. auto. - Qed. - - Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Proof. - unfold ge; intros. auto. - Qed. - - Definition bot := empty. - Definition lub := union. - - Lemma ge_bot: forall (x:t), ge x bot. - Proof. - unfold ge; intros. rewrite mem_empty in H. discriminate. - Qed. - - Lemma lub_commut: forall (x y: t), lub x y = lub y x. - Proof. - intros. unfold lub; unfold union. apply P.combine_commut. - intros; case i; case j; auto. - Qed. - - Lemma ge_lub_left: forall (x y: t), ge (lub x y) x. - Proof. - unfold ge, lub; intros. - rewrite mem_union. rewrite H. reflexivity. - Qed. - - Lemma ge_lub_right: forall (x y: t), ge (lub x y) y. - Proof. - intros. rewrite lub_commut. apply ge_lub_left. - Qed. - -End MakeSet. diff --git a/lib/union_find.v b/lib/union_find.v deleted file mode 100644 index 452459fa..00000000 --- a/lib/union_find.v +++ /dev/null @@ -1,484 +0,0 @@ -(** A purely functional union-find algorithm *) - -Require Import Wf. -Require Recdef. - -(** The ``union-find'' algorithm is used to represent equivalence classes - over a given type. It maintains a data structure representing a partition - of the type into equivalence classes. Three operations are provided: -- [empty], which returns the finest partition: each element of the type - is equivalent to itself only. -- [repr part x] returns a canonical representative for the equivalence - class of element [x] in partition [part]. Two elements [x] and [y] - are in the same equivalence class if and only if - [repr part x = repr part y]. -- [identify part x y] returns a new partition where the equivalence - classes of [x] and [y] are merged, and all equivalences valid in [part] - are still valid. - - The partitions are represented by partial mappings from elements - to elements. If [part] maps [x] to [y], this means that [x] and [y] - are in the same equivalence class. The canonical representative - of the class of [x] is obtained by iteratively following these mappings - until an element not mapped to anything is reached; this element is the - canonical representative, as returned by [repr]. - - In algorithm textbooks, the mapping is maintained imperatively by - storing pointers within elements. Here, we give a purely functional - presentation where the mapping is a separate functional data structure. -*) - -(** The elements of equivalence classes are represented by the following - signature: a type with a decidable equality. *) - -Module Type ELEMENT. - Variable T: Set. - Variable eq: forall (a b: T), {a = b} + {a <> b}. -End ELEMENT. - -(** The mapping structure over elements is represented by the following - signature. *) - -Module Type MAP. - Variable elt: Set. - Variable T: Set. - Variable empty: T. - Variable get: elt -> T -> option elt. - Variable add: elt -> elt -> T -> T. - - Hypothesis get_empty: forall (x: elt), get x empty = None. - Hypothesis get_add_1: - forall (x y: elt) (m: T), get x (add x y m) = Some y. - Hypothesis get_add_2: - forall (x y z: elt) (m: T), z <> x -> get z (add x y m) = get z m. -End MAP. - -(** Our implementation of union-find is a functor, parameterized by - a structure for elements and a structure for maps. It returns a - module with the following structure. *) - -Module Type UNIONFIND. - Variable elt: Set. - (** The type of partitions. *) - Variable T: Set. - - (** The operations over partitions. *) - Variable empty: T. - Variable repr: T -> elt -> elt. - Variable identify: T -> elt -> elt -> T. - - (** The relation implied by the partition [m]. *) - Definition sameclass (m: T) (x y: elt) : Prop := repr m x = repr m y. - - (* [sameclass] is an equivalence relation *) - Hypothesis sameclass_refl: - forall (m: T) (x: elt), sameclass m x x. - Hypothesis sameclass_sym: - forall (m: T) (x y: elt), sameclass m x y -> sameclass m y x. - Hypothesis sameclass_trans: - forall (m: T) (x y z: elt), - sameclass m x y -> sameclass m y z -> sameclass m x z. - - (* [repr m x] is a canonical representative of the equivalence class - of [x] in partition [m]. *) - Hypothesis repr_repr: - forall (m: T) (x: elt), repr m (repr m x) = repr m x. - Hypothesis sameclass_repr: - forall (m: T) (x: elt), sameclass m x (repr m x). - - (* [empty] is the finest partition *) - Hypothesis repr_empty: - forall (x: elt), repr empty x = x. - Hypothesis sameclass_empty: - forall (x y: elt), sameclass empty x y -> x = y. - - (* [identify] preserves existing equivalences and adds an equivalence - between the two elements provided. *) - Hypothesis sameclass_identify_1: - forall (m: T) (x y: elt), sameclass (identify m x y) x y. - Hypothesis sameclass_identify_2: - forall (m: T) (x y u v: elt), - sameclass m u v -> sameclass (identify m x y) u v. - -End UNIONFIND. - -(** Implementation of the union-find algorithm. *) - -Module Unionfind (E: ELEMENT) (M: MAP with Definition elt := E.T) - <: UNIONFIND with Definition elt := E.T. - -Definition elt := E.T. - -(* 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. -*) - -(** Such a map induces an ordering over type [elt]: - [repr_order m a a'] if and only if [M.get a' m = Some a]. - This ordering must be well founded (no cycles). *) - -Definition repr_order (m: M.T) (a a': elt) : Prop := - M.get a' m = Some a. - -(** The canonical representative of an element. - Needs Noetherian recursion. *) - -Section REPR. - -Variable m: M.T. -Variable wf: well_founded (repr_order m). - -Function repr_aux (a: elt) {wf (repr_order m) a} : elt := - match M.get a m with - | Some a' => repr_aux a' - | None => a - end. -Proof. - intros. assumption. - assumption. -Qed. - -Lemma repr_aux_none: - forall (a: elt), - M.get a m = None -> - repr_aux a = a. -Proof. - intros. rewrite repr_aux_equation. rewrite H. auto. -Qed. - -Lemma repr_aux_some: - forall (a a': elt), - M.get a m = Some a' -> - repr_aux a = repr_aux a'. -Proof. - intros. rewrite repr_aux_equation. rewrite H. auto. -Qed. - -Lemma repr_aux_canon: - forall (a: elt), M.get (repr_aux a) m = None. -Proof. - intros a0. - apply (repr_aux_ind (fun a a' => M.get a' m = None)). - auto. auto. -Qed. - -End REPR. - -(** The empty partition (each element in its own class) is well founded. *) - -Lemma wf_empty: - well_founded (repr_order M.empty). -Proof. - red. intro. apply Acc_intro. - intros b RO. - red in RO. - rewrite M.get_empty in RO. - discriminate. -Qed. - -(** Merging two equivalence classes. *) - -Section IDENTIFY. - -Variable m: M.T. -Hypothesis mwf: well_founded (repr_order m). -Variable a b: elt. -Hypothesis a_diff_b: a <> b. -Hypothesis a_canon: M.get a m = None. -Hypothesis b_canon: M.get b m = None. - -(** Identifying two distinct canonical representatives [a] and [b] - is achieved by mapping one to the other. *) - -Definition identify_base: M.T := M.add a b m. - -Lemma identify_base_b_canon: - M.get b identify_base = None. -Proof. - unfold identify_base. - rewrite M.get_add_2. - auto. - apply sym_not_eq. auto. -Qed. - -Lemma identify_base_a_maps_to_b: - M.get a identify_base = Some b. -Proof. - unfold identify_base. rewrite M.get_add_1. auto. -Qed. - -Lemma identify_base_repr_order: - forall (x y: elt), - repr_order identify_base x y -> - repr_order m x y \/ (y = a /\ x = b). -Proof. - intros x y. unfold identify_base. - unfold repr_order. - case (E.eq a y); intro. - rewrite e. rewrite M.get_add_1. - intro. injection H. intro. rewrite H0. tauto. - rewrite M.get_add_2; auto. -Qed. - -(** [identify_base] preserves well foundation. *) - -Lemma identify_base_order_wf: - well_founded (repr_order identify_base). -Proof. - red. - cut (forall (x: elt), Acc (repr_order m) x -> Acc (repr_order identify_base) x). - intro CUT. intro x. apply CUT. apply mwf. - - induction 1. - apply Acc_intro. intros. - destruct (identify_base_repr_order y x H1) as [A | [A B]]. - apply H0; auto. - subst x y. apply Acc_intro. intros z H4. - red in H4. rewrite identify_base_b_canon in H4. discriminate. -Qed. - -Lemma identify_aux_decomp: - forall (x: elt), - (M.get x m = None /\ M.get x identify_base = None) - \/ (x = a /\ M.get x m = None /\ M.get x identify_base = Some b) - \/ (exists y, M.get x m = Some y /\ M.get x identify_base = Some y). -Proof. - intro x. - unfold identify_base. - case (E.eq a x); intro. - rewrite <- e. rewrite M.get_add_1. - tauto. - rewrite M.get_add_2; auto. - case (M.get x m); intros. - right; right; exists e; tauto. - tauto. -Qed. - -Lemma identify_base_repr: - forall (x: elt), - repr_aux identify_base identify_base_order_wf x = - (if E.eq (repr_aux m mwf x) a then b else repr_aux m mwf x). -Proof. - apply (well_founded_ind mwf - (fun (x: elt) => - repr_aux identify_base identify_base_order_wf x = - (if E.eq (repr_aux m mwf x) a then b else repr_aux m mwf x))); - intros. - destruct (identify_aux_decomp x) as [[A B] | [[A [B C]] | [y [A B]]]]. - - rewrite (repr_aux_none identify_base); auto. - rewrite (repr_aux_none m mwf x); auto. - case (E.eq x a); intro. - subst x. - rewrite identify_base_a_maps_to_b in B. discriminate. - auto. - - subst x. rewrite (repr_aux_none m mwf a); auto. - case (E.eq a a); intro. - rewrite (repr_aux_some identify_base identify_base_order_wf a b); auto. - rewrite (repr_aux_none identify_base identify_base_order_wf b); auto. - apply identify_base_b_canon. - tauto. - - rewrite (repr_aux_some identify_base identify_base_order_wf x y); auto. - rewrite (repr_aux_some m mwf x y); auto. -Qed. - -Lemma identify_base_sameclass_1: - forall (x y: elt), - repr_aux m mwf x = repr_aux m mwf y -> - repr_aux identify_base identify_base_order_wf x = - repr_aux identify_base identify_base_order_wf y. -Proof. - intros. - rewrite identify_base_repr. - rewrite identify_base_repr. - rewrite H. - auto. -Qed. - -Lemma identify_base_sameclass_2: - forall (x y: elt), - repr_aux m mwf x = a -> - repr_aux m mwf y = b -> - repr_aux identify_base identify_base_order_wf x = - repr_aux identify_base identify_base_order_wf y. -Proof. - intros. - rewrite identify_base_repr. - rewrite identify_base_repr. - rewrite H. - case (E.eq a a); intro. - case (E.eq (repr_aux m mwf y) a); auto. - tauto. -Qed. - -End IDENTIFY. - -(** The union-find data structure is a record encapsulating a mapping - and a proof of well foundation. *) - -Record unionfind : Set := mkunionfind - { map: M.T; wf: well_founded (repr_order map) }. - -Definition T := unionfind. - -Definition repr (uf: unionfind) (a: elt) : elt := - repr_aux (map uf) (wf uf) a. - -Lemma repr_repr: - forall (uf: unionfind) (a: elt), repr uf (repr uf a) = repr uf a. -Proof. - intros. - unfold repr. - rewrite (repr_aux_none (map uf) (wf uf) (repr_aux (map uf) (wf uf) a)). - auto. - apply repr_aux_canon. -Qed. - -Definition empty := mkunionfind M.empty wf_empty. - -(** [identify] computes canonical representatives for the two elements - and adds a mapping from one to the other, unless they are already - equal. *) - -Definition identify (uf: unionfind) (a b: elt) : unionfind := - match E.eq (repr uf a) (repr uf b) with - | left EQ => - uf - | right NOTEQ => - mkunionfind - (identify_base (map uf) (repr uf a) (repr uf b)) - (identify_base_order_wf (map uf) (wf uf) - (repr uf a) (repr uf b) - NOTEQ - (repr_aux_canon (map uf) (wf uf) b)) - end. - -Definition sameclass (uf: unionfind) (a b: elt) : Prop := - repr uf a = repr uf b. - -Lemma sameclass_refl: - forall (uf: unionfind) (a: elt), sameclass uf a a. -Proof. - intros. red. auto. -Qed. - -Lemma sameclass_sym: - forall (uf: unionfind) (a b: elt), sameclass uf a b -> sameclass uf b a. -Proof. - intros. red. symmetry. exact H. -Qed. - -Lemma sameclass_trans: - forall (uf: unionfind) (a b c: elt), - 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: unionfind) (a: elt), sameclass uf a (repr uf a). -Proof. - intros. red. symmetry. rewrite repr_repr. auto. -Qed. - -Lemma repr_empty: - forall (a: elt), repr empty a = a. -Proof. - intro a. unfold repr; unfold empty. - simpl. - apply repr_aux_none. - apply M.get_empty. -Qed. - -Lemma sameclass_empty: - forall (a b: elt), sameclass empty a b -> a = b. -Proof. - intros. red in H. rewrite repr_empty in H. - rewrite repr_empty in H. auto. -Qed. - -Lemma sameclass_identify_2: - forall (uf: unionfind) (a b x y: elt), - sameclass uf x y -> sameclass (identify uf a b) x y. -Proof. - intros. - unfold identify. - case (E.eq (repr uf a) (repr uf b)). - intro. auto. - intros; red; unfold repr; simpl. - apply identify_base_sameclass_1. - apply repr_aux_canon. - exact H. -Qed. - -Lemma sameclass_identify_1: - forall (uf: unionfind) (a b: elt), - sameclass (identify uf a b) a b. -Proof. - intros. - unfold identify. - case (E.eq (repr uf a) (repr uf b)). - intro. auto. - intros. - red; unfold repr; simpl. - apply identify_base_sameclass_2. - apply repr_aux_canon. - auto. - auto. -Qed. - -End Unionfind. - -(* Example of use 1: with association lists *) - -(* - -Require Import List. - -Module AListMap(E: ELEMENT) : MAP. - -Definition elt := E.T. -Definition T := list (elt * elt). -Definition empty : T := nil. -Fixpoint get (x: elt) (m: T) {struct m} : option elt := - match m with - | nil => None - | (a,b) :: t => - match E.eq x a with - | left _ => Some b - | right _ => get x t - end - end. -Definition add (x y: elt) (m: T) := (x,y) :: m. - -Lemma get_empty: forall (x: elt), get x empty = None. -Proof. - intro. unfold empty. simpl. auto. -Qed. - -Lemma get_add_1: - forall (x y: elt) (m: T), get x (add x y m) = Some y. -Proof. - intros. unfold add. simpl. - case (E.eq x x); intro. - auto. - tauto. -Qed. - -Lemma get_add_2: - forall (x y z: elt) (m: T), z <> x -> get z (add x y m) = get z m. -Proof. - intros. unfold add. simpl. - case (E.eq z x); intro. - subst z; tauto. - auto. -Qed. - -End AListMap. - -*) - |