Assorted cleanups, esp. to avoid generating _rec and _rect recursors in

submodules.  (Extraction does not remove them, then.)  
common/Switch: replaced use of FMaps by our own Maps.


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

6 files changed, 177 insertions, 164 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index 4f697b9..d99e20f 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -62,6 +62,7 @@ module P = struct
   let gt x y = (Pos.compare x y = Gt)
   let le x y = (Pos.compare x y <> Gt)
   let ge x y = (Pos.compare x y <> Lt)
+  let compare x y = match Pos.compare x y with Lt -> -1 | Eq -> 0 | Gt -> 1
 
   let rec to_int = function
   | Coq_xI p -> (to_int p lsl 1) + 1
@@ -129,6 +130,7 @@ module Z = struct
   let gt x y = (Z.compare x y = Gt)
   let le x y = (Z.compare x y <> Gt)
   let ge x y = (Z.compare x y <> Lt)
+  let compare x y = match Z.compare x y with Lt -> -1 | Eq -> 0 | Gt -> 1
 
   let to_int = function
   | Z0 -> 0
diff --git a/lib/Heaps.v b/lib/Heaps.v
index a5c0d61..0ee07a5 100644
--- a/lib/Heaps.v
+++ b/lib/Heaps.v
@@ -25,6 +25,10 @@ Require Import Coqlib.
 Require Import FSets.
 Require Import Ordered.
 
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 Module SplayHeapSet(E: OrderedType).
 
 (** "Raw" implementation.  The "is a binary search tree" invariant
@@ -36,7 +40,7 @@ Inductive heap: Type :=
   | Empty
   | Node (l: heap) (x: E.t) (r: heap).
 
-Function partition (pivot: E.t) (h: heap) { struct h } : heap * heap :=
+Fixpoint partition (pivot: E.t) (h: heap) { struct h } : heap * heap :=
   match h with
   | Empty => (Empty, Empty)
   | Node a x b =>
@@ -83,7 +87,7 @@ Fixpoint findMin (h: heap) : option E.t :=
   | Node a x b => findMin a
   end.
 
-Function deleteMin (h: heap) : heap :=
+Fixpoint deleteMin (h: heap) : heap :=
   match h with
   | Empty => Empty
   | Node Empty x b => b
@@ -98,7 +102,7 @@ Fixpoint findMax (h: heap) : option E.t :=
   | Node a x b => findMax b
   end.
 
-Function deleteMax (h: heap) : heap :=
+Fixpoint deleteMax (h: heap) : heap :=
   match h with
   | Empty => Empty
   | Node b x Empty => b
@@ -106,6 +110,13 @@ Function deleteMax (h: heap) : heap :=
   | Node a x (Node b y c) => Node (Node a x b) y (deleteMax c)
   end.
 
+(** Induction principles for some of the operators. *)
+
+Scheme heap_ind := Induction for heap Sort Prop.
+Functional Scheme partition_ind := Induction for partition Sort Prop.
+Functional Scheme deleteMin_ind := Induction for deleteMin Sort Prop.
+Functional Scheme deleteMax_ind := Induction for deleteMax Sort Prop.
+
 (** Specification *)
 
 Fixpoint In (x: E.t) (h: heap) : Prop :=
@@ -191,50 +202,38 @@ Lemma In_partition:
   forall h, bst h -> (In x h <-> In x (fst (partition pivot h)) \/ In x (snd (partition pivot h))).
 Proof.
   intros x pivot NEQ h0. functional induction (partition pivot h0); simpl; intros.
-  tauto.
-  intuition. elim NEQ. eapply E.eq_trans; eauto.
-  intuition.
-  intuition. elim NEQ. eapply E.eq_trans; eauto.
-  rewrite e3 in IHp; simpl in IHp. intuition.
-  rewrite e3 in IHp; simpl in IHp. intuition.
-  intuition. 
-  intuition. elim NEQ. eapply E.eq_trans; eauto. 
-  rewrite e3 in IHp; simpl in IHp. intuition.
-  rewrite e3 in IHp; simpl in IHp. intuition.
+- tauto.
+- tauto.
+- rewrite e3 in *; simpl in *; intuition.
+- intuition. elim NEQ. eapply E.eq_trans; eauto. 
+- rewrite e3 in *; simpl in *; intuition.
+- intuition. elim NEQ. eapply E.eq_trans; eauto. 
+- intuition. 
+- rewrite e3 in *; simpl in *; intuition.
+- intuition. elim NEQ. eapply E.eq_trans; eauto. 
+- rewrite e3 in *; simpl in *; intuition.
 Qed.
 
 Lemma partition_lt:
   forall x pivot h,
   lt_heap h x -> lt_heap (fst (partition pivot h)) x /\ lt_heap (snd (partition pivot h)) x.
 Proof.
-  intros x pivot h0. functional induction (partition pivot h0); simpl.
-  tauto.
-  tauto.
-  tauto.
-  tauto.
-  rewrite e3 in IHp; simpl in IHp. tauto. 
-  rewrite e3 in IHp; simpl in IHp. tauto. 
-  tauto.
-  tauto.
-  rewrite e3 in IHp; simpl in IHp. tauto. 
-  rewrite e3 in IHp; simpl in IHp. tauto. 
+  intros x pivot h0. functional induction (partition pivot h0); simpl; try tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
 Qed.
  
 Lemma partition_gt:
   forall x pivot h,
   gt_heap h x -> gt_heap (fst (partition pivot h)) x /\ gt_heap (snd (partition pivot h)) x.
 Proof.
-  intros x pivot h0. functional induction (partition pivot h0); simpl.
-  tauto.
-  tauto.
-  tauto.
-  tauto.
-  rewrite e3 in IHp; simpl in IHp. tauto. 
-  rewrite e3 in IHp; simpl in IHp. tauto. 
-  tauto.
-  tauto.
-  rewrite e3 in IHp; simpl in IHp. tauto. 
-  rewrite e3 in IHp; simpl in IHp. tauto. 
+  intros x pivot h0. functional induction (partition pivot h0); simpl; try tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
+- rewrite e3 in *; simpl in *; tauto.
 Qed.
 
 Lemma partition_split:
@@ -242,28 +241,32 @@ Lemma partition_split:
   bst h -> lt_heap (fst (partition pivot h)) pivot /\ gt_heap (snd (partition pivot h)) pivot.
 Proof.
   intros pivot h0. functional induction (partition pivot h0); simpl.
-  tauto.
-  intuition. eapply lt_heap_trans; eauto. red; auto. eapply gt_heap_trans; eauto. red; left; apply E.eq_sym; auto. 
-  intuition. eapply lt_heap_trans; eauto. red; auto.
-  intuition. eapply lt_heap_trans; eauto. red; auto. 
-    eapply lt_heap_trans; eauto. red; auto.
-    apply gt_heap_trans with y; auto. red. left; apply E.eq_sym; auto.
-  rewrite e3 in IHp; simpl in IHp. intuition.
-    eapply lt_heap_trans; eauto. red; auto.
-    eapply lt_heap_trans; eauto. red; auto.
-  rewrite e3 in IHp; simpl in IHp. intuition.
-    eapply lt_heap_trans; eauto. red; auto.
-    apply gt_heap_trans with y; eauto. red; auto.
-  intuition. eapply gt_heap_trans; eauto. red; auto.
-  intuition. apply lt_heap_trans with y; eauto. red; auto.
-    eapply gt_heap_trans; eauto. red; left; apply E.eq_sym; auto.
-    eapply gt_heap_trans; eauto. red; auto.
-  rewrite e3 in IHp; simpl in IHp. intuition.
-    apply lt_heap_trans with y; eauto. red; auto.
-    eapply gt_heap_trans; eauto. red; auto.
-  rewrite e3 in IHp; simpl in IHp. intuition.
-    apply gt_heap_trans with y; eauto. red; auto.
-    apply gt_heap_trans with x; eauto. red; auto.
+- tauto.
+- intuition. eapply lt_heap_trans; eauto. red; auto.
+- rewrite e3 in *; simpl in *. intuition.
+  eapply lt_heap_trans; eauto. red; auto.
+  eapply lt_heap_trans; eauto. red; auto.
+- intuition.
+  eapply lt_heap_trans; eauto. red; auto.
+  eapply lt_heap_trans; eauto. red; auto.
+  eapply gt_heap_trans with y; eauto. red. left. apply E.eq_sym; auto. 
+- rewrite e3 in *; simpl in *; intuition.
+  eapply lt_heap_trans; eauto. red; auto.
+  eapply gt_heap_trans with y; eauto. red; auto.
+- intuition. 
+  eapply lt_heap_trans; eauto. red; auto.
+  eapply gt_heap_trans; eauto. red; auto.
+- intuition. eapply gt_heap_trans; eauto. red; auto. 
+- rewrite e3 in *; simpl in *. intuition.
+  eapply lt_heap_trans with y; eauto. red; auto.
+  eapply gt_heap_trans; eauto. red; auto.
+- intuition. 
+  eapply lt_heap_trans with y; eauto. red; auto.
+  eapply gt_heap_trans; eauto. red; auto.
+  eapply gt_heap_trans with x; eauto. red; auto.
+- rewrite e3 in *; simpl in *; intuition.
+  eapply gt_heap_trans; eauto. red; auto.
+  eapply gt_heap_trans; eauto. red; auto.
 Qed.
 
 Lemma partition_bst:
@@ -271,25 +274,19 @@ Lemma partition_bst:
   bst h ->
   bst (fst (partition pivot h)) /\ bst (snd (partition pivot h)).
 Proof.
-  intros pivot h0. functional induction (partition pivot h0); simpl.
-  tauto.
-  tauto.
-  tauto.
-  tauto.
-  rewrite e3 in IHp; simpl in IHp. intuition. 
+  intros pivot h0. functional induction (partition pivot h0); simpl; try tauto.
+- rewrite e3 in *; simpl in *. intuition. 
     apply lt_heap_trans with x; auto. red; auto.
     generalize (partition_gt y pivot b2 H7). rewrite e3; simpl. tauto.
-  rewrite e3 in IHp; simpl in IHp. intuition.
+- rewrite e3 in *; simpl in *. intuition. 
     generalize (partition_gt x pivot b1 H3). rewrite e3; simpl. tauto.
     generalize (partition_lt y pivot b1 H4). rewrite e3; simpl. tauto.
-  tauto.
-  tauto.
-  rewrite e3 in IHp; simpl in IHp. intuition.
+- rewrite e3 in *; simpl in *. intuition.
     generalize (partition_gt y pivot a2 H6). rewrite e3; simpl. tauto.
     generalize (partition_lt x pivot a2 H8). rewrite e3; simpl. tauto.
-  rewrite e3 in IHp; simpl in IHp. intuition.
+- rewrite e3 in *; simpl in *. intuition. 
     generalize (partition_lt y pivot a1 H3). rewrite e3; simpl. tauto.
-    apply gt_heap_trans with x; auto. red. auto.
+    apply gt_heap_trans with x; auto. red; auto.
 Qed.
 
 (** Properties of [insert] *)
@@ -322,11 +319,12 @@ Qed.
 Lemma deleteMin_lt:
   forall x h, lt_heap h x -> lt_heap (deleteMin h) x.
 Proof.
-  intros x h0. functional induction (deleteMin h0); simpl; intros.
+Opaque deleteMin.
+  intros x h0. functional induction (deleteMin h0) ; simpl; intros.
   auto.
   tauto.
-  tauto. 
-  intuition. 
+  tauto.
+  intuition. apply IHh. simpl. tauto.  
 Qed.
 
 Lemma deleteMin_bst:
@@ -337,8 +335,9 @@ Proof.
   tauto.
   tauto.
   intuition.
-    apply deleteMin_lt; auto. 
-    apply gt_heap_trans with y; auto. red; auto. 
+  apply IHh. simpl; auto.
+  apply deleteMin_lt; auto. simpl; auto.  
+  apply gt_heap_trans with y; auto. red; auto. 
 Qed.
 
 Lemma In_deleteMin:
@@ -346,11 +345,12 @@ Lemma In_deleteMin:
   findMin h = Some x ->
   (In y h <-> E.eq y x \/ In y (deleteMin h)).
 Proof.
+Transparent deleteMin.
   intros y x h0. functional induction (deleteMin h0); simpl; intros.
-  congruence.
+  discriminate. 
   inv H. tauto.
   inv H. tauto. 
-  destruct a. contradiction. tauto.
+  destruct _x. inv H. simpl. tauto. generalize (IHh H). simpl. tauto.
 Qed.
 
 Lemma gt_heap_In:
@@ -392,11 +392,12 @@ Qed.
 Lemma deleteMax_gt:
   forall x h, gt_heap h x -> gt_heap (deleteMax h) x.
 Proof.
+Opaque deleteMax.
   intros x h0. functional induction (deleteMax h0); simpl; intros.
   auto.
   tauto.
   tauto. 
-  intuition. 
+  intuition. apply IHh. simpl. tauto.  
 Qed.
 
 Lemma deleteMax_bst:
@@ -407,8 +408,9 @@ Proof.
   tauto.
   tauto.
   intuition.
+    apply IHh. simpl; auto.
     apply lt_heap_trans with x; auto. red; auto.
-    apply deleteMax_gt; auto.
+    apply deleteMax_gt; auto. simpl; auto. 
 Qed.
 
 Lemma In_deleteMax:
@@ -416,11 +418,12 @@ Lemma In_deleteMax:
   findMax h = Some x ->
   (In y h <-> E.eq y x \/ In y (deleteMax h)).
 Proof.
+Transparent deleteMax.
   intros y x h0. functional induction (deleteMax h0); simpl; intros.
   congruence.
   inv H. tauto.
   inv H. tauto. 
-  destruct c. contradiction. tauto.
+  destruct _x1. inv H. simpl. tauto. generalize (IHh H). simpl. tauto.
 Qed.
 
 Lemma lt_heap_In:
diff --git a/lib/Integers.v b/lib/Integers.v
index 0575436..2c74e80 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -57,6 +57,10 @@ Module Type WORDSIZE.
   Axiom wordsize_not_zero: wordsize <> 0%nat.
 End WORDSIZE.
 
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 Module Make(WS: WORDSIZE).
 
 Definition wordsize: nat := WS.wordsize.
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 51a7976..fd05b34 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -16,6 +16,10 @@ Require Import Coqlib.
 Require Import Maps.
 Require Import FSets.
 
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 (** * Signatures of semi-lattices *)
 
 (** A semi-lattice is a type [t] equipped with an equivalence relation [eq],
diff --git a/lib/Maps.v b/lib/Maps.v
index bd5c0e9..0c97ba5 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -34,6 +34,10 @@
 
 Require Import Coqlib.
 
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 Set Implicit Arguments.
 
 (** * The abstract signatures of trees *)
@@ -42,8 +46,6 @@ Module Type TREE.
   Variable elt: Type.
   Variable elt_eq: forall (a b: elt), {a = b} + {a <> b}.
   Variable t: Type -> Type.
-  Variable eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
-                forall (a b: t A), {a = b} + {a <> b}.
   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.
@@ -202,18 +204,10 @@ Module PTree <: TREE.
   .
   Implicit Arguments Leaf [A].
   Implicit Arguments Node [A].
+  Scheme tree_ind := Induction for tree Sort Prop.
 
   Definition t := tree.
 
-  Theorem eq : forall (A : Type),
-    (forall (x y: A), {x=y} + {x<>y}) ->
-    forall (a b : t A), {a = b} + {a <> b}.
-  Proof.
-    intros A eqA.
-    decide equality.
-    generalize o o0; decide equality.
-  Qed.
-
   Definition empty (A : Type) := (Leaf : t A).
 
   Fixpoint get (A : Type) (i : positive) (m : t A) {struct i} : option A :=
@@ -1084,14 +1078,6 @@ Module PMap <: MAP.
 
   Definition t (A : Type) : Type := (A * PTree.t A)%type.
 
-  Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
-                 forall (a b: t A), {a = b} + {a <> b}.
-  Proof.
-    intros. 
-    generalize (PTree.eq X). intros. 
-    decide equality.
-  Qed.
-
   Definition init (A : Type) (x : A) :=
     (x, PTree.empty A).
 
@@ -1175,8 +1161,6 @@ Module IMap(X: INDEXED_TYPE).
   Definition elt := X.t.
   Definition elt_eq := X.eq.
   Definition t : Type -> Type := PMap.t.
-  Definition eq: forall (A: Type), (forall (x y: A), {x=y} + {x<>y}) ->
-                 forall (a b: t A), {a = b} + {a <> b} := PMap.eq.
   Definition init (A: Type) (x: A) := PMap.init x.
   Definition get (A: Type) (i: X.t) (m: t A) := PMap.get (X.index i) m.
   Definition set (A: Type) (i: X.t) (v: A) (m: t A) := PMap.set (X.index i) v m.
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 84d0348..46a886e 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -15,14 +15,16 @@
 
 (** A persistent union-find data structure. *)
 
-Require Recdef.
-Require Setoid.
 Require Coq.Program.Wf.
 Require Import Coqlib.
 
 Open Scope nat_scope.
 Set Implicit Arguments.
 
+(* To avoid useless definitions of inductors in extracted code. *)
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 Module Type MAP.
   Variable elt: Type.
   Variable elt_eq: forall (x y: elt), {x=y} + {x<>y}.
@@ -151,20 +153,33 @@ Record unionfind : Type := mk { m: M.t elt; mwf: well_founded (order m) }.
 
 Definition t := unionfind.
 
+Definition getlink (m: M.t elt) (a: elt) : {a' | M.get a m = Some a'} + {M.get a m = None}.
+Proof.
+  destruct (M.get a m). left. exists e; auto. right; auto. 
+Defined.
+
 (* 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
+Definition F_repr (a: elt) (rec: forall b, order uf.(m) b a -> elt) : elt :=
+  match getlink uf.(m) a with
+  | inleft (exist a' P) => rec a' P
+  | inright _ => a
   end.
+
+Definition repr (a: elt) : elt := Fix uf.(mwf) (fun _ => elt) F_repr a.
+
+Lemma repr_unroll:
+  forall a, repr a = match M.get a uf.(m) with Some a' => repr a' | None => a end.
 Proof.
-  intros. auto.
-  apply mwf. 
+  intros. unfold repr at 1. rewrite Fix_eq. 
+  unfold F_repr. destruct (getlink uf.(m) a) as [[a' P] | Q]. 
+  rewrite P; auto.
+  rewrite Q; auto.
+  intros. unfold F_repr. destruct (getlink (m uf) x) as [[a' P] | Q]; auto. 
 Qed.
 
 Lemma repr_none:
@@ -172,8 +187,7 @@ Lemma repr_none:
   M.get a uf.(m) = None ->
   repr a = a.
 Proof.
-  intros.
-  functional induction (repr a). congruence. auto.
+  intros. rewrite repr_unroll. rewrite H; auto. 
 Qed.
 
 Lemma repr_some:
@@ -181,14 +195,14 @@ Lemma repr_some:
   M.get a uf.(m) = Some a' ->
   repr a = repr a'.
 Proof.
-  intros.
-  functional induction (repr a). congruence. congruence.
+  intros. rewrite repr_unroll. rewrite H; auto. 
 Qed.
 
 Lemma repr_res_none:
   forall (a: elt), M.get (repr a) uf.(m) = None.
 Proof.
-  intros. functional induction (repr a). auto. auto.
+  apply (well_founded_ind (mwf uf)). intros. 
+  rewrite repr_unroll. destruct (M.get x (m uf)) as [y|] eqn:X; auto.
 Qed.
 
 Lemma repr_canonical:
@@ -308,25 +322,23 @@ 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.
+  intros x0; pattern x0. apply (well_founded_ind (mwf uf)); intros.
+  rewrite (repr_unroll uf) in *. 
+  destruct (M.get x (m uf)) as [a'|] eqn:X.
+  rewrite <- H; auto.
+  apply repr_some. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. congruence.
+  apply repr_none. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto.  
 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.
+  intros x0; pattern x0. apply (well_founded_ind (mwf uf)); intros.
+  rewrite (repr_unroll uf) in H0. destruct (M.get x (m uf)) as [a'|] eqn:X.
+  rewrite <- (H a'); auto. 
+  apply repr_some. simpl. rewrite M.gsspec. rewrite dec_eq_false; auto. congruence.
+  subst x. rewrite (repr_unroll identify). simpl. rewrite M.gsspec. 
+  rewrite dec_eq_true. apply repr_identify_1. auto.
 Qed.
 
 End IDENTIFY.
@@ -474,14 +486,22 @@ 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
+Definition F_pathlen (a: elt) (rec: forall b, order uf.(m) b a -> nat) : nat :=
+  match getlink uf.(m) a with
+  | inleft (exist a' P) => S (rec a' P)
+  | inright _ => O
   end.
+
+Definition pathlen (a: elt) : nat := Fix uf.(mwf) (fun _ => nat) F_pathlen a.
+
+Lemma pathlen_unroll:
+  forall a, pathlen a = match M.get a uf.(m) with Some a' => S(pathlen a') | None => O end.
 Proof.
-  intros. auto.
-  apply mwf. 
+  intros. unfold pathlen at 1. rewrite Fix_eq. 
+  unfold F_pathlen. destruct (getlink uf.(m) a) as [[a' P] | Q]. 
+  rewrite P; auto.
+  rewrite Q; auto.
+  intros. unfold F_pathlen. destruct (getlink (m uf) x) as [[a' P] | Q]; auto. 
 Qed.
 
 Lemma pathlen_none:
@@ -489,8 +509,7 @@ Lemma pathlen_none:
   M.get a uf.(m) = None ->
   pathlen a = 0.
 Proof.
-  intros.
-  functional induction (pathlen a). congruence. auto.
+  intros. rewrite pathlen_unroll. rewrite H; auto. 
 Qed.
 
 Lemma pathlen_some:
@@ -498,8 +517,7 @@ Lemma pathlen_some:
   M.get a uf.(m) = Some a' ->
   pathlen a = S (pathlen a').
 Proof.
-  intros.
-  functional induction (pathlen a). congruence. congruence.
+  intros. rewrite pathlen_unroll. rewrite H; auto.
 Qed.
 
 Lemma pathlen_zero:
@@ -507,9 +525,8 @@ Lemma pathlen_zero:
 Proof.
   intros; split; intros.
   apply pathlen_none. rewrite <- H. apply repr_res_none. 
-  functional induction (pathlen a).
-  congruence.
-  apply repr_none. auto.
+  apply repr_none. rewrite pathlen_unroll in H. 
+  destruct (M.get a (m uf)); congruence.
 Qed.
 
 End PATHLEN.
@@ -529,23 +546,19 @@ 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.
+  set (uf' := identify uf (repr uf a) b (repr_res_none uf a) (not_eq_sym n)).
+  pattern x. apply (well_founded_ind (mwf uf')); intros.
+  rewrite (pathlen_unroll uf'). destruct (M.get x0 (m uf')) as [x'|] eqn:G.
+  rewrite H; auto. simpl in G. rewrite M.gsspec in G. 
+  destruct (M.elt_eq x0 (repr uf a)). rewrite e. rewrite repr_canonical. rewrite dec_eq_true.
+  inversion G. subst x'. rewrite dec_eq_false; auto. 
+  replace (pathlen uf (repr uf a)) with 0. omega. 
+  symmetry. apply pathlen_none. apply repr_res_none. 
+  rewrite (repr_unroll uf x0), (pathlen_unroll uf x0); rewrite G.
+  destruct (M.elt_eq (repr uf x') (repr uf a)); omega. 
+  simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)); try discriminate.
+  rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto. 
+  symmetry. apply pathlen_zero; auto. apply repr_none; auto. 
 Qed.
 
 Lemma pathlen_gt_merge:
@@ -604,13 +617,16 @@ 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.
+  apply (well_founded_ind (mwf compress)); intros.
+  rewrite (repr_unroll compress).
+  destruct (M.get x (m compress)) as [y|] eqn:G.
+  rewrite H; auto. 
+  simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a). 
+  inversion G. subst x y. rewrite <- a_repr_b. apply repr_canonical.
+  symmetry; apply repr_some; auto.
+  simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x a). 
+  congruence.
+  symmetry; apply repr_none; auto.
 Qed.
 
 End COMPRESS.