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

1 files changed, 702 insertions, 0 deletions

diff --git a/lib/UnionFind.v b/lib/UnionFind.v
new file mode 100644
index 0000000..d74a20a
--- /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.
+