- notations &&& and ||| equivalent to andb and orb,

  but with lazy behavior while (vm_)computing
- FSetAVL.split has now a dedicated output type instead of ( ,( , ))
- Some proof adaptations.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10725 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 138 insertions, 143 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 686118e4b..9db151e32 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -684,7 +684,7 @@ Proof.
   destruct b; intuition.
 Qed.
 
-(* Rewrite rules about andb, orb and if (used in romega) *)
+(** Rewrite rules about andb, orb and if (used in romega) *)
 
 Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool), 
   (if b && b' then a else a') = 
@@ -700,7 +700,28 @@ Proof.
  destruct b; auto.
 Qed.
 
-(* Compatibility *)
+(*****************************************)
+(** * Alternative versions of [andb] and [orb] 
+    with lazy behavior (for vm_compute)  *)
+(*****************************************)
+
+Notation "a &&& b" := (if a then b else false) 
+ (at level 40, left associativity) : bool_scope.
+Notation "a ||| b" := (if a then true else b)
+ (at level 50, left associativity) : bool_scope.
+
+Lemma andb_lazy_alt : forall a b : bool, a && b = a &&& b.
+Proof.
+ unfold andb; auto.
+Qed.
+
+Lemma orb_lazy_alt : forall a b : bool, a || b = a ||| b.
+Proof.
+ unfold orb; auto.
+Qed.
+
+
+(** Compatibility *)
 
 Notation andb := Datatypes.andb (only parsing).
 Notation orb := Datatypes.orb (only parsing).
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 442d18b57..e55478494 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -42,21 +42,21 @@ Require Import FSetInterface FSetList ZArith Int.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Raw (Import I:Int)(X:OrderedType).
-Open Local Scope Int_scope.
-
-Definition elt := X.t.
-
-(** Workaround to get lazy andb and orb operations with vm_computation *)
+(** Notations and helper lemma about pairs *)
 
-Notation "a &&& b" := (if a then b else false) (at level 40, left associativity) : bool_scope.
-Notation "a ||| b" := (if a then true else b) (at level 50, left associativity) : bool_scope.
+Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
+Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
 
-(** Notations and helper lemma about pairs *)
+(** * Raw 
+   
+   Functor of pure functions + a posteriori proofs of invariant 
+   preservation *)
 
-Notation "s #1" := (fst s) (at level 9, format "s '#1'").
-Notation "s #2" := (snd s) (at level 9, format "s '#2'").
+Module Raw (Import I:Int)(X:OrderedType).
+Open Local Scope pair_scope.
+Open Local Scope Int_scope.
 
+Definition elt := X.t.
 
 (** * Trees
 
@@ -123,7 +123,7 @@ Definition create l x r :=
 
 Definition assert_false := create.
 
-Fixpoint bal l x r := 
+Definition bal l x r := 
   let hl := height l in 
   let hr := height r in
   if gt_le_dec hl (hr+2) then 
@@ -208,7 +208,7 @@ Fixpoint remove_min l x r : t*elt :=
   [|height t1 - height t2| <= 2].
 *)
 
-Fixpoint merge s1 s2 :=  match s1,s2 with 
+Definition merge s1 s2 :=  match s1,s2 with 
   | Leaf, _ => s2 
   | _, Leaf => s1
   | _, Node l2 x2 r2 h2 => 
@@ -252,11 +252,11 @@ Definition choose := min_elt.
     Same as [merge] but does not assume anything about heights.
 *)
 
-Fixpoint concat s1 s2 := 
+Definition concat s1 s2 := 
    match s1, s2 with 
       | Leaf, _ => s2 
       | _, Leaf => s1
-      | _, Node l2 x2 r2 h2 => 
+      | _, Node l2 x2 r2 _ => 
             let (s2',m) := remove_min l2 x2 r2 in 
             join s1 m s2'
    end.
@@ -269,17 +269,19 @@ Fixpoint concat s1 s2 :=
     - [present] is [true] if and only if [s] contains  [x].
 *)
 
