New file FMapFullAVL containing the balancing proofs about FMapAVL:

As for FSetAVL vs. FSetFullAVL, preservation of the balancing of trees
is not necessary anymore for just fulfilling the Map interface. But we
still want theses proofs to exists somewhere, since they ensure the
correct efficiency of the FMapAVL operations.

In addition, FSetFullAVL also contains the non-structural,
ocaml-faithful version of compare.



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

1 files changed, 18 insertions, 18 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 31c3baca4..521fd13d8 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -536,6 +536,24 @@ end.
 
 Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo).
 
+(* Function/Functional Scheme can't deal with internal fix. 
+   Let's do its job by hand: *)
+
+Ltac join_tac := 
+ intros l; induction l as [| ll _ lx ld lr Hlr lh]; 
+   [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join;
+     [ | destruct (gt_le_dec lh (rh+2)); 
+       [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
+           replace (bal u v w z) 
+           with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
+         end 
+       | destruct (gt_le_dec rh (lh+2)); 
+         [ match goal with |- context [ bal ?u ?v ?w ?z ] => 
+             replace (bal u v w z) 
+             with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] 
+           end
+         | ] ] ] ]; intros.
+
 Section Elt.
 Variable elt:Type.
 Implicit Types m r : t elt.
@@ -1079,24 +1097,6 @@ Qed.
 
 (** * join *)
 
-(* Function/Functional Scheme can't deal with internal fix. 
-   Let's do its job by hand: *)
-
-Ltac join_tac := 
- intros l; induction l as [| ll _ lx ld lr Hlr lh]; 
-   [ | intros x d r; induction r as [| rl Hrl rx rd rr _ rh]; unfold join;
-     [ | destruct (gt_le_dec lh (rh+2)); 
-       [ match goal with |- context [ bal ?u ?v ?w ?z ] =>
-           replace (bal u v w z) 
-           with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
-         end 
-       | destruct (gt_le_dec rh (lh+2)); 
-         [ match goal with |- context [ bal ?u ?v ?w ?z ] => 
-             replace (bal u v w z) 
-             with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto] 
-           end
-         | ] ] ] ]; intros.
-
 Lemma join_in : forall l x d r y, 
  In y (join l x d r) <-> X.eq y x \/ In y l \/ In y r.
 Proof.