Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Finite map library.  *)

FMapFullAVL

This file contains some complements to FMapAVL.

Functor AvlProofs proves that trees of FMapAVL are not only

binary search trees, but moreover well-balanced ones. This is done by proving that all operations preserve the balancing.

We then pack the previous elements in a IntMake functor

similar to the one of FMapAVL, but richer.

In final IntMake_ord functor, the compare function is

different from the one in FMapAVL: this non-structural version is closer to the original Ocaml code.

Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia.

Set Implicit Arguments.
Unset Strict Implicit.

Module AvlProofs (Import I:Int)(X: OrderedType).
Module Import Raw := Raw I X.
Module Import II:=MoreInt(I).
Import Raw.Proofs.
Local Open Scope pair_scope.
Local Open Scope Int_scope.

Ltac omega_max := i2z_refl; lia.

Section Elt.
Variable elt : Type.
Implicit Types m r : t elt.

AVL trees

avl s : s is a properly balanced AVL tree, i.e. for any node the heights of the two children differ by at most 2

Inductive avl : t elt -> Prop :=
  | RBLeaf : avl (Leaf _)
  | RBNode : forall x e l r h,
      avl l ->
      avl r ->
      -(2) <= height l - height r <= 2 ->
      h = max (height l) (height r) + 1 ->
      avl (Node l x e r h).

Automation and dedicated tactics about avl.

Hint Constructors avl : core.

Lemma height_non_negative : forall (s : t elt), avl s ->
 height s >= 0.elt:Type
forall s : t elt, avl s -> height s >= 0
Proof.elt:Type
forall s : t elt, avl s -> height s >= 0
 induction s; simpl; intros; auto with zarith.elt:Type
s1:Raw.t elt
k:key
e:elt
s2:Raw.t elt
t:I.t
IHs1:avl s1 -> height s1 >= 0
IHs2:avl s2 -> height s2 >= 0
H:avl (Node s1 k e s2 t)
t >= 0
 inv avl; intuition; omega_max.
Qed.

Ltac avl_nn_hyp H :=
     let nz := fresh "nz" in assert (nz := height_non_negative H).

Ltac avl_nn h :=
  let t := type of h in
  match type of t with
   | Prop => avl_nn_hyp h
   | _ => match goal with H : avl h |- _ => avl_nn_hyp H end
  end.

(* Repeat the previous tactic.
   Drawback: need to clear the [avl _] hyps ... Thank you Ltac *)

Ltac avl_nns :=
  match goal with
     | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns
     | _ => idtac
  end.

Basic results about avl, height

Lemma avl_node : forall x e l r, avl l -> avl r ->
 -(2) <= height l - height r <= 2 ->
 avl (Node l x e r (max (height l) (height r) + 1)).elt:Type
forall (x : key) (e : elt) (l r : t elt),
avl l ->
avl r ->
- (2) <= height l - height r <= 2 ->
avl (Node l x e r (max (height l) (height r) + 1))
Proof.elt:Type
forall (x : key) (e : elt) (l r : t elt),
avl l ->
avl r ->
- (2) <= height l - height r <= 2 ->
avl (Node l x e r (max (height l) (height r) + 1))
  intros; auto.
Qed.
Hint Resolve avl_node : core.

Results about height

Lemma height_0 : forall l, avl l -> height l = 0 ->
 l = Leaf _.elt:Type
forall l : t elt,
avl l -> height l = 0 -> l = Leaf elt
Proof.elt:Type
forall l : t elt,
avl l -> height l = 0 -> l = Leaf elt
 destruct 1; intuition; simpl in *.elt:Type
x:key
e:elt
l, r:t elt
h:I.t
H:avl l
H0:avl r
H2:h = max (height l) (height r) + 1
H3:h = 0
H4:- (2) <= height l - height r
H5:height l - height r <= 2
Node l x e r h = Leaf elt
 avl_nns; simpl in *; exfalso; omega_max.
Qed.

Empty map

Lemma empty_avl : avl (empty elt).elt:Type
avl (empty elt)
Proof.elt:Type
avl (empty elt)
 unfold empty; auto.
Qed.

Helper functions

Lemma create_avl :
 forall l x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 ->
 avl (create l x e r).elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (2) <= height l - height r <= 2 ->
avl (create l x e r)
Proof.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (2) <= height l - height r <= 2 ->
avl (create l x e r)
 unfold create; auto.
Qed.

Lemma create_height :
 forall l x e r, avl l -> avl r ->  -(2) <= height l - height r <= 2 ->
 height (create l x e r) = max (height l) (height r) + 1.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (2) <= height l - height r <= 2 ->
height (create l x e r) =
max (height l) (height r) + 1
Proof.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (2) <= height l - height r <= 2 ->
height (create l x e r) =
max (height l) (height r) + 1
 unfold create; intros; auto.
Qed.

Lemma bal_avl : forall l x e r, avl l -> avl r ->
 -(3) <= height l - height r <= 3 -> avl (bal l x e r).elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (3) <= height l - height r <= 3 -> avl (bal l x e r)
Proof.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (3) <= height l - height r <= 3 -> avl (bal l x e r)
 intros l x e r; functional induction (bal l x e r); intros; clearf;
 inv avl; simpl in *;
 match goal with |- avl (assert_false _ _ _ _) => avl_nns
  | _ => repeat apply create_avl; simpl in *; auto
 end; omega_max.
Qed.

Lemma bal_height_1 : forall l x e r, avl l -> avl r ->
 -(3) <= height l - height r <= 3 ->
 0 <= height (bal l x e r) - max (height l) (height r) <= 1.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (3) <= height l - height r <= 3 ->
0 <=
height (bal l x e r) - max (height l) (height r) <= 1
Proof.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (3) <= height l - height r <= 3 ->
0 <=
height (bal l x e r) - max (height l) (height r) <= 1
 intros l x e r; functional induction (bal l x e r); intros; clearf;
 inv avl; avl_nns; simpl in *; omega_max.
Qed.

Lemma bal_height_2 :
 forall l x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 ->
 height (bal l x e r) == max (height l) (height r) +1.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (2) <= height l - height r <= 2 ->
height (bal l x e r) == max (height l) (height r) + 1
Proof.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt),
avl l ->
avl r ->
- (2) <= height l - height r <= 2 ->
height (bal l x e r) == max (height l) (height r) + 1
 intros l x e r; functional induction (bal l x e r); intros; clearf;
 inv avl; avl_nns; simpl in *; omega_max.
Qed.

Ltac omega_bal := match goal with
  | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?e ?r ] =>
     generalize (bal_height_1 x e H H') (bal_height_2 x e H H');
     omega_max
  end.

Insertion

Lemma add_avl_1 :  forall m x e, avl m ->
 avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1.elt:Type
forall (m : t elt) (x : key) (e : elt),
avl m ->
avl (add x e m) /\
0 <= height (add x e m) - height m <= 1
Proof.elt:Type
forall (m : t elt) (x : key) (e : elt),
avl m ->
avl (add x e m) /\
0 <= height (add x e m) - height m <= 1
 intros m x e; functional induction (add x e m); intros; inv avl; simpl in *.elt:Type
x:key
e:elt
avl (Node (Leaf elt) x e (Leaf elt) 1) /\
0 <= 1 - 0 <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt x y
e1:X.compare x y = LT _x
IHt:avl l -> avl (add x e l) /\ 0 <= height (add x e l) - height l <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (bal (add x e l) y d' r) /\
0 <= height (bal (add x e l) y d' r) - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.eq x y
e1:X.compare x y = EQ _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (Node l y e r h) /\ 0 <= h - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
IHt:avl r -> avl (add x e r) /\ 0 <= height (add x e r) - height r <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (bal l y d' (add x e r)) /\
0 <= height (bal l y d' (add x e r)) - h <= 1
 intuition; try constructor; simpl; auto; try omega_max.elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt x y
e1:X.compare x y = LT _x
IHt:avl l -> avl (add x e l) /\ 0 <= height (add x e l) - height l <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (bal (add x e l) y d' r) /\
0 <= height (bal (add x e l) y d' r) - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.eq x y
e1:X.compare x y = EQ _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (Node l y e r h) /\ 0 <= h - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
IHt:avl r -> avl (add x e r) /\ 0 <= height (add x e r) - height r <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (bal l y d' (add x e r)) /\
0 <= height (bal l y d' (add x e r)) - h <= 1
 (* LT *)
 destruct IHt; auto.elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt x y
e1:X.compare x y = LT _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
H:avl (add x e l)
H4:0 <= height (add x e l) - height l <= 1
avl (bal (add x e l) y d' r) /\
0 <= height (bal (add x e l) y d' r) - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.eq x y
e1:X.compare x y = EQ _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (Node l y e r h) /\ 0 <= h - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
IHt:avl r -> avl (add x e r) /\ 0 <= height (add x e r) - height r <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (bal l y d' (add x e r)) /\
0 <= height (bal l y d' (add x e r)) - h <= 1
 split.elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt x y
