Library Stdlib.FSets.FMapAVL
FMapAVL
Notations and helper lemma about pairs
Declare Scope pair_scope.
Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.
Module Raw (Import I:Int)(X: OrderedType).
Local Open Scope pair_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope Int_scope.
Local Notation int := I.t.
Definition key := X.t.
#[global]
Hint Transparent key : core.
#[universes(template)]
Inductive tree {elt : Type} :=
| Leaf : tree
| Node : tree -> key -> elt -> tree -> int -> tree.
Arguments tree : clear implicits.
Section Elt.
Variable elt : Type.
Notation t := (tree elt).
Implicit Types m : t.
Definition height (m : t) : int :=
match m with
| Leaf => 0
| Node _ _ _ _ h => h
end.
Fixpoint cardinal (m : t) : nat :=
match m with
| Leaf => 0%nat
| Node l _ _ r _ => S (cardinal l + cardinal r)
end.
Membership
Fixpoint mem x m : bool :=
match m with
| Leaf => false
| Node l y _ r _ => match X.compare x y with
| LT _ => mem x l
| EQ _ => true
| GT _ => mem x r
end
end.
Fixpoint find x m : option elt :=
match m with
| Leaf => None
| Node l y d r _ => match X.compare x y with
| LT _ => find x l
| EQ _ => Some d
| GT _ => find x r
end
end.
Helper functions
bal l x e r acts as create, but performs one step of
rebalancing if necessary, i.e. assumes |height l - height r| <= 3.
Definition assert_false := create.
Definition bal l x d r :=
let hl := height l in
let hr := height r in
if gt_le_dec hl (hr+2) then
match l with
| Leaf => assert_false l x d r
| Node ll lx ld lr _ =>
if ge_lt_dec (height ll) (height lr) then
create ll lx ld (create lr x d r)
else
match lr with
| Leaf => assert_false l x d r
| Node lrl lrx lrd lrr _ =>
create (create ll lx ld lrl) lrx lrd (create lrr x d r)
end
end
else
if gt_le_dec hr (hl+2) then
match r with
| Leaf => assert_false l x d r
| Node rl rx rd rr _ =>
if ge_lt_dec (height rr) (height rl) then
create (create l x d rl) rx rd rr
else
match rl with
| Leaf => assert_false l x d r
| Node rll rlx rld rlr _ =>
create (create l x d rll) rlx rld (create rlr rx rd rr)
end
end
else
create l x d r.
Fixpoint add x d m :=
match m with
| Leaf => Node Leaf x d Leaf 1
| Node l y d' r h =>
match X.compare x y with
| LT _ => bal (add x d l) y d' r
| EQ _ => Node l y d r h
| GT _ => bal l y d' (add x d r)
end
end.
Extraction of minimum binding
Fixpoint remove_min l x d r : t*(key*elt) :=
match l with
| Leaf => (r,(x,d))
| Node ll lx ld lr lh =>
let (l',m) := remove_min ll lx ld lr in
(bal l' x d r, m)
end.
Merging two trees
Definition merge s1 s2 := match s1,s2 with
| Leaf, _ => s2
| _, Leaf => s1
| _, Node l2 x2 d2 r2 h2 =>
match remove_min l2 x2 d2 r2 with
(s2',(x,d)) => bal s1 x d s2'
end
end.
Fixpoint remove x m := match m with
| Leaf => Leaf
| Node l y d r h =>
match X.compare x y with
| LT _ => bal (remove x l) y d r
| EQ _ => merge l r
| GT _ => bal l y d (remove x r)
end
end.
Fixpoint join l : key -> elt -> t -> t :=
match l with
| Leaf => add
| Node ll lx ld lr lh => fun x d =>
fix join_aux (r:t) : t := match r with
| Leaf => add x d l
| Node rl rx rd rr rh =>
if gt_le_dec lh (rh+2) then bal ll lx ld (join lr x d r)
else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rd rr
else create l x d r
end
end.
Splitting
- l is the set of elements of m that are < x
- r is the set of elements of m that are > x
- o is the result of find x m.
Record triple := mktriple { t_left:t; t_opt:option elt; t_right:t }.
Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
Fixpoint split x m : triple := match m with
| Leaf => << Leaf, None, Leaf >>
| Node l y d r h =>
match X.compare x y with
| LT _ => let (ll,o,rl) := split x l in << ll, o, join rl y d r >>
| EQ _ => << l, Some d, r >>
| GT _ => let (rl,o,rr) := split x r in << join l y d rl, o, rr >>
end
end.
Definition concat m1 m2 :=
match m1, m2 with
| Leaf, _ => m2
| _ , Leaf => m1
| _, Node l2 x2 d2 r2 _ =>
let (m2',xd) := remove_min l2 x2 d2 r2 in
join m1 xd#1 xd#2 m2'
end.
Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) :=
match m with
| Leaf => acc
| Node l x d r _ => elements_aux ((x,d) :: elements_aux acc r) l
end.
then elements is an instantiation with an empty acc
Fixpoint fold (A : Type) (f : key -> elt -> A -> A) (m : t) : A -> A :=
fun a => match m with
| Leaf => a
| Node l x d r _ => fold f r (f x d (fold f l a))
end.
Inductive enumeration :=
| End : enumeration
| More : key -> elt -> t -> enumeration -> enumeration.
cons m e adds the elements of tree m on the head of
enumeration e.
Fixpoint cons m e : enumeration :=
match m with
| Leaf => e
| Node l x d r h => cons l (More x d r e)
end.
One step of comparison of elements
Definition equal_more x1 d1 (cont:enumeration->bool) e2 :=
match e2 with
| End => false
| More x2 d2 r2 e2 =>
match X.compare x1 x2 with
| EQ _ => cmp d1 d2 &&& cont (cons r2 e2)
| _ => false
end
end.
Comparison of left tree, middle element, then right tree
Fixpoint equal_cont m1 (cont:enumeration->bool) e2 :=
match m1 with
| Leaf => cont e2
| Node l1 x1 d1 r1 _ =>
equal_cont l1 (equal_more x1 d1 (equal_cont r1 cont)) e2
end.
Initial continuation
The complete comparison
Definition equal m1 m2 := equal_cont m1 equal_end (cons m2 End).
End Elt.
Notation t := tree.
Arguments Leaf : clear implicits.
Arguments Node [elt].
Notation "<< l , b , r >>" := (mktriple l b r) (at level 9).
Notation "t #l" := (t_left t) (at level 9, format "t '#l'").
Notation "t #o" := (t_opt t) (at level 9, format "t '#o'").
Notation "t #r" := (t_right t) (at level 9, format "t '#r'").
Fixpoint map (elt elt' : Type)(f : elt -> elt')(m : t elt) : t elt' :=
match m with
| Leaf _ => Leaf _
| Node l x d r h => Node (map f l) x (f d) (map f r) h
end.
Fixpoint mapi (elt elt' : Type)(f : key -> elt -> elt')(m : t elt) : t elt' :=
match m with
| Leaf _ => Leaf _
| Node l x d r h => Node (mapi f l) x (f x d) (mapi f r) h
end.
Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt)
: t elt' :=
match m with
| Leaf _ => Leaf _
| Node l x d r h =>
match f x d with
| Some d' => join (map_option f l) x d' (map_option f r)
| None => concat (map_option f l) (map_option f r)
end
end.
Optimized map2
- f which is a specialisation of f0 when first option isn't None
- mapl treats a tree elt with f0 when second option is None
- mapr treats a tree elt' with f0 when first option is None
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''.
Fixpoint map2_opt m1 m2 :=
match m1, m2 with
| Leaf _, _ => mapr m2
| _, Leaf _ => mapl m1
| Node l1 x1 d1 r1 h1, _ =>
let (l2',o2,r2') := split x1 m2 in
match f x1 d1 o2 with
| Some e => join (map2_opt l1 l2') x1 e (map2_opt r1 r2')
| None => concat (map2_opt l1 l2') (map2_opt r1 r2')
end
end.
End Map2_opt.
Section Map2.
Variable elt elt' elt'' : Type.
Variable f : option elt -> option elt' -> option elt''.
Definition map2 : t elt -> t elt' -> t elt'' :=
map2_opt
(fun _ d o => f (Some d) o)
(map_option (fun _ d => f (Some d) None))
(map_option (fun _ d' => f None (Some d'))).
End Map2.
Inductive MapsTo (x : key)(e : elt) : t elt -> Prop :=
| MapsRoot : forall l r h y,
X.eq x y -> MapsTo x e (Node l y e r h)
| MapsLeft : forall l r h y e',
MapsTo x e l -> MapsTo x e (Node l y e' r h)
| MapsRight : forall l r h y e',
MapsTo x e r -> MapsTo x e (Node l y e' r h).
Inductive In (x : key) : t elt -> Prop :=
| InRoot : forall l r h y e,
X.eq x y -> In x (Node l y e r h)
| InLeft : forall l r h y e',
In x l -> In x (Node l y e' r h)
| InRight : forall l r h y e',
In x r -> In x (Node l y e' r h).
Definition In0 k m := exists e:elt, MapsTo k e m.
Definition lt_tree x m := forall y, In y m -> X.lt y x.
Definition gt_tree x m := forall y, In y m -> X.lt x y.
bst t : t is a binary search tree
Inductive bst : t elt -> Prop :=
| BSLeaf : bst (Leaf _)
| BSNode : forall x e l r h, bst l -> bst r ->
lt_tree x l -> gt_tree x r -> bst (Node l x e r h).
End Invariants.
Module Proofs.
Module MX := OrderedTypeFacts X.
Module PX := KeyOrderedType X.
Module L := FMapList.Raw X.
#[local] Ltac caseq :=
match goal with [ |- context [match ?t with _ => _ end] ] =>
let cmp := fresh in
let H := fresh in
remember t as cmp eqn:H; symmetry in H; destruct cmp
end.
Lemma mem_ind [elt : Type] [x : X.t] [P : t elt -> bool -> Prop] :
(forall m : t elt, m = Leaf elt -> P (Leaf elt) false) ->
(forall (m l : t elt) (y : key) (_x : elt) (r : t elt) (_x0 : int),
m = Node l y _x r _x0 ->
forall _x1 : X.lt x y,
X.compare x y = LT _x1 -> P l (mem x l) -> P (Node l y _x r _x0) (mem x l)) ->
(forall (m l : t elt) (y : key) (_x : elt) (r : t elt) (_x0 : int),
m = Node l y _x r _x0 ->
forall _x1 : X.eq x y, X.compare x y = EQ _x1 -> P (Node l y _x r _x0) true) ->
(forall (m l : t elt) (y : key) (_x : elt) (r : t elt) (_x0 : int),
m = Node l y _x r _x0 ->
forall _x1 : X.lt y x,
X.compare x y = GT _x1 -> P r (mem x r) -> P (Node l y _x r _x0) (mem x r)) ->
forall m : t elt, P m (mem x m).
Lemma find_ind [elt : Type] [x : X.t] [P : t elt -> option elt -> Prop] :
(forall m : t elt, m = Leaf elt -> P (Leaf elt) None) ->
(forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
m = Node l y d r _x ->
forall _x0 : X.lt x y,
X.compare x y = LT _x0 -> P l (find x l) -> P (Node l y d r _x) (find x l)) ->
(forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
m = Node l y d r _x ->
forall _x0 : X.eq x y, X.compare x y = EQ _x0 -> P (Node l y d r _x) (Some d)) ->
(forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
m = Node l y d r _x ->
forall _x0 : X.lt y x,
X.compare x y = GT _x0 -> P r (find x r) -> P (Node l y d r _x) (find x r)) ->
forall m : t elt, P m (find x m).
Lemma bal_ind [elt : Type] [P : t elt -> key -> elt -> t elt -> t elt -> Prop] :
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
let hl := height l in
let hr := height r in
forall _x : hl > hr + 2,
gt_le_dec hl (hr + 2) = left _x -> l = Leaf elt -> P (Leaf elt) x d r (assert_false l x d r)) ->
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
let hl := height l in
let hr := height r in
forall _x : hl > hr + 2,
gt_le_dec hl (hr + 2) = left _x ->
forall (ll : t elt) (lx : key) (ld : elt) (lr : t elt) (_x0 : int),
l = Node ll lx ld lr _x0 ->
forall _x1 : height ll >= height lr,
ge_lt_dec (height ll) (height lr) = left _x1 ->
P (Node ll lx ld lr _x0) x d r (create ll lx ld (create lr x d r))) ->
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
let hl := height l in
let hr := height r in
forall _x : hl > hr + 2,
gt_le_dec hl (hr + 2) = left _x ->
forall (ll : t elt) (lx : key) (ld : elt) (lr : t elt) (_x0 : int),
l = Node ll lx ld lr _x0 ->
forall _x1 : height ll < height lr,
ge_lt_dec (height ll) (height lr) = right _x1 ->
lr = Leaf elt -> P (Node ll lx ld (Leaf elt) _x0) x d r (assert_false l x d r)) ->
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
let hl := height l in
let hr := height r in
forall _x : hl > hr + 2,
gt_le_dec hl (hr + 2) = left _x ->
forall (ll : t elt) (lx : key) (ld : elt) (lr : t elt) (_x0 : int),
l = Node ll lx ld lr _x0 ->
forall _x1 : height ll < height lr,
ge_lt_dec (height ll) (height lr) = right _x1 ->
forall (lrl : t elt) (lrx : key) (lrd : elt) (lrr : t elt) (_x2 : int),
lr = Node lrl lrx lrd lrr _x2 ->
P (Node ll lx ld (Node lrl lrx lrd lrr _x2) _x0) x d r
(create (create ll lx ld lrl) lrx lrd (create lrr x d r))) ->
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
let hl := height l in
let hr := height r in
forall _x : hl <= hr + 2,
gt_le_dec hl (hr + 2) = right _x ->
forall _x0 : hr > hl + 2,
gt_le_dec hr (hl + 2) = left _x0 -> r = Leaf elt -> P l x d (Leaf elt) (assert_false l x d r)) ->
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
let hl := height l in
let hr := height r in
forall _x : hl <= hr + 2,
gt_le_dec hl (hr + 2) = right _x ->
forall _x0 : hr > hl + 2,
gt_le_dec hr (hl + 2) = left _x0 ->
forall (rl : t elt) (rx : key) (rd : elt) (rr : t elt) (_x1 : int),
r = Node rl rx rd rr _x1 ->
forall _x2 : height rr >= height rl,
ge_lt_dec (height rr) (height rl) = left _x2 ->
P l x d (Node rl rx rd rr _x1) (create (create l x d rl) rx rd rr)) ->
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
let hl := height l in
let hr := height r in
forall _x : hl <= hr + 2,
gt_le_dec hl (hr + 2) = right _x ->
forall _x0 : hr > hl + 2,
gt_le_dec hr (hl + 2) = left _x0 ->
forall (rl : t elt) (rx : key) (rd : elt) (rr : t elt) (_x1 : int),
r = Node rl rx rd rr _x1 ->
forall _x2 : height rr < height rl,
ge_lt_dec (height rr) (height rl) = right _x2 ->
rl = Leaf elt -> P l x d (Node (Leaf elt) rx rd rr _x1) (assert_false l x d r)) ->
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
let hl := height l in
let hr := height r in
forall _x : hl <= hr + 2,
gt_le_dec hl (hr + 2) = right _x ->
forall _x0 : hr > hl + 2,
gt_le_dec hr (hl + 2) = left _x0 ->
forall (rl : t elt) (rx : key) (rd : elt) (rr : t elt) (_x1 : int),
r = Node rl rx rd rr _x1 ->
forall _x2 : height rr < height rl,
ge_lt_dec (height rr) (height rl) = right _x2 ->
forall (rll : t elt) (rlx : key) (rld : elt) (rlr : t elt) (_x3 : int),
rl = Node rll rlx rld rlr _x3 ->
P l x d (Node (Node rll rlx rld rlr _x3) rx rd rr _x1)
(create (create l x d rll) rlx rld (create rlr rx rd rr))) ->
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
let hl := height l in
let hr := height r in
forall _x : hl <= hr + 2,
gt_le_dec hl (hr + 2) = right _x ->
forall _x0 : hr <= hl + 2, gt_le_dec hr (hl + 2) = right _x0 -> P l x d r (create l x d r)) ->
forall (l : t elt) (x : key) (d : elt) (r : t elt), P l x d r (bal l x d r).
Lemma add_ind [elt : Type] [x : key] [d : elt] [P : t elt -> t elt -> Prop] :
(forall m : t elt, m = Leaf elt -> P (Leaf elt) (Node (Leaf elt) x d (Leaf elt) 1)) ->
(forall (m l : t elt) (y : key) (d' : elt) (r : t elt) (h : int),
m = Node l y d' r h ->
forall _x : X.lt x y,
X.compare x y = LT _x -> P l (add x d l) -> P (Node l y d' r h) (bal (add x d l) y d' r)) ->
(forall (m l : t elt) (y : key) (d' : elt) (r : t elt) (h : int),
m = Node l y d' r h ->
forall _x : X.eq x y, X.compare x y = EQ _x -> P (Node l y d' r h) (Node l y d r h)) ->
(forall (m l : t elt) (y : key) (d' : elt) (r : t elt) (h : int),
m = Node l y d' r h ->
forall _x : X.lt y x,
X.compare x y = GT _x -> P r (add x d r) -> P (Node l y d' r h) (bal l y d' (add x d r))) ->
forall m : t elt, P m (add x d m).
Lemma remove_min_ind [elt : Type] [P : t elt -> key -> elt -> t elt -> t elt * (key * elt) -> Prop] :
(forall (l : t elt) (x : key) (d : elt) (r : t elt),
l = Leaf elt -> P (Leaf elt) x d r (r, (x, d))) ->
(forall (l : t elt) (x : key) (d : elt) (r ll : t elt) (lx : key)
(ld : elt) (lr : t elt) (_x : int),
l = Node ll lx ld lr _x ->
P ll lx ld lr (remove_min ll lx ld lr) ->
forall (l' : t elt) (m : key * elt),
remove_min ll lx ld lr = (l', m) -> P (Node ll lx ld lr _x) x d r (bal l' x d r, m)) ->
forall (l : t elt) (x : key) (d : elt) (r : t elt), P l x d r (remove_min l x d r).
Lemma merge_ind [elt : Type] [P : t elt -> t elt -> t elt -> Prop] :
(forall s1 s2 : t elt, s1 = Leaf elt -> P (Leaf elt) s2 s2) ->
(forall (s1 s2 _x : t elt) (_x0 : key) (_x1 : elt) (_x2 : t elt) (_x3 : int),
s1 = Node _x _x0 _x1 _x2 _x3 -> s2 = Leaf elt -> P (Node _x _x0 _x1 _x2 _x3) (Leaf elt) s1) ->
(forall (s1 s2 _x : t elt) (_x0 : key) (_x1 : elt) (_x2 : t elt) (_x3 : int),
s1 = Node _x _x0 _x1 _x2 _x3 ->
forall (l2 : t elt) (x2 : key) (d2 : elt) (r2 : t elt) (_x4 : int),
s2 = Node l2 x2 d2 r2 _x4 ->
forall (s2' : t elt) (p : key * elt),
remove_min l2 x2 d2 r2 = (s2', p) ->
forall (x : key) (d : elt),
p = (x, d) -> P (Node _x _x0 _x1 _x2 _x3) (Node l2 x2 d2 r2 _x4) (bal s1 x d s2')) ->
forall s1 s2 : t elt, P s1 s2 (merge s1 s2).
Lemma remove_ind [elt : Type] [x : X.t] [P : t elt -> t elt -> Prop] :
(forall m : t elt, m = Leaf elt -> P (Leaf elt) (Leaf elt)) ->
(forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
m = Node l y d r _x ->
forall _x0 : X.lt x y,
X.compare x y = LT _x0 -> P l (remove x l) -> P (Node l y d r _x) (bal (remove x l) y d r)) ->
(forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
m = Node l y d r _x ->
forall _x0 : X.eq x y, X.compare x y = EQ _x0 -> P (Node l y d r _x) (merge l r)) ->
(forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
m = Node l y d r _x ->
forall _x0 : X.lt y x,
X.compare x y = GT _x0 -> P r (remove x r) -> P (Node l y d r _x) (bal l y d (remove x r))) ->
forall m : t elt, P m (remove x m).
Lemma concat_ind [elt : Type] [P : t elt -> t elt -> t elt -> Prop] :
(forall m1 m2 : t elt, m1 = Leaf elt -> P (Leaf elt) m2 m2) ->
(forall (m1 m2 _x : t elt) (_x0 : key) (_x1 : elt) (_x2 : t elt) (_x3 : int),
m1 = Node _x _x0 _x1 _x2 _x3 -> m2 = Leaf elt -> P (Node _x _x0 _x1 _x2 _x3) (Leaf elt) m1) ->
(forall (m1 m2 _x : t elt) (_x0 : key) (_x1 : elt) (_x2 : t elt) (_x3 : int),
m1 = Node _x _x0 _x1 _x2 _x3 ->
forall (l2 : t elt) (x2 : key) (d2 : elt) (r2 : t elt) (_x4 : int),
m2 = Node l2 x2 d2 r2 _x4 ->
forall (m2' : t elt) (xd : key * elt),
remove_min l2 x2 d2 r2 = (m2', xd) ->
P (Node _x _x0 _x1 _x2 _x3) (Node l2 x2 d2 r2 _x4) (join m1 xd#1 xd#2 m2')) ->
forall m1 m2 : t elt, P m1 m2 (concat m1 m2).
Lemma split_ind [elt : Type] [x : X.t] [P : t elt -> triple elt -> Prop] :
(forall m : t elt, m = Leaf elt -> P (Leaf elt) << Leaf elt, None, Leaf elt >>) ->
(forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
m = Node l y d r _x ->
forall _x0 : X.lt x y,
X.compare x y = LT _x0 ->
P l (split x l) ->
forall (ll : t elt) (o : option elt) (rl : t elt),
split x l = << ll, o, rl >> -> P (Node l y d r _x) << ll, o, join rl y d r >>) ->
(forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
m = Node l y d r _x ->
forall _x0 : X.eq x y, X.compare x y = EQ _x0 -> P (Node l y d r _x) << l, Some d, r >>) ->
(forall (m l : t elt) (y : key) (d : elt) (r : t elt) (_x : int),
m = Node l y d r _x ->
forall _x0 : X.lt y x,
X.compare x y = GT _x0 ->
P r (split x r) ->
forall (rl : t elt) (o : option elt) (rr : t elt),
split x r = << rl, o, rr >> -> P (Node l y d r _x) << join l y d rl, o, rr >>) ->
forall m : t elt, P m (split x m).
Lemma map_option_ind [elt elt' : Type] [f : key -> elt -> option elt'] [P : t elt -> t elt' -> Prop] :
(forall m : t elt, m = Leaf elt -> P (Leaf elt) (Leaf elt')) ->
(forall (m l : t elt) (x : key) (d : elt) (r : t elt) (_x : int),
m = Node l x d r _x ->
forall d' : elt',
f x d = Some d' ->
P l (map_option f l) ->
P r (map_option f r) -> P (Node l x d r _x) (join (map_option f l) x d' (map_option f r))) ->
(forall (m l : t elt) (x : key) (d : elt) (r : t elt) (_x : int),
m = Node l x d r _x ->
f x d = None ->
P l (map_option f l) ->
P r (map_option f r) -> P (Node l x d r _x) (concat (map_option f l) (map_option f r))) ->
forall m : t elt, P m (map_option f m).
Lemma map2_opt_ind [elt elt' elt'' : Type] [f : key -> elt -> option elt' -> option elt'']
[mapl : t elt -> t elt''] [mapr : t elt' -> t elt'']
[P : t elt -> t elt' -> t elt'' -> Prop] :
(forall (m1 : t elt) (m2 : t elt'), m1 = Leaf elt -> P (Leaf elt) m2 (mapr m2)) ->
(forall (m1 : t elt) (m2 : t elt') (l1 : t elt) (x1 : key) (d1 : elt) (r1 : t elt) (_x : int),
m1 = Node l1 x1 d1 r1 _x -> m2 = Leaf elt' -> P (Node l1 x1 d1 r1 _x) (Leaf elt') (mapl m1)) ->
(forall (m1 : t elt) (m2 : t elt') (l1 : t elt) (x1 : key) (d1 : elt) (r1 : t elt) (_x : int),
m1 = Node l1 x1 d1 r1 _x ->
forall (_x0 : t elt') (_x1 : key) (_x2 : elt') (_x3 : t elt') (_x4 : int),
m2 = Node _x0 _x1 _x2 _x3 _x4 ->
forall (l2' : t elt') (o2 : option elt') (r2' : t elt'),
split x1 m2 = << l2', o2, r2' >> ->
forall e : elt'',
f x1 d1 o2 = Some e ->
P l1 l2' (map2_opt f mapl mapr l1 l2') ->
P r1 r2' (map2_opt f mapl mapr r1 r2') ->
P (Node l1 x1 d1 r1 _x) (Node _x0 _x1 _x2 _x3 _x4)
(join (map2_opt f mapl mapr l1 l2') x1 e (map2_opt f mapl mapr r1 r2'))) ->
(forall (m1 : t elt) (m2 : t elt') (l1 : t elt) (x1 : key) (d1 : elt) (r1 : t elt) (_x : int),
m1 = Node l1 x1 d1 r1 _x ->
forall (_x0 : t elt') (_x1 : key) (_x2 : elt') (_x3 : t elt') (_x4 : int),
m2 = Node _x0 _x1 _x2 _x3 _x4 ->
forall (l2' : t elt') (o2 : option elt') (r2' : t elt'),
split x1 m2 = << l2', o2, r2' >> ->
f x1 d1 o2 = None ->
P l1 l2' (map2_opt f mapl mapr l1 l2') ->
P r1 r2' (map2_opt f mapl mapr r1 r2') ->
P (Node l1 x1 d1 r1 _x) (Node _x0 _x1 _x2 _x3 _x4)
(concat (map2_opt f mapl mapr l1 l2') (map2_opt f mapl mapr r1 r2'))) ->
forall (m1 : t elt) (m2 : t elt'), P m1 m2 (map2_opt f mapl mapr m1 m2).
#[global]
Hint Constructors tree MapsTo In bst : core.
#[global]
Hint Unfold lt_tree gt_tree : core.
Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h)
"as" ident(s) :=
set (s:=Node l x d r h) in *; clearbody s; clear l x d r h.
A tactic for cleaning hypothesis after use of functional induction.
Ltac clearf :=
match goal with
| H := _ |- _ => subst; subst H; clearf
| H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf
| H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf
| _ => idtac
end.
A tactic to repeat inversion_clear on all hyps of the
form (f (Node ...))
Ltac inv f :=
match goal with
| H:f (Leaf _) |- _ => inversion_clear H; inv f
| H:f _ (Leaf _) |- _ => inversion_clear H; inv f
| H:f _ _ (Leaf _) |- _ => inversion_clear H; inv f
| H:f _ _ _ (Leaf _) |- _ => inversion_clear H; inv f
| H:f (Node _ _ _ _ _) |- _ => inversion_clear H; inv f
| H:f _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f
| H:f _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f
| H:f _ _ _ (Node _ _ _ _ _) |- _ => inversion_clear H; inv f
| _ => idtac
end.
Ltac inv_all f :=
match goal with
| H: f _ |- _ => inversion_clear H; inv f
| H: f _ _ |- _ => inversion_clear H; inv f
| H: f _ _ _ |- _ => inversion_clear H; inv f
| H: f _ _ _ _ |- _ => inversion_clear H; inv f
| _ => idtac
end.
Helper tactic concerning order of elements.
Ltac order := match goal with
| U: lt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order
| U: gt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order
| _ => MX.order
end.
Ltac intuition_in := repeat (intuition auto; inv In; inv MapsTo).
Ltac join_tac :=
intros ?l; induction l as [| ?ll _ ?lx ?ld ?lr ?Hlr ?lh];
[ | intros ?x ?d ?r; induction r as [| ?rl ?Hrl ?rx ?rd ?rr _ ?rh]; unfold join;
[ | destruct (gt_le_dec lh (rh+2)) as [?GT|?LE];
[ match goal with |- context [ bal ?u ?v ?w ?z ] =>
replace (bal u v w z)
with (bal ll lx ld (join lr x d (Node rl rx rd rr rh))); [ | auto]
end
| destruct (gt_le_dec rh (lh+2)) as [?GT'|?LE'];
[ match goal with |- context [ bal ?u ?v ?w ?z ] =>
replace (bal u v w z)
with (bal (join (Node ll lx ld lr lh) x d rl) rx rd rr); [ | auto]
end
| ] ] ] ]; intros.
Section Elt.
Variable elt:Type.
Implicit Types m r : t elt.
Lemma MapsTo_In : forall k e m, MapsTo k e m -> In k m.
#[local]
Hint Resolve MapsTo_In : core.
Lemma In_MapsTo : forall k m, In k m -> exists e, MapsTo k e m.
Lemma In_alt : forall k m, In0 k m <-> In k m.
Lemma MapsTo_1 :
forall m x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m.
#[local]
Hint Immediate MapsTo_1 : core.
Lemma In_1 :
forall m x y, X.eq x y -> In x m -> In y m.
Lemma In_node_iff :
forall l x e r h y,
In y (Node l x e r h) <-> In y l \/ X.eq y x \/ In y r.
Results about lt_tree and gt_tree
Lemma lt_leaf : forall x, lt_tree x (Leaf elt).
Lemma gt_leaf : forall x, gt_tree x (Leaf elt).
Lemma lt_tree_node : forall x y l r e h,
lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y e r h).
Lemma gt_tree_node : forall x y l r e h,
gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y e r h).
#[local]
Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.
Lemma lt_left : forall x y l r e h,
lt_tree x (Node l y e r h) -> lt_tree x l.
Lemma lt_right : forall x y l r e h,
lt_tree x (Node l y e r h) -> lt_tree x r.
Lemma gt_left : forall x y l r e h,
gt_tree x (Node l y e r h) -> gt_tree x l.
Lemma gt_right : forall x y l r e h,
gt_tree x (Node l y e r h) -> gt_tree x r.
#[local]
Hint Resolve lt_left lt_right gt_left gt_right : core.
Lemma lt_tree_not_in :
forall x m, lt_tree x m -> ~ In x m.
Lemma lt_tree_trans :
forall x y, X.lt x y -> forall m, lt_tree x m -> lt_tree y m.
Lemma gt_tree_not_in :
forall x m, gt_tree x m -> ~ In x m.
Lemma gt_tree_trans :
forall x y, X.lt y x -> forall m, gt_tree x m -> gt_tree y m.
#[local]
Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.
Definition Empty m := forall (a:key)(e:elt) , ~ MapsTo a e m.
Lemma empty_bst : bst (empty elt).
Lemma empty_1 : Empty (empty elt).
Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true.
Lemma mem_2 : forall m x, mem x m = true -> In x m.
Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e.
Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
Lemma find_iff : forall m x e, bst m ->
(find x m = Some e <-> MapsTo x e m).
Lemma find_in : forall m x, find x m <> None -> In x m.
Lemma in_find : forall m x, bst m -> In x m -> find x m <> None.
Lemma find_in_iff : forall m x, bst m ->
(find x m <> None <-> In x m).
Lemma not_find_iff : forall m x, bst m ->
(find x m = None <-> ~In x m).
Lemma find_find : forall m m' x,
find x m = find x m' <->
(forall d, find x m = Some d <-> find x m' = Some d).
Lemma find_mapsto_equiv : forall m m' x, bst m -> bst m' ->
(find x m = find x m' <->
(forall d, MapsTo x d m <-> MapsTo x d m')).
Lemma find_in_equiv : forall m m' x, bst m -> bst m' ->
find x m = find x m' ->
(In x m <-> In x m').
Lemma create_bst :
forall l x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r ->
bst (create l x e r).
#[local]
Hint Resolve create_bst : core.
Lemma create_in :
forall l x e r y,
In y (create l x e r) <-> X.eq y x \/ In y l \/ In y r.
Lemma bal_bst : forall l x e r, bst l -> bst r ->
lt_tree x l -> gt_tree x r -> bst (bal l x e r).
#[local]
Hint Resolve bal_bst : core.
Lemma bal_in : forall l x e r y,
In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r.
Lemma bal_mapsto : forall l x e r y e',
MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r).
Lemma bal_find : forall l x e r y,
bst l -> bst r -> lt_tree x l -> gt_tree x r ->
find y (bal l x e r) = find y (create l x e r).
Lemma add_in : forall m x y e,
In y (add x e m) <-> X.eq y x \/ In y m.
Lemma add_bst : forall m x e, bst m -> bst (add x e m).
#[local]
Hint Resolve add_bst : core.
Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
Lemma add_2 : forall m x y e e', ~X.eq x y ->
MapsTo y e m -> MapsTo y e (add x e' m).
Lemma add_3 : forall m x y e e', ~X.eq x y ->
MapsTo y e (add x e' m) -> MapsTo y e m.
Lemma add_find : forall m x y e, bst m ->
find y (add x e m) =
match X.compare y x with EQ _ => Some e | _ => find y m end.
Lemma remove_min_in : forall l x e r h y,
In y (Node l x e r h) <->
X.eq y (remove_min l x e r)#2#1 \/ In y (remove_min l x e r)#1.
Lemma remove_min_mapsto : forall l x e r h y e',
MapsTo y e' (Node l x e r h) <->
((X.eq y (remove_min l x e r)#2#1) /\ e' = (remove_min l x e r)#2#2)
\/ MapsTo y e' (remove_min l x e r)#1.
Lemma remove_min_bst : forall l x e r h,
bst (Node l x e r h) -> bst (remove_min l x e r)#1.
#[local]
Hint Resolve remove_min_bst : core.
Lemma remove_min_gt_tree : forall l x e r h,
bst (Node l x e r h) ->
gt_tree (remove_min l x e r)#2#1 (remove_min l x e r)#1.
#[local]
Hint Resolve remove_min_gt_tree : core.
Lemma remove_min_find : forall l x e r h y,
bst (Node l x e r h) ->
find y (Node l x e r h) =
match X.compare y (remove_min l x e r)#2#1 with
| LT _ => None
| EQ _ => Some (remove_min l x e r)#2#2
| GT _ => find y (remove_min l x e r)#1
end.
Lemma merge_in : forall m1 m2 y, bst m1 -> bst m2 ->
(In y (merge m1 m2) <-> In y m1 \/ In y m2).
Lemma merge_mapsto : forall m1 m2 y e, bst m1 -> bst m2 ->
(MapsTo y e (merge m1 m2) <-> MapsTo y e m1 \/ MapsTo y e m2).
Lemma merge_bst : forall m1 m2, bst m1 -> bst m2 ->
(forall y1 y2 : key, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
bst (merge m1 m2).
Lemma remove_in : forall m x y, bst m ->
(In y (remove x m) <-> ~ X.eq y x /\ In y m).
Lemma remove_bst : forall m x, bst m -> bst (remove x m).
Lemma remove_1 : forall m x y, bst m -> X.eq x y -> ~ In y (remove x m).
Lemma remove_2 : forall m x y e, bst m -> ~X.eq x y ->
MapsTo y e m -> MapsTo y e (remove x m).
Lemma remove_3 : forall m x y e, bst m ->
MapsTo y e (remove x m) -> MapsTo y e m.
Lemma join_in : forall l x d r y,
In y (join l x d r) <-> X.eq y x \/ In y l \/ In y r.
Lemma join_bst : forall l x d r, bst l -> bst r ->
lt_tree x l -> gt_tree x r -> bst (join l x d r).
#[local]
Hint Resolve join_bst : core.
Lemma join_find : forall l x d r y,
bst l -> bst r -> lt_tree x l -> gt_tree x r ->
find y (join l x d r) = find y (create l x d r).
Lemma split_in_1 : forall m x, bst m -> forall y,
(In y (split x m)#l <-> In y m /\ X.lt y x).
Lemma split_in_2 : forall m x, bst m -> forall y,
(In y (split x m)#r <-> In y m /\ X.lt x y).
Lemma split_in_3 : forall m x, bst m ->
(split x m)#o = find x m.
Lemma split_bst : forall m x, bst m ->
bst (split x m)#l /\ bst (split x m)#r.
Lemma split_lt_tree : forall m x, bst m -> lt_tree x (split x m)#l.
Lemma split_gt_tree : forall m x, bst m -> gt_tree x (split x m)#r.
Lemma split_find : forall m x y, bst m ->
find y m = match X.compare y x with
| LT _ => find y (split x m)#l
| EQ _ => (split x m)#o
| GT _ => find y (split x m)#r
end.
Lemma concat_in : forall m1 m2 y,
In y (concat m1 m2) <-> In y m1 \/ In y m2.
Lemma concat_bst : forall m1 m2, bst m1 -> bst m2 ->
(forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
bst (concat m1 m2).
#[local]
Hint Resolve concat_bst : core.
Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 ->
(forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
find y (concat m1 m2) =
match find y m2 with Some d => Some d | None => find y m1 end.
Notation eqk := (PX.eqk (elt:= elt)).
Notation eqke := (PX.eqke (elt:= elt)).
Notation ltk := (PX.ltk (elt:= elt)).
Lemma elements_aux_mapsto : forall (s:t elt) acc x e,
InA eqke (x,e) (elements_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc.
Lemma elements_mapsto : forall (s:t elt) x e, InA eqke (x,e) (elements s) <-> MapsTo x e s.
Lemma elements_in : forall (s:t elt) x, L.PX.In x (elements s) <-> In x s.
Lemma elements_aux_sort : forall (s:t elt) acc, bst s -> sort ltk acc ->
(forall x e y, InA eqke (x,e) acc -> In y s -> X.lt y x) ->
sort ltk (elements_aux acc s).
Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s).
#[local]
Hint Resolve elements_sort : core.
Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s).
Lemma elements_aux_cardinal :
forall (m:t elt) acc, (length acc + cardinal m)%nat = length (elements_aux acc m).
Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m).
Lemma elements_app :
forall (s:t elt) acc, elements_aux acc s = elements s ++ acc.
Lemma elements_node :
forall (t1 t2:t elt) x e z l,
elements t1 ++ (x,e) :: elements t2 ++ l =
elements (Node t1 x e t2 z) ++ l.
Definition fold' (A : Type) (f : key -> elt -> A -> A)(s : t elt) :=
L.fold f (elements s).
Lemma fold_equiv_aux :
forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A) acc,
L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a).
Lemma fold_equiv :
forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A),
fold f s a = fold' f s a.
Lemma fold_1 :
forall (s:t elt)(Hs:bst s)(A : Type)(i:A)(f : key -> elt -> A -> A),
fold f s i = fold_left (fun a p => f p#1 p#2 a) (elements s) i.
Comparison
Fixpoint flatten_e (e : enumeration elt) : list (key*elt) := match e with
| End _ => nil
| More x e t r => (x,e) :: elements t ++ flatten_e r
end.
Lemma flatten_e_elements :
forall (l:t elt) r x d z e,
elements l ++ flatten_e (More x d r e) =
elements (Node l x d r z) ++ flatten_e e.
Lemma cons_1 : forall (s:t elt) e,
flatten_e (cons s e) = elements s ++ flatten_e e.
Proof of correction for the comparison
Variable cmp : elt->elt->bool.
Definition IfEq b l1 l2 := L.equal cmp l1 l2 = b.
Lemma cons_IfEq : forall b x1 x2 d1 d2 l1 l2,
X.eq x1 x2 -> cmp d1 d2 = true ->
IfEq b l1 l2 ->
IfEq b ((x1,d1)::l1) ((x2,d2)::l2).
Lemma equal_end_IfEq : forall e2,
IfEq (equal_end e2) nil (flatten_e e2).
Lemma equal_more_IfEq :
forall x1 d1 (cont:enumeration elt -> bool) x2 d2 r2 e2 l,
IfEq (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) ->
IfEq (equal_more cmp x1 d1 cont (More x2 d2 r2 e2)) ((x1,d1)::l)
(flatten_e (More x2 d2 r2 e2)).
Lemma equal_cont_IfEq : forall m1 cont e2 l,
(forall e, IfEq (cont e) l (flatten_e e)) ->
IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2).
Lemma equal_IfEq : forall (m1 m2:t elt),
IfEq (equal cmp m1 m2) (elements m1) (elements m2).
Definition Equivb m m' :=
(forall k, In k m <-> In k m') /\
(forall k e e', MapsTo k e m -> MapsTo k e' m' -> cmp e e' = true).
Lemma Equivb_elements : forall s s',
Equivb s s' <-> L.Equivb cmp (elements s) (elements s').
Lemma equal_Equivb : forall (s s': t elt), bst s -> bst s' ->
(equal cmp s s' = true <-> Equivb s s').
End Elt.
Section Map.
Variable elt elt' : Type.
Variable f : elt -> elt'.
Lemma map_1 : forall (m: t elt)(x:key)(e:elt),
MapsTo x e m -> MapsTo x (f e) (map f m).
Lemma map_2 : forall (m: t elt)(x:key),
In x (map f m) -> In x m.
Lemma map_bst : forall m, bst m -> bst (map f m).
End Map.
Section Mapi.
Variable elt elt' : Type.
Variable f : key -> elt -> elt'.
Lemma mapi_1 : forall (m: tree elt)(x:key)(e:elt),
MapsTo x e m -> exists y, X.eq y x /\ MapsTo x (f y e) (mapi f m).
Lemma mapi_2 : forall (m: t elt)(x:key),
In x (mapi f m) -> In x m.
Lemma mapi_bst : forall m, bst m -> bst (mapi f m).
End Mapi.
Section Map_option.
Variable elt elt' : Type.
Variable f : key -> elt -> option elt'.
Hypothesis f_compat : forall x x' d, X.eq x x' -> f x d = f x' d.
Lemma map_option_2 : forall (m:t elt)(x:key),
In x (map_option f m) -> exists d, MapsTo x d m /\ f x d <> None.
Lemma map_option_bst : forall m, bst m -> bst (map_option f m).
#[local]
Hint Resolve map_option_bst : core.
Ltac nonify e :=
replace e with (@None elt) by
(symmetry; rewrite not_find_iff; auto; intro; order).
Lemma map_option_find : forall (m:t elt)(x:key),
bst m ->
find x (map_option f m) =
match (find x m) with Some d => f x d | None => None end.
End Map_option.
Section Map2_opt.
Variable elt elt' elt'' : Type.
Variable f0 : key -> option elt -> option elt' -> option elt''.
Variable f : key -> elt -> option elt' -> option elt''.
Variable mapl : t elt -> t elt''.
Variable mapr : t elt' -> t elt''.
Hypothesis f0_f : forall x d o, f x d o = f0 x (Some d) o.
Hypothesis mapl_bst : forall m, bst m -> bst (mapl m).
Hypothesis mapr_bst : forall m', bst m' -> bst (mapr m').
Hypothesis mapl_f0 : forall x m, bst m ->
find x (mapl m) =
match find x m with Some d => f0 x (Some d) None | None => None end.
Hypothesis mapr_f0 : forall x m', bst m' ->
find x (mapr m') =
match find x m' with Some d' => f0 x None (Some d') | None => None end.
Hypothesis f0_compat : forall x x' o o', X.eq x x' -> f0 x o o' = f0 x' o o'.
Notation map2_opt := (map2_opt f mapl mapr).
Lemma map2_opt_2 : forall m m' y, bst m -> bst m' ->
In y (map2_opt m m') -> In y m \/ In y m'.
Lemma map2_opt_bst : forall m m', bst m -> bst m' ->
bst (map2_opt m m').
#[local]
Hint Resolve map2_opt_bst : core.
Ltac map2_aux :=
match goal with
| H : In ?x _ \/ In ?x ?m,
H' : find ?x ?m = find ?x ?m', B:bst ?m, B':bst ?m' |- _ =>
destruct H; [ intuition_in; order |
rewrite <-(find_in_equiv B B' H'); auto ]
end.
Ltac nonify t :=
match t with (find ?y (map2_opt ?m ?m')) =>
replace t with (@None elt'');
[ | symmetry; rewrite not_find_iff; auto; intro;
destruct (@map2_opt_2 m m' y); auto; order ]
end.
Lemma map2_opt_1 : forall m m' y, bst m -> bst m' ->
In y m \/ In y m' ->
find y (map2_opt m m') = f0 y (find y m) (find y m').
End Map2_opt.
Section Map2.
Variable elt elt' elt'' : Type.
Variable f : option elt -> option elt' -> option elt''.
Lemma map2_bst : forall m m', bst m -> bst m' -> bst (map2 f m m').
Lemma map2_1 : forall m m' y, bst m -> bst m' ->
In y m \/ In y m' -> find y (map2 f m m') = f (find y m) (find y m').
Lemma map2_2 : forall m m' y, bst m -> bst m' ->
In y (map2 f m m') -> In y m \/ In y m'.
End Map2.
End Proofs.
End Raw.
Encapsulation
Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
Module E := X.
Module Raw := Raw I X.
Import Raw.Proofs.
#[universes(template)]
Record bst (elt:Type) :=
Bst {this :> Raw.tree elt; is_bst : Raw.bst this}.
Definition t := bst.
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 := Bst (empty_bst elt).
Definition is_empty m : bool := Raw.is_empty (this m).
Definition add x e m : t elt := Bst (add_bst x e (is_bst m)).
Definition remove x m : t elt := Bst (remove_bst x (is_bst m)).
Definition mem x m : bool := Raw.mem x (this m).
Definition find x m : option elt := Raw.find x (this m).
Definition map f m : t elt' := Bst (map_bst f (is_bst m)).
Definition mapi (f:key->elt->elt') m : t elt' :=
Bst (mapi_bst f (is_bst m)).
Definition map2 f m (m':t elt') : t elt'' :=
Bst (map2_bst f (is_bst m) (is_bst m')).
Definition elements m : list (key*elt) := Raw.elements (this m).
Definition cardinal m := Raw.cardinal (this m).
Definition fold (A:Type) (f:key->elt->A->A) m i := Raw.fold (A:=A) f (this m) i.
Definition equal cmp m m' : bool := Raw.equal cmp (this m) (this m').
Definition MapsTo x e m : Prop := Raw.MapsTo x e (this m).
Definition In x m : Prop := Raw.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.
Lemma mem_1 : forall m x, In x m -> mem x m = true.
Lemma mem_2 : forall m x, mem x m = true -> In x m.
Lemma empty_1 : Empty empty.
Lemma is_empty_1 : forall m, Empty m -> is_empty m = true.
Lemma is_empty_2 : forall m, is_empty m = true -> Empty m.
Lemma add_1 : forall m x y e, E.eq x y -> MapsTo y e (add x e m).
Lemma add_2 : forall m x y e e', ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m).
Lemma add_3 : forall m x y e e', ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m.
Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m).
Lemma remove_2 : forall m x y e, ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m).
Lemma remove_3 : forall m x y e, MapsTo y e (remove x m) -> MapsTo y e m.
Lemma find_1 : forall m x e, MapsTo x e m -> find x m = Some e.
Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
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.
Lemma elements_1 : forall m x e,
MapsTo x e m -> InA eq_key_elt (x,e) (elements m).
Lemma elements_2 : forall m x e,
InA eq_key_elt (x,e) (elements m) -> MapsTo x e m.
Lemma elements_3 : forall m, sort lt_key (elements m).
Lemma elements_3w : forall m, NoDupA eq_key (elements m).
Lemma cardinal_1 : forall m, cardinal m = length (elements m).
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'.
Lemma equal_1 : forall m m' cmp,
Equivb cmp m m' -> equal cmp m m' = true.
Lemma equal_2 : forall m m' cmp,
equal cmp m m' = true -> Equivb cmp m m'.
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).
Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m.
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).
Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
(f:key->elt->elt'), In x (mapi f m) -> In x m.
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').
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'.
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).
Module LO := FMapList.Make_ord(X)(D).
Module R := Raw.
Module P := Raw.Proofs.
Definition t := MapS.t D.t.
Definition cmp e e' :=
match D.compare e e' with EQ _ => true | _ => false end.
One step of comparison of elements
Definition compare_more x1 d1 (cont:R.enumeration D.t -> comparison) e2 :=
match e2 with
| R.End _ => Gt
| R.More x2 d2 r2 e2 =>
match X.compare x1 x2 with
| EQ _ => match D.compare d1 d2 with
| EQ _ => cont (R.cons r2 e2)
| LT _ => Lt
| GT _ => Gt
end
| LT _ => Lt
| GT _ => Gt
end
end.
Comparison of left tree, middle element, then right tree
Fixpoint compare_cont s1 (cont:R.enumeration D.t -> comparison) e2 :=
match s1 with
| R.Leaf _ => cont e2
| R.Node l1 x1 d1 r1 _ =>
compare_cont l1 (compare_more x1 d1 (compare_cont r1 cont)) e2
end.
Initial continuation
The complete comparison
Correctness of this comparison
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).
#[global]
Hint Resolve cons_Cmp : core.
Lemma compare_end_Cmp :
forall e2, Cmp (compare_end e2) nil (P.flatten_e e2).
Lemma compare_more_Cmp : forall x1 d1 cont x2 d2 r2 e2 l,
Cmp (cont (R.cons r2 e2)) l (R.elements r2 ++ P.flatten_e e2) ->
Cmp (compare_more x1 d1 cont (R.More x2 d2 r2 e2)) ((x1,d1)::l)
(P.flatten_e (R.More x2 d2 r2 e2)).
Lemma compare_cont_Cmp : forall s1 cont e2 l,
(forall e, Cmp (cont e) l (P.flatten_e e)) ->
Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2).
Lemma compare_Cmp : forall s1 s2,
Cmp (compare_pure s1 s2) (R.elements s1) (R.elements s2).
The dependent-style compare
Definition eq (m1 m2 : t) := LO.eq_list (elements m1) (elements m2).
Definition lt (m1 m2 : t) := LO.lt_list (elements m1) (elements m2).
Definition compare (s s':t) : Compare lt eq s s'.
Definition selements (m1 : t) :=
LO.MapS.Build_slist (P.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.
Lemma lt_slt : forall m1 m2, lt m1 m2 <-> slt m1 m2.
Lemma eq_1 : forall (m m' : t), Equivb cmp m m' -> eq m m'.
Lemma eq_2 : forall m m', eq m m' -> Equivb cmp m m'.
Lemma eq_refl : forall m : t, eq m m.
Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1.
Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3.
Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2.
End IntMake_ord.
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).