-Fixpoint split x s : t * (bool * t) := match s with 
-  | Leaf => (Leaf, (false, Leaf))
+Record triple := mktriple { t_left:t; t_in:bool; t_right:t }.
+Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
+Notation "t #l" := (t_left t) (at level 9, format "t '#l'").
+Notation "t #b" := (t_in t) (at level 9, format "t '#b'").
+Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
+
+Fixpoint split x s : triple := match s with
+  | Leaf => << Leaf, false, Leaf >>
   | Node l y r h => 
      match X.compare x y with 
-      | LT _ => match split x l with 
-                 | (ll,(pres,rl)) => (ll, (pres, join rl y r))
-                end
-      | EQ _ => (l, (true, r))
-      | GT _ => match split x r with 
-                 | (rl,(pres,rr)) => (join l y rl, (pres, rr))
-                end
+      | LT _ => let (ll,b,rl) := split x l in << ll, b, join rl y r >>
+      | EQ _ => << l, true, r >>
+      | GT _ => let (rl,b,rr) := split x r in << join l y rl, b, rr >>
      end
  end.
 
@@ -288,11 +290,10 @@ Fixpoint split x s : t * (bool * t) := match s with
 Fixpoint inter s1 s2 := match s1, s2 with 
     | Leaf, _ => Leaf
     | _, Leaf => Leaf
-    | Node l1 x1 r1 h1, Node l2 x2 r2 h2 => 
-            match split x1 s2 with
-               | (l2',(true,r2')) => join (inter l1 l2') x1 (inter r1 r2')
-               | (l2',(false,r2')) => concat (inter l1 l2') (inter r1 r2')
-            end
+    | Node l1 x1 r1 h1, _ => 
+            let (l2',pres,r2') := split x1 s2 in 
+            if pres then join (inter l1 l2') x1 (inter r1 r2')
+            else concat (inter l1 l2') (inter r1 r2')
     end.
 
 (** * Difference *)
@@ -300,11 +301,10 @@ Fixpoint inter s1 s2 := match s1, s2 with
 Fixpoint diff s1 s2 := match s1, s2 with 
  | Leaf, _ => Leaf
  | _, Leaf => s1
- | Node l1 x1 r1 h1, Node l2 x2 r2 h2 => 
-    match split x1 s2 with 
-      | (l2',(true,r2')) => concat (diff l1 l2') (diff r1 r2')
-      | (l2',(false,r2')) => join (diff l1 l2') x1 (diff r1 r2')
-    end
+ | Node l1 x1 r1 h1, _ => 
+    let (l2',pres,r2') := split x1 s2 in 
+    if pres then concat (diff l1 l2') (diff r1 r2')
+    else join (diff l1 l2') x1 (diff r1 r2')
 end.
 
 (** * Union *)
@@ -323,10 +323,10 @@ end.
 Fixpoint union s1 s2 := 
  match s1, s2 with 
   | Leaf, _ => s2
