Suppression de lib/Sets.v, utilisation de FSet a la place. Generalisation de Lattice pour utiliser une notion d'egalite possiblement differente de =. Adaptation de Kildall et de ses utilisateurs en consequence.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@182 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 248 insertions, 706 deletions

diff --git a/lib/Lattice.v b/lib/Lattice.v
index 7adcffb..7ef1b9e 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.
 
 
+
diff --git a/lib/Maps.v b/lib/Maps.v
index 22d9a37..238009b 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -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 0a809fc..0000000
--- 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 452459f..0000000
--- 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.
-
-*)
-