e1:X.compare x y = LT _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
H:avl (add x e l)
H4:0 <= height (add x e l) - height l <= 1
avl (bal (add x e l) y d' r)
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt x y
e1:X.compare x y = LT _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
H:avl (add x e l)
H4:0 <= height (add x e l) - height l <= 1
0 <= height (bal (add x e l) y d' r) - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.eq x y
e1:X.compare x y = EQ _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (Node l y e r h) /\ 0 <= h - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
IHt:avl r -> avl (add x e r) /\ 0 <= height (add x e r) - height r <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (bal l y d' (add x e r)) /\
0 <= height (bal l y d' (add x e r)) - h <= 1
 apply bal_avl; auto; omega_max.elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt x y
e1:X.compare x y = LT _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
H:avl (add x e l)
H4:0 <= height (add x e l) - height l <= 1
0 <= height (bal (add x e l) y d' r) - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.eq x y
e1:X.compare x y = EQ _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (Node l y e r h) /\ 0 <= h - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
IHt:avl r -> avl (add x e r) /\ 0 <= height (add x e r) - height r <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (bal l y d' (add x e r)) /\
0 <= height (bal l y d' (add x e r)) - h <= 1
 omega_bal.elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.eq x y
e1:X.compare x y = EQ _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (Node l y e r h) /\ 0 <= h - h <= 1
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
IHt:avl r -> avl (add x e r) /\ 0 <= height (add x e r) - height r <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (bal l y d' (add x e r)) /\
0 <= height (bal l y d' (add x e r)) - h <= 1
 (* EQ *)
 intuition; omega_max.elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
IHt:avl r -> avl (add x e r) /\ 0 <= height (add x e r) - height r <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
avl (bal l y d' (add x e r)) /\
0 <= height (bal l y d' (add x e r)) - h <= 1
 (* GT *)
 destruct IHt; auto.elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
H:avl (add x e r)
H4:0 <= height (add x e r) - height r <= 1
avl (bal l y d' (add x e r)) /\
0 <= height (bal l y d' (add x e r)) - h <= 1
 split.elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
H:avl (add x e r)
H4:0 <= height (add x e r) - height r <= 1
avl (bal l y d' (add x e r))
elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
H:avl (add x e r)
H4:0 <= height (add x e r) - height r <= 1
0 <= height (bal l y d' (add x e r)) - h <= 1
 apply bal_avl; auto; omega_max.elt:Type
x:key
e:elt
l:t elt
y:key
d':elt
r:t elt
h:I.t
_x:X.lt y x
e1:X.compare x y = GT _x
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:h = max (height l) (height r) + 1
H:avl (add x e r)
H4:0 <= height (add x e r) - height r <= 1
0 <= height (bal l y d' (add x e r)) - h <= 1
 omega_bal.
Qed.

Lemma add_avl : forall m x e, avl m -> avl (add x e m).elt:Type
forall (m : t elt) (x : key) (e : elt),
avl m -> avl (add x e m)
Proof.elt:Type
forall (m : t elt) (x : key) (e : elt),
avl m -> avl (add x e m)
 intros; generalize (add_avl_1 x e H); intuition.
Qed.
Hint Resolve add_avl : core.

Extraction of minimum binding

Lemma remove_min_avl_1 : forall l x e r h, avl (Node l x e r h) ->
 avl (remove_min l x e r)#1 /\
 0 <= height (Node l x e r h) - height (remove_min l x e r)#1 <= 1.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt)
  (h : I.t),
avl (Node l x e r h) ->
avl (remove_min l x e r)#1 /\
0 <=
height (Node l x e r h) -
height (remove_min l x e r)#1 <= 1
Proof.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt)
  (h : I.t),
avl (Node l x e r h) ->
avl (remove_min l x e r)#1 /\
0 <=
height (Node l x e r h) -
height (remove_min l x e r)#1 <= 1
 intros l x e r; functional induction (remove_min l x e r); simpl in *; intros.elt:Type
x:key
d:elt
r:t elt
h:I.t
H:avl (Node (Leaf elt) x d r h)
avl r /\ 0 <= h - height r <= 1
elt:Type
x:key
d:elt
r, ll:t elt
lx:key
ld:elt
lr:t elt
_x:I.t
l':t elt
m:(key * elt)%type
e0:remove_min ll lx ld lr = (l', m)
IHp:forall h0 : I.t,
avl (Node ll lx ld lr h0) ->
avl (remove_min ll lx ld lr)#1 /\
0 <= h0 - height (remove_min ll lx ld lr)#1 <= 1
h:I.t
H:avl (Node (Node ll lx ld lr _x) x d r h)
avl (bal l' x d r) /\
0 <= h - height (bal l' x d r) <= 1
 inv avl; simpl in *; split; auto.elt:Type
x:key
d:elt
r:t elt
h:I.t
H1:avl r
H2:- (2) <= 0 - height r <= 2
H3:h = max 0 (height r) + 1
0 <= h - height r <= 1
elt:Type
x:key
d:elt
r, ll:t elt
lx:key
ld:elt
lr:t elt
_x:I.t
l':t elt
m:(key * elt)%type
e0:remove_min ll lx ld lr = (l', m)
IHp:forall h0 : I.t,
avl (Node ll lx ld lr h0) ->
avl (remove_min ll lx ld lr)#1 /\
0 <= h0 - height (remove_min ll lx ld lr)#1 <= 1
h:I.t
H:avl (Node (Node ll lx ld lr _x) x d r h)
avl (bal l' x d r) /\
0 <= h - height (bal l' x d r) <= 1
 avl_nns; omega_max.elt:Type
x:key
d:elt
r, ll:t elt
lx:key
ld:elt
lr:t elt
_x:I.t
l':t elt
m:(key * elt)%type
e0:remove_min ll lx ld lr = (l', m)
IHp:forall h0 : I.t,
avl (Node ll lx ld lr h0) ->
avl (remove_min ll lx ld lr)#1 /\
0 <= h0 - height (remove_min ll lx ld lr)#1 <= 1
h:I.t
H:avl (Node (Node ll lx ld lr _x) x d r h)
avl (bal l' x d r) /\
0 <= h - height (bal l' x d r) <= 1
 inversion_clear H.elt:Type
x:key
d:elt
r, ll:t elt
lx:key
ld:elt
lr:t elt
_x:I.t
l':t elt
m:(key * elt)%type
e0:remove_min ll lx ld lr = (l', m)
IHp:forall h0 : I.t,
avl (Node ll lx ld lr h0) ->
avl (remove_min ll lx ld lr)#1 /\
0 <= h0 - height (remove_min ll lx ld lr)#1 <= 1
h:I.t
H0:avl (Node ll lx ld lr _x)
H1:avl r
H2:- (2) <=
height (Node ll lx ld lr _x) - height r <= 2
H3:h =
max (height (Node ll lx ld lr _x)) (height r) + 1
avl (bal l' x d r) /\
0 <= h - height (bal l' x d r) <= 1
 rewrite e0 in IHp;simpl in IHp;destruct (IHp _x); auto.elt:Type
x:key
d:elt
r, ll:t elt
lx:key
ld:elt
lr:t elt
_x:I.t
l':t elt
m:(key * elt)%type
e0:remove_min ll lx ld lr = (l', m)
IHp:forall h0 : I.t,
avl (Node ll lx ld lr h0) -> avl l' /\ 0 <= h0 - height l' <= 1
h:I.t
H0:avl (Node ll lx ld lr _x)
H1:avl r
H2:- (2) <=
height (Node ll lx ld lr _x) - height r <= 2
H3:h =
max (height (Node ll lx ld lr _x)) (height r) + 1
H:avl l'
H4:0 <= _x - height l' <= 1
avl (bal l' x d r) /\
0 <= h - height (bal l' x d r) <= 1
 split; simpl in *.elt:Type
x:key
d:elt
r, ll:t elt
lx:key
ld:elt
lr:t elt
_x:I.t
l':t elt
m:(key * elt)%type
e0:remove_min ll lx ld lr = (l', m)
IHp:forall h0 : I.t,
avl (Node ll lx ld lr h0) -> avl l' /\ 0 <= h0 - height l' <= 1
h:I.t
H0:avl (Node ll lx ld lr _x)
H1:avl r
H2:- (2) <= _x - height r <= 2
H3:h = max _x (height r) + 1
H:avl l'
H4:0 <= _x - height l' <= 1
avl (bal l' x d r)
elt:Type
x:key
d:elt
r, ll:t elt
lx:key
ld:elt
lr:t elt
_x:I.t
l':t elt
m:(key * elt)%type
e0:remove_min ll lx ld lr = (l', m)
IHp:forall h0 : I.t,
avl (Node ll lx ld lr h0) -> avl l' /\ 0 <= h0 - height l' <= 1
h:I.t
H0:avl (Node ll lx ld lr _x)
H1:avl r
H2:- (2) <= _x - height r <= 2
H3:h = max _x (height r) + 1
H:avl l'
H4:0 <= _x - height l' <= 1
0 <= h - height (bal l' x d r) <= 1
 apply bal_avl; auto; omega_max.elt:Type
x:key
d:elt
r, ll:t elt
lx:key
ld:elt
lr:t elt
_x:I.t
l':t elt
m:(key * elt)%type
e0:remove_min ll lx ld lr = (l', m)
IHp:forall h0 : I.t,
avl (Node ll lx ld lr h0) -> avl l' /\ 0 <= h0 - height l' <= 1
h:I.t
H0:avl (Node ll lx ld lr _x)
H1:avl r
H2:- (2) <= _x - height r <= 2
H3:h = max _x (height r) + 1
H:avl l'
H4:0 <= _x - height l' <= 1
0 <= h - height (bal l' x d r) <= 1
 omega_bal.
Qed.

Lemma remove_min_avl : forall l x e r h, avl (Node l x e r h) ->
    avl (remove_min l x e r)#1.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt)
  (h : I.t),
avl (Node l x e r h) -> avl (remove_min l x e r)#1
Proof.elt:Type
forall (l : t elt) (x : key) (e : elt) (r : t elt)
  (h : I.t),
avl (Node l x e r h) -> avl (remove_min l x e r)#1
 intros; generalize (remove_min_avl_1 H); intuition.
Qed.

Merging two trees

Lemma merge_avl_1 : forall m1 m2, avl m1 -> avl m2 ->
 -(2) <= height m1 - height m2 <= 2 ->
 avl (merge m1 m2) /\
 0<= height (merge m1 m2) - max (height m1) (height m2) <=1.elt:Type
forall m1 m2 : t elt,
avl m1 ->
avl m2 ->
- (2) <= height m1 - height m2 <= 2 ->
avl (merge m1 m2) /\
0 <=
height (merge m1 m2) - max (height m1) (height m2) <=
1
Proof.elt:Type
forall m1 m2 : t elt,
avl m1 ->
avl m2 ->
- (2) <= height m1 - height m2 <= 2 ->
avl (merge m1 m2) /\
0 <=
height (merge m1 m2) - max (height m1) (height m2) <=
1
 intros m1 m2; functional induction (merge m1 m2); intros;
 try factornode _x _x0 _x1 _x2 _x3 as m1.elt:Type
s2:t elt
H:avl (Leaf elt)
H0:avl s2
H1:- (2) <= height (Leaf elt) - height s2 <= 2
avl s2 /\
0 <=
height s2 - max (height (Leaf elt)) (height s2) <= 1
elt:Type
m1:t elt
H:avl m1
H0:avl (Leaf elt)
H1:- (2) <= height m1 - height (Leaf elt) <= 2
avl m1 /\
0 <=
height m1 - max (height m1) (height (Leaf elt)) <= 1
elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
avl (bal m1 x d s2') /\
0 <=
height (bal m1 x d s2') -
max (height m1) (height (Node l2 x2 d2 r2 _x4)) <= 1
 simpl; split; auto; avl_nns; omega_max.elt:Type
m1:t elt
H:avl m1
H0:avl (Leaf elt)
H1:- (2) <= height m1 - height (Leaf elt) <= 2
avl m1 /\
0 <=
height m1 - max (height m1) (height (Leaf elt)) <= 1
elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
avl (bal m1 x d s2') /\
0 <=
height (bal m1 x d s2') -
max (height m1) (height (Node l2 x2 d2 r2 _x4)) <= 1
 simpl; split; auto; avl_nns; omega_max.elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
avl (bal m1 x d s2') /\
0 <=
height (bal m1 x d s2') -
max (height m1) (height (Node l2 x2 d2 r2 _x4)) <= 1
 generalize (remove_min_avl_1 H0).elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
avl (remove_min l2 x2 d2 r2)#1 /\
0 <=
height (Node l2 x2 d2 r2 _x4) -
height (remove_min l2 x2 d2 r2)#1 <= 1 ->
avl (bal m1 x d s2') /\
0 <=
height (bal m1 x d s2') -
max (height m1) (height (Node l2 x2 d2 r2 _x4)) <= 1
 rewrite e1; destruct 1.elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
H2:avl (s2', (x, d))#1
H3:0 <=
height (Node l2 x2 d2 r2 _x4) -
height (s2', (x, d))#1 <= 1
avl (bal m1 x d s2') /\
0 <=
height (bal m1 x d s2') -
max (height m1) (height (Node l2 x2 d2 r2 _x4)) <= 1
 split.elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
H2:avl (s2', (x, d))#1
H3:0 <=
height (Node l2 x2 d2 r2 _x4) -
height (s2', (x, d))#1 <= 1
avl (bal m1 x d s2')
elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
H2:avl (s2', (x, d))#1
H3:0 <=
height (Node l2 x2 d2 r2 _x4) -
height (s2', (x, d))#1 <= 1
0 <=
height (bal m1 x d s2') -
max (height m1) (height (Node l2 x2 d2 r2 _x4)) <= 1
 apply bal_avl; auto.elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
H2:avl (s2', (x, d))#1
H3:0 <=
height (Node l2 x2 d2 r2 _x4) -
height (s2', (x, d))#1 <= 1
- (3) <= height m1 - height s2' <= 3
elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
H2:avl (s2', (x, d))#1
H3:0 <=
height (Node l2 x2 d2 r2 _x4) -
height (s2', (x, d))#1 <= 1
0 <=
height (bal m1 x d s2') -
max (height m1) (height (Node l2 x2 d2 r2 _x4)) <= 1
 omega_max.elt:Type
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
s2':t elt
x:key
d:elt
e1:remove_min l2 x2 d2 r2 = (s2', (x, d))
m1:t elt
H:avl m1
H0:avl (Node l2 x2 d2 r2 _x4)
H1:- (2) <=
height m1 - height (Node l2 x2 d2 r2 _x4) <= 2
H2:avl (s2', (x, d))#1
H3:0 <=
height (Node l2 x2 d2 r2 _x4) -
height (s2', (x, d))#1 <= 1
0 <=
height (bal m1 x d s2') -
max (height m1) (height (Node l2 x2 d2 r2 _x4)) <= 1
 omega_bal.
Qed.

Lemma merge_avl : forall m1 m2, avl m1 -> avl m2 ->
  -(2) <= height m1 - height m2 <= 2 -> avl (merge m1 m2).elt:Type
forall m1 m2 : t elt,
avl m1 ->
avl m2 ->
- (2) <= height m1 - height m2 <= 2 ->
avl (merge m1 m2)
Proof.elt:Type
forall m1 m2 : t elt,
avl m1 ->
avl m2 ->
- (2) <= height m1 - height m2 <= 2 ->
avl (merge m1 m2)
 intros; generalize (merge_avl_1 H H0 H1); intuition.
Qed.

Deletion

Lemma remove_avl_1 : forall m x, avl m ->
 avl (remove x m) /\ 0 <= height m - height (remove x m) <= 1.elt:Type
forall (m : t elt) (x : X.t),
avl m ->
avl (remove x m) /\
0 <= height m - height (remove x m) <= 1
Proof.elt:Type
forall (m : t elt) (x : X.t),
avl m ->
avl (remove x m) /\
0 <= height m - height (remove x m) <= 1
 intros m x; functional induction (remove x m); intros.elt:Type
x:X.t
H:avl (Leaf elt)
avl (Leaf elt) /\
0 <= height (Leaf elt) - height (Leaf elt) <= 1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
IHt:avl l -> avl (remove x l) /\ 0 <= height l - height (remove x l) <= 1
H:avl (Node l y d r _x)
avl (bal (remove x l) y d r) /\
0 <=
height (Node l y d r _x) -
height (bal (remove x l) y d r) <= 1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H:avl (Node l y d r _x)
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 split; auto; omega_max.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
IHt:avl l -> avl (remove x l) /\ 0 <= height l - height (remove x l) <= 1
H:avl (Node l y d r _x)
avl (bal (remove x l) y d r) /\
0 <=
height (Node l y d r _x) -
height (bal (remove x l) y d r) <= 1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H:avl (Node l y d r _x)
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 (* LT *)
 inv avl.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
IHt:avl l -> avl (remove x l) /\ 0 <= height l - height (remove x l) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
avl (bal (remove x l) y d r) /\
0 <=
height (Node l y d r _x) -
height (bal (remove x l) y d r) <= 1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H:avl (Node l y d r _x)
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 destruct (IHt H0).elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
IHt:avl l -> avl (remove x l) /\ 0 <= height l - height (remove x l) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x l)
H4:0 <= height l - height (remove x l) <= 1
avl (bal (remove x l) y d r) /\
0 <=
height (Node l y d r _x) -
height (bal (remove x l) y d r) <= 1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H:avl (Node l y d r _x)
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 split.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
IHt:avl l -> avl (remove x l) /\ 0 <= height l - height (remove x l) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x l)
H4:0 <= height l - height (remove x l) <= 1
avl (bal (remove x l) y d r)
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
IHt:avl l -> avl (remove x l) /\ 0 <= height l - height (remove x l) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x l)
H4:0 <= height l - height (remove x l) <= 1
0 <=
height (Node l y d r _x) -
height (bal (remove x l) y d r) <= 1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H:avl (Node l y d r _x)
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 apply bal_avl; auto.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
IHt:avl l -> avl (remove x l) /\ 0 <= height l - height (remove x l) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x l)
H4:0 <= height l - height (remove x l) <= 1
- (3) <= height (remove x l) - height r <= 3
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
IHt:avl l -> avl (remove x l) /\ 0 <= height l - height (remove x l) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x l)
H4:0 <= height l - height (remove x l) <= 1
0 <=
height (Node l y d r _x) -
height (bal (remove x l) y d r) <= 1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H:avl (Node l y d r _x)
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 omega_max.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
IHt:avl l -> avl (remove x l) /\ 0 <= height l - height (remove x l) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x l)
H4:0 <= height l - height (remove x l) <= 1
0 <=
height (Node l y d r _x) -
height (bal (remove x l) y d r) <= 1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H:avl (Node l y d r _x)
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 omega_bal.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H:avl (Node l y d r _x)
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 (* EQ *)
 inv avl.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 generalize (merge_avl_1 H0 H1 H2).elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
avl (merge l r) /\
0 <= height (merge l r) - max (height l) (height r) <=
1 ->
avl (merge l r) /\
0 <= height (Node l y d r _x) - height (merge l r) <=
1
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 intuition omega_max.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H:avl (Node l y d r _x)
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 (* GT *)
 inv avl.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 destruct (IHt H1).elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x r)
H4:0 <= height r - height (remove x r) <= 1
avl (bal l y d (remove x r)) /\
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 split.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x r)
H4:0 <= height r - height (remove x r) <= 1
avl (bal l y d (remove x r))
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x r)
H4:0 <= height r - height (remove x r) <= 1
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 apply bal_avl; auto.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x r)
H4:0 <= height r - height (remove x r) <= 1
- (3) <= height l - height (remove x r) <= 3
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x r)
H4:0 <= height r - height (remove x r) <= 1
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 omega_max.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
IHt:avl r -> avl (remove x r) /\ 0 <= height r - height (remove x r) <= 1
H0:avl l
H1:avl r
H2:- (2) <= height l - height r <= 2
H3:_x = max (height l) (height r) + 1
H:avl (remove x r)
H4:0 <= height r - height (remove x r) <= 1
0 <=
height (Node l y d r _x) -
height (bal l y d (remove x r)) <= 1
 omega_bal.
Qed.

Lemma remove_avl : forall m x, avl m -> avl (remove x m).elt:Type
forall (m : t elt) (x : X.t),
avl m -> avl (remove x m)
Proof.elt:Type
forall (m : t elt) (x : X.t),
avl m -> avl (remove x m)
 intros; generalize (remove_avl_1 x H); intuition.
Qed.
Hint Resolve remove_avl : core.

Join

Lemma join_avl_1 : forall l x d r, avl l -> avl r ->
 avl (join l x d r) /\
 0<= height (join l x d r) - max (height l) (height r) <= 1.elt:Type
forall (l : t elt) (x : key) (d : elt) (r : t elt),
avl l ->
avl r ->
avl (join l x d r) /\
0 <=
height (join l x d r) - max (height l) (height r) <= 1
Proof.elt:Type
forall (l : t elt) (x : key) (d : elt) (r : t elt),
avl l ->
avl r ->
avl (join l x d r) /\
0 <=
height (join l x d r) - max (height l) (height r) <= 1
 join_tac.elt:Type
x:key
d:elt
r:t elt
H:avl (Leaf elt)
H0:avl r
avl (join (Leaf elt) x d r) /\
0 <=
height (join (Leaf elt) x d r) -
max (height (Leaf elt)) (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
H:avl (Node ll lx ld lr lh)
H0:avl (Leaf elt)
avl (add x d (Node ll lx ld lr lh)) /\
0 <=
height (add x d (Node ll lx ld lr lh)) -
max (height (Node ll lx ld lr lh)) (height (Leaf elt)) <=
1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1

 split; simpl; auto.elt:Type
x:key
d:elt
r:t elt
H:avl (Leaf elt)
H0:avl r
0 <= height (add x d r) - max 0 (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
H:avl (Node ll lx ld lr lh)
H0:avl (Leaf elt)
avl (add x d (Node ll lx ld lr lh)) /\
0 <=
height (add x d (Node ll lx ld lr lh)) -
max (height (Node ll lx ld lr lh)) (height (Leaf elt)) <=
1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 destruct (add_avl_1 x d H0).elt:Type
x:key
d:elt
r:t elt
H:avl (Leaf elt)
H0:avl r
H1:avl (add x d r)
H2:0 <= height (add x d r) - height r <= 1
0 <= height (add x d r) - max 0 (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
H:avl (Node ll lx ld lr lh)
H0:avl (Leaf elt)
avl (add x d (Node ll lx ld lr lh)) /\
0 <=
height (add x d (Node ll lx ld lr lh)) -
max (height (Node ll lx ld lr lh)) (height (Leaf elt)) <=
1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 avl_nns; omega_max.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
H:avl (Node ll lx ld lr lh)
H0:avl (Leaf elt)
avl (add x d (Node ll lx ld lr lh)) /\
0 <=
height (add x d (Node ll lx ld lr lh)) -
max (height (Node ll lx ld lr lh)) (height (Leaf elt)) <=
1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 set (l:=Node ll lx ld lr lh) in *.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
l:=Node ll lx ld lr lh:t elt
H:avl l
H0:avl (Leaf elt)
avl (add x d l) /\
0 <=
height (add x d l) -
max (height l) (height (Leaf elt)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 split; auto.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
l:=Node ll lx ld lr lh:t elt
H:avl l
H0:avl (Leaf elt)
0 <=
height (add x d l) -
max (height l) (height (Leaf elt)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 destruct (add_avl_1 x d H).elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
l:=Node ll lx ld lr lh:t elt
H:avl l
H0:avl (Leaf elt)
H1:avl (add x d l)
H2:0 <= height (add x d l) - height l <= 1
0 <=
height (add x d l) -
max (height l) (height (Leaf elt)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 simpl (height (Leaf elt)).elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
l:=Node ll lx ld lr lh:t elt
H:avl l
H0:avl (Leaf elt)
H1:avl (add x d l)
H2:0 <= height (add x d l) - height l <= 1
0 <= height (add x d l) - max (height l) 0 <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 avl_nns; omega_max.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1

 inversion_clear H.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H0:avl (Node rl rx rd rr rh)
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 assert (height (Node rl rx rd rr rh) = rh); auto.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
H0:avl (Node rl rx rd rr rh)
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
H:height (Node rl rx rd rr rh) = rh
avl (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) /\
0 <=
height
  (bal ll lx ld (join lr x d (Node rl rx rd rr rh))) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 set (r := Node rl rx rd rr rh) in *; clearbody r.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r0 : t elt),
avl lr ->
avl r0 ->
avl (join lr x0 d0 r0) /\
0 <= height (join lr x0 d0 r0) - max (height lr) (height r0) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
GT:lh > rh + 2
r:t elt
H0:avl r
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
H:height r = rh
avl (bal ll lx ld (join lr x d r)) /\
0 <=
height (bal ll lx ld (join lr x d r)) -
max (height (Node ll lx ld lr lh)) (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 destruct (Hlr x d r H2 H0); clear Hrl Hlr.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
GT:lh > rh + 2
r:t elt
H0:avl r
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
H:height r = rh
H5:avl (join lr x d r)
H6:0 <=
height (join lr x d r) -
max (height lr) (height r) <= 1
avl (bal ll lx ld (join lr x d r)) /\
0 <=
height (bal ll lx ld (join lr x d r)) -
max (height (Node ll lx ld lr lh)) (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 set (j := join lr x d r) in *; clearbody j.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
GT:lh > rh + 2
r:t elt
H0:avl r
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
H:height r = rh
j:t elt
H5:avl j
H6:0 <= height j - max (height lr) (height r) <= 1
avl (bal ll lx ld j) /\
0 <=
height (bal ll lx ld j) -
max (height (Node ll lx ld lr lh)) (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 simpl.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
GT:lh > rh + 2
r:t elt
H0:avl r
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
H:height r = rh
j:t elt
H5:avl j
H6:0 <= height j - max (height lr) (height r) <= 1
avl (bal ll lx ld j) /\
0 <= height (bal ll lx ld j) - max lh (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 assert (-(3) <= height ll - height j <= 3) by omega_max.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
GT:lh > rh + 2
r:t elt
H0:avl r
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
H:height r = rh
j:t elt
H5:avl j
H6:0 <= height j - max (height lr) (height r) <= 1
H7:- (3) <= height ll - height j <= 3
avl (bal ll lx ld j) /\
0 <= height (bal ll lx ld j) - max lh (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 split.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
GT:lh > rh + 2
r:t elt
H0:avl r
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
H:height r = rh
j:t elt
H5:avl j
H6:0 <= height j - max (height lr) (height r) <= 1
H7:- (3) <= height ll - height j <= 3
avl (bal ll lx ld j)
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
GT:lh > rh + 2
r:t elt
H0:avl r
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
H:height r = rh
j:t elt
H5:avl j
H6:0 <= height j - max (height lr) (height r) <= 1
H7:- (3) <= height ll - height j <= 3
0 <= height (bal ll lx ld j) - max lh (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 apply bal_avl; auto.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
GT:lh > rh + 2
r:t elt
H0:avl r
H1:avl ll
H2:avl lr
H3:- (2) <= height ll - height lr <= 2
H4:lh = max (height ll) (height lr) + 1
H:height r = rh
j:t elt
H5:avl j
H6:0 <= height j - max (height lr) (height r) <= 1
H7:- (3) <= height ll - height j <= 3
0 <= height (bal ll lx ld j) - max lh (height r) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 omega_bal.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1

 inversion_clear H0.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 assert (height (Node ll lx ld lr lh) = lh); auto.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl (Node ll lx ld lr lh)
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
H0:height (Node ll lx ld lr lh) = lh
avl (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) /\
0 <=
height
  (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 set (l := Node ll lx ld lr lh) in *; clearbody l.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
l:t elt
Hrl:avl l ->
avl rl ->
avl (join l x d rl) /\
0 <= height (join l x d rl) - max (height l) (height rl) <= 1
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl l
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
H0:height l = lh
avl (bal (join l x d rl) rx rd rr) /\
0 <=
height (bal (join l x d rl) rx rd rr) -
max (height l) (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 destruct (Hrl H H1); clear Hrl Hlr.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
l:t elt
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl l
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
H0:height l = lh
H5:avl (join l x d rl)
H6:0 <=
height (join l x d rl) -
max (height l) (height rl) <= 1
avl (bal (join l x d rl) rx rd rr) /\
0 <=
height (bal (join l x d rl) rx rd rr) -
max (height l) (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 set (j := join l x d rl) in *; clearbody j.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
l:t elt
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl l
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
H0:height l = lh
j:t elt
H5:avl j
H6:0 <= height j - max (height l) (height rl) <= 1
avl (bal j rx rd rr) /\
0 <=
height (bal j rx rd rr) -
max (height l) (height (Node rl rx rd rr rh)) <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 simpl.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
l:t elt
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl l
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
H0:height l = lh
j:t elt
H5:avl j
H6:0 <= height j - max (height l) (height rl) <= 1
avl (bal j rx rd rr) /\
0 <= height (bal j rx rd rr) - max (height l) rh <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 assert (-(3) <= height j - height rr <= 3) by omega_max.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
l:t elt
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl l
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
H0:height l = lh
j:t elt
H5:avl j
H6:0 <= height j - max (height l) (height rl) <= 1
H7:- (3) <= height j - height rr <= 3
avl (bal j rx rd rr) /\
0 <= height (bal j rx rd rr) - max (height l) rh <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 split.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
l:t elt
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl l
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
H0:height l = lh
j:t elt
H5:avl j
H6:0 <= height j - max (height l) (height rl) <= 1
H7:- (3) <= height j - height rr <= 3
avl (bal j rx rd rr)
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
l:t elt
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl l
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
H0:height l = lh
j:t elt
H5:avl j
H6:0 <= height j - max (height l) (height rl) <= 1
H7:- (3) <= height j - height rr <= 3
0 <= height (bal j rx rd rr) - max (height l) rh <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 apply bal_avl; auto.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
l:t elt
LE:lh <= rh + 2
GT':rh > lh + 2
H:avl l
H1:avl rl
H2:avl rr
H3:- (2) <= height rl - height rr <= 2
H4:rh = max (height rl) (height rr) + 1
H0:height l = lh
j:t elt
H5:avl j
H6:0 <= height j - max (height l) (height rl) <= 1
H7:- (3) <= height j - height rr <= 3
0 <= height (bal j rx rd rr) - max (height l) rh <= 1
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 omega_bal.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
Hlr:forall (x0 : key) (d0 : elt) (r : t elt),
avl lr ->
avl r ->
avl (join lr x0 d0 r) /\
0 <= height (join lr x0 d0 r) - max (height lr) (height r) <= 1
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
Hrl:avl (Node ll lx ld lr lh) ->
avl rl ->
avl (join (Node ll lx ld lr lh) x d rl) /\
0 <=
height (join (Node ll lx ld lr lh) x d rl) -
max (height (Node ll lx ld lr lh)) (height rl) <= 1
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1

 clear Hrl Hlr.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 assert (height (Node ll lx ld lr lh) = lh); auto.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
H1:height (Node ll lx ld lr lh) = lh
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 assert (height (Node rl rx rd rr rh) = rh); auto.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
LE:lh <= rh + 2
LE':rh <= lh + 2
H:avl (Node ll lx ld lr lh)
H0:avl (Node rl rx rd rr rh)
H1:height (Node ll lx ld lr lh) = lh
H2:height (Node rl rx rd rr rh) = rh
avl
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) /\
0 <=
height
  (create (Node ll lx ld lr lh) x d
     (Node rl rx rd rr rh)) -
max (height (Node ll lx ld lr lh))
  (height (Node rl rx rd rr rh)) <= 1
 set (l := Node ll lx ld lr lh) in *; clearbody l.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
LE:lh <= rh + 2
LE':rh <= lh + 2
l:t elt
H:avl l
H0:avl (Node rl rx rd rr rh)
H1:height l = lh
H2:height (Node rl rx rd rr rh) = rh
avl (create l x d (Node rl rx rd rr rh)) /\
0 <=
height (create l x d (Node rl rx rd rr rh)) -
max (height l) (height (Node rl rx rd rr rh)) <= 1
 set (r := Node rl rx rd rr rh) in *; clearbody r.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
LE:lh <= rh + 2
LE':rh <= lh + 2
l:t elt
H:avl l
r:t elt
H0:avl r
H1:height l = lh
H2:height r = rh
avl (create l x d r) /\
0 <=
height (create l x d r) - max (height l) (height r) <=
1
 assert (-(2) <= height l - height r <= 2) by omega_max.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
LE:lh <= rh + 2
LE':rh <= lh + 2
l:t elt
H:avl l
r:t elt
H0:avl r
H1:height l = lh
H2:height r = rh
H3:- (2) <= height l - height r <= 2
avl (create l x d r) /\
0 <=
height (create l x d r) - max (height l) (height r) <=
1
 split.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
LE:lh <= rh + 2
LE':rh <= lh + 2
l:t elt
H:avl l
r:t elt
H0:avl r
H1:height l = lh
H2:height r = rh
H3:- (2) <= height l - height r <= 2
avl (create l x d r)
elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
LE:lh <= rh + 2
LE':rh <= lh + 2
l:t elt
H:avl l
r:t elt
H0:avl r
H1:height l = lh
H2:height r = rh
H3:- (2) <= height l - height r <= 2
0 <=
height (create l x d r) - max (height l) (height r) <=
1
 apply create_avl; auto.elt:Type
ll:t elt
lx:key
ld:elt
lr:t elt
lh:I.t
x:key
d:elt
rl:t elt
rx:key
rd:elt
rr:t elt
rh:I.t
LE:lh <= rh + 2
LE':rh <= lh + 2
l:t elt
H:avl l
r:t elt
H0:avl r
H1:height l = lh
H2:height r = rh
H3:- (2) <= height l - height r <= 2
0 <=
height (create l x d r) - max (height l) (height r) <=
1
 rewrite create_height; auto; omega_max.
Qed.

Lemma join_avl : forall l x d r, avl l -> avl r -> avl (join l x d r).elt:Type
forall (l : t elt) (x : key) (d : elt) (r : t elt),
avl l -> avl r -> avl (join l x d r)
Proof.elt:Type
forall (l : t elt) (x : key) (d : elt) (r : t elt),
avl l -> avl r -> avl (join l x d r)
 intros; destruct (join_avl_1 x d H H0); auto.
Qed.
Hint Resolve join_avl : core.

concat

Lemma concat_avl : forall m1 m2, avl m1 -> avl m2 -> avl (concat m1 m2).elt:Type
forall m1 m2 : t elt,
avl m1 -> avl m2 -> avl (concat m1 m2)
Proof.elt:Type
forall m1 m2 : t elt,
avl m1 -> avl m2 -> avl (concat m1 m2)
 intros m1 m2; functional induction (concat m1 m2); auto.elt:Type
_x:t elt
_x0:key
_x1:elt
_x2:t elt
_x3:I.t
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
m2':t elt
xd:(key * elt)%type
e1:remove_min l2 x2 d2 r2 = (m2', xd)
avl (Node _x _x0 _x1 _x2 _x3) ->
avl (Node l2 x2 d2 r2 _x4) ->
avl (join (Node _x _x0 _x1 _x2 _x3) xd#1 xd#2 m2')
 intros; apply join_avl; auto.elt:Type
_x:t elt
_x0:key
_x1:elt
_x2:t elt
_x3:I.t
l2:t elt
x2:key
d2:elt
r2:t elt
_x4:I.t
m2':t elt
xd:(key * elt)%type
e1:remove_min l2 x2 d2 r2 = (m2', xd)
H:avl (Node _x _x0 _x1 _x2 _x3)
H0:avl (Node l2 x2 d2 r2 _x4)
avl m2'
 generalize (remove_min_avl H0); rewrite e1; simpl; auto.
Qed.
Hint Resolve concat_avl : core.

split

Lemma split_avl : forall m x, avl m ->
  avl (split x m)#l /\ avl (split x m)#r.elt:Type
forall (m : t elt) (x : X.t),
avl m -> avl (split x m)#l /\ avl (split x m)#r
Proof.elt:Type
forall (m : t elt) (x : X.t),
avl m -> avl (split x m)#l /\ avl (split x m)#r
 intros m x; functional induction (split x m); simpl; auto.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt x y
e0:X.compare x y = LT _x0
ll:t elt
o:option elt
rl:t elt
e1:split x l = << ll, o, rl >>
IHt:avl l -> avl (split x l)#l /\ avl (split x l)#r
avl (Node l y d r _x) -> avl ll /\ avl (join rl y d r)
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
avl (Node l y d r _x) -> avl l /\ avl r
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
rl:t elt
o:option elt
rr:t elt
e1:split x r = << rl, o, rr >>
IHt:avl r -> avl (split x r)#l /\ avl (split x r)#r
avl (Node l y d r _x) -> avl (join l y d rl) /\ avl rr
 rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.eq x y
e0:X.compare x y = EQ _x0
avl (Node l y d r _x) -> avl l /\ avl r
elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
rl:t elt
o:option elt
rr:t elt
e1:split x r = << rl, o, rr >>
IHt:avl r -> avl (split x r)#l /\ avl (split x r)#r
avl (Node l y d r _x) -> avl (join l y d rl) /\ avl rr
 simpl; inversion_clear 1; auto.elt:Type
x:X.t
l:t elt
y:key
d:elt
r:t elt
_x:I.t
_x0:X.lt y x
e0:X.compare x y = GT _x0
rl:t elt
o:option elt
rr:t elt
e1:split x r = << rl, o, rr >>
IHt:avl r -> avl (split x r)#l /\ avl (split x r)#r
avl (Node l y d r _x) -> avl (join l y d rl) /\ avl rr
 rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition.
Qed.

End Elt.
Hint Constructors avl : core.

Section Map.
Variable elt elt' : Type.
Variable f : elt -> elt'.

Lemma map_height : forall m, height (map f m) = height m.elt, elt':Type
f:elt -> elt'
forall m : t elt, height (map f m) = height m
Proof.elt, elt':Type
f:elt -> elt'
forall m : t elt, height (map f m) = height m
destruct m; simpl; auto.
Qed.

Lemma map_avl : forall m, avl m -> avl (map f m).elt, elt':Type
f:elt -> elt'
forall m : t elt, avl m -> avl (map f m)
Proof.elt, elt':Type
f:elt -> elt'
forall m : t elt, avl m -> avl (map f m)
induction m; simpl; auto.elt, elt':Type
f:elt -> elt'
m1:Raw.t elt
k:key
e:elt
m2:Raw.t elt
t:I.t
IHm1:avl m1 -> avl (map f m1)
IHm2:avl m2 -> avl (map f m2)
avl (Node m1 k e m2 t) ->
avl (Node (map f m1) k (f e) (map f m2) t)
inversion_clear 1; constructor; auto; do 2 rewrite map_height; auto.
Qed.

End Map.

Section Mapi.
Variable elt elt' : Type.
Variable f : key -> elt -> elt'.

Lemma mapi_height : forall m, height (mapi f m) = height m.elt, elt':Type
f:key -> elt -> elt'
forall m : t elt, height (mapi f m) = height m
Proof.elt, elt':Type
f:key -> elt -> elt'
forall m : t elt, height (mapi f m) = height m
destruct m; simpl; auto.
Qed.

Lemma mapi_avl : forall m, avl m -> avl (mapi f m).elt, elt':Type
f:key -> elt -> elt'
forall m : t elt, avl m -> avl (mapi f m)
Proof.elt, elt':Type
f:key -> elt -> elt'
forall m : t elt, avl m -> avl (mapi f m)
induction m; simpl; auto.elt, elt':Type
f:key -> elt -> elt'
m1:Raw.t elt
k:key
e:elt
m2:Raw.t elt
t:I.t
IHm1:avl m1 -> avl (mapi f m1)
IHm2:avl m2 -> avl (mapi f m2)
avl (Node m1 k e m2 t) ->
avl (Node (mapi f m1) k (f k e) (mapi f m2) t)
inversion_clear 1; constructor; auto; do 2 rewrite mapi_height; auto.
Qed.

End Mapi.

Section Map_option.
Variable elt elt' : Type.
Variable f : key -> elt -> option elt'.

Lemma map_option_avl : forall m, avl m -> avl (map_option f m).elt, elt':Type
f:key -> elt -> option elt'
forall m : t elt, avl m -> avl (map_option f m)
Proof.elt, elt':Type
f:key -> elt -> option elt'
forall m : t elt, avl m -> avl (map_option f m)
induction m; simpl; auto; intros.elt, elt':Type
f:key -> elt -> option elt'
m1:Raw.t elt
k:key
e:elt
m2:Raw.t elt
t:I.t
IHm1:avl m1 -> avl (map_option f m1)
IHm2:avl m2 -> avl (map_option f m2)
H:avl (Node m1 k e m2 t)
avl
  match f k e with
  | Some d' =>
      join (map_option f m1) k d' (map_option f m2)
  | None => concat (map_option f m1) (map_option f m2)
  end
inv avl; destruct (f k e); auto using join_avl, concat_avl.
Qed.

End Map_option.

Section Map2_opt.
Variable elt elt' elt'' : Type.
Variable f : key -> elt -> option elt' -> option elt''.
Variable mapl : t elt -> t elt''.
Variable mapr : t elt' -> t elt''.
Hypothesis mapl_avl : forall m, avl m -> avl (mapl m).
Hypothesis mapr_avl : forall m', avl m' -> avl (mapr m').

Notation map2_opt := (map2_opt f mapl mapr).

Lemma map2_opt_avl : forall m1 m2, avl m1 -> avl m2 ->
 avl (map2_opt m1 m2).elt, elt', elt'':Type
f:key -> elt -> option elt' -> option elt''
mapl:t elt -> t elt''
mapr:t elt' -> t elt''
mapl_avl:forall m : t elt, avl m -> avl (mapl m)
mapr_avl:forall m' : t elt', avl m' -> avl (mapr m')
forall (m1 : t elt) (m2 : t elt'),
avl m1 -> avl m2 -> avl (map2_opt m1 m2)
Proof.elt, elt', elt'':Type
f:key -> elt -> option elt' -> option elt''
mapl:t elt -> t elt''
mapr:t elt' -> t elt''
mapl_avl:forall m : t elt, avl m -> avl (mapl m)
mapr_avl:forall m' : t elt', avl m' -> avl (mapr m')
forall (m1 : t elt) (m2 : t elt'),
avl m1 -> avl m2 -> avl (map2_opt m1 m2)
intros m1 m2; functional induction (map2_opt m1 m2); auto;
factornode _x0 _x1 _x2 _x3 _x4 as r2; intros;
destruct (split_avl x1 H0); rewrite e1 in *; simpl in *; inv avl;
auto using join_avl, concat_avl.
Qed.

End Map2_opt.

Section Map2.
Variable elt elt' elt'' : Type.
Variable f : option elt -> option elt' -> option elt''.

Lemma map2_avl : forall m1 m2, avl m1 -> avl m2 -> avl (map2 f m1 m2).elt, elt', elt'':Type
f:option elt -> option elt' -> option elt''
forall (m1 : t elt) (m2 : t elt'),
avl m1 -> avl m2 -> avl (map2 f m1 m2)
Proof.elt, elt', elt'':Type
f:option elt -> option elt' -> option elt''
forall (m1 : t elt) (m2 : t elt'),
avl m1 -> avl m2 -> avl (map2 f m1 m2)
unfold map2; auto using map2_opt_avl, map_option_avl.
Qed.

End Map2.
End AvlProofs.

Encapsulation

We can implement S with balanced binary search trees. When compared to FMapAVL, we maintain here two invariants (bst and avl) instead of only bst, which is enough for fulfilling the FMap interface.

Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.

 Module E := X.
 Module Import AvlProofs := AvlProofs I X.
 Import Raw.
 Import Raw.Proofs.

 #[universes(template)]
 Record bbst (elt:Type) :=
  Bbst {this :> tree elt; is_bst : bst this; is_avl: avl this}.

 Definition t := bbst.
 Definition key := E.t.

 Section Elt.
 Variable elt elt' elt'': Type.

 Implicit Types m : t elt.
 Implicit Types x y : key.
 Implicit Types e : elt.

 Definition empty : t elt := Bbst (empty_bst elt) (empty_avl elt).
 Definition is_empty m : bool := is_empty (this m).
 Definition add x e m : t elt :=
  Bbst (add_bst x e (is_bst m)) (add_avl x e (is_avl m)).
 Definition remove x m : t elt :=
  Bbst (remove_bst x (is_bst m)) (remove_avl x (is_avl m)).
 Definition mem x m : bool := mem x (this m).
 Definition find x m : option elt := find x (this m).
 Definition map f m : t elt' :=
  Bbst (map_bst f (is_bst m)) (map_avl f (is_avl m)).
 Definition mapi (f:key->elt->elt') m : t elt' :=
  Bbst (mapi_bst f (is_bst m)) (mapi_avl f (is_avl m)).
 Definition map2 f m (m':t elt') : t elt'' :=
  Bbst (map2_bst f (is_bst m) (is_bst m')) (map2_avl f (is_avl m) (is_avl m')).
 Definition elements m : list (key*elt) := elements (this m).
 Definition cardinal m := cardinal (this m).
 Definition fold (A:Type) (f:key->elt->A->A) m i := fold (A:=A) f (this m) i.
 Definition equal cmp m m' : bool := equal cmp (this m) (this m').

 Definition MapsTo x e m : Prop := MapsTo x e (this m).
 Definition In x m : Prop := In0 x (this m).
 Definition Empty m : Prop := Empty (this m).

 Definition eq_key : (key*elt) -> (key*elt) -> Prop := @PX.eqk elt.
 Definition eq_key_elt : (key*elt) -> (key*elt) -> Prop := @PX.eqke elt.
 Definition lt_key : (key*elt) -> (key*elt) -> Prop := @PX.ltk elt.

 Lemma MapsTo_1 : forall m x y e, E.eq x y -> MapsTo x e m -> MapsTo y e m.elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e : elt),
E.eq x y -> MapsTo x e m -> MapsTo y e m
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e : elt),
E.eq x y -> MapsTo x e m -> MapsTo y e m intros m; exact (@MapsTo_1 _ (this m)). Qed.

 Lemma mem_1 : forall m x, In x m -> mem x m = true.elt, elt', elt'':Type
forall (m : t elt) (x : key), In x m -> mem x m = true
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x : key), In x m -> mem x m = true
 unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto.elt, elt', elt'':Type
m:t elt
x:key
bst m
 apply (is_bst m).
 Qed.

 Lemma mem_2 : forall m x, mem x m = true -> In x m.elt, elt', elt'':Type
forall (m : t elt) (x : key), mem x m = true -> In x m
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x : key), mem x m = true -> In x m
 unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto.
 Qed.

 Lemma empty_1 : Empty empty.elt, elt', elt'':Type
Empty empty
 Proof.elt, elt', elt'':Type
Empty empty exact (@empty_1 elt). Qed.

 Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.elt, elt', elt'':Type
forall m : t elt, Empty m -> is_empty m = true
 Proof.elt, elt', elt'':Type
forall m : t elt, Empty m -> is_empty m = true intros m; exact (@is_empty_1 _ (this m)). Qed.
 Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.elt, elt', elt'':Type
forall m : t elt, is_empty m = true -> Empty m
 Proof.elt, elt', elt'':Type
forall m : t elt, is_empty m = true -> Empty m intros m; exact (@is_empty_2 _ (this m)). Qed.

 Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e : elt),
E.eq x y -> MapsTo y e (add x e m)
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e : elt),
E.eq x y -> MapsTo y e (add x e m) intros m x y e; exact (@add_1 elt _ x y e). Qed.
 Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e e' : elt),
~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m)
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e e' : elt),
~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m) intros m x y e e'; exact (@add_2 elt _ x y e e'). Qed.
 Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e e' : elt),
~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e e' : elt),
~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m intros m x y e e'; exact (@add_3 elt _ x y e e'). Qed.

 Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).elt, elt', elt'':Type
forall (m : t elt) (x y : key),
E.eq x y -> ~ In y (remove x m)
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x y : key),
E.eq x y -> ~ In y (remove x m)
 unfold In, remove; intros m x y; rewrite In_alt; simpl; apply remove_1; auto.elt, elt', elt'':Type
m:t elt
x, y:key
bst m
 apply (is_bst m).
 Qed.
 Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e : elt),
~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m)
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e : elt),
~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m) intros m x y e; exact (@remove_2 elt _ x y e (is_bst m)). Qed.
 Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e : elt),
MapsTo y e (remove x m) -> MapsTo y e m
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x y : key) (e : elt),
MapsTo y e (remove x m) -> MapsTo y e m intros m x y e; exact (@remove_3 elt _ x y e (is_bst m)). Qed.


 Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.elt, elt', elt'':Type
forall (m : t elt) (x : key) (e : elt),
MapsTo x e m -> find x m = Some e
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x : key) (e : elt),
MapsTo x e m -> find x m = Some e intros m x e; exact (@find_1 elt _ x e (is_bst m)). Qed.
 Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.elt, elt', elt'':Type
forall (m : t elt) (x : key) (e : elt),
find x m = Some e -> MapsTo x e m
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x : key) (e : elt),
find x m = Some e -> MapsTo x e m intros m; exact (@find_2 elt (this m)). Qed.

 Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
        fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.elt, elt', elt'':Type
forall (m : t elt) (A : Type) (i : A)
  (f : key -> elt -> A -> A),
fold f m i =
fold_left
  (fun (a : A) (p : key * elt) => f (fst p) (snd p) a)
  (elements m) i
 Proof.elt, elt', elt'':Type
forall (m : t elt) (A : Type) (i : A)
  (f : key -> elt -> A -> A),
fold f m i =
fold_left
  (fun (a : A) (p : key * elt) => f (fst p) (snd p) a)
  (elements m) i intros m; exact (@fold_1 elt (this m) (is_bst m)). Qed.

 Lemma elements_1 : forall m x e,
   MapsTo x e m -> InA eq_key_elt (x,e) (elements m).elt, elt', elt'':Type
forall (m : t elt) (x : key) (e : elt),
MapsTo x e m -> InA eq_key_elt (x, e) (elements m)
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x : key) (e : elt),
MapsTo x e m -> InA eq_key_elt (x, e) (elements m)
 intros; unfold elements, MapsTo, eq_key_elt; rewrite elements_mapsto; auto.
 Qed.

 Lemma elements_2 : forall m x e,
   InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.elt, elt', elt'':Type
forall (m : t elt) (x : key) (e : elt),
InA eq_key_elt (x, e) (elements m) -> MapsTo x e m
 Proof.elt, elt', elt'':Type
forall (m : t elt) (x : key) (e : elt),
InA eq_key_elt (x, e) (elements m) -> MapsTo x e m
 intros; unfold elements, MapsTo, eq_key_elt; rewrite <- elements_mapsto; auto.
 Qed.

 Lemma elements_3 : forall m, sort lt_key (elements m).elt, elt', elt'':Type
forall m : t elt, Sorted lt_key (elements m)
 Proof.elt, elt', elt'':Type
forall m : t elt, Sorted lt_key (elements m) intros m; exact (@elements_sort elt (this m) (is_bst m)). Qed.

 Lemma elements_3w : forall m, NoDupA eq_key (elements m).elt, elt', elt'':Type
forall m : t elt, NoDupA eq_key (elements m)
 Proof.elt, elt', elt'':Type
forall m : t elt, NoDupA eq_key (elements m) intros m; exact (@elements_nodup elt (this m) (is_bst m)). Qed.

 Lemma cardinal_1 : forall m, cardinal m = length (elements m).elt, elt', elt'':Type
forall m : t elt, cardinal m = length (elements m)
 Proof.elt, elt', elt'':Type
forall m : t elt, cardinal m = length (elements m) intro m; exact (@elements_cardinal elt (this m)). Qed.

 Definition Equal m m' := forall y, find y m = find y m'.
 Definition Equiv (eq_elt:elt->elt->Prop) m m' :=
   (forall k, In k m <-> In k m') /\
   (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e').
 Definition Equivb cmp := Equiv (Cmp cmp).

 Lemma Equivb_Equivb : forall cmp m m',
  Equivb cmp m m' <-> Raw.Proofs.Equivb cmp m m'.elt, elt', elt'':Type
forall (cmp : elt -> elt -> bool) (m m' : t elt),
Equivb cmp m m' <-> Proofs.Equivb cmp m m'
 Proof.elt, elt', elt'':Type
forall (cmp : elt -> elt -> bool) (m m' : t elt),
Equivb cmp m m' <-> Proofs.Equivb cmp m m'
 intros; unfold Equivb, Equiv, Raw.Proofs.Equivb, In; intuition.elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : key, In0 k0 m <-> In0 k0 m'
H1:forall (k0 : key) (e e' : elt),
MapsTo k0 e m -> MapsTo k0 e' m' -> Cmp cmp e e'
k:Raw.key
H:Raw.In k m
Raw.In k m'
elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : key, In0 k0 m <-> In0 k0 m'
H1:forall (k0 : key) (e e' : elt),
MapsTo k0 e m -> MapsTo k0 e' m' -> Cmp cmp e e'
k:Raw.key
H:Raw.In k m'
Raw.In k m
elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : Raw.key, Raw.In k0 m <-> Raw.In k0 m'
H1:forall (k0 : Raw.key) (e e' : elt),
Raw.MapsTo k0 e m ->
Raw.MapsTo k0 e' m' -> cmp e e' = true
k:key
H:In0 k m
In0 k m'
elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : Raw.key, Raw.In k0 m <-> Raw.In k0 m'
H1:forall (k0 : Raw.key) (e e' : elt),
Raw.MapsTo k0 e m ->
Raw.MapsTo k0 e' m' -> cmp e e' = true
k:key
H:In0 k m'
In0 k m
 generalize (H0 k); do 2 rewrite In_alt; intuition.elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : key, In0 k0 m <-> In0 k0 m'
H1:forall (k0 : key) (e e' : elt),
MapsTo k0 e m -> MapsTo k0 e' m' -> Cmp cmp e e'
k:Raw.key
H:Raw.In k m'
Raw.In k m
elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : Raw.key, Raw.In k0 m <-> Raw.In k0 m'
H1:forall (k0 : Raw.key) (e e' : elt),
Raw.MapsTo k0 e m ->
Raw.MapsTo k0 e' m' -> cmp e e' = true
k:key
H:In0 k m
In0 k m'
elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : Raw.key, Raw.In k0 m <-> Raw.In k0 m'
H1:forall (k0 : Raw.key) (e e' : elt),
Raw.MapsTo k0 e m ->
Raw.MapsTo k0 e' m' -> cmp e e' = true
k:key
H:In0 k m'
In0 k m
 generalize (H0 k); do 2 rewrite In_alt; intuition.elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : Raw.key, Raw.In k0 m <-> Raw.In k0 m'
H1:forall (k0 : Raw.key) (e e' : elt),
Raw.MapsTo k0 e m ->
Raw.MapsTo k0 e' m' -> cmp e e' = true
k:key
H:In0 k m
In0 k m'
elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : Raw.key, Raw.In k0 m <-> Raw.In k0 m'
H1:forall (k0 : Raw.key) (e e' : elt),
Raw.MapsTo k0 e m ->
Raw.MapsTo k0 e' m' -> cmp e e' = true
k:key
H:In0 k m'
In0 k m
 generalize (H0 k); do 2 rewrite <- In_alt; intuition.elt, elt', elt'':Type
cmp:elt -> elt -> bool
m, m':t elt
H0:forall k0 : Raw.key, Raw.In k0 m <-> Raw.In k0 m'
H1:forall (k0 : Raw.key) (e e' : elt),
Raw.MapsTo k0 e m ->
Raw.MapsTo k0 e' m' -> cmp e e' = true
k:key
H:In0 k m'
In0 k m
 generalize (H0 k); do 2 rewrite <- In_alt; intuition.
 Qed.

 Lemma equal_1 : forall m m' cmp,
   Equivb cmp m m' -> equal cmp m m' = true.elt, elt', elt'':Type
forall (m m' : t elt) (cmp : elt -> elt -> bool),
Equivb cmp m m' -> equal cmp m m' = true
 Proof.elt, elt', elt'':Type
forall (m m' : t elt) (cmp : elt -> elt -> bool),
Equivb cmp m m' -> equal cmp m m' = true
 unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb;
  intros; simpl in *; rewrite equal_Equivb; auto.
 Qed.

 Lemma equal_2 : forall m m' cmp,
   equal cmp m m' = true -> Equivb cmp m m'.elt, elt', elt'':Type
forall (m m' : t elt) (cmp : elt -> elt -> bool),
equal cmp m m' = true -> Equivb cmp m m'
 Proof.elt, elt', elt'':Type
forall (m m' : t elt) (cmp : elt -> elt -> bool),
equal cmp m m' = true -> Equivb cmp m m'
 unfold equal; intros (m,b,a) (m',b',a') cmp; rewrite Equivb_Equivb;
  intros; simpl in *; rewrite <-equal_Equivb; auto.
 Qed.

 End Elt.

 Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
        MapsTo x e m -> MapsTo x (f e) (map f m).forall (elt elt' : Type) (m : t elt) (x : key)
  (e : elt) (f : elt -> elt'),
MapsTo x e m -> MapsTo x (f e) (map f m)
 Proof.forall (elt elt' : Type) (m : t elt) (x : key)
  (e : elt) (f : elt -> elt'),
MapsTo x e m -> MapsTo x (f e) (map f m) intros elt elt' m x e f; exact (@map_1 elt elt' f (this m) x e). Qed.

 Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.forall (elt elt' : Type) (m : t elt) (x : key)
  (f : elt -> elt'),
In (elt:=elt') x (map f m) -> In (elt:=elt) x m
 Proof.forall (elt elt' : Type) (m : t elt) (x : key)
  (f : elt -> elt'),
In (elt:=elt') x (map f m) -> In (elt:=elt) x m
 intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite In_alt; simpl.elt, elt':Type
m:t elt
x:key
f:elt -> elt'
Raw.In x (Raw.map f m) -> Raw.In x m
 apply map_2; auto.
 Qed.

 Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)
        (f:key->elt->elt'), MapsTo x e m ->
        exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m).forall (elt elt' : Type) (m : t elt) (x : key)
  (e : elt) (f : key -> elt -> elt'),
MapsTo x e m ->
exists y : E.t,
  E.eq y x /\ MapsTo x (f y e) (mapi f m)
 Proof.forall (elt elt' : Type) (m : t elt) (x : key)
  (e : elt) (f : key -> elt -> elt'),
MapsTo x e m ->
exists y : E.t,
  E.eq y x /\ MapsTo x (f y e) (mapi f m) intros elt elt' m x e f; exact (@mapi_1 elt elt' f (this m) x e). Qed.
 Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
        (f:key->elt->elt'), In x (mapi f m) -> In x m.forall (elt elt' : Type) (m : t elt) (x : key)
  (f : key -> elt -> elt'),
In (elt:=elt') x (mapi f m) -> In (elt:=elt) x m
 Proof.forall (elt elt' : Type) (m : t elt) (x : key)
  (f : key -> elt -> elt'),
In (elt:=elt') x (mapi f m) -> In (elt:=elt) x m
 intros elt elt' m x f; unfold In in *; do 2 rewrite In_alt; simpl; apply mapi_2; auto.
 Qed.

 Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
    (x:key)(f:option elt->option elt'->option elt''),
    In x m \/ In x m' ->
    find x (map2 f m m') = f (find x m) (find x m').forall (elt elt' elt'' : Type) (m : t elt)
  (m' : t elt') (x : key)
  (f : option elt -> option elt' -> option elt''),
In (elt:=elt) x m \/ In (elt:=elt') x m' ->
find (elt:=elt'') x (map2 f m m') =
f (find (elt:=elt) x m) (find (elt:=elt') x m')
 Proof.forall (elt elt' elt'' : Type) (m : t elt)
  (m' : t elt') (x : key)
  (f : option elt -> option elt' -> option elt''),
In (elt:=elt) x m \/ In (elt:=elt') x m' ->
find (elt:=elt'') x (map2 f m m') =
f (find (elt:=elt) x m) (find (elt:=elt') x m')
 unfold find, map2, In; intros elt elt' elt'' m m' x f.elt, elt', elt'':Type
m:t elt
m':t elt'
x:key
f:option elt -> option elt' -> option elt''
In0 x m \/ In0 x m' ->
Raw.find x
  {|
  this := Raw.map2 f m m';
  is_bst := map2_bst f (is_bst m) (is_bst m');
  is_avl := map2_avl f (is_avl m) (is_avl m') |} =
f (Raw.find x m) (Raw.find x m')
 do 2 rewrite In_alt; intros; simpl; apply map2_1; auto.elt, elt', elt'':Type
m:t elt
m':t elt'
x:key
f:option elt -> option elt' -> option elt''
H:Raw.In x m \/ Raw.In x m'
bst m
elt, elt', elt'':Type
m:t elt
m':t elt'
x:key
f:option elt -> option elt' -> option elt''
H:Raw.In x m \/ Raw.In x m'
bst m'
 apply (is_bst m).elt, elt', elt'':Type
m:t elt
m':t elt'
x:key
f:option elt -> option elt' -> option elt''
H:Raw.In x m \/ Raw.In x m'
bst m'
 apply (is_bst m').
 Qed.

 Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt')
     (x:key)(f:option elt->option elt'->option elt''),
     In x (map2 f m m') -> In x m \/ In x m'.forall (elt elt' elt'' : Type) (m : t elt)
  (m' : t elt') (x : key)
  (f : option elt -> option elt' -> option elt''),
In (elt:=elt'') x (map2 f m m') ->
In (elt:=elt) x m \/ In (elt:=elt') x m'
 Proof.forall (elt elt' elt'' : Type) (m : t elt)
  (m' : t elt') (x : key)
  (f : option elt -> option elt' -> option elt''),
In (elt:=elt'') x (map2 f m m') ->
In (elt:=elt) x m \/ In (elt:=elt') x m'
 unfold In, map2; intros elt elt' elt'' m m' x f.elt, elt', elt'':Type
m:t elt
m':t elt'
x:key
f:option elt -> option elt' -> option elt''
In0 x
  {|
  this := Raw.map2 f m m';
  is_bst := map2_bst f (is_bst m) (is_bst m');
  is_avl := map2_avl f (is_avl m) (is_avl m') |} ->
In0 x m \/ In0 x m'
 do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto.elt, elt', elt'':Type
m:t elt
m':t elt'
x:key
f:option elt -> option elt' -> option elt''
H:Raw.In x (Raw.map2 f m m')
bst m
elt, elt', elt'':Type
m:t elt
m':t elt'
x:key
f:option elt -> option elt' -> option elt''
H:Raw.In x (Raw.map2 f m m')
bst m'
 apply (is_bst m).elt, elt', elt'':Type
m:t elt
m':t elt'
x:key
f:option elt -> option elt' -> option elt''
H:Raw.In x (Raw.map2 f m m')
bst m'
 apply (is_bst m').
 Qed.

End IntMake.


Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
    Sord with Module Data := D
            with Module MapS.E := X.

  Module Data := D.
  Module Import MapS := IntMake(I)(X).
  Import AvlProofs.
  Import Raw.Proofs.
  Module Import MD := OrderedTypeFacts(D).
  Module LO := FMapList.Make_ord(X)(D).

  Definition t := MapS.t D.t.

  Definition cmp e e' :=
   match D.compare e e' with EQ _ => true | _ => false end.

  Definition elements (m:t) :=
    LO.MapS.Build_slist (Raw.Proofs.elements_sort (is_bst m)).

As comparison function, we propose here a non-structural

version faithful to the code of Ocaml's Map library, instead of the structural version of FMapAVL

  Fixpoint cardinal_e (e:Raw.enumeration D.t) :=
    match e with
     | Raw.End _ => 0%nat
     | Raw.More _ _ r e => S (Raw.cardinal r + cardinal_e e)
    end.

  Lemma cons_cardinal_e : forall m e,
   cardinal_e (Raw.cons m e) = (Raw.cardinal m + cardinal_e e)%nat.forall (m : Raw.t D.t) (e : Raw.enumeration D.t),
cardinal_e (Raw.cons m e) =
Raw.cardinal m + cardinal_e e
  Proof.forall (m : Raw.t D.t) (e : Raw.enumeration D.t),
cardinal_e (Raw.cons m e) =
Raw.cardinal m + cardinal_e e
   induction m; simpl; intros; auto.m1:Raw.t D.t
k:Raw.key
e:D.t
m2:Raw.t D.t
t0:I.t
IHm1:forall e1 : Raw.enumeration D.t,
cardinal_e (Raw.cons m1 e1) =
Raw.cardinal m1 + cardinal_e e1
IHm2:forall e1 : Raw.enumeration D.t,
cardinal_e (Raw.cons m2 e1) =
Raw.cardinal m2 + cardinal_e e1
e0:Raw.enumeration D.t
cardinal_e (Raw.cons m1 (Raw.More k e m2 e0)) =
S (Raw.cardinal m1 + Raw.cardinal m2 + cardinal_e e0)
   rewrite IHm1; simpl; rewrite <- plus_n_Sm; auto with arith.
  Qed.

  Definition cardinal_e_2 ee :=
   (cardinal_e (fst ee) + cardinal_e (snd ee))%nat.

  Local Unset Keyed Unification.

  Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t)
   { measure cardinal_e_2 ee } : comparison :=
  match ee with
  | (Raw.End _, Raw.End _) => Eq
  | (Raw.End _, Raw.More _ _ _ _) => Lt
  | (Raw.More _ _ _ _, Raw.End _) => Gt
  | (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) =>
      match X.compare x1 x2 with
      | EQ _ => match D.compare d1 d2 with
                | EQ _ => compare_aux (Raw.cons r1 e1, Raw.cons r2 e2)
                | LT _ => Lt
                | GT _ => Gt
                end
      | LT _ => Lt
      | GT _ => Gt
      end
  end.forall
  (ee : Raw.enumeration D.t * Raw.enumeration D.t)
  (e e0 : Raw.enumeration D.t) (x1 : Raw.key)
  (d1 : D.t) (r1 : Raw.t D.t)
  (e1 : Raw.enumeration D.t),
e = Raw.More x1 d1 r1 e1 ->
forall (x2 : Raw.key) (d2 : D.t) (r2 : Raw.t D.t)
  (e2 : Raw.enumeration D.t),
e0 = Raw.More x2 d2 r2 e2 ->
ee = (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) ->
forall e3 : X.eq x1 x2,
X.compare x1 x2 = EQ e3 ->
forall e4 : D.eq d1 d2,
D.compare d1 d2 = EQ e4 ->
cardinal_e_2 (Raw.cons r1 e1, Raw.cons r2 e2) <
cardinal_e_2
  (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2)
  Proof.forall
  (ee : Raw.enumeration D.t * Raw.enumeration D.t)
  (e e0 : Raw.enumeration D.t) (x1 : Raw.key)
  (d1 : D.t) (r1 : Raw.t D.t)
  (e1 : Raw.enumeration D.t),
e = Raw.More x1 d1 r1 e1 ->
forall (x2 : Raw.key) (d2 : D.t) (r2 : Raw.t D.t)
  (e2 : Raw.enumeration D.t),
e0 = Raw.More x2 d2 r2 e2 ->
ee = (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2) ->
forall e3 : X.eq x1 x2,
X.compare x1 x2 = EQ e3 ->
forall e4 : D.eq d1 d2,
D.compare d1 d2 = EQ e4 ->
cardinal_e_2 (Raw.cons r1 e1, Raw.cons r2 e2) <
cardinal_e_2
  (Raw.More x1 d1 r1 e1, Raw.More x2 d2 r2 e2)
  intros; unfold cardinal_e_2; simpl;
  abstract (do 2 rewrite cons_cardinal_e; lia ).
  Defined.

  Definition Cmp c :=
   match c with
    | Eq => LO.eq_list
    | Lt => LO.lt_list
    | Gt => (fun l1 l2 => LO.lt_list l2 l1)
   end.

  Lemma cons_Cmp : forall c x1 x2 d1 d2 l1 l2,
   X.eq x1 x2 -> D.eq d1 d2 ->
   Cmp c l1 l2 -> Cmp c ((x1,d1)::l1) ((x2,d2)::l2).forall (c : comparison) (x1 x2 : X.t) (d1 d2 : D.t)
  (l1 l2 : list (X.t * D.t)),
X.eq x1 x2 ->
D.eq d1 d2 ->
Cmp c l1 l2 -> Cmp c ((x1, d1) :: l1) ((x2, d2) :: l2)
  Proof.forall (c : comparison) (x1 x2 : X.t) (d1 d2 : D.t)
  (l1 l2 : list (X.t * D.t)),
X.eq x1 x2 ->
D.eq d1 d2 ->
Cmp c l1 l2 -> Cmp c ((x1, d1) :: l1) ((x2, d2) :: l2)
   destruct c; simpl; intros; MX.elim_comp; auto.
  Qed.
  Hint Resolve cons_Cmp : core.

  Lemma compare_aux_Cmp : forall e,
   Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)).forall e : Raw.enumeration D.t * Raw.enumeration D.t,
Cmp (compare_aux e) (flatten_e (fst e))
  (flatten_e (snd e))
  Proof.forall e : Raw.enumeration D.t * Raw.enumeration D.t,
Cmp (compare_aux e) (flatten_e (fst e))
  (flatten_e (snd e))
  intros e; functional induction (compare_aux e); simpl in *;
   auto; intros; try clear e0; try clear e3; try MX.elim_comp; auto.x1:Raw.key
d1:D.t
r1:Raw.t D.t
e1:Raw.enumeration D.t
x2:Raw.key
d2:D.t
r2:Raw.t D.t
e2:Raw.enumeration D.t
_x:X.eq x1 x2
_x0:D.eq d1 d2
IHc:Cmp (compare_aux (Raw.cons r1 e1, Raw.cons r2 e2))
(flatten_e (Raw.cons r1 e1)) (flatten_e (Raw.cons r2 e2))
Cmp (compare_aux (Raw.cons r1 e1, Raw.cons r2 e2))
  ((x1, d1) :: Raw.elements r1 ++ flatten_e e1)
  ((x2, d2) :: Raw.elements r2 ++ flatten_e e2)
  rewrite 2 cons_1 in IHc; auto.
  Qed.

  Lemma compare_Cmp : forall m1 m2,
    Cmp (compare_aux (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _)))
     (Raw.elements m1) (Raw.elements m2).forall m1 m2 : Raw.t D.t,
Cmp
  (compare_aux
     (Raw.cons m1 (Raw.End D.t),
     Raw.cons m2 (Raw.End D.t))) (Raw.elements m1)
  (Raw.elements m2)
  Proof.forall m1 m2 : Raw.t D.t,
Cmp
  (compare_aux
     (Raw.cons m1 (Raw.End D.t),
     Raw.cons m2 (Raw.End D.t))) (Raw.elements m1)
  (Raw.elements m2)
  intros.m1, m2:Raw.t D.t
Cmp
  (compare_aux
     (Raw.cons m1 (Raw.End D.t),
     Raw.cons m2 (Raw.End D.t))) (Raw.elements m1)
  (Raw.elements m2)
  assert (H1:=cons_1 m1 (Raw.End _)).m1, m2:Raw.t D.t
H1:flatten_e (Raw.cons m1 (Raw.End D.t)) =
Raw.elements m1 ++ flatten_e (Raw.End D.t)
Cmp
  (compare_aux
     (Raw.cons m1 (Raw.End D.t),
     Raw.cons m2 (Raw.End D.t))) (Raw.elements m1)
  (Raw.elements m2)
  assert (H2:=cons_1 m2 (Raw.End _)).m1, m2:Raw.t D.t
H1:flatten_e (Raw.cons m1 (Raw.End D.t)) =
Raw.elements m1 ++ flatten_e (Raw.End D.t)
H2:flatten_e (Raw.cons m2 (Raw.End D.t)) =
Raw.elements m2 ++ flatten_e (Raw.End D.t)
Cmp
  (compare_aux
     (Raw.cons m1 (Raw.End D.t),
     Raw.cons m2 (Raw.End D.t))) (Raw.elements m1)
  (Raw.elements m2)
  simpl in *; rewrite app_nil_r in *; rewrite <-H1,<-H2.m1, m2:Raw.t D.t
H1:flatten_e (Raw.cons m1 (Raw.End D.t)) =
Raw.elements m1
H2:flatten_e (Raw.cons m2 (Raw.End D.t)) =
Raw.elements m2
Cmp
  (compare_aux
     (Raw.cons m1 (Raw.End D.t),
     Raw.cons m2 (Raw.End D.t)))
  (flatten_e (Raw.cons m1 (Raw.End D.t)))
  (flatten_e (Raw.cons m2 (Raw.End D.t)))
  apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _),
                           Raw.cons m2 (Raw.End _))).
  Qed.

  Definition eq (m1 m2 : t) := LO.eq_list (Raw.elements m1) (Raw.elements m2).
  Definition lt (m1 m2 : t) := LO.lt_list (Raw.elements m1) (Raw.elements m2).

  Definition compare (s s':t) : Compare lt eq s s'.s, s':t
Compare lt eq s s'
  Proof.s, s':t
Compare lt eq s s'
   destruct s as (s,b,a), s' as (s',b',a').s:Raw.t D.t
b:Raw.bst s
a:avl s
s':Raw.t D.t
b':Raw.bst s'
a':avl s'
Compare lt eq
  {| this := s; is_bst := b; is_avl := a |}
  {| this := s'; is_bst := b'; is_avl := a' |}
   generalize (compare_Cmp s s').s:Raw.t D.t
b:Raw.bst s
a:avl s
s':Raw.t D.t
b':Raw.bst s'
a':avl s'
Cmp
  (compare_aux
     (Raw.cons s (Raw.End D.t),
     Raw.cons s' (Raw.End D.t))) (Raw.elements s)
  (Raw.elements s') ->
Compare lt eq
  {| this := s; is_bst := b; is_avl := a |}
  {| this := s'; is_bst := b'; is_avl := a' |}
   destruct compare_aux; intros; [apply EQ|apply LT|apply GT]; red; auto.
  Defined.


  (* Proofs about [eq] and [lt] *)

  Definition selements (m1 : t) :=
   LO.MapS.Build_slist (elements_sort (is_bst m1)).

  Definition seq (m1 m2 : t) := LO.eq (selements m1) (selements m2).
  Definition slt (m1 m2 : t) := LO.lt (selements m1) (selements m2).

  Lemma eq_seq : forall m1 m2, eq m1 m2 <-> seq m1 m2.forall m1 m2 : t, eq m1 m2 <-> seq m1 m2
  Proof.forall m1 m2 : t, eq m1 m2 <-> seq m1 m2
   unfold eq, seq, selements, elements, LO.eq; intuition.
  Qed.

  Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2.forall m1 m2 : t, lt m1 m2 <-> slt m1 m2
  Proof.forall m1 m2 : t, lt m1 m2 <-> slt m1 m2
   unfold lt, slt, selements, elements, LO.lt; intuition.
  Qed.

  Lemma eq_1 : forall (m m' : t), MapS.Equivb cmp m m' -> eq m m'.forall m m' : t, MapS.Equivb cmp m m' -> eq m m'
  Proof.forall m m' : t, MapS.Equivb cmp m m' -> eq m m'
  intros m m'.m, m':t
MapS.Equivb cmp m m' -> eq m m'
  rewrite eq_seq; unfold seq.m, m':t
MapS.Equivb cmp m m' ->
LO.eq (selements m) (selements m')
  rewrite Equivb_Equivb.m, m':t
Equivb cmp m m' -> LO.eq (selements m) (selements m')
  rewrite Equivb_elements.m, m':t
L.Equivb cmp (Raw.elements m) (Raw.elements m') ->
LO.eq (selements m) (selements m')
  auto using LO.eq_1.
  Qed.

  Lemma eq_2 : forall m m', eq m m' -> MapS.Equivb cmp m m'.forall m m' : t, eq m m' -> MapS.Equivb cmp m m'
  Proof.forall m m' : t, eq m m' -> MapS.Equivb cmp m m'
  intros m m'.m, m':t
eq m m' -> MapS.Equivb cmp m m'
  rewrite eq_seq; unfold seq.m, m':t
LO.eq (selements m) (selements m') ->
MapS.Equivb cmp m m'
  rewrite Equivb_Equivb.m, m':t
LO.eq (selements m) (selements m') -> Equivb cmp m m'
  rewrite Equivb_elements.m, m':t
LO.eq (selements m) (selements m') ->
L.Equivb cmp (Raw.elements m) (Raw.elements m')
  intros.m, m':t
H:LO.eq (selements m) (selements m')
L.Equivb cmp (Raw.elements m) (Raw.elements m')
  generalize (LO.eq_2 H).m, m':t
H:LO.eq (selements m) (selements m')
LO.MapS.Equivb LO.cmp (selements m) (selements m') ->
L.Equivb cmp (Raw.elements m) (Raw.elements m')
  auto.
  Qed.

  Lemma eq_refl : forall m : t, eq m m.forall m : t, eq m m
  Proof.forall m : t, eq m m
  intros; rewrite eq_seq; unfold seq; intros; apply LO.eq_refl.
  Qed.

  Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.forall m1 m2 : t, eq m1 m2 -> eq m2 m1
  Proof.forall m1 m2 : t, eq m1 m2 -> eq m2 m1
  intros m1 m2; rewrite 2 eq_seq; unfold seq; intros; apply LO.eq_sym; auto.
  Qed.

  Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3
  Proof.forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3
  intros m1 m2 M3; rewrite 3 eq_seq; unfold seq.m1, m2, M3:t
LO.eq (selements m1) (selements m2) ->
LO.eq (selements m2) (selements M3) ->
LO.eq (selements m1) (selements M3)
   intros; eapply LO.eq_trans; eauto.
  Qed.

  Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3
  Proof.forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3
  intros m1 m2 m3; rewrite 3 lt_slt; unfold slt;
   intros; eapply LO.lt_trans; eauto.
  Qed.

  Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2
  Proof.forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2
  intros m1 m2; rewrite lt_slt, eq_seq; unfold slt, seq;
   intros; apply LO.lt_not_eq; auto.
  Qed.

End IntMake_ord.

(* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *)

Module Make (X: OrderedType) <: S with Module E := X
 :=IntMake(Z_as_Int)(X).

Module Make_ord (X: OrderedType)(D: OrderedType)
 <: Sord with Module Data := D
            with Module MapS.E := X
 :=IntMake_ord(Z_as_Int)(X)(D).