-  | Node _ _ _ _, Leaf => s1
-  | Node l1 x1 r1 h1, Node l2 x2 r2 h2 => 
-     let (l2',r2') := split x1 s2 in 
-     join (union l1 l2') x1 (union r1 r2'#2)
+  | _, Leaf => s1
+  | Node l1 x1 r1 h1, _ => 
+     let (l2',_,r2') := split x1 s2 in 
+     join (union l1 l2') x1 (union r1 r2')
  end.
 
 (** * Elements *)
@@ -547,24 +547,6 @@ Module Proofs.
  Module MX := OrderedTypeFacts X.
  Module L := FSetList.Raw X.
 
-(** * Helper lemma about [orb], [andb], [pair] *)
-
-Lemma andb_alt : forall a b : bool, a &&& b = a && b.
-Proof.
- destruct a; simpl; auto.
-Qed.
-
-Lemma orb_alt : forall a b : bool, a ||| b = a || b.
-Proof.
- destruct a; simpl; auto.
-Qed.
-
-Lemma distr_pair : forall (A B:Type)(s:A*B)(a:A)(b:B), s = (a,b) -> 
- s#1 = a /\ s#2 = b.
-Proof.
- destruct s; simpl; injection 1; auto.
-Qed.
-
 (** * Automation and dedicated tactics *)
 
 Hint Constructors In bst.
@@ -1067,7 +1049,7 @@ Proof.
  rewrite join_in, remove_min_in, e1; simpl; intuition.
 Qed.
  
-Lemma concat_bst :   forall s1 s2, bst s1 -> bst s2 -> 
+Lemma concat_bst : forall s1 s2, bst s1 -> bst s2 -> 
  (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> 
  bst (concat s1 s2).
 Proof. 
@@ -1086,42 +1068,42 @@ Hint Resolve concat_bst.
 (** * Splitting *)
 
 Lemma split_in_1 : forall s x y, bst s -> 
- (In y (split x s)#1 <-> In y s /\ X.lt y x).
+ (In y (split x s)#l <-> In y s /\ X.lt y x).
 Proof.
  intros s x; functional induction (split x s); simpl; intros; 
   inv bst; try clear e0.
  intuition_in.
- rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
  intuition_in; order.
  rewrite join_in.
- rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
 Qed.
 
 Lemma split_in_2 : forall s x y, bst s -> 
- (In y (split x s)#2#2 <-> In y s /\ X.lt x y).
+ (In y (split x s)#r <-> In y s /\ X.lt x y).
 Proof. 
  intros s x; functional induction (split x s); subst; simpl; intros; 
   inv bst; try clear e0.
  intuition_in.
  rewrite join_in.
- rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
  intuition_in; order.
- rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
 Qed.
 
 Lemma split_in_3 : forall s x, bst s -> 
- ((split x s)#2#1 = true <-> In x s).
+ ((split x s)#b = true <-> In x s).
 Proof. 
  intros s x; functional induction (split x s); subst; simpl; intros; 
   inv bst; try clear e0.
  intuition_in; try discriminate.
- rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
  intuition.
- rewrite e1 in IHp; simpl in IHp; rewrite IHp; intuition_in; order.
+ rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order.
 Qed.
 
 Lemma split_bst : forall s x, bst s -> 
- bst (split x s)#1 /\ bst (split x s)#2#2.
+ bst (split x s)#l /\ bst (split x s)#r.
 Proof. 
  intros s x; functional induction (split x s); subst; simpl; intros; 
   inv bst; try clear e0; try rewrite e1 in *; simpl in *; intuition;
@@ -1143,26 +1125,23 @@ Proof.
  [intuition_in|intuition_in | | ]; 
  factornode _x0 _x1 _x2 _x3 as s2; 
  generalize (split_bst x1 B2); 
-  rewrite e1; simpl; destruct 1; inv bst; 
+  rewrite e1; simpl; destruct 1; inv bst;
  destruct IHt as (IHb1,IHi1); auto; 
- destruct IHt0 as (IHb2,IHi2); auto; 
- destruct (distr_pair e1); clear e1;
- destruct (distr_pair H6); clear H6; split.
+ destruct IHt0 as (IHb2,IHi2); auto;
+ generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1)
+  (split_in_3 x1 B2)(split_bst x1 B2);
+ rewrite e1; simpl; split; intros.
  (* bst join *)
- apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition.
- (* In join *)
- intros.
- rewrite join_in, IHi1, IHi2, <- H5, <- H8, split_in_1, split_in_2; auto.
- rewrite split_in_3 in H7; intuition_in.
+ apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *)
+ rewrite join_in, IHi1, IHi2, H5, H6; intuition_in.
  apply In_1 with x1; auto.
  (* bst concat *)
  apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  (* In concat *)
- intros.
- rewrite concat_in, IHi1, IHi2, <- H5, <- H8, split_in_1, split_in_2; auto.
- assert (~In x1 s2) by (rewrite <- split_in_3, H7; auto).
+ rewrite concat_in, IHi1, IHi2, H5, H6; auto.
+ assert (~In x1 s2) by (rewrite <- H7; auto).
  intuition_in.
- elim H6.
+ elim H9.
  apply In_1 with y; auto.
 Qed.
 
@@ -1191,24 +1170,21 @@ Proof.
  inv avl; inv bst; 
  destruct IHt as (IHb1,IHi1); auto; 
  destruct IHt0 as (IHb2,IHi2); auto; 
- destruct (distr_pair e1); clear e1; 
- destruct (distr_pair H6); clear H6; split.
+ generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1)
+  (split_in_3 x1 B2)(split_bst x1 B2);
+ rewrite e1; simpl; split; intros.
  (* bst concat *)
  apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  (* In concat *)
- intros.
- rewrite concat_in, IHi1, IHi2, <-H5, <- H8, split_in_1, split_in_2; auto.
- rewrite split_in_3 in H7; intuition_in.
- elim H10.
+ rewrite concat_in, IHi1, IHi2, H5, H6; intuition_in.
+ elim H13.
  apply In_1 with x1; auto.
  (* bst join *)
- apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition.
- (* In join *)
- intros.
- rewrite join_in, IHi1, IHi2, <-H5, <-H8, split_in_1, split_in_2; auto.
- assert (~In x1 s2) by (rewrite <- split_in_3, H7; auto).
+ apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *)
+ rewrite join_in, IHi1, IHi2, H5, H6; auto.
+ assert (~In x1 s2) by (rewrite <- H7; auto).
  intuition_in.
- elim H6.
+ elim H9.
  apply In_1 with y; auto.
 Qed.
 
@@ -1232,11 +1208,11 @@ Proof.
  intros s1 s2; functional induction union s1 s2; intros y B1 B2.
  intuition_in.
  intuition_in.
- generalize (split_bst x1 B2) (split_in_1 x1 y B2) (split_in_2 x1 y B2).
+ factornode _x0 _x1 _x2 _x3 as s2.
+ generalize (split_in_1 x1 y B2)(split_in_2 x1 y B2)(split_bst x1 B2).
  rewrite e1; simpl.
- destruct 1; inv bst.
- rewrite join_in, IHt, IHt0; auto.
- do 2 (intro Eq; rewrite Eq; clear Eq).
+ destruct 3; inv bst.
+ rewrite join_in, IHt, IHt0, H, H0; auto.
  case (X.compare y x1); intuition_in.
 Qed.
 
@@ -1244,15 +1220,13 @@ Lemma union_bst : forall s1 s2, bst s1 -> bst s2 ->
  bst (union s1 s2).
 Proof.
  intros s1 s2; functional induction union s1 s2; intros B1 B2; auto.
- generalize (split_bst x1 B2) .
+ factornode _x0 _x1 _x2 _x3 as s2.
+ generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1)(split_bst x1 B2).
+ rewrite e1; simpl; destruct 3.
  inv bst.
- rewrite e1; simpl; destruct 1.
- destruct (distr_pair e1) as (L,R); clear e1.
  apply join_bst; auto.
- intro y; rewrite union_in; auto; simpl.
- rewrite <- L, split_in_1; auto; intuition_in.
- intro y; rewrite union_in; auto; simpl.
- rewrite <- R, split_in_2; auto; intuition_in.
+ intro y; rewrite union_in, H; intuition_in.
+ intro y; rewrite union_in, H0; intuition_in.
 Qed.
 
 
@@ -1492,7 +1466,7 @@ Qed.
 Lemma exists_1 : forall s, compat_bool X.eq f ->
  Exists (fun x => f x = true) s -> exists_ f s = true.
 Proof.
- induction s; simpl; destruct 2 as (x,(U,V)); inv In; rewrite ? orb_alt.
+ induction s; simpl; destruct 2 as (x,(U,V)); inv In; rewrite <- ?orb_lazy_alt.
  rewrite (H _ _ (X.eq_sym H0)); rewrite V; auto.
  apply orb_true_intro; left.
  apply orb_true_intro; right; apply IHs1; auto; exists x; auto.
@@ -1502,7 +1476,7 @@ Qed.
 Lemma exists_2 : forall s, compat_bool X.eq f ->
  exists_ f s = true -> Exists (fun x => f x = true) s.
 Proof. 
- induction s; simpl; intros; rewrite ? orb_alt in *.
+ induction s; simpl; intros; rewrite <- ?orb_lazy_alt in *.
  discriminate.
  destruct (orb_true_elim _ _ H0) as [H1|H1]. 
  destruct (orb_true_elim _ _ H1) as [H2|H2].
@@ -1582,7 +1556,7 @@ Proof.
  assert (X.eq a x2) by order; intuition_in.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
 
- rewrite andb_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2.
+ rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2.
  unfold Subset. intuition_in.
  assert (H':=mem_2 H6); apply In_1 with x1; auto.
  apply mem_1; auto.
@@ -1604,7 +1578,7 @@ Proof.
  inv bst. clear H7.
  destruct X.compare.
 
- rewrite andb_alt, andb_true_iff, H1 by auto;  clear H1 IHl2 IHr2.
+ rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto;  clear H1 IHl2 IHr2.
  unfold Subset. intuition_in.
  assert (H':=mem_2 H1); apply In_1 with x1; auto.
  apply mem_1; auto.
@@ -1633,21 +1607,21 @@ Proof.
  inv bst.
  destruct X.compare.
 
- rewrite andb_alt, andb_true_iff, IHr1 by auto.
+ rewrite <-andb_lazy_alt, andb_true_iff, IHr1 by auto.
  rewrite (@subsetl_12 (subset l1) l1 x1 h1) by auto.
  clear IHl1 IHr1.
  unfold Subset; intuition_in.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
 
- rewrite andb_alt, andb_true_iff, IHl1, IHr1 by auto.
+ rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto.
  clear IHl1 IHr1.
  unfold Subset; intuition_in.
  assert (X.eq a x2) by order; intuition_in.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
  assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order.
  
- rewrite andb_alt, andb_true_iff, IHl1 by auto.
+ rewrite <-andb_lazy_alt, andb_true_iff, IHl1 by auto.
  rewrite (@subsetr_12 (subset r1) r1 x1 h1) by auto.
  clear IHl1 IHr1.
  unfold Subset; intuition_in.
diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v
index a5066aae0..5f04e73c6 100644
--- a/theories/FSets/FSetFullAVL.v
+++ b/theories/FSets/FSetFullAVL.v
@@ -39,6 +39,7 @@ Module AvlProofs (Import I:Int)(X:OrderedType).
 Module Import Raw := Raw I X.
 Import Raw.Proofs.
 Module Import II := MoreInt I.
+Open Local Scope pair_scope.
 Open Local Scope Int_scope.
 
 (** * AVL trees *)
@@ -358,12 +359,12 @@ Hint Resolve concat_avl.
 (** split *)
 
 Lemma split_avl : forall s x, avl s -> 
-  avl (split x s)#1 /\ avl (split x s)#2#2.
+  avl (split x s)#l /\ avl (split x s)#r.
 Proof. 
  intros s x; functional induction (split x s); simpl; auto.
- rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition.
+ rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
  simpl; inversion_clear 1; auto.
- rewrite e1 in IHp;simpl in IHp;inversion_clear 1; intuition.
+ rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
 Qed.
 
 (** inter *)
@@ -454,6 +455,7 @@ Module Import AvlProofs := AvlProofs I X.
 Import Raw.
 Import Raw.Proofs.
 Import II.
+Open Local Scope pair_scope.
 Open Local Scope nat_scope.
 
 (** Properties of cardinal *)
@@ -489,24 +491,24 @@ Proof.
 Qed.
 
 Lemma split_cardinal_1 : forall x s, 
- (cardinal (split x s)#1 <= cardinal s)%nat.
+ (cardinal (split x s)#l <= cardinal s)%nat.
 Proof.
  intros x s; functional induction split x s; simpl; auto.
- rewrite e1 in IHp; simpl in *.
+ rewrite e1 in IHt; simpl in *.
  romega with *.
  romega with *.
- rewrite e1 in IHp; simpl in *.
+ rewrite e1 in IHt; simpl in *.
  generalize (@join_cardinal l y rl); romega with *.
 Qed.
 
 Lemma split_cardinal_2 : forall x s, 
- (cardinal (split x s)#2#2 <= cardinal s)%nat.
+ (cardinal (split x s)#r <= cardinal s)%nat.
 Proof.
  intros x s; functional induction split x s; simpl; auto.
- rewrite e1 in IHp; simpl in *.
+ rewrite e1 in IHt; simpl in *.
  generalize (@join_cardinal rl y r); romega with *.
  romega with *.
- rewrite e1 in IHp; simpl in *; romega with *.
+ rewrite e1 in IHt; simpl in *; romega with *.
 Qed.
 
 (** * [ocaml_union], an union faithful to the original ocaml code *)
@@ -530,12 +532,12 @@ Function ocaml_union (s : t * t) { measure cardinal2 s } : t  :=
   | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) => 
         if ge_lt_dec h1 h2 then
           if eq_dec h2 1%I then add x2 s#1 else
-          let (l2',r2') := split x1 s#2 in 
-             join (ocaml_union (l1,l2')) x1 (ocaml_union (r1,r2'#2))
+          let (l2',_,r2') := split x1 s#2 in 
+             join (ocaml_union (l1,l2')) x1 (ocaml_union (r1,r2'))
         else
           if eq_dec h1 1%I then add x1 s#2 else
-          let (l1',r1') := split x2 s#1 in 
-             join (ocaml_union (l1',l2)) x2 (ocaml_union (r1'#2,r2))
+          let (l1',_,r1') := split x2 s#1 in 
+             join (ocaml_union (l1',l2)) x2 (ocaml_union (r1',r2))
  end.
 Proof.
 abstract ocaml_union_tac.
@@ -558,7 +560,7 @@ Proof.
  rewrite (height_0 H); [ | avl_nn l2; omega_max].
  rewrite (height_0 H0); [ | avl_nn r2; omega_max].
  rewrite add_in; intuition_in.
- (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *)
+ (* join (union (l1,l2')) x1 (union (r1,r2')) *)
  generalize
   (split_avl x1 A2) (split_bst x1 B2)
   (split_in_1 x1 y B2) (split_in_2 x1 y B2).
@@ -572,7 +574,7 @@ Proof.
  rewrite (height_0 H3); [ | avl_nn l1; omega_max].
  rewrite (height_0 H4); [ | avl_nn r1; omega_max].
  rewrite add_in; auto; intuition_in.
- (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *)
+ (* join (union (l1',l2)) x1 (union (r1',r2)) *)
  generalize 
   (split_avl x2 A1) (split_bst x2 B1)
   (split_in_1 x2 y B1) (split_in_2 x2 y B1).
@@ -589,28 +591,26 @@ Proof.
  intros s; functional induction ocaml_union s; intros B1 A1 B2 A2;
   simpl fst in *; simpl snd in *; try clear e0 e1; 
   try apply add_bst; auto.
- (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *)
- generalize (split_avl x1 A2) (split_bst x1 B2).
+ (* join (union (l1,l2')) x1 (union (r1,r2')) *)
+ clear _x _x0; factornode l2 x2 r2 h2 as s2.
+ generalize (split_avl x1 A2) (split_bst x1 B2)
+  (@split_in_1 s2 x1)(@split_in_2 s2 x1).
  rewrite e2; simpl.
- destruct 1; destruct 1.
- destruct (distr_pair e2) as (L,R); clear e2.
+ destruct 1; destruct 1; intros.
  inv bst; inv avl.
  apply join_bst; auto.
- intro y; rewrite ocaml_union_in; auto; simpl.
- rewrite <- L, split_in_1; auto; intuition_in.
- intro y; rewrite ocaml_union_in; auto; simpl.
- rewrite <- R, split_in_2; auto; intuition_in.
- (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *)
- generalize (split_avl x2 A1) (split_bst x2 B1).
+ intro y; rewrite ocaml_union_in, H3; intuition_in.
+ intro y; rewrite ocaml_union_in, H4; intuition_in.
+ (* join (union (l1',l2)) x1 (union (r1',r2)) *)
+ clear _x _x0; factornode l1 x1 r1 h1 as s1.
+ generalize (split_avl x2 A1) (split_bst x2 B1)
+  (@split_in_1 s1 x2)(@split_in_2 s1 x2).
  rewrite e2; simpl.
- destruct 1; destruct 1.
- destruct (distr_pair e2) as (L,R); clear e2.
+ destruct 1; destruct 1; intros.
  inv bst; inv avl.
  apply join_bst; auto.
- intro y; rewrite ocaml_union_in; auto; simpl.
- rewrite <- L, split_in_1; auto; intuition_in.
- intro y; rewrite ocaml_union_in; auto; simpl.
- rewrite <- R, split_in_2; auto; intuition_in.
+ intro y; rewrite ocaml_union_in, H3; intuition_in.
+ intro y; rewrite ocaml_union_in, H4; intuition_in.
 Qed.
 
 Lemma ocaml_union_avl : forall s,