diff options
Diffstat (limited to 'theories')
-rw-r--r-- | theories/FSets/FMapAVL.v | 2026 | ||||
-rw-r--r-- | theories/FSets/FMapIntMap.v | 622 | ||||
-rw-r--r-- | theories/FSets/FMapPositive.v | 1153 | ||||
-rw-r--r-- | theories/FSets/FMaps.v | 5 | ||||
-rw-r--r-- | theories/FSets/FSetAVL.v | 2883 | ||||
-rw-r--r-- | theories/FSets/FSetToFiniteSet.v | 139 | ||||
-rw-r--r-- | theories/FSets/FSets.v | 3 | ||||
-rw-r--r-- | theories/FSets/Int.v | 421 | ||||
-rw-r--r-- | theories/FSets/OrderedTypeAlt.v | 129 | ||||
-rw-r--r-- | theories/FSets/OrderedTypeEx.v | 248 |
10 files changed, 7629 insertions, 0 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v new file mode 100644 index 000000000..a24b1adbf --- /dev/null +++ b/theories/FSets/FMapAVL.v @@ -0,0 +1,2026 @@ + +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite map library. *) + +(* $Id$ *) + +(** This module implements map using AVL trees. + It follows the implementation from Ocaml's standard library. *) + +Require Import FSetInterface. +Require Import FMapInterface. +Require Import FMapList. + +Require Import ZArith. +Require Import Int. + +Set Firstorder Depth 3. +Set Implicit Arguments. +Unset Strict Implicit. + + +Module Raw (I:Int)(X: OrderedType). +Import I. +Module II:=MoreInt(I). +Import II. +Open Scope Int_scope. + +Module E := X. +Module MX := OrderedTypeFacts X. +Module PX := KeyOrderedType X. +Module L := FMapList.Raw X. +Import MX. +Import PX. + +Definition key := X.t. + +(** * Trees *) + +Section Elt. + +Variable elt : Set. + +(* Now in KeyOrderedType: +Definition eqk (p p':key*elt) := X.eq (fst p) (fst p'). +Definition eqke (p p':key*elt) := + X.eq (fst p) (fst p') /\ (snd p) = (snd p'). +Definition ltk (p p':key*elt) := X.lt (fst p) (fst p'). +*) + +Notation eqk := (eqk (elt:= elt)). +Notation eqke := (eqke (elt:= elt)). +Notation ltk := (ltk (elt:= elt)). + +Inductive tree : Set := + | Leaf : tree + | Node : tree -> key -> elt -> tree -> int -> tree. + +Notation t := tree. + +(** The Sixth field of [Node] is the height of the tree *) + +(** * Occurrence in a tree *) + +Inductive MapsTo (x : key)(e : elt) : tree -> 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) : tree -> 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:key)(m:t) : Prop := exists e:elt, MapsTo k e m. + +(** * Binary search trees *) + +(** [lt_tree x s]: all elements in [s] are smaller than [x] + (resp. greater for [gt_tree]) *) + +Definition lt_tree x s := forall y:key, In y s -> X.lt y x. +Definition gt_tree x s := forall y:key, In y s -> X.lt x y. + +(** [bst t] : [t] is a binary search tree *) + +Inductive bst : tree -> 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). + +(** * 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 *) + +Definition height (s : tree) : int := + match s with + | Leaf => 0 + | Node _ _ _ _ h => h + end. + +Inductive avl : tree -> 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). + +(* We should end this section before the big proofs that follows, + otherwise the discharge takes a lot of time. *) +End Elt. + +(** Some helpful hints and tactics. *) + +Notation t := tree. +Hint Constructors tree. +Hint Constructors MapsTo. +Hint Constructors In. +Hint Constructors bst. +Hint Constructors avl. +Hint Unfold lt_tree gt_tree. + +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 safe_inv f := match goal with + | H:f (Node _ _ _ _ _) |- _ => + generalize H; inversion_clear H; safe_inv f + | H:f _ (Node _ _ _ _ _) |- _ => + generalize H; inversion_clear H; safe_inv f + | _ => intros + 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. + +Ltac order := match goal with + | H: lt_tree ?x ?s, H1: In ?y ?s |- _ => generalize (H _ H1); clear H; order + | H: gt_tree ?x ?s, H1: In ?y ?s |- _ => generalize (H _ H1); clear H; order + | _ => MX.order +end. + +Ltac intuition_in := repeat progress (intuition; inv In; inv MapsTo). +Ltac firstorder_in := repeat progress (firstorder; inv In; inv MapsTo). + +Lemma height_non_negative : forall elt (s : t elt), avl s -> height s >= 0. +Proof. + induction s; simpl; intros; auto with zarith. + 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. + + +(** Facts about [MapsTo] and [In]. *) + +Lemma MapsTo_In : forall elt k e (m:t elt), MapsTo k e m -> In k m. +Proof. + induction 1; auto. +Qed. +Hint Resolve MapsTo_In. + +Lemma In_MapsTo : forall elt k (m:t elt), In k m -> exists e, MapsTo k e m. +Proof. + induction 1; try destruct IHIn as (e,He); exists e; auto. +Qed. + +Lemma In_alt : forall elt k (m:t elt), In0 k m <-> In k m. +Proof. + split. + intros (e,H); eauto. + unfold In0; apply In_MapsTo; auto. +Qed. + +Lemma MapsTo_1 : + forall elt (m:t elt) x y e, X.eq x y -> MapsTo x e m -> MapsTo y e m. +Proof. + induction m; simpl; intuition_in; eauto. +Qed. +Hint Immediate MapsTo_1. + +Lemma In_1 : + forall elt (m:t elt) x y, X.eq x y -> In x m -> In y m. +Proof. + intros elt m x y; induction m; simpl; intuition_in; eauto. +Qed. + + +(** Results about [lt_tree] and [gt_tree] *) + +Lemma lt_leaf : forall elt x, lt_tree x (Leaf elt). +Proof. + unfold lt_tree in |- *; intros; intuition_in. +Qed. + +Lemma gt_leaf : forall elt x, gt_tree x (Leaf elt). +Proof. + unfold gt_tree in |- *; intros; intuition_in. +Qed. + +Lemma lt_tree_node : forall elt x y (l:t elt) r e h, + lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y e r h). +Proof. + unfold lt_tree in *; firstorder_in; order. +Qed. + +Lemma gt_tree_node : forall elt x y (l:t elt) r e h, + gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y e r h). +Proof. + unfold gt_tree in *; firstorder_in; order. +Qed. + +Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. + +Lemma lt_left : forall elt x y (l: t elt) r e h, + lt_tree x (Node l y e r h) -> lt_tree x l. +Proof. + intuition_in. +Qed. + +Lemma lt_right : forall elt x y (l:t elt) r e h, + lt_tree x (Node l y e r h) -> lt_tree x r. +Proof. + intuition_in. +Qed. + +Lemma gt_left : forall elt x y (l:t elt) r e h, + gt_tree x (Node l y e r h) -> gt_tree x l. +Proof. + intuition_in. +Qed. + +Lemma gt_right : forall elt x y (l:t elt) r e h, + gt_tree x (Node l y e r h) -> gt_tree x r. +Proof. + intuition_in. +Qed. + +Hint Resolve lt_left lt_right gt_left gt_right. + +Lemma lt_tree_not_in : + forall elt x (t : t elt), lt_tree x t -> ~ In x t. +Proof. + intros; intro; generalize (H _ H0); order. +Qed. + +Lemma lt_tree_trans : + forall elt x y, X.lt x y -> forall (t:t elt), lt_tree x t -> lt_tree y t. +Proof. + firstorder eauto. +Qed. + +Lemma gt_tree_not_in : + forall elt x (t : t elt), gt_tree x t -> ~ In x t. +Proof. + intros; intro; generalize (H _ H0); order. +Qed. + +Lemma gt_tree_trans : + forall elt x y, X.lt y x -> forall (t:t elt), gt_tree x t -> gt_tree y t. +Proof. + firstorder eauto. +Qed. + +Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. + +(** Results about [avl] *) + +Lemma avl_node : forall elt x e (l:t elt) r, + avl l -> + avl r -> + -(2) <= height l - height r <= 2 -> + avl (Node l x e r (max (height l) (height r) + 1)). +Proof. + intros; auto. +Qed. +Hint Resolve avl_node. + +(** * Helper functions *) + +(** [create l x r] creates a node, assuming [l] and [r] + to be balanced and [|height l - height r| <= 2]. *) + +Definition create elt (l:t elt) x e r := + Node l x e r (max (height l) (height r) + 1). + +Lemma create_bst : + forall elt (l:t elt) x e r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> + bst (create l x e r). +Proof. + unfold create; auto. +Qed. +Hint Resolve create_bst. + +Lemma create_avl : + forall elt (l:t elt) x e r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> + avl (create l x e r). +Proof. + unfold create; auto. +Qed. + +Lemma create_height : + forall elt (l:t elt) 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. +Proof. + unfold create; intros; auto. +Qed. + +Lemma create_in : + forall elt (l:t elt) x e r y, In y (create l x e r) <-> X.eq y x \/ In y l \/ In y r. +Proof. + unfold create; split; [ inversion_clear 1 | ]; intuition. +Qed. + +(** trick for emulating [assert false] in Coq *) + +Notation assert_false := Leaf. + +(** [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 bal elt (l: tree elt) x e 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 _ + | Node ll lx le lr _ => + if ge_lt_dec (height ll) (height lr) then + create ll lx le (create lr x e r) + else + match lr with + | Leaf => assert_false _ + | Node lrl lrx lre lrr _ => + create (create ll lx le lrl) lrx lre (create lrr x e r) + end + end + else + if gt_le_dec hr (hl+2) then + match r with + | Leaf => assert_false _ + | Node rl rx re rr _ => + if ge_lt_dec (height rr) (height rl) then + create (create l x e rl) rx re rr + else + match rl with + | Leaf => assert_false _ + | Node rll rlx rle rlr _ => + create (create l x e rll) rlx rle (create rlr rx re rr) + end + end + else + create l x e r. + +Ltac bal_tac := + intros elt l x e r; + unfold bal; + destruct (gt_le_dec (height l) (height r + 2)); + [ destruct l as [ |ll lx le lr lh]; + [ | destruct (ge_lt_dec (height ll) (height lr)); + [ | destruct lr ] ] + | destruct (gt_le_dec (height r) (height l + 2)); + [ destruct r as [ |rl rx re rr rh]; + [ | destruct (ge_lt_dec (height rr) (height rl)); + [ | destruct rl ] ] + | ] ]; intros. + +Ltac bal_tac_imp := match goal with + | |- context [ assert_false ] => + inv avl; avl_nns; simpl in *; false_omega + | _ => idtac +end. + +Lemma bal_bst : forall elt (l:t elt) x e r, bst l -> bst r -> + lt_tree x l -> gt_tree x r -> bst (bal l x e r). +Proof. + bal_tac; + inv bst; repeat apply create_bst; auto; unfold create; + apply lt_tree_node || apply gt_tree_node; auto; + eapply lt_tree_trans || eapply gt_tree_trans || eauto; eauto. +Qed. + +Lemma bal_avl : forall elt (l:t elt) x e r, avl l -> avl r -> + -(3) <= height l - height r <= 3 -> avl (bal l x e r). +Proof. + bal_tac; inv avl; repeat apply create_avl; simpl in *; auto; omega_max. +Qed. + +Lemma bal_height_1 : forall elt (l:t elt) 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. +Proof. + bal_tac; inv avl; avl_nns; simpl in *; omega_max. +Qed. + +Lemma bal_height_2 : + forall elt (l:t elt) 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. +Proof. + bal_tac; inv avl; simpl in *; omega_max. +Qed. + +Lemma bal_in : forall elt (l:t elt) x e r y, avl l -> avl r -> + (In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r). +Proof. + bal_tac; bal_tac_imp; repeat rewrite create_in; intuition_in. +Qed. + +Lemma bal_mapsto : forall elt (l:t elt) x e r y e', avl l -> avl r -> + (MapsTo y e' (bal l x e r) <-> MapsTo y e' (create l x e r)). +Proof. + bal_tac; bal_tac_imp; unfold create; intuition_in. +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 *) + +Fixpoint add (elt:Set)(x:key)(e:elt)(s:t elt) { struct s } : t elt := match s with + | Leaf => Node (Leaf _) x e (Leaf _) 1 + | Node l y e' r h => + match X.compare x y with + | LT _ => bal (add x e l) y e' r + | EQ _ => Node l y e r h + | GT _ => bal l y e' (add x e r) + end + end. + +Lemma add_avl_1 : forall elt (m:t elt) x e, avl m -> + avl (add x e m) /\ 0 <= height (add x e m) - height m <= 1. +Proof. + intros elt m x e; functional induction add elt x e m; intros; inv avl; simpl in *. + intuition; try constructor; simpl; auto; try omega_max. + (* LT *) + destruct H; auto. + split. + apply bal_avl; auto; omega_max. + omega_bal. + (* EQ *) + intuition; omega_max. + (* GT *) + destruct H; auto. + split. + apply bal_avl; auto; omega_max. + omega_bal. +Qed. + +Lemma add_avl : forall elt (m:t elt) x e, avl m -> avl (add x e m). +Proof. + intros; generalize (add_avl_1 x e H); intuition. +Qed. +Hint Resolve add_avl. + +Lemma add_in : forall elt (m:t elt) x y e, avl m -> + (In y (add x e m) <-> X.eq y x \/ In y m). +Proof. + intros elt m x y e; functional induction add elt x e m; auto; intros. + intuition_in. + (* LT *) + inv avl. + rewrite bal_in; auto. + rewrite (H H1); intuition_in. + (* EQ *) + inv avl. + firstorder_in. + eapply In_1; eauto. + (* GT *) + inv avl. + rewrite bal_in; auto. + rewrite (H H2); intuition_in. +Qed. + +Lemma add_bst : forall elt (m:t elt) x e, bst m -> avl m -> bst (add x e m). +Proof. + intros elt m x e; functional induction add elt x e m; + intros; inv bst; inv avl; auto; apply bal_bst; auto. + (* lt_tree -> lt_tree (add ...) *) + red; red in H4. + intros. + rewrite (add_in x y0 e H0) in H1. + intuition. + eauto. + (* gt_tree -> gt_tree (add ...) *) + red; red in H4. + intros. + rewrite (add_in x y0 e H6) in H1. + intuition. + apply lt_eq with x; auto. +Qed. + +Lemma add_1 : forall elt (m:t elt) x y e, avl m -> X.eq x y -> MapsTo y e (add x e m). +Proof. + intros elt m x y e; functional induction add elt x e m; + intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; eauto. +Qed. + +Lemma add_2 : forall elt (m:t elt) x y e e', avl m -> ~X.eq x y -> + MapsTo y e m -> MapsTo y e (add x e' m). +Proof. + intros elt m x y e e'; induction m; simpl; auto. + destruct (X.compare x k); + intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; auto; + inv MapsTo; auto; order. +Qed. + +Lemma add_3 : forall elt (m:t elt) x y e e', avl m -> ~X.eq x y -> + MapsTo y e (add x e' m) -> MapsTo y e m. +Proof. + intros elt m x y e e'; induction m; simpl; auto. + intros; inv avl; inv MapsTo; auto; order. + destruct (X.compare x k); intro; inv avl; + try rewrite bal_mapsto; auto; unfold create; intros; inv MapsTo; auto; + order. +Qed. + + +(** * Extraction of minimum binding + + morally, [remove_min] is to be applied to a non-empty tree + [t = Node l x e r h]. Since we can't deal here with [assert false] + for [t=Leaf], we pre-unpack [t] (and forget about [h]). +*) + +Fixpoint remove_min (elt:Set)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t elt*(key*elt) := + match l with + | Leaf => (r,(x,e)) + | Node ll lx le lr lh => let (l',m) := remove_min ll lx le lr in (bal l' x e r, m) + end. + +Lemma remove_min_avl_1 : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> + avl (fst (remove_min l x e r)) /\ + 0 <= height (Node l x e r h) - height (fst (remove_min l x e r)) <= 1. +Proof. + intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + inv avl; simpl in *; split; auto. + avl_nns; omega_max. + (* l = Node *) + inversion_clear H0. + destruct (H lh); auto. + split; simpl in *. + apply bal_avl; auto; omega_max. + omega_bal. +Qed. + +Lemma remove_min_avl : forall elt (l:t elt) x e r h, avl (Node l x e r h) -> + avl (fst (remove_min l x e r)). +Proof. + intros; generalize (remove_min_avl_1 H); intuition. +Qed. + +Lemma remove_min_in : forall elt (l:t elt) x e r h y, avl (Node l x e r h) -> + (In y (Node l x e r h) <-> + X.eq y (fst (snd (remove_min l x e r))) \/ In y (fst (remove_min l x e r))). +Proof. + intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + intuition_in. + (* l = Node *) + inversion_clear H0. + generalize (remove_min_avl H1). + rewrite H_eq_0; simpl; intros. + rewrite bal_in; auto. + generalize (H lh y H1). + intuition. + inversion_clear H8; intuition. +Qed. + +Lemma remove_min_mapsto : forall elt (l:t elt) x e r h y e', avl (Node l x e r h) -> + (MapsTo y e' (Node l x e r h) <-> + ((X.eq y (fst (snd (remove_min l x e r))) /\ e' = (snd (snd (remove_min l x e r)))) + \/ MapsTo y e' (fst (remove_min l x e r)))). +Proof. + intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + intuition_in; subst; auto. + (* l = Node *) + inversion_clear H0. + generalize (remove_min_avl H1). + rewrite H_eq_0; simpl; intros. + rewrite bal_mapsto; auto; unfold create. + destruct (H lh y e'). + auto. + intuition. + inversion_clear H3; intuition. + inversion_clear H10; intuition. +Qed. + +Lemma remove_min_bst : forall elt (l:t elt) x e r h, + bst (Node l x e r h) -> avl (Node l x e r h) -> bst (fst (remove_min l x e r)). +Proof. + intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + inv bst; auto. + inversion_clear H0; inversion_clear H1. + apply bal_bst; auto. + firstorder. + intro; intros. + generalize (remove_min_in y H0). + rewrite H_eq_0; simpl. + destruct 1. + apply H4; intuition. +Qed. + +Lemma remove_min_gt_tree : forall elt (l:t elt) x e r h, + bst (Node l x e r h) -> avl (Node l x e r h) -> + gt_tree (fst (snd (remove_min l x e r))) (fst (remove_min l x e r)). +Proof. + intros elt l x e r; functional induction remove_min elt l x e r; simpl in *; intros. + inv bst; auto. + inversion_clear H0; inversion_clear H1. + intro; intro. + generalize (H lh H2 H0); clear H8 H7 H. + generalize (remove_min_avl H0). + generalize (remove_min_in (fst m) H0). + rewrite H_eq_0; simpl; intros. + rewrite (bal_in x e y H7 H6) in H1. + destruct H. + firstorder. + apply lt_eq with x; auto. + apply X.lt_trans with x; auto. +Qed. + +(** * Merging two trees + + [merge t1 t2] builds the union of [t1] and [t2] assuming all elements + of [t1] to be smaller than all elements of [t2], and + [|height t1 - height t2| <= 2]. +*) + +Definition merge elt (s1 s2 : t elt) := match s1,s2 with + | Leaf, _ => s2 + | _, Leaf => s1 + | _, Node l2 x2 e2 r2 h2 => + let (s2',m) := remove_min l2 x2 e2 r2 in + let (x,e) := m in + bal s1 x e s2' +end. + +Lemma merge_avl_1 : forall elt (s1 s2:t elt), avl s1 -> avl s2 -> + -(2) <= height s1 - height s2 <= 2 -> + avl (merge s1 s2) /\ + 0<= height (merge s1 s2) - max (height s1) (height s2) <=1. +Proof. + intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros. + split; auto; avl_nns; omega_max. + split; auto; avl_nns; simpl in *; omega_max. + generalize (remove_min_avl_1 H0). + rewrite H_eq_1; simpl; destruct 1. + rewrite H_eq_2; simpl. + split. + apply bal_avl; auto. + simpl; omega_max. + omega_bal. +Qed. + +Lemma merge_avl : forall elt (s1 s2:t elt), avl s1 -> avl s2 -> + -(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2). +Proof. + intros; generalize (merge_avl_1 H H0 H1); intuition. +Qed. + +Lemma merge_in : forall elt (s1 s2:t elt) y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (In y (merge s1 s2) <-> In y s1 \/ In y s2). +Proof. + intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros. + intuition_in. + intuition_in. + rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H_eq_1; auto]. + rewrite bal_in; auto. + generalize (remove_min_avl H2); rewrite H_eq_1; simpl; auto. + generalize (remove_min_in y0 H2); rewrite H_eq_1; simpl; intro. + rewrite H3; intuition. +Qed. + +Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (MapsTo y e (merge s1 s2) <-> MapsTo y e s1 \/ MapsTo y e s2). +Proof. + intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros. + intuition_in. + intuition_in. + rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. + replace s2' with (fst (remove_min l2 x2 e2 r2)); [|rewrite H_eq_1; auto]. + rewrite bal_mapsto; auto; unfold create. + generalize (remove_min_avl H2); rewrite H_eq_1; simpl; auto. + generalize (remove_min_mapsto y0 e0 H2); rewrite H_eq_1; simpl; intro. + rewrite H3; intuition (try subst; auto). + inversion_clear H3; intuition. +Qed. + +Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (forall y1 y2 : key, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> + bst (merge s1 s2). +Proof. + intros elt s1 s2; functional induction merge elt s1 s2; simpl in *; intros; auto. + rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. + apply bal_bst; auto. + generalize (remove_min_bst H1); rewrite H_eq_1; simpl in *; auto. + intro; intro. + apply H3; auto. + generalize (remove_min_in x H2); rewrite H_eq_1; simpl; intuition. + generalize (remove_min_gt_tree H1); rewrite H_eq_1; simpl; auto. +Qed. + +(** * Deletion *) + +Fixpoint remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with + | Leaf => Leaf _ + | Node l y e r h => + match X.compare x y with + | LT _ => bal (remove x l) y e r + | EQ _ => merge l r + | GT _ => bal l y e (remove x r) + end + end. + +Lemma remove_avl_1 : forall elt (s:t elt) x, avl s -> + avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1. +Proof. + intros elt s x; functional induction remove elt x s; simpl; intros. + split; auto; omega_max. + (* LT *) + inv avl. + destruct (H H1). + split. + apply bal_avl; auto. + omega_max. + omega_bal. + (* EQ *) + inv avl. + generalize (merge_avl_1 H0 H1 H2). + intuition omega_max. + (* GT *) + inv avl. + destruct (H H2). + split. + apply bal_avl; auto. + omega_max. + omega_bal. +Qed. + +Lemma remove_avl : forall elt (s:t elt) x, avl s -> avl (remove x s). +Proof. + intros; generalize (remove_avl_1 x H); intuition. +Qed. +Hint Resolve remove_avl. + +Lemma remove_in : forall elt (s:t elt) x y, bst s -> avl s -> + (In y (remove x s) <-> ~ X.eq y x /\ In y s). +Proof. + intros elt s x; functional induction remove elt x s; simpl; intros. + intuition_in. + (* LT *) + inv avl; inv bst; clear H_eq_0. + rewrite bal_in; auto. + generalize (H y0 H1); intuition; [ order | order | intuition_in ]. + (* EQ *) + inv avl; inv bst; clear H_eq_0. + rewrite merge_in; intuition; [ order | order | intuition_in ]. + elim H9; eauto. + (* GT *) + inv avl; inv bst; clear H_eq_0. + rewrite bal_in; auto. + generalize (H y0 H6); intuition; [ order | order | intuition_in ]. +Qed. + +Lemma remove_bst : forall elt (s:t elt) x, bst s -> avl s -> bst (remove x s). +Proof. + intros elt s x; functional induction remove elt x s; simpl; intros. + auto. + (* LT *) + inv avl; inv bst. + apply bal_bst; auto. + intro; intro. + rewrite (remove_in x y0 H1) in H0; auto. + destruct H0; eauto. + (* EQ *) + inv avl; inv bst. + apply merge_bst; eauto. + (* GT *) + inv avl; inv bst. + apply bal_bst; auto. + intro; intro. + rewrite (remove_in x y0 H6) in H0; auto. + destruct H0; eauto. +Qed. + +Lemma remove_1 : forall elt (m:t elt) x y, bst m -> avl m -> X.eq x y -> ~ In y (remove x m). +Proof. + intros; rewrite remove_in; intuition. +Qed. + +Lemma remove_2 : forall elt (m:t elt) x y e, bst m -> avl m -> ~X.eq x y -> + MapsTo y e m -> MapsTo y e (remove x m). +Proof. + intros elt m x y e; induction m; simpl; auto. + destruct (X.compare x k); + intros; inv bst; inv avl; try rewrite bal_mapsto; unfold create; auto; + try solve [inv MapsTo; auto]. + rewrite merge_mapsto; auto. + inv MapsTo; auto; order. +Qed. + +Lemma remove_3 : forall elt (m:t elt) x y e, bst m -> avl m -> + MapsTo y e (remove x m) -> MapsTo y e m. +Proof. + intros elt m x y e; induction m; simpl; auto. + destruct (X.compare x k); intros Bs Av; inv avl; inv bst; + try rewrite bal_mapsto; auto; unfold create. + intros; inv MapsTo; auto. + rewrite merge_mapsto; intuition. + intros; inv MapsTo; auto. +Qed. + +Section Elt2. + +Variable elt:Set. + +Notation eqk := (eqk (elt:= elt)). +Notation eqke := (eqke (elt:= elt)). +Notation ltk := (ltk (elt:= elt)). + +(** * Empty map *) + +Definition Empty m := forall (a : key)(e:elt) , ~ MapsTo a e m. + +Definition empty := (Leaf elt). + +Lemma empty_bst : bst empty. +Proof. + unfold empty; auto. +Qed. + +Lemma empty_avl : avl empty. +Proof. + unfold empty; auto. +Qed. + +Lemma empty_1 : Empty empty. +Proof. + unfold empty, Empty; intuition_in. +Qed. + +(** * Emptyness test *) + +Definition is_empty (s:t elt) := match s with Leaf => true | _ => false end. + +Lemma is_empty_1 : forall s, Empty s -> is_empty s = true. +Proof. + destruct s as [|r x e l h]; simpl; auto. + intro H; elim (H x e); auto. +Qed. + +Lemma is_empty_2 : forall s, is_empty s = true -> Empty s. +Proof. + destruct s; simpl; intros; try discriminate; red; intuition_in. +Qed. + +(** * Appartness *) + +(** The [mem] function is deciding appartness. It exploits the [bst] property + to achieve logarithmic complexity. *) + +Fixpoint mem (x:key)(m:t elt) { struct m } : bool := + match m with + | Leaf => false + | Node l y e r _ => match X.compare x y with + | LT _ => mem x l + | EQ _ => true + | GT _ => mem x r + end + end. +Implicit Arguments mem. + +Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true. +Proof. + intros s x. + functional induction mem x s; inversion_clear 1; auto. + intuition_in. + intuition_in; firstorder; absurd (X.lt x y); eauto. + intuition_in; firstorder; absurd (X.lt y x); eauto. +Qed. + +Lemma mem_2 : forall s x, mem x s = true -> In x s. +Proof. + intros s x. + functional induction mem x s; firstorder; intros; try discriminate. +Qed. + +Fixpoint find (x:key)(m:t elt) { struct m } : option elt := + match m with + | Leaf => None + | Node l y e r _ => match X.compare x y with + | LT _ => find x l + | EQ _ => Some e + | GT _ => find x r + end + end. + +Lemma find_1 : forall m x e, bst m -> MapsTo x e m -> find x m = Some e. +Proof. + intros m x e. + functional induction find x m; inversion_clear 1; auto. + intuition_in. + intuition_in; firstorder; absurd (X.lt x y); eauto. + intuition_in; auto. + absurd (X.lt x y); eauto. + absurd (X.lt y x); eauto. + intuition_in; firstorder; absurd (X.lt y x); eauto. +Qed. + +Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m. +Proof. + intros m x. + functional induction find x m; firstorder; intros; try discriminate. + inversion H; subst; auto. +Qed. + +(** An all-in-one spec for [add] used later in the naive [map2] *) + +Lemma add_spec : forall m x y e , bst m -> avl m -> + find x (add y e m) = if eq_dec x y then Some e else find x m. +Proof. +intros. +destruct (eq_dec x y). +apply find_1. +apply add_bst; auto. +eapply MapsTo_1 with y; eauto. +apply add_1; auto. +case_eq (find x m); intros. +apply find_1. +apply add_bst; auto. +apply add_2; auto. +apply find_2; auto. +case_eq (find x (add y e m)); auto; intros. +rewrite <- H1; symmetry. +apply find_1; auto. +eapply add_3; eauto. +apply find_2; eauto. +Qed. + +(** * Elements *) + +(** [elements_tree_aux acc t] catenates the elements of [t] in infix + order to the list [acc] *) + +Fixpoint elements_aux (acc : list (key*elt)) (t : t elt) {struct t} : list (key*elt) := + match t with + | Leaf => acc + | Node l x e r _ => elements_aux ((x,e) :: elements_aux acc r) l + end. + +(** then [elements] is an instanciation with an empty [acc] *) + +Definition elements := elements_aux nil. + +Lemma elements_aux_mapsto : forall s acc x e, + InA eqke (x,e) (elements_aux acc s) <-> MapsTo x e s \/ InA eqke (x,e) acc. +Proof. + induction s as [ | l Hl x e r Hr h ]; simpl; auto. + intuition. + inversion H0. + intros. + rewrite Hl. + destruct (Hr acc x0 e0); clear Hl Hr. + intuition; inversion_clear H3; intuition. + destruct H0; simpl in *; subst; intuition. +Qed. + +Lemma elements_mapsto : forall s x e, InA eqke (x,e) (elements s) <-> MapsTo x e s. +Proof. + intros; generalize (elements_aux_mapsto s nil x e); intuition. + inversion_clear H0. +Qed. + +Lemma elements_in : forall s x, L.PX.In x (elements s) <-> In x s. +Proof. + intros. + unfold L.PX.In. + rewrite <- In_alt; unfold In0. + firstorder. + exists x0. + rewrite <- elements_mapsto; auto. + exists x0. + unfold L.PX.MapsTo; rewrite elements_mapsto; auto. +Qed. + +Lemma elements_aux_sort : forall s 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). +Proof. + induction s as [ | l Hl y e r Hr h]; simpl; intuition. + inv bst. + apply Hl; auto. + constructor. + apply Hr; eauto. + apply (InA_InfA (eqke_refl (elt:=elt))); intros (y',e') H6. + destruct (elements_aux_mapsto r acc y' e'); intuition. + red; simpl; eauto. + red; simpl; eauto. + intros. + inversion_clear H. + destruct H7; simpl in *. + order. + destruct (elements_aux_mapsto r acc x e0); intuition eauto. +Qed. + +Lemma elements_sort : forall s : t elt, bst s -> sort ltk (elements s). +Proof. + intros; unfold elements; apply elements_aux_sort; auto. + intros; inversion H0. +Qed. +Hint Resolve elements_sort. + + +(** * Fold *) + +Fixpoint fold (A : Set) (f : key -> elt -> A -> A)(s : t elt) {struct s} : A -> A := + fun a => match s with + | Leaf => a + | Node l x e r _ => fold f r (f x e (fold f l a)) + end. + +Definition fold' (A : Set) (f : key -> elt -> A -> A)(s : t elt) := + L.fold f (elements s). + +Lemma fold_equiv_aux : + forall (A : Set) (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). +Proof. + simple induction s. + simpl in |- *; intuition. + simpl in |- *; intros. + rewrite H. + simpl. + apply H0. +Qed. + +Lemma fold_equiv : + forall (A : Set) (s : t elt) (f : key -> elt -> A -> A) (a : A), + fold f s a = fold' f s a. +Proof. + unfold fold', elements in |- *. + simple induction s; simpl in |- *; auto; intros. + rewrite fold_equiv_aux. + rewrite H0. + simpl in |- *; auto. +Qed. + +Lemma fold_1 : + forall (s:t elt)(Hs:bst s)(A : Set)(i:A)(f : key -> elt -> A -> A), + fold f s i = fold_left (fun a p => f (fst p) (snd p) a) (elements s) i. +Proof. + intros. + rewrite fold_equiv. + unfold fold'. + rewrite L.fold_1. + unfold L.elements; auto. +Qed. + +(** * Comparison *) + +Definition Equal (cmp:elt->elt->bool) 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). + +(** ** Enumeration of the elements of a tree *) + +Inductive enumeration : Set := + | End : enumeration + | More : key -> elt -> t elt -> enumeration -> enumeration. + +(** [flatten_e e] returns the list of elements of [e] i.e. the list + of elements actually compared *) + +Fixpoint flatten_e (e : enumeration) : list (key*elt) := match e with + | End => nil + | More x e t r => (x,e) :: elements t ++ flatten_e r + end. + +(** [sorted_e e] expresses that elements in the enumeration [e] are + sorted, and that all trees in [e] are binary search trees. *) + +Inductive In_e (p:key*elt) : enumeration -> Prop := + | InEHd1 : + forall (y : key)(d:elt) (s : t elt) (e : enumeration), + eqke p (y,d) -> In_e p (More y d s e) + | InEHd2 : + forall (y : key) (d:elt) (s : t elt) (e : enumeration), + MapsTo (fst p) (snd p) s -> In_e p (More y d s e) + | InETl : + forall (y : key) (d:elt) (s : t elt) (e : enumeration), + In_e p e -> In_e p (More y d s e). + +Hint Constructors In_e. + +Inductive sorted_e : enumeration -> Prop := + | SortedEEnd : sorted_e End + | SortedEMore : + forall (x : key) (d:elt) (s : t elt) (e : enumeration), + bst s -> + (gt_tree x s) -> + sorted_e e -> + (forall p, In_e p e -> ltk (x,d) p) -> + (forall p, + MapsTo (fst p) (snd p) s -> forall q, In_e q e -> ltk p q) -> + sorted_e (More x d s e). + +Hint Constructors sorted_e. + +Lemma in_flatten_e : + forall p e, InA eqke p (flatten_e e) -> In_e p e. +Proof. + simple induction e; simpl in |- *; intuition. + inversion_clear H. + inversion_clear H0; auto. + elim (InA_app H1); auto. + destruct (elements_mapsto t a b); auto. +Qed. + +Lemma sorted_flatten_e : + forall e : enumeration, sorted_e e -> sort ltk (flatten_e e). +Proof. + simple induction e; simpl in |- *; intuition. + apply cons_sort. + apply (SortA_app (eqke_refl (elt:=elt))); inversion_clear H0; auto. + intros; apply H5; auto. + rewrite <- elements_mapsto; auto; destruct x; auto. + apply in_flatten_e; auto. + inversion_clear H0. + apply In_InfA; intros. + intros; elim (in_app_or _ _ _ H0); intuition. + generalize (In_InA (eqke_refl (elt:=elt)) H6). + destruct y; rewrite elements_mapsto; eauto. + apply H4; apply in_flatten_e; auto. + apply In_InA; auto. +Qed. + +Lemma elements_app : + forall s acc, elements_aux acc s = elements s ++ acc. +Proof. + simple induction s; simpl in |- *; intuition. + rewrite H0. + rewrite H. + unfold elements; simpl. + do 2 rewrite H. + rewrite H0. + repeat rewrite <- app_nil_end. + repeat rewrite app_ass; auto. +Qed. + +Lemma compare_flatten_1 : + forall t1 t2 x e z l, + elements t1 ++ (x,e) :: elements t2 ++ l = + elements (Node t1 x e t2 z) ++ l. +Proof. + simpl in |- *; unfold elements in |- *; simpl in |- *; intuition. + repeat rewrite elements_app. + repeat rewrite <- app_nil_end. + repeat rewrite app_ass; auto. +Qed. + +(** key lemma for correctness *) + +Lemma flatten_e_elements : + forall l r x d z e, + elements l ++ flatten_e (More x d r e) = + elements (Node l x d r z) ++ flatten_e e. +Proof. + intros; simpl. + apply compare_flatten_1. +Qed. + +Open Scope Z_scope. + +(** termination of [compare_aux] *) + +Fixpoint measure_e_t (s : t elt) : Z := match s with + | Leaf => 0 + | Node l _ _ r _ => 1 + measure_e_t l + measure_e_t r + end. + +Fixpoint measure_e (e : enumeration) : Z := match e with + | End => 0 + | More _ _ s r => 1 + measure_e_t s + measure_e r + end. + +Ltac Measure_e_t := unfold measure_e_t in |- *; fold measure_e_t in |- *. +Ltac Measure_e := unfold measure_e in |- *; fold measure_e in |- *. + +Lemma measure_e_t_0 : forall s : t elt, measure_e_t s >= 0. +Proof. + simple induction s. + simpl in |- *; omega. + intros. + Measure_e_t; omega. +Qed. + +Ltac Measure_e_t_0 s := generalize (@measure_e_t_0 s); intro. + +Lemma measure_e_0 : forall e : enumeration, measure_e e >= 0. +Proof. + simple induction e. + simpl in |- *; omega. + intros. + Measure_e; Measure_e_t_0 t; omega. +Qed. + +Ltac Measure_e_0 e := generalize (@measure_e_0 e); intro. + +(** Induction principle over the sum of the measures for two lists *) + +Definition compare_rec2 : + forall P : enumeration -> enumeration -> Set, + (forall x x' : enumeration, + (forall y y' : enumeration, + measure_e y + measure_e y' < measure_e x + measure_e x' -> P y y') -> + P x x') -> + forall x x' : enumeration, P x x'. +Proof. + intros P H x x'. + apply well_founded_induction_type_2 + with (R := fun yy' xx' : enumeration * enumeration => + measure_e (fst yy') + measure_e (snd yy') < + measure_e (fst xx') + measure_e (snd xx')); auto. + apply Wf_nat.well_founded_lt_compat + with (f := fun xx' : enumeration * enumeration => + Zabs_nat (measure_e (fst xx') + measure_e (snd xx'))). + intros; apply Zabs.Zabs_nat_lt. + Measure_e_0 (fst x0); Measure_e_0 (snd x0); Measure_e_0 (fst y); + Measure_e_0 (snd y); intros; omega. +Qed. + +(** [cons t e] adds the elements of tree [t] on the head of + enumeration [e]. Code: + +let rec cons s e = match s with + | Empty -> e + | Node(l, k, d, r, _) -> cons l (More(k, d, r, e)) +*) + +Definition cons : forall s e, bst s -> sorted_e e -> + (forall x y, MapsTo (fst x) (snd x) s -> In_e y e -> ltk x y) -> + { r : enumeration + | sorted_e r /\ + measure_e r = measure_e_t s + measure_e e /\ + flatten_e r = elements s ++ flatten_e e + }. +Proof. + simple induction s; intuition. + (* s = Leaf *) + exists e; intuition. + (* s = Node t k e t0 z *) + clear H0. + case (H (More k e t0 e0)); clear H; intuition. + inv bst; auto. + constructor; inversion_clear H1; auto. + inversion_clear H0; inv bst; intuition. + destruct y; red; red in H4; simpl in *; intuition. + apply lt_eq with k; eauto. + destruct y; red; simpl in *; intuition. + apply X.lt_trans with k; eauto. + exists x; intuition. + generalize H4; Measure_e; intros; Measure_e_t; omega. + rewrite H5. + apply flatten_e_elements. +Qed. + +Definition equal_aux : + forall (cmp: elt -> elt -> bool)(e1 e2:enumeration), + sorted_e e1 -> sorted_e e2 -> + { L.Equal cmp (flatten_e e1) (flatten_e e2) } + + { ~ L.Equal cmp (flatten_e e1) (flatten_e e2) }. +Proof. + intros cmp e1 e2; pattern e1, e2 in |- *; apply compare_rec2. + simple destruct x; simple destruct x'; intuition. + (* x = x' = End *) + left; unfold L.Equal in |- *; intuition. + inversion H2. + (* x = End x' = More *) + right; simpl in |- *; auto. + destruct 1. + destruct (H2 k). + destruct H5; auto. + exists e; auto. + inversion H5. + (* x = More x' = End *) + right; simpl in |- *; auto. + destruct 1. + destruct (H2 k). + destruct H4; auto. + exists e; auto. + inversion H4. + (* x = More k e t e0, x' = More k0 e3 t0 e4 *) + case (X.compare k k0); intro. + (* k < k0 *) + right. + destruct 1. + clear H3 H. + assert (L.PX.In k (flatten_e (More k0 e3 t0 e4))). + destruct (H2 k). + apply H; simpl; exists e; auto. + destruct H. + generalize (Sort_In_cons_2 (sorted_flatten_e H1) (InA_eqke_eqk H)). + compute. + intuition order. + (* k = k0 *) + case_eq (cmp e e3). + intros EQ. + destruct (@cons t e0) as [c1 (H2,(H3,H4))]; try inversion_clear H0; auto. + destruct (@cons t0 e4) as [c2 (H5,(H6,H7))]; try inversion_clear H1; auto. + destruct (H c1 c2); clear H; intuition. + Measure_e; omega. + left. + rewrite H4 in e6; rewrite H7 in e6. + simpl; rewrite <- L.equal_cons; auto. + apply (sorted_flatten_e H0). + apply (sorted_flatten_e H1). + right. + simpl; rewrite <- L.equal_cons; auto. + apply (sorted_flatten_e H0). + apply (sorted_flatten_e H1). + swap f. + rewrite H4; rewrite H7; auto. + right. + destruct 1. + rewrite (H4 k) in H2; try discriminate; simpl; auto. + (* k > k0 *) + right. + destruct 1. + clear H3 H. + assert (L.PX.In k0 (flatten_e (More k e t e0))). + destruct (H2 k0). + apply H3; simpl; exists e3; auto. + destruct H. + generalize (Sort_In_cons_2 (sorted_flatten_e H0) (InA_eqke_eqk H)). + compute. + intuition order. +Qed. + +Lemma Equal_elements : forall cmp s s', + Equal cmp s s' <-> L.Equal cmp (elements s) (elements s'). +Proof. +unfold Equal, L.Equal; split; split; intros. +do 2 rewrite elements_in; firstorder. +destruct H. +apply (H2 k); rewrite <- elements_mapsto; auto. +do 2 rewrite <- elements_in; firstorder. +destruct H. +apply (H2 k); unfold L.PX.MapsTo; rewrite elements_mapsto; auto. +Qed. + +Definition equal : forall cmp s s', bst s -> bst s' -> + {Equal cmp s s'} + {~ Equal cmp s s'}. +Proof. + intros cmp s1 s2 s1_bst s2_bst; simpl. + destruct (@cons s1 End); auto. + inversion_clear 2. + destruct (@cons s2 End); auto. + inversion_clear 2. + simpl in a; rewrite <- app_nil_end in a. + simpl in a0; rewrite <- app_nil_end in a0. + destruct (@equal_aux cmp x x0); intuition. + left. + rewrite H4 in e; rewrite H5 in e. + rewrite Equal_elements; auto. + right. + swap n. + rewrite H4; rewrite H5. + rewrite <- Equal_elements; auto. +Qed. + +End Elt2. + +Section Elts. + +Variable elt elt' elt'' : Set. + +Section Map. +Variable f : elt -> elt'. + +Fixpoint map (m:t elt) {struct m} : t elt' := + match m with + | Leaf => Leaf _ + | Node l v d r h => Node (map l) v (f d) (map r) h + end. + +Lemma map_height : forall m, height (map m) = height m. +Proof. +destruct m; simpl; auto. +Qed. + +Lemma map_avl : forall m, avl m -> avl (map m). +Proof. +induction m; simpl; auto. +inversion_clear 1; constructor; auto; do 2 rewrite map_height; auto. +Qed. + +Lemma map_1 : forall (m: tree elt)(x:key)(e:elt), + MapsTo x e m -> MapsTo x (f e) (map m). +Proof. +induction m; simpl; inversion_clear 1; auto. +Qed. + +Lemma map_2 : forall (m: t elt)(x:key), + In x (map m) -> In x m. +Proof. +induction m; simpl; inversion_clear 1; auto. +Qed. + +Lemma map_bst : forall m, bst m -> bst (map m). +Proof. +induction m; simpl; auto. +inversion_clear 1; constructor; auto. +red; intros; apply H2; apply map_2; auto. +red; intros; apply H3; apply map_2; auto. +Qed. + +End Map. +Section Mapi. +Variable f : key -> elt -> elt'. + +Fixpoint mapi (m:t elt) {struct m} : t elt' := + match m with + | Leaf => Leaf _ + | Node l v d r h => Node (mapi l) v (f v d) (mapi r) h + end. + +Lemma mapi_height : forall m, height (mapi m) = height m. +Proof. +destruct m; simpl; auto. +Qed. + +Lemma mapi_avl : forall m, avl m -> avl (mapi m). +Proof. +induction m; simpl; auto. +inversion_clear 1; constructor; auto; do 2 rewrite mapi_height; auto. +Qed. + +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 m). +Proof. +induction m; simpl; inversion_clear 1; auto. +exists k; auto. +destruct (IHm1 _ _ H0). +exists x0; intuition. +destruct (IHm2 _ _ H0). +exists x0; intuition. +Qed. + +Lemma mapi_2 : forall (m: t elt)(x:key), + In x (mapi m) -> In x m. +Proof. +induction m; simpl; inversion_clear 1; auto. +Qed. + +Lemma mapi_bst : forall m, bst m -> bst (mapi m). +Proof. +induction m; simpl; auto. +inversion_clear 1; constructor; auto. +red; intros; apply H2; apply mapi_2; auto. +red; intros; apply H3; apply mapi_2; auto. +Qed. + +End Mapi. + +Section Map2. +Variable f : option elt -> option elt' -> option elt''. + +(* Not exactly pretty nor perfect, but should suffice as a first naive implem. + Anyway, map2 isn't in Ocaml... +*) + +Definition anti_elements (l:list (key*elt'')) := L.fold (@add _) l (empty _). + +Definition map2 (m:t elt)(m':t elt') : t elt'' := + anti_elements (L.map2 f (elements m) (elements m')). + +Lemma anti_elements_avl_aux : forall (l:list (key*elt''))(m:t elt''), + avl m -> avl (L.fold (@add _) l m). +Proof. +unfold anti_elements; induction l. +simpl; auto. +simpl; destruct a; intros. +apply IHl. +apply add_avl; auto. +Qed. + +Lemma anti_elements_avl : forall l, avl (anti_elements l). +Proof. +unfold anti_elements, empty; intros; apply anti_elements_avl_aux; auto. +Qed. + +Lemma anti_elements_bst_aux : forall (l:list (key*elt''))(m:t elt''), + bst m -> avl m -> bst (L.fold (@add _) l m). +Proof. +induction l. +simpl; auto. +simpl; destruct a; intros. +apply IHl. +apply add_bst; auto. +apply add_avl; auto. +Qed. + +Lemma anti_elements_bst : forall l, bst (anti_elements l). +Proof. +unfold anti_elements, empty; intros; apply anti_elements_bst_aux; auto. +Qed. + +Lemma anti_elements_mapsto_aux : forall (l:list (key*elt'')) m k e, + bst m -> avl m -> NoDupA (eqk (elt:=elt'')) l -> + (forall x, L.PX.In x l -> In x m -> False) -> + (MapsTo k e (L.fold (@add _) l m) <-> L.PX.MapsTo k e l \/ MapsTo k e m). +Proof. +induction l. +simpl; auto. +intuition. +inversion H4. +simpl; destruct a; intros. +rewrite IHl; clear IHl. +apply add_bst; auto. +apply add_avl; auto. +inversion H1; auto. +intros. +inversion_clear H1. +assert (~X.eq x k). + swap H5. + destruct H3. + apply InA_eqA with (x,x0); eauto. +apply (H2 x). +destruct H3; exists x0; auto. +revert H4; do 2 rewrite <- In_alt; destruct 1; exists x0; auto. +eapply add_3; eauto. +intuition. +assert (find k0 (add k e m) = Some e0). + apply find_1; auto. + apply add_bst; auto. +clear H4. +rewrite add_spec in H3; auto. +destruct (eq_dec k0 k). +inversion_clear H3; subst; auto. +right; apply find_2; auto. +inversion_clear H4; auto. +compute in H3; destruct H3. +subst; right; apply add_1; auto. +inversion_clear H1. +destruct (eq_dec k0 k). +destruct (H2 k); eauto. +right; apply add_2; auto. +Qed. + +Lemma anti_elements_mapsto : forall l k e, NoDupA (eqk (elt:=elt'')) l -> + (MapsTo k e (anti_elements l) <-> L.PX.MapsTo k e l). +Proof. +intros. +unfold anti_elements. +rewrite anti_elements_mapsto_aux; auto; unfold empty; auto. +inversion 2. +intuition. +inversion H1. +Qed. + +Lemma map2_avl : forall (m: t elt)(m': t elt'), avl (map2 m m'). +Proof. +unfold map2; intros; apply anti_elements_avl; auto. +Qed. + +Lemma map2_bst : forall (m: t elt)(m': t elt'), bst (map2 m m'). +Proof. +unfold map2; intros; apply anti_elements_bst; auto. +Qed. + +Lemma find_elements : forall (elt:Set)(m: t elt) x, bst m -> + L.find x (elements m) = find x m. +Proof. +intros. +case_eq (find x m); intros. +apply L.find_1. +apply elements_sort; auto. +red; rewrite elements_mapsto. +apply find_2; auto. +case_eq (L.find x (elements m)); auto; intros. +rewrite <- H0; symmetry. +apply find_1; auto. +rewrite <- elements_mapsto. +apply L.find_2; auto. +Qed. + +Lemma find_anti_elements : forall (l: list (key*elt'')) x, sort (@ltk _) l -> + find x (anti_elements l) = L.find x l. +Proof. +intros. +case_eq (L.find x l); intros. +apply find_1. +apply anti_elements_bst; auto. +rewrite anti_elements_mapsto. +apply L.PX.Sort_NoDupA; auto. +apply L.find_2; auto. +case_eq (find x (anti_elements l)); auto; intros. +rewrite <- H0; symmetry. +apply L.find_1; auto. +rewrite <- anti_elements_mapsto. +apply L.PX.Sort_NoDupA; auto. +apply find_2; auto. +Qed. + +Lemma map2_1 : forall (m: t elt)(m': t elt')(x:key), bst m -> bst m' -> + In x m \/ In x m' -> find x (map2 m m') = f (find x m) (find x m'). +Proof. +unfold map2; intros. +rewrite find_anti_elements; auto. +rewrite <- find_elements; auto. +rewrite <- find_elements; auto. +apply L.map2_1; auto. +apply elements_sort; auto. +apply elements_sort; auto. +do 2 rewrite elements_in; auto. +apply L.map2_sorted; auto. +apply elements_sort; auto. +apply elements_sort; auto. +Qed. + +Lemma map2_2 : forall (m: t elt)(m': t elt')(x:key), bst m -> bst m' -> + In x (map2 m m') -> In x m \/ In x m'. +Proof. +unfold map2; intros. +do 2 rewrite <- elements_in. +apply L.map2_2 with (f:=f); auto. +apply elements_sort; auto. +apply elements_sort; auto. +revert H1. +rewrite <- In_alt. +destruct 1. +exists x0. +rewrite <- anti_elements_mapsto; auto. +apply L.PX.Sort_NoDupA; auto. +apply L.map2_sorted; auto. +apply elements_sort; auto. +apply elements_sort; auto. +Qed. + +End Map2. +End Elts. +End Raw. + +(** * Encapsulation + + Now, in order to really provide a functor implementing [S], we + need to encapsulate everything into a type of balanced binary search trees. *) + +Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. + + Module E := X. + Module Raw := Raw I X. + Import Raw. + + Record bbst (elt:Set) : Set := Bbst {this :> tree elt; is_bst : bst this; is_avl: avl this}. + + Definition t := bbst. + Definition key := X.t. + + Section Elt. + Variable elt elt' elt'': Set. + + Implicit Types m : t elt. + + Definition empty := Bbst (empty_bst elt) (empty_avl elt). + Definition is_empty m := is_empty m.(this). + Definition add x e m := + Bbst (add_bst x e m.(is_bst) m.(is_avl)) (add_avl x e m.(is_avl)). + Definition remove x m := + Bbst (remove_bst x m.(is_bst) m.(is_avl)) (remove_avl x m.(is_avl)). + Definition mem x m := mem x m.(this). + Definition find x m := find x m.(this). + Definition map f m : t elt' := + Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)). + Definition mapi f m : t elt' := + Bbst (mapi_bst f m.(is_bst)) (mapi_avl f m.(is_avl)). + Definition map2 f m (m':t elt') : t elt'' := + Bbst (map2_bst f m m') (map2_avl f m m'). + Definition elements m := elements m.(this). + Definition fold (A:Set) f m i := fold (A:=A) f m.(this) i. + Definition equal cmp m m' := + if (equal cmp m.(is_bst) m'.(is_bst)) then true else false. + + Definition MapsTo x e m := MapsTo x e m.(this). + Definition In x m := In0 x m.(this). + Definition Empty m := Empty m.(this). + + Definition eq_key := @Raw.PX.eqk elt. + Definition eq_key_elt := @Raw.PX.eqke elt. + Definition lt_key := @Raw.PX.ltk elt. + + Definition MapsTo_1 m := @MapsTo_1 _ m.(this). + + Lemma mem_1 : forall m x, In x m -> mem x m = true. + Proof. + unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_1; auto. + apply m.(is_bst). + Qed. + + Lemma mem_2 : forall m x, mem x m = true -> In x m. + Proof. + unfold In, mem; intros m x; rewrite In_alt; simpl; apply mem_2; auto. + Qed. + + Definition empty_1 := empty_1. + + Definition is_empty_1 m := @is_empty_1 _ m.(this). + Definition is_empty_2 m := @is_empty_2 _ m.(this). + + Definition add_1 m x y e := @add_1 elt m.(this) x y e m.(is_avl). + Definition add_2 m x y e e':= @add_2 elt m.(this) x y e e' m.(is_avl). + Definition add_3 m x y e e' := @add_3 elt m.(this) x y e e' m.(is_avl). + + Lemma remove_1 : forall m x y, E.eq x y -> ~ In y (remove x m). + Proof. + unfold In, remove; intros m x y; rewrite In_alt; simpl; apply remove_1; auto. + apply m.(is_bst). + apply m.(is_avl). + Qed. + + Definition remove_2 m x y e := @remove_2 elt m.(this) x y e m.(is_bst) m.(is_avl). + Definition remove_3 m x y e := @remove_3 elt m.(this) x y e m.(is_bst) m.(is_avl). + + Definition find_1 m x e := @find_1 elt m.(this) x e m.(is_bst). + Definition find_2 m x e := @find_2 elt m.(this) x e. + + Definition fold_1 m := @fold_1 elt m.(this) m.(is_bst). + + Definition map_1 m x e f := @map_1 elt elt' f m.(this) x e. + Lemma map_2 : forall m x f, In0 x (map f m) -> In0 x m. + Proof. + intros m x f; do 2 rewrite In_alt; simpl; apply map_2; auto. + Qed. + + Definition mapi_1 m x e f := @mapi_1 elt elt' f m.(this) x e. + Lemma mapi_2 : forall m x f, In0 x (mapi f m) -> In0 x m. + Proof. + intros m x f; do 2 rewrite In_alt; simpl; apply mapi_2; auto. + Qed. + + Lemma elements_1 : forall m x e, + MapsTo x e m -> InA eq_key_elt (x,e) (elements m). + Proof. + 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. + Proof. + intros; unfold elements, MapsTo, eq_key_elt; rewrite <- elements_mapsto; auto. + Qed. + + Definition elements_3 m := @elements_sort elt m.(this) m.(is_bst). + + Definition Equal cmp 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 Equal_Equal : forall cmp m m', Equal cmp m m' <-> Raw.Equal cmp m m'. + Proof. + intros; unfold Equal, Raw.Equal, In; intuition. + generalize (H0 k); do 2 rewrite In_alt; intuition. + generalize (H0 k); do 2 rewrite In_alt; intuition. + generalize (H0 k); do 2 rewrite <- In_alt; intuition. + generalize (H0 k); do 2 rewrite <- In_alt; intuition. + Qed. + + Lemma equal_1 : forall m m' cmp, + Equal cmp m m' -> equal cmp m m' = true. + Proof. + unfold equal; intros m m' cmp; rewrite Equal_Equal. + destruct (@Raw.equal _ cmp m m'); auto. + Qed. + + Lemma equal_2 : forall m m' cmp, + equal cmp m m' = true -> Equal cmp m m'. + Proof. + unfold equal; intros; rewrite Equal_Equal. + destruct (@Raw.equal _ cmp m m'); auto; try discriminate. + Qed. + + End Elt. + + Lemma map2_1 : forall (elt elt' elt'':Set)(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'). + Proof. + unfold find, map2, In; intros elt elt' elt'' m m' x f. + do 2 rewrite In_alt; intros; simpl; apply map2_1; auto. + apply m.(is_bst). + apply m'.(is_bst). + Qed. + + Lemma map2_2 : forall (elt elt' elt'':Set)(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'. + Proof. + unfold In, map2; intros elt elt' elt'' m m' x f. + do 3 rewrite In_alt; intros; simpl in *; eapply map2_2; eauto. + apply m.(is_bst). + apply m'.(is_bst). + 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 MapS := IntMake(I)(X). + Import MapS. + + Module MD := OrderedTypeFacts(D). + Import MD. + + 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.elements_sort m.(is_bst)). + + Definition eq : t -> t -> Prop := + fun m1 m2 => LO.eq (elements m1) (elements m2). + + Definition lt : t -> t -> Prop := + fun m1 m2 => LO.lt (elements m1) (elements m2). + + Lemma eq_1 : forall m m', Equal cmp m m' -> eq m m'. + Proof. + intros m m'. + unfold eq. + rewrite Equal_Equal. + rewrite Raw.Equal_elements. + intros. + apply LO.eq_1. + auto. + Qed. + + Lemma eq_2 : forall m m', eq m m' -> Equal cmp m m'. + Proof. + intros m m'. + unfold eq. + rewrite Equal_Equal. + rewrite Raw.Equal_elements. + intros. + generalize (LO.eq_2 H). + auto. + Qed. + + Lemma eq_refl : forall m : t, eq m m. + Proof. + unfold eq; intros; apply LO.eq_refl. + Qed. + + Lemma eq_sym : forall m1 m2 : t, eq m1 m2 -> eq m2 m1. + Proof. + unfold eq; intros; apply LO.eq_sym; auto. + Qed. + + Lemma eq_trans : forall m1 m2 m3 : t, eq m1 m2 -> eq m2 m3 -> eq m1 m3. + Proof. + unfold eq; intros; eapply LO.eq_trans; eauto. + Qed. + + Lemma lt_trans : forall m1 m2 m3 : t, lt m1 m2 -> lt m2 m3 -> lt m1 m3. + Proof. + unfold lt; intros; eapply LO.lt_trans; eauto. + Qed. + + Lemma lt_not_eq : forall m1 m2 : t, lt m1 m2 -> ~ eq m1 m2. + Proof. + unfold lt, eq; intros; apply LO.lt_not_eq; auto. + Qed. + + Import Raw. + + Definition flatten_slist (e:enumeration D.t)(He:sorted_e e) := + LO.MapS.Build_slist (sorted_flatten_e He). + + Open Scope Z_scope. + + Definition compare_aux : + forall (e1 e2:enumeration D.t)(He1:sorted_e e1)(He2: sorted_e e2), + Compare LO.lt LO.eq (flatten_slist He1) (flatten_slist He2). + Proof. + intros e1 e2; pattern e1, e2 in |- *; apply compare_rec2. + simple destruct x; simple destruct x'; intuition. + (* x = x' = End *) + constructor 2. + compute; auto. + (* x = End x' = More *) + constructor 1. + compute; auto. + (* x = More x' = End *) + constructor 3. + compute; auto. + (* x = More k t0 t1 e, x' = More k0 t2 t3 e0 *) + case (X.compare k k0); intro. + (* k < k0 *) + constructor 1. + compute; MX.elim_comp; auto. + (* k = k0 *) + destruct (D.compare t t1). + constructor 1. + compute; MX.elim_comp; auto. + destruct (@cons _ t0 e) as [c1 (H2,(H3,H4))]; try inversion_clear He1; auto. + destruct (@cons _ t2 e0) as [c2 (H5,(H6,H7))]; try inversion_clear He2; auto. + assert (measure_e c1 + measure_e c2 < + measure_e (More k t t0 e) + + measure_e (More k0 t1 t2 e0)). + unfold measure_e in *; fold measure_e in *; omega. + destruct (H c1 c2 H0 H2 H5); clear H. + constructor 1. + unfold flatten_slist, LO.lt in *; simpl; simpl in l. + MX.elim_comp. + right; split; auto. + rewrite <- H7; rewrite <- H4; auto. + constructor 2. + unfold flatten_slist, LO.eq in *; simpl; simpl in e5. + MX.elim_comp. + split; auto. + rewrite <- H7; rewrite <- H4; auto. + constructor 3. + unfold flatten_slist, LO.lt in *; simpl; simpl in l. + MX.elim_comp. + right; split; auto. + rewrite <- H7; rewrite <- H4; auto. + constructor 3. + compute; MX.elim_comp; auto. + (* k > k0 *) + constructor 3. + compute; MX.elim_comp; auto. + Qed. + + Definition compare : forall m1 m2, Compare lt eq m1 m2. + Proof. + intros (m1,m1_bst,m1_avl) (m2,m2_bst,m2_avl); simpl. + destruct (@cons _ m1 (End _)) as [x1 (H1,H11)]; auto. + apply SortedEEnd. + inversion_clear 2. + destruct (@cons _ m2 (End _)) as [x2 (H2,H22)]; auto. + apply SortedEEnd. + inversion_clear 2. + simpl in H11; rewrite <- app_nil_end in H11. + simpl in H22; rewrite <- app_nil_end in H22. + destruct (compare_aux H1 H2); intuition. + constructor 1. + unfold lt, LO.lt, IntMake_ord.elements, flatten_slist in *; simpl in *. + rewrite <- H0; rewrite <- H4; auto. + constructor 2. + unfold eq, LO.eq, IntMake_ord.elements, flatten_slist in *; simpl in *. + rewrite <- H0; rewrite <- H4; auto. + constructor 3. + unfold lt, LO.lt, IntMake_ord.elements, flatten_slist in *; simpl in *. + rewrite <- H0; rewrite <- H4; 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). diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v new file mode 100644 index 000000000..5e4da1cd6 --- /dev/null +++ b/theories/FSets/FMapIntMap.v @@ -0,0 +1,622 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +Require Import Bool. +Require Import NArith Ndigits Ndec Nnat. +Require Import Allmaps. +Require Import OrderedType. +Require Import OrderedTypeEx. +Require Import FMapInterface FMapList. + + +Set Implicit Arguments. + +(** * An implementation of [FMapInterface.S] based on [IntMap] *) + +(** Keys are of type [N]. The main functions are directly taken from + [IntMap]. Since they have no exact counterpart in [IntMap], functions + [fold], [map2] and [equal] are for now obtained by translation + to sorted lists. *) + +(** [N] is an ordered type, using not the usual order on numbers, + but lexicographic ordering on bits (lower bit considered first). *) + +Module NUsualOrderedType <: UsualOrderedType. + Definition t:=N. + Definition eq:=@eq N. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt p q:= Nless p q = true. + + Definition lt_trans := Nless_trans. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + intros; intro. + rewrite H0 in H. + red in H. + rewrite Nless_not_refl in H; discriminate. + Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + intros x y. + destruct (Nless_total x y) as [[H|H]|H]. + apply LT; unfold lt; auto. + apply GT; unfold lt; auto. + apply EQ; auto. + Qed. + +End NUsualOrderedType. + + +(** The module of maps over [N] keys based on [IntMap] *) + +Module MapIntMap <: S with Module E:=NUsualOrderedType. + + Module E:=NUsualOrderedType. + Module ME:=OrderedTypeFacts(E). + Module PE:=KeyOrderedType(E). + + Definition key := N. + + Definition t := Map. + + Section A. + Variable A:Set. + + Definition empty : t A := M0 A. + + Definition is_empty (m : t A) : bool := + MapEmptyp _ (MapCanonicalize _ m). + + Definition find (x:key)(m: t A) : option A := MapGet _ m x. + + Definition mem (x:key)(m: t A) : bool := + match find x m with + | Some _ => true + | None => false + end. + + Definition add (x:key)(v:A)(m:t A) : t A := MapPut _ m x v. + + Definition remove (x:key)(m:t A) : t A := MapRemove _ m x. + + Definition elements (m : t A) : list (N*A) := alist_of_Map _ m. + + Definition MapsTo (x:key)(v:A)(m:t A) := find x m = Some v. + + Definition In (x:key)(m:t A) := exists e:A, MapsTo x e m. + + Definition Empty m := forall (a : key)(e:A) , ~ MapsTo a e m. + + Definition eq_key (p p':key*A) := E.eq (fst p) (fst p'). + + Definition eq_key_elt (p p':key*A) := + E.eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Definition lt_key (p p':key*A) := E.lt (fst p) (fst p'). + + Lemma Empty_alt : forall m, Empty m <-> forall a, find a m = None. + Proof. + unfold Empty, MapsTo. + intuition. + generalize (H a). + destruct (find a m); intuition. + elim (H0 a0); auto. + rewrite H in H0; discriminate. + Qed. + + Section Spec. + Variable m m' m'' : t A. + Variable x y z : key. + Variable e e' : A. + + Lemma MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m. + Proof. intros; rewrite <- H; auto. Qed. + + Lemma find_1 : MapsTo x e m -> find x m = Some e. + Proof. unfold MapsTo; auto. Qed. + + Lemma find_2 : find x m = Some e -> MapsTo x e m. + Proof. red; auto. Qed. + + Lemma empty_1 : Empty empty. + Proof. + rewrite Empty_alt; intros; unfold empty, find; simpl; auto. + Qed. + + Lemma is_empty_1 : Empty m -> is_empty m = true. + Proof. + unfold Empty, is_empty, find; intros. + cut (MapCanonicalize _ m = M0 _). + intros; rewrite H0; simpl; auto. + apply mapcanon_unique. + apply mapcanon_exists_2. + constructor. + red; red; simpl; intros. + rewrite <- (mapcanon_exists_1 _ m). + unfold MapsTo, find in *. + generalize (H a). + destruct (MapGet _ m a); auto. + intros; generalize (H0 a0); destruct 1; auto. + Qed. + + Lemma is_empty_2 : is_empty m = true -> Empty m. + Proof. + unfold Empty, is_empty, MapsTo, find; intros. + generalize (MapEmptyp_complete _ _ H); clear H; intros. + rewrite (mapcanon_exists_1 _ m). + rewrite H; simpl; auto. + discriminate. + Qed. + + Lemma mem_1 : In x m -> mem x m = true. + Proof. + unfold In, MapsTo, mem. + destruct (find x m); auto. + destruct 1; discriminate. + Qed. + + Lemma mem_2 : forall m x, mem x m = true -> In x m. + Proof. + unfold In, MapsTo, mem. + intros. + destruct (find x0 m0); auto; try discriminate. + exists a; auto. + Qed. + + Lemma add_1 : E.eq x y -> MapsTo y e (add x e m). + Proof. + unfold MapsTo, find, add. + intro H; rewrite H; clear H. + rewrite MapPut_semantics. + rewrite Neqb_correct; auto. + Qed. + + Lemma add_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). + Proof. + unfold MapsTo, find, add. + intros. + rewrite MapPut_semantics. + rewrite H0. + generalize (Neqb_complete x y). + destruct (Neqb x y); auto. + intros. + elim H; auto. + apply H1; auto. + Qed. + + Lemma add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. + Proof. + unfold MapsTo, find, add. + rewrite MapPut_semantics. + intro H. + generalize (Neqb_complete x y). + destruct (Neqb x y); auto. + intros; elim H; auto. + apply H0; auto. + Qed. + + Lemma remove_1 : E.eq x y -> ~ In y (remove x m). + Proof. + unfold In, MapsTo, find, remove. + rewrite MapRemove_semantics. + intro H. + rewrite H; rewrite Neqb_correct. + red; destruct 1; discriminate. + Qed. + + Lemma remove_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). + Proof. + unfold MapsTo, find, remove. + rewrite MapRemove_semantics. + intros. + rewrite H0. + generalize (Neqb_complete x y). + destruct (Neqb x y); auto. + intros; elim H; apply H1; auto. + Qed. + + Lemma remove_3 : MapsTo y e (remove x m) -> MapsTo y e m. + Proof. + unfold MapsTo, find, remove. + rewrite MapRemove_semantics. + destruct (Neqb x y); intros; auto. + discriminate. + Qed. + + Lemma alist_sorted_sort : forall l, alist_sorted A l=true -> sort lt_key l. + Proof. + induction l. + auto. + simpl. + destruct a. + destruct l. + auto. + destruct p. + intros; destruct (andb_prop _ _ H); auto. + Qed. + + Lemma elements_3 : sort lt_key (elements m). + Proof. + unfold elements. + apply alist_sorted_sort. + apply alist_of_Map_sorts. + Qed. + + Lemma elements_1 : + MapsTo x e m -> InA eq_key_elt (x,e) (elements m). + Proof. + unfold MapsTo, find, elements. + rewrite InA_alt. + intro H. + exists (x,e). + split. + red; simpl; unfold E.eq; auto. + rewrite alist_of_Map_semantics in H. + generalize H. + set (l:=alist_of_Map A m); clearbody l; clear. + induction l; simpl; auto. + intro; discriminate. + destruct a; simpl; auto. + generalize (Neqb_complete a x). + destruct (Neqb a x); auto. + left. + injection H0; auto. + intros; f_equal; auto. + Qed. + + Lemma elements_2 : + InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. + Proof. + generalize elements_3. + unfold MapsTo, find, elements. + rewrite InA_alt. + intros H ((e0,a),(H0,H1)). + red in H0; simpl in H0; unfold E.eq in H0; destruct H0; subst. + rewrite alist_of_Map_semantics. + generalize H H1; clear H H1. + set (l:=alist_of_Map A m); clearbody l; clear. + induction l; simpl; auto. + intro; contradiction. + intros. + destruct a0; simpl. + inversion H1. + injection H0; intros; subst. + rewrite Neqb_correct; auto. + assert (InA eq_key (e0,a) l). + rewrite InA_alt. + exists (e0,a); split; auto. + red; simpl; auto; red; auto. + generalize (PE.Sort_In_cons_1 H H2). + unfold PE.ltk; simpl. + intros H3; generalize (E.lt_not_eq H3). + generalize (Neqb_complete a0 e0). + destruct (Neqb a0 e0); auto. + destruct 2. + apply H4; auto. + inversion H; auto. + Qed. + + Definition Equal cmp 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). + + (** unfortunately, the [MapFold] of [IntMap] isn't compatible with + the FMap interface. We use a naive version for now : *) + + Definition fold (B:Set)(f:key -> A -> B -> B)(m:t A)(i:B) : B := + fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. + + Lemma fold_1 : + forall (B:Set) (i : B) (f : key -> A -> B -> B), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. + Proof. auto. Qed. + + End Spec. + + Variable B : Set. + + Fixpoint mapi_aux (pf:N->N)(f : N -> A -> B)(m:t A) { struct m }: t B := + match m with + | M0 => M0 _ + | M1 x y => M1 _ x (f (pf x) y) + | M2 m0 m1 => M2 _ (mapi_aux (fun n => pf (Ndouble n)) f m0) + (mapi_aux (fun n => pf (Ndouble_plus_one n)) f m1) + end. + + Definition mapi := mapi_aux (fun n => n). + + Definition map (f:A->B) := mapi (fun _ => f). + + End A. + + Lemma mapi_aux_1 : forall (elt elt':Set)(m: t elt)(pf:N->N)(x:key)(e:elt) + (f:key->elt->elt'), MapsTo x e m -> + exists y, E.eq y x /\ MapsTo x (f (pf y) e) (mapi_aux pf f m). + Proof. + unfold MapsTo; induction m; simpl; auto. + inversion 1. + + intros. + exists x; split; [red; auto|]. + generalize (Neqb_complete a x). + destruct (Neqb a x); try discriminate. + injection H; intros; subst; auto. + rewrite H1; auto. + + intros. + exists x; split; [red;auto|]. + destruct x; simpl in *. + destruct (IHm1 (fun n : N => pf (Ndouble n)) _ _ f H) as (y,(Hy,Hy')). + rewrite Hy in Hy'; simpl in Hy'; auto. + destruct p; simpl in *. + destruct (IHm2 (fun n : N => pf (Ndouble_plus_one n)) _ _ f H) as (y,(Hy,Hy')). + rewrite Hy in Hy'; simpl in Hy'; auto. + destruct (IHm1 (fun n : N => pf (Ndouble n)) _ _ f H) as (y,(Hy,Hy')). + rewrite Hy in Hy'; simpl in Hy'; auto. + destruct (IHm2 (fun n : N => pf (Ndouble_plus_one n)) _ _ f H) as (y,(Hy,Hy')). + rewrite Hy in Hy'; simpl in Hy'; auto. + Qed. + + Lemma mapi_1 : forall (elt elt':Set)(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). + Proof. + intros elt elt' m; exact (mapi_aux_1 (fun n => n)). + Qed. + + Lemma mapi_aux_2 : forall (elt elt':Set)(m: t elt)(pf:N->N)(x:key) + (f:key->elt->elt'), In x (mapi_aux pf f m) -> In x m. + Proof. + unfold In, MapsTo. + induction m; simpl in *. + intros pf x f (e,He); inversion He. + intros pf x f (e,He). + exists a0. + destruct (Neqb a x); try discriminate; auto. + intros pf x f (e,He). + destruct x; [|destruct p]; eauto. + Qed. + + Lemma mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + (f:key->elt->elt'), In x (mapi f m) -> In x m. + Proof. + intros elt elt' m; exact (mapi_aux_2 m (fun n => n)). + Qed. + + Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + MapsTo x e m -> MapsTo x (f e) (map f m). + Proof. + unfold map; intros. + destruct (@mapi_1 _ _ m x e (fun _ => f)) as (e',(_,H0)); auto. + Qed. + + Lemma map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), + In x (map f m) -> In x m. + Proof. + unfold map; intros. + eapply mapi_2; eauto. + Qed. + + Module L := FMapList.Raw E. + + (** Not exactly pretty nor perfect, but should suffice as a first naive implem. + Anyway, map2 isn't in Ocaml... + *) + + Definition anti_elements (A:Set)(l:list (key*A)) := L.fold (@add _) l (empty _). + + Definition map2 (A B C:Set)(f:option A->option B -> option C)(m:t A)(m':t B) : t C := + anti_elements (L.map2 f (elements m) (elements m')). + + Lemma add_spec : forall (A:Set)(m:t A) x y e, + find x (add y e m) = if ME.eq_dec x y then Some e else find x m. + Proof. + intros. + destruct (ME.eq_dec x y). + apply find_1. + eapply MapsTo_1 with y; eauto. + red; auto. + apply add_1; auto. + red; auto. + case_eq (find x m); intros. + apply find_1. + apply add_2; auto. + case_eq (find x (add y e m)); auto; intros. + rewrite <- H; symmetry. + apply find_1; auto. + apply (@add_3 _ m y x a e); auto. + Qed. + + Lemma anti_elements_mapsto_aux : forall (A:Set)(l:list (key*A)) m k e, + NoDupA (eq_key (A:=A)) l -> + (forall x, L.PX.In x l -> In x m -> False) -> + (MapsTo k e (L.fold (@add _) l m) <-> L.PX.MapsTo k e l \/ MapsTo k e m). + Proof. + induction l. + simpl; auto. + intuition. + inversion H2. + simpl; destruct a; intros. + rewrite IHl; clear IHl. + inversion H; auto. + intros. + inversion_clear H. + assert (~E.eq x k). + swap H3. + destruct H1. + apply InA_eqA with (x,x0); eauto. + unfold eq_key, E.eq; eauto. + unfold eq_key, E.eq; congruence. + apply (H0 x). + destruct H1; exists x0; auto. + revert H2. + unfold In. + intros (e',He'). + exists e'; apply (@add_3 _ m k x e' a); unfold E.eq; auto. + intuition. + red in H2. + rewrite add_spec in H2; auto. + destruct (ME.eq_dec k0 k). + inversion_clear H2; subst; auto. + right; apply find_2; auto. + inversion_clear H2; auto. + compute in H1; destruct H1. + subst; right; apply add_1; auto. + red; auto. + inversion_clear H. + destruct (ME.eq_dec k0 k). + subst. + destruct (H0 k); eauto. + red; eauto. + right; apply add_2; auto. + Qed. + + Lemma anti_elements_mapsto : forall (A:Set) l k e, NoDupA (eq_key (A:=A)) l -> + (MapsTo k e (anti_elements l) <-> L.PX.MapsTo k e l). + Proof. + intros. + unfold anti_elements. + rewrite anti_elements_mapsto_aux; auto; unfold empty; auto. + inversion 2. + inversion H2. + intuition. + inversion H1. + Qed. + + Lemma find_anti_elements : forall (A:Set)(l: list (key*A)) x, sort (@lt_key _) l -> + find x (anti_elements l) = L.find x l. + Proof. + intros. + case_eq (L.find x l); intros. + apply find_1. + rewrite anti_elements_mapsto. + apply L.PX.Sort_NoDupA; auto. + apply L.find_2; auto. + case_eq (find x (anti_elements l)); auto; intros. + rewrite <- H0; symmetry. + apply L.find_1; auto. + rewrite <- anti_elements_mapsto. + apply L.PX.Sort_NoDupA; auto. + apply find_2; auto. + Qed. + + Lemma find_elements : forall (A:Set)(m: t A) x, + L.find x (elements m) = find x m. + Proof. + intros. + case_eq (find x m); intros. + apply L.find_1. + apply elements_3; auto. + red; apply elements_1. + apply find_2; auto. + case_eq (L.find x (elements m)); auto; intros. + rewrite <- H; symmetry. + apply find_1; auto. + apply elements_2. + apply L.find_2; auto. + Qed. + + Lemma elements_in : forall (A:Set)(s:t A) x, L.PX.In x (elements s) <-> In x s. + Proof. + intros. + unfold L.PX.In, In. + firstorder. + exists x0. + red; rewrite <- find_elements; auto. + apply L.find_1; auto. + apply elements_3. + exists x0. + apply L.find_2. + rewrite find_elements; auto. + Qed. + + Lemma map2_1 : forall (A B C:Set)(m: t A)(m': t B)(x:key) + (f:option A->option B ->option C), + In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). + Proof. + unfold map2; intros. + rewrite find_anti_elements; auto. + rewrite <- find_elements; auto. + rewrite <- find_elements; auto. + apply L.map2_1; auto. + apply elements_3; auto. + apply elements_3; auto. + do 2 rewrite elements_in; auto. + apply L.map2_sorted; auto. + apply elements_3; auto. + apply elements_3; auto. + Qed. + + Lemma map2_2 : forall (A B C: Set)(m: t A)(m': t B)(x:key) + (f:option A->option B ->option C), + In x (map2 f m m') -> In x m \/ In x m'. + Proof. + unfold map2; intros. + do 2 rewrite <- elements_in. + apply L.map2_2 with (f:=f); auto. + apply elements_3; auto. + apply elements_3; auto. + destruct H. + exists x0. + rewrite <- anti_elements_mapsto; auto. + apply L.PX.Sort_NoDupA; auto. + apply L.map2_sorted; auto. + apply elements_3; auto. + apply elements_3; auto. + Qed. + + (** same trick for [equal] *) + + Definition equal (A:Set)(cmp:A -> A -> bool)(m m' : t A) : bool := + L.equal cmp (elements m) (elements m'). + + Lemma equal_1 : + forall (A:Set)(m: t A)(m': t A)(cmp: A -> A -> bool), + Equal cmp m m' -> equal cmp m m' = true. + Proof. + unfold equal, Equal. + intros. + apply L.equal_1. + apply elements_3. + apply elements_3. + unfold L.Equal. + destruct H. + split; intros. + do 2 rewrite elements_in; auto. + apply (H0 k); + red; rewrite <- find_elements; apply L.find_1; auto; + apply elements_3. + Qed. + + Lemma equal_2 : + forall (A:Set)(m: t A)(m': t A)(cmp: A -> A -> bool), + equal cmp m m' = true -> Equal cmp m m'. + Proof. + unfold equal, Equal. + intros. + destruct (L.equal_2 (elements_3 m) (elements_3 m') H); clear H. + split. + intros; do 2 rewrite <- elements_in; auto. + intros; apply (H1 k); + apply L.find_2; rewrite find_elements;auto. + Qed. + +End MapIntMap. + diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v new file mode 100644 index 000000000..7c6374899 --- /dev/null +++ b/theories/FSets/FMapPositive.v @@ -0,0 +1,1153 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +Require Import ZArith. +Require Import OrderedType. +Require Import FMapInterface. + +Set Implicit Arguments. + +Open Scope positive_scope. + +(** * An implementation of [FMapInterface.S] for positive keys. *) + +(** This file is an adaptation to the [FMap] framework of a work by + Xavier Leroy and Sandrine Blazy (used for building certified compilers). + Keys are of type [positive], and maps are binary trees: the sequence + of binary digits of a positive number corresponds to a path in such a tree. + This is quite similar to the [IntMap] library, except that no path compression + is implemented, and that the current file is simple enough to be + self-contained. *) + +(** Even if [positive] can be seen as an ordered type with respect to the + usual order (see [OrderedTypeEx]), we use here a lexicographic order + over bits, which is more natural here (lower bits are considered first). *) + +Module PositiveOrderedTypeBits <: OrderedType. + Definition t:=positive. + Definition eq:=@eq positive. + + Fixpoint bits_lt (p q:positive) { struct p } : Prop := + match p, q with + | xH, xI _ => True + | xH, _ => False + | xO p, xO q => bits_lt p q + | xO _, _ => True + | xI p, xI q => bits_lt p q + | xI _, _ => False + end. + + Definition lt:=bits_lt. + + Lemma eq_refl : forall x : t, eq x x. + Proof. red; auto. Qed. + + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Proof. red; auto. Qed. + + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Proof. red; intros; transitivity y; auto. Qed. + + Lemma bits_lt_trans : forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z. + Proof. + induction x. + induction y; destruct z; simpl; eauto; intuition. + induction y; destruct z; simpl; eauto; intuition. + induction y; destruct z; simpl; eauto; intuition. + Qed. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. + exact bits_lt_trans. + Qed. + + Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x. + Proof. + induction x; simpl; auto. + Qed. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + intros; intro. + rewrite <- H0 in H; clear H0 y. + unfold lt in H. + exact (bits_lt_antirefl x H). + Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + induction x; destruct y. + (* I I *) + destruct (IHx y). + apply LT; auto. + apply EQ; rewrite e; red; auto. + apply GT; auto. + (* I O *) + apply GT; simpl; auto. + (* I H *) + apply GT; simpl; auto. + (* O I *) + apply LT; simpl; auto. + (* O O *) + destruct (IHx y). + apply LT; auto. + apply EQ; rewrite e; red; auto. + apply GT; auto. + (* O H *) + apply LT; simpl; auto. + (* H I *) + apply LT; simpl; auto. + (* H O *) + apply GT; simpl; auto. + (* H H *) + apply EQ; red; auto. + Qed. + +End PositiveOrderedTypeBits. + +(** Other positive stuff *) + +Lemma peq_dec (x y: positive): {x = y} + {x <> y}. +Proof. + intros. case_eq ((x ?= y) Eq); intros. + left. apply Pcompare_Eq_eq; auto. + right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. + right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate. +Qed. + +Fixpoint append (i j : positive) {struct i} : positive := + match i with + | xH => j + | xI ii => xI (append ii j) + | xO ii => xO (append ii j) + end. + +Lemma append_assoc_0 : + forall (i j : positive), append i (xO j) = append (append i (xO xH)) j. +Proof. + induction i; intros; destruct j; simpl; + try rewrite (IHi (xI j)); + try rewrite (IHi (xO j)); + try rewrite <- (IHi xH); + auto. +Qed. + +Lemma append_assoc_1 : + forall (i j : positive), append i (xI j) = append (append i (xI xH)) j. +Proof. + induction i; intros; destruct j; simpl; + try rewrite (IHi (xI j)); + try rewrite (IHi (xO j)); + try rewrite <- (IHi xH); + auto. +Qed. + +Lemma append_neutral_r : forall (i : positive), append i xH = i. +Proof. + induction i; simpl; congruence. +Qed. + +Lemma append_neutral_l : forall (i : positive), append xH i = i. +Proof. + simpl; auto. +Qed. + + +(** The module of maps over positive keys *) + +Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. + + Module E:=PositiveOrderedTypeBits. + + Definition key := positive. + + Inductive tree (A : Set) : Set := + | Leaf : tree A + | Node : tree A -> option A -> tree A -> tree A. + + Definition t := tree. + + Section A. + Variable A:Set. + + Implicit Arguments Leaf [A]. + + Definition empty : t A := Leaf. + + Fixpoint is_empty (m : t A) {struct m} : bool := + match m with + | Leaf => true + | Node l None r => (is_empty l) && (is_empty r) + | _ => false + end. + + Fixpoint find (i : positive) (m : t A) {struct i} : option A := + match m with + | Leaf => None + | Node l o r => + match i with + | xH => o + | xO ii => find ii l + | xI ii => find ii r + end + end. + + Fixpoint mem (i : positive) (m : t A) {struct i} : bool := + match m with + | Leaf => false + | Node l o r => + match i with + | xH => match o with None => false | _ => true end + | xO ii => mem ii l + | xI ii => mem ii r + end + end. + + Fixpoint add (i : positive) (v : A) (m : t A) {struct i} : t A := + match m with + | Leaf => + match i with + | xH => Node Leaf (Some v) Leaf + | xO ii => Node (add ii v Leaf) None Leaf + | xI ii => Node Leaf None (add ii v Leaf) + end + | Node l o r => + match i with + | xH => Node l (Some v) r + | xO ii => Node (add ii v l) o r + | xI ii => Node l o (add ii v r) + end + end. + + Fixpoint remove (i : positive) (m : t A) {struct i} : t A := + match i with + | xH => + match m with + | Leaf => Leaf + | Node Leaf o Leaf => Leaf + | Node l o r => Node l None r + end + | xO ii => + match m with + | Leaf => Leaf + | Node l None Leaf => + match remove ii l with + | Leaf => Leaf + | mm => Node mm None Leaf + end + | Node l o r => Node (remove ii l) o r + end + | xI ii => + match m with + | Leaf => Leaf + | Node Leaf None r => + match remove ii r with + | Leaf => Leaf + | mm => Node Leaf None mm + end + | Node l o r => Node l o (remove ii r) + end + end. + + (** [elements] *) + + Fixpoint xelements (m : t A) (i : positive) {struct m} + : list (positive * A) := + match m with + | Leaf => nil + | Node l None r => + (xelements l (append i (xO xH))) ++ (xelements r (append i (xI xH))) + | Node l (Some x) r => + (xelements l (append i (xO xH))) + ++ ((i, x) :: xelements r (append i (xI xH))) + end. + + (* Note: function [xelements] above is inefficient. We should apply + deforestation to it, but that makes the proofs even harder. *) + + Definition elements (m : t A) := xelements m xH. + + Section CompcertSpec. + + Theorem gempty: + forall (i: positive), find i empty = None. + Proof. + destruct i; simpl; auto. + Qed. + + Theorem gss: + forall (i: positive) (x: A) (m: t A), find i (add i x m) = Some x. + Proof. + induction i; destruct m; simpl; auto. + Qed. + + Lemma gleaf : forall (i : positive), find i (Leaf : t A) = None. + Proof. exact gempty. Qed. + + Theorem gso: + forall (i j: positive) (x: A) (m: t A), + i <> j -> find i (add j x m) = find i m. + Proof. + induction i; intros; destruct j; destruct m; simpl; + try rewrite <- (gleaf i); auto; try apply IHi; congruence. + Qed. + + Lemma rleaf : forall (i : positive), remove i (Leaf : t A) = Leaf. + Proof. destruct i; simpl; auto. Qed. + + Theorem grs: + forall (i: positive) (m: t A), find i (remove i m) = None. + Proof. + induction i; destruct m. + simpl; auto. + destruct m1; destruct o; destruct m2 as [ | ll oo rr]; simpl; auto. + rewrite (rleaf i); auto. + cut (find i (remove i (Node ll oo rr)) = None). + destruct (remove i (Node ll oo rr)); auto; apply IHi. + apply IHi. + simpl; auto. + destruct m1 as [ | ll oo rr]; destruct o; destruct m2; simpl; auto. + rewrite (rleaf i); auto. + cut (find i (remove i (Node ll oo rr)) = None). + destruct (remove i (Node ll oo rr)); auto; apply IHi. + apply IHi. + simpl; auto. + destruct m1; destruct m2; simpl; auto. + Qed. + + Theorem gro: + forall (i j: positive) (m: t A), + i <> j -> find i (remove j m) = find i m. + Proof. + induction i; intros; destruct j; destruct m; + try rewrite (rleaf (xI j)); + try rewrite (rleaf (xO j)); + try rewrite (rleaf 1); auto; + destruct m1; destruct o; destruct m2; + simpl; + try apply IHi; try congruence; + try rewrite (rleaf j); auto; + try rewrite (gleaf i); auto. + cut (find i (remove j (Node m2_1 o m2_2)) = find i (Node m2_1 o m2_2)); + [ destruct (remove j (Node m2_1 o m2_2)); try rewrite (gleaf i); auto + | apply IHi; congruence ]. + destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf i); + auto. + destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf i); + auto. + cut (find i (remove j (Node m1_1 o0 m1_2)) = find i (Node m1_1 o0 m1_2)); + [ destruct (remove j (Node m1_1 o0 m1_2)); try rewrite (gleaf i); auto + | apply IHi; congruence ]. + destruct (remove j (Node m2_1 o m2_2)); simpl; try rewrite (gleaf i); + auto. + destruct (remove j (Node m1_1 o0 m1_2)); simpl; try rewrite (gleaf i); + auto. + Qed. + + Lemma xelements_correct: + forall (m: t A) (i j : positive) (v: A), + find i m = Some v -> List.In (append j i, v) (xelements m j). + Proof. + induction m; intros. + rewrite (gleaf i) in H; congruence. + destruct o; destruct i; simpl; simpl in H. + rewrite append_assoc_1; apply in_or_app; right; apply in_cons; + apply IHm2; auto. + rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. + rewrite append_neutral_r; apply in_or_app; injection H; + intro EQ; rewrite EQ; right; apply in_eq. + rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. + rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. + congruence. + Qed. + + Theorem elements_correct: + forall (m: t A) (i: positive) (v: A), + find i m = Some v -> List.In (i, v) (elements m). + Proof. + intros m i v H. + exact (xelements_correct m i xH H). + Qed. + + Fixpoint xfind (i j : positive) (m : t A) {struct j} : option A := + match i, j with + | _, xH => find i m + | xO ii, xO jj => xfind ii jj m + | xI ii, xI jj => xfind ii jj m + | _, _ => None + end. + + Lemma xfind_left : + forall (j i : positive) (m1 m2 : t A) (o : option A) (v : A), + xfind i (append j (xO xH)) m1 = Some v -> xfind i j (Node m1 o m2) = Some v. + Proof. + induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. + destruct i; congruence. + Qed. + + Lemma xelements_ii : + forall (m: t A) (i j : positive) (v: A), + List.In (xI i, v) (xelements m (xI j)) -> List.In (i, v) (xelements m j). + Proof. + induction m. + simpl; auto. + intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); + apply in_or_app. + left; apply IHm1; auto. + right; destruct (in_inv H0). + injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq. + apply in_cons; apply IHm2; auto. + left; apply IHm1; auto. + right; apply IHm2; auto. + Qed. + + Lemma xelements_io : + forall (m: t A) (i j : positive) (v: A), + ~List.In (xI i, v) (xelements m (xO j)). + Proof. + induction m. + simpl; auto. + intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). + apply (IHm1 _ _ _ H0). + destruct (in_inv H0). + congruence. + apply (IHm2 _ _ _ H1). + apply (IHm1 _ _ _ H0). + apply (IHm2 _ _ _ H0). + Qed. + + Lemma xelements_oo : + forall (m: t A) (i j : positive) (v: A), + List.In (xO i, v) (xelements m (xO j)) -> List.In (i, v) (xelements m j). + Proof. + induction m. + simpl; auto. + intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); + apply in_or_app. + left; apply IHm1; auto. + right; destruct (in_inv H0). + injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq. + apply in_cons; apply IHm2; auto. + left; apply IHm1; auto. + right; apply IHm2; auto. + Qed. + + Lemma xelements_oi : + forall (m: t A) (i j : positive) (v: A), + ~List.In (xO i, v) (xelements m (xI j)). + Proof. + induction m. + simpl; auto. + intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). + apply (IHm1 _ _ _ H0). + destruct (in_inv H0). + congruence. + apply (IHm2 _ _ _ H1). + apply (IHm1 _ _ _ H0). + apply (IHm2 _ _ _ H0). + Qed. + + Lemma xelements_ih : + forall (m1 m2: t A) (o: option A) (i : positive) (v: A), + List.In (xI i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m2 xH). + Proof. + destruct o; simpl; intros; destruct (in_app_or _ _ _ H). + absurd (List.In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto. + destruct (in_inv H0). + congruence. + apply xelements_ii; auto. + absurd (List.In (xI i, v) (xelements m1 2)); auto; apply xelements_io; auto. + apply xelements_ii; auto. + Qed. + + Lemma xelements_oh : + forall (m1 m2: t A) (o: option A) (i : positive) (v: A), + List.In (xO i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m1 xH). + Proof. + destruct o; simpl; intros; destruct (in_app_or _ _ _ H). + apply xelements_oo; auto. + destruct (in_inv H0). + congruence. + absurd (List.In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. + apply xelements_oo; auto. + absurd (List.In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. + Qed. + + Lemma xelements_hi : + forall (m: t A) (i : positive) (v: A), + ~List.In (xH, v) (xelements m (xI i)). + Proof. + induction m; intros. + simpl; auto. + destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). + generalize H0; apply IHm1; auto. + destruct (in_inv H0). + congruence. + generalize H1; apply IHm2; auto. + generalize H0; apply IHm1; auto. + generalize H0; apply IHm2; auto. + Qed. + + Lemma xelements_ho : + forall (m: t A) (i : positive) (v: A), + ~List.In (xH, v) (xelements m (xO i)). + Proof. + induction m; intros. + simpl; auto. + destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). + generalize H0; apply IHm1; auto. + destruct (in_inv H0). + congruence. + generalize H1; apply IHm2; auto. + generalize H0; apply IHm1; auto. + generalize H0; apply IHm2; auto. + Qed. + + Lemma find_xfind_h : + forall (m: t A) (i: positive), find i m = xfind i xH m. + Proof. + destruct i; simpl; auto. + Qed. + + Lemma xelements_complete: + forall (i j : positive) (m: t A) (v: A), + List.In (i, v) (xelements m j) -> xfind i j m = Some v. + Proof. + induction i; simpl; intros; destruct j; simpl. + apply IHi; apply xelements_ii; auto. + absurd (List.In (xI i, v) (xelements m (xO j))); auto; apply xelements_io. + destruct m. + simpl in H; tauto. + rewrite find_xfind_h. apply IHi. apply (xelements_ih _ _ _ _ _ H). + absurd (List.In (xO i, v) (xelements m (xI j))); auto; apply xelements_oi. + apply IHi; apply xelements_oo; auto. + destruct m. + simpl in H; tauto. + rewrite find_xfind_h. apply IHi. apply (xelements_oh _ _ _ _ _ H). + absurd (List.In (xH, v) (xelements m (xI j))); auto; apply xelements_hi. + absurd (List.In (xH, v) (xelements m (xO j))); auto; apply xelements_ho. + destruct m. + simpl in H; tauto. + destruct o; simpl in H; destruct (in_app_or _ _ _ H). + absurd (List.In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. + destruct (in_inv H0). + congruence. + absurd (List.In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. + absurd (List.In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. + absurd (List.In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. + Qed. + + Theorem elements_complete: + forall (m: t A) (i: positive) (v: A), + List.In (i, v) (elements m) -> find i m = Some v. + Proof. + intros m i v H. + unfold elements in H. + rewrite find_xfind_h. + exact (xelements_complete i xH m v H). + Qed. + + End CompcertSpec. + + Definition MapsTo (i:positive)(v:A)(m:t A) := find i m = Some v. + + Definition In (i:positive)(m:t A) := exists e:A, MapsTo i e m. + + Definition Empty m := forall (a : positive)(e:A) , ~ MapsTo a e m. + + Definition eq_key (p p':positive*A) := E.eq (fst p) (fst p'). + + Definition eq_key_elt (p p':positive*A) := + E.eq (fst p) (fst p') /\ (snd p) = (snd p'). + + Definition lt_key (p p':positive*A) := E.lt (fst p) (fst p'). + + Lemma mem_find : + forall m x, mem x m = match find x m with None => false | _ => true end. + Proof. + induction m; destruct x; simpl; auto. + Qed. + + Lemma Empty_alt : forall m, Empty m <-> forall a, find a m = None. + Proof. + unfold Empty, MapsTo. + intuition. + generalize (H a). + destruct (find a m); intuition. + elim (H0 a0); auto. + rewrite H in H0; discriminate. + Qed. + + Lemma Empty_Node : forall l o r, Empty (Node l o r) <-> o=None /\ Empty l /\ Empty r. + Proof. + intros l o r. + split. + rewrite Empty_alt. + split. + destruct o; auto. + generalize (H 1); simpl; auto. + split; rewrite Empty_alt; intros. + generalize (H (xO a)); auto. + generalize (H (xI a)); auto. + intros (H,(H0,H1)). + subst. + rewrite Empty_alt; intros. + destruct a; auto. + simpl; generalize H1; rewrite Empty_alt; auto. + simpl; generalize H0; rewrite Empty_alt; auto. + Qed. + + Section FMapSpec. + + Lemma mem_1 : forall m x, In x m -> mem x m = true. + Proof. + unfold In, MapsTo; intros m x; rewrite mem_find. + destruct 1 as (e0,H0); rewrite H0; auto. + Qed. + + Lemma mem_2 : forall m x, mem x m = true -> In x m. + Proof. + unfold In, MapsTo; intros m x; rewrite mem_find. + destruct (find x m). + exists a; auto. + intros; discriminate. + Qed. + + Variable m m' m'' : t A. + Variable x y z : key. + Variable e e' : A. + + Lemma MapsTo_1 : E.eq x y -> MapsTo x e m -> MapsTo y e m. + Proof. intros; rewrite <- H; auto. Qed. + + Lemma find_1 : MapsTo x e m -> find x m = Some e. + Proof. unfold MapsTo; auto. Qed. + + Lemma find_2 : find x m = Some e -> MapsTo x e m. + Proof. red; auto. Qed. + + Lemma empty_1 : Empty empty. + Proof. + rewrite Empty_alt; apply gempty. + Qed. + + Lemma is_empty_1 : Empty m -> is_empty m = true. + Proof. + induction m; simpl; auto. + rewrite Empty_Node. + intros (H,(H0,H1)). + subst; simpl. + rewrite IHt0_1; simpl; auto. + Qed. + + Lemma is_empty_2 : is_empty m = true -> Empty m. + Proof. + induction m; simpl; auto. + rewrite Empty_alt. + intros _; exact gempty. + rewrite Empty_Node. + destruct o. + intros; discriminate. + intro H; destruct (andb_prop _ _ H); intuition. + Qed. + + Lemma add_1 : E.eq x y -> MapsTo y e (add x e m). + Proof. + unfold MapsTo. + intro H; rewrite H; clear H. + apply gss. + Qed. + + Lemma add_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (add x e' m). + Proof. + unfold MapsTo. + intros; rewrite gso; auto. + Qed. + + Lemma add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m. + Proof. + unfold MapsTo. + intro H; rewrite gso; auto. + Qed. + + Lemma remove_1 : E.eq x y -> ~ In y (remove x m). + Proof. + intros; intro. + generalize (mem_1 H0). + rewrite mem_find. + rewrite H. + rewrite grs. + intros; discriminate. + Qed. + + Lemma remove_2 : ~ E.eq x y -> MapsTo y e m -> MapsTo y e (remove x m). + Proof. + unfold MapsTo. + intro H; rewrite gro; auto. + Qed. + + Lemma remove_3 : MapsTo y e (remove x m) -> MapsTo y e m. + Proof. + unfold MapsTo. + destruct (peq_dec x y). + subst. + rewrite grs; intros; discriminate. + rewrite gro; auto. + Qed. + + Lemma elements_1 : + MapsTo x e m -> InA eq_key_elt (x,e) (elements m). + Proof. + unfold MapsTo. + rewrite InA_alt. + intro H. + exists (x,e). + split. + red; simpl; unfold E.eq; auto. + apply elements_correct; auto. + Qed. + + Lemma elements_2 : + InA eq_key_elt (x,e) (elements m) -> MapsTo x e m. + Proof. + unfold MapsTo. + rewrite InA_alt. + intros ((e0,a),(H,H0)). + red in H; simpl in H; unfold E.eq in H; destruct H; subst. + apply elements_complete; auto. + Qed. + + Lemma xelements_bits_lt_1 : forall p p0 q m v, + List.In (p0,v) (xelements m (append p (xO q))) -> E.bits_lt p0 p. + Proof. + intros. + generalize (xelements_complete _ _ _ _ H); clear H; intros. + revert H; revert v; revert m; revert q; revert p0. + induction p; destruct p0; simpl; intros; eauto; try discriminate. + Qed. + + Lemma xelements_bits_lt_2 : forall p p0 q m v, + List.In (p0,v) (xelements m (append p (xI q))) -> E.bits_lt p p0. + Proof. + intros. + generalize (xelements_complete _ _ _ _ H); clear H; intros. + revert H; revert v; revert m; revert q; revert p0. + induction p; destruct p0; simpl; intros; eauto; try discriminate. + Qed. + + Lemma xelements_sort : forall p, sort lt_key (xelements m p). + Proof. + induction m. + simpl; auto. + destruct o; simpl; intros. + (* Some *) + apply (SortA_app (eqA:=eq_key_elt)); auto. + compute; intuition. + constructor; auto. + apply In_InfA; intros. + destruct y0. + red; red; simpl. + eapply xelements_bits_lt_2; eauto. + intros x0 y0. + do 2 rewrite InA_alt. + intros (y1,(Hy1,H)) (y2,(Hy2,H0)). + destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst. + destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. + red; red; simpl. + destruct H0. + injection H0; clear H0; intros _ H0; subst. + eapply xelements_bits_lt_1; eauto. + apply E.bits_lt_trans with p. + eapply xelements_bits_lt_1; eauto. + eapply xelements_bits_lt_2; eauto. + (* None *) + apply (SortA_app (eqA:=eq_key_elt)); auto. + compute; intuition. + intros x0 y0. + do 2 rewrite InA_alt. + intros (y1,(Hy1,H)) (y2,(Hy2,H0)). + destruct y1; destruct x0; compute in Hy1; destruct Hy1; subst. + destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. + red; red; simpl. + apply E.bits_lt_trans with p. + eapply xelements_bits_lt_1; eauto. + eapply xelements_bits_lt_2; eauto. + Qed. + + Lemma elements_3 : sort lt_key (elements m). + Proof. + unfold elements. + apply xelements_sort; auto. + Qed. + + End FMapSpec. + + (** [map] and [mapi] *) + + Variable B : Set. + + Fixpoint xmapi (f : positive -> A -> B) (m : t A) (i : positive) + {struct m} : t B := + match m with + | Leaf => @Leaf B + | Node l o r => Node (xmapi f l (append i (xO xH))) + (option_map (f i) o) + (xmapi f r (append i (xI xH))) + end. + + Definition mapi (f : positive -> A -> B) m := xmapi f m xH. + + Definition map (f : A -> B) m := mapi (fun _ => f) m. + + End A. + + Lemma xgmapi: + forall (A B: Set) (f: positive -> A -> B) (i j : positive) (m: t A), + find i (xmapi f m j) = option_map (f (append j i)) (find i m). + Proof. + induction i; intros; destruct m; simpl; auto. + rewrite (append_assoc_1 j i); apply IHi. + rewrite (append_assoc_0 j i); apply IHi. + rewrite (append_neutral_r j); auto. + Qed. + + Theorem gmapi: + forall (A B: Set) (f: positive -> A -> B) (i: positive) (m: t A), + find i (mapi f m) = option_map (f i) (find i m). + Proof. + intros. + unfold mapi. + replace (f i) with (f (append xH i)). + apply xgmapi. + rewrite append_neutral_l; auto. + Qed. + + Lemma mapi_1 : + forall (elt elt':Set)(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). + Proof. + intros. + exists x. + split; [red; auto|]. + apply find_2. + generalize (find_1 H); clear H; intros. + rewrite gmapi. + rewrite H. + simpl; auto. + Qed. + + Lemma mapi_2 : + forall (elt elt':Set)(m: t elt)(x:key)(f:key->elt->elt'), + In x (mapi f m) -> In x m. + Proof. + intros. + apply mem_2. + rewrite mem_find. + destruct H as (v,H). + generalize (find_1 H); clear H; intros. + rewrite gmapi in H. + destruct (find x m); auto. + simpl in *; discriminate. + Qed. + + Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + MapsTo x e m -> MapsTo x (f e) (map f m). + Proof. + intros; unfold map. + destruct (mapi_1 (fun _ => f) H); intuition. + Qed. + + Lemma map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), + In x (map f m) -> In x m. + Proof. + intros; unfold map in *; eapply mapi_2; eauto. + Qed. + + Section map2. + Variable A B C : Set. + Variable f : option A -> option B -> option C. + + Implicit Arguments Leaf [A]. + + Fixpoint xmap2_l (m : t A) {struct m} : t C := + match m with + | Leaf => Leaf + | Node l o r => Node (xmap2_l l) (f o None) (xmap2_l r) + end. + + Lemma xgmap2_l : forall (i : positive) (m : t A), + f None None = None -> find i (xmap2_l m) = f (find i m) None. + Proof. + induction i; intros; destruct m; simpl; auto. + Qed. + + Fixpoint xmap2_r (m : t B) {struct m} : t C := + match m with + | Leaf => Leaf + | Node l o r => Node (xmap2_r l) (f None o) (xmap2_r r) + end. + + Lemma xgmap2_r : forall (i : positive) (m : t B), + f None None = None -> find i (xmap2_r m) = f None (find i m). + Proof. + induction i; intros; destruct m; simpl; auto. + Qed. + + Fixpoint _map2 (m1 : t A)(m2 : t B) {struct m1} : t C := + match m1 with + | Leaf => xmap2_r m2 + | Node l1 o1 r1 => + match m2 with + | Leaf => xmap2_l m1 + | Node l2 o2 r2 => Node (_map2 l1 l2) (f o1 o2) (_map2 r1 r2) + end + end. + + Lemma gmap2: forall (i: positive)(m1:t A)(m2: t B), + f None None = None -> + find i (_map2 m1 m2) = f (find i m1) (find i m2). + Proof. + induction i; intros; destruct m1; destruct m2; simpl; auto; + try apply xgmap2_r; try apply xgmap2_l; auto. + Qed. + + End map2. + + Definition map2 (elt elt' elt'':Set)(f:option elt->option elt'->option elt'') := + _map2 (fun o1 o2 => match o1,o2 with None,None => None | _, _ => f o1 o2 end). + + Lemma map2_1 : forall (elt elt' elt'':Set)(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'). + Proof. + intros. + unfold map2. + rewrite gmap2; auto. + generalize (@mem_1 _ m x) (@mem_1 _ m' x). + do 2 rewrite mem_find. + destruct (find x m); simpl; auto. + destruct (find x m'); simpl; auto. + intros. + destruct H; intuition; try discriminate. + Qed. + + Lemma map2_2 : forall (elt elt' elt'':Set)(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'. + Proof. + intros. + generalize (mem_1 H); clear H; intros. + rewrite mem_find in H. + unfold map2 in H. + rewrite gmap2 in H; auto. + generalize (@mem_2 _ m x) (@mem_2 _ m' x). + do 2 rewrite mem_find. + destruct (find x m); simpl in *; auto. + destruct (find x m'); simpl in *; auto. + Qed. + + + Definition fold (A B : Set) (f: positive -> A -> B -> B) (tr: t A) (v: B) := + List.fold_left (fun a p => f (fst p) (snd p) a) (elements tr) v. + + Lemma fold_1 : + forall (A:Set)(m:t A)(B:Set)(i : B) (f : key -> A -> B -> B), + fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. + Proof. + intros; unfold fold; auto. + Qed. + + Fixpoint equal (A:Set)(cmp : A -> A -> bool)(m1 m2 : t A) {struct m1} : bool := + match m1, m2 with + | Leaf, _ => is_empty m2 + | _, Leaf => is_empty m1 + | Node l1 o1 r1, Node l2 o2 r2 => + (match o1, o2 with + | None, None => true + | Some v1, Some v2 => cmp v1 v2 + | _, _ => false + end) + && equal cmp l1 l2 && equal cmp r1 r2 + end. + + Definition Equal (A:Set)(cmp:A->A->bool)(m m':t A) := + (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 equal_1 : forall (A:Set)(m m':t A)(cmp:A->A->bool), + Equal cmp m m' -> equal cmp m m' = true. + Proof. + induction m. + (* m = Leaf *) + destruct 1. + simpl. + apply is_empty_1. + red; red; intros. + assert (In a (Leaf A)). + rewrite H. + exists e; auto. + destruct H2; red in H2. + destruct a; simpl in *; discriminate. + (* m = Node *) + destruct m'. + (* m' = Leaf *) + destruct 1. + simpl. + destruct o. + assert (In xH (Leaf A)). + rewrite <- H. + exists a; red; auto. + destruct H1; red in H1; simpl in H1; discriminate. + apply andb_true_intro; split; apply is_empty_1; red; red; intros. + assert (In (xO a) (Leaf A)). + rewrite <- H. + exists e; auto. + destruct H2; red in H2; simpl in H2; discriminate. + assert (In (xI a) (Leaf A)). + rewrite <- H. + exists e; auto. + destruct H2; red in H2; simpl in H2; discriminate. + (* m' = Node *) + destruct 1. + assert (Equal cmp m1 m'1). + split. + intros k; generalize (H (xO k)); unfold In, MapsTo; simpl; auto. + intros k e e'; generalize (H0 (xO k) e e'); unfold In, MapsTo; simpl; auto. + assert (Equal cmp m2 m'2). + split. + intros k; generalize (H (xI k)); unfold In, MapsTo; simpl; auto. + intros k e e'; generalize (H0 (xI k) e e'); unfold In, MapsTo; simpl; auto. + simpl. + destruct o; destruct o0; simpl. + repeat (apply andb_true_intro; split); auto. + apply (H0 xH); red; auto. + generalize (H xH); unfold In, MapsTo; simpl; intuition. + destruct H4; try discriminate; eauto. + generalize (H xH); unfold In, MapsTo; simpl; intuition. + destruct H5; try discriminate; eauto. + apply andb_true_intro; split; auto. + Qed. + + Lemma equal_2 : forall (A:Set)(m m':t A)(cmp:A->A->bool), + equal cmp m m' = true -> Equal cmp m m'. + Proof. + induction m. + (* m = Leaf *) + simpl. + split; intros. + split. + destruct 1; red in H0; destruct k; discriminate. + destruct 1; elim (is_empty_2 H H0). + red in H0; destruct k; discriminate. + (* m = Node *) + destruct m'. + (* m' = Leaf *) + simpl. + destruct o; intros; try discriminate. + destruct (andb_prop _ _ H); clear H. + split; intros. + split; unfold In, MapsTo; destruct 1. + destruct k; simpl in *; try discriminate. + destruct (is_empty_2 H1 (find_2 _ _ H)). + destruct (is_empty_2 H0 (find_2 _ _ H)). + destruct k; simpl in *; discriminate. + unfold In, MapsTo; destruct k; simpl in *; discriminate. + (* m' = Node *) + destruct o; destruct o0; simpl; intros; try discriminate. + destruct (andb_prop _ _ H); clear H. + destruct (andb_prop _ _ H0); clear H0. + destruct (IHm1 _ _ H2); clear H2 IHm1. + destruct (IHm2 _ _ H1); clear H1 IHm2. + split; intros. + destruct k; unfold In, MapsTo in *; simpl; auto. + split; eauto. + destruct k; unfold In, MapsTo in *; simpl in *. + eapply H4; eauto. + eapply H3; eauto. + congruence. + destruct (andb_prop _ _ H); clear H. + destruct (IHm1 _ _ H0); clear H0 IHm1. + destruct (IHm2 _ _ H1); clear H1 IHm2. + split; intros. + destruct k; unfold In, MapsTo in *; simpl; auto. + split; eauto. + destruct k; unfold In, MapsTo in *; simpl in *. + eapply H3; eauto. + eapply H2; eauto. + try discriminate. + Qed. + +End PositiveMap. + +(** Here come some additionnal facts about this implementation. + Most are facts that cannot be derivable from the general interface. *) + + +Module PositiveMapAdditionalFacts. + Import PositiveMap. + + (* Derivable from the Map interface *) + Theorem gsspec: + forall (A:Set)(i j: positive) (x: A) (m: t A), + find i (add j x m) = if peq_dec i j then Some x else find i m. + Proof. + intros. + destruct (peq_dec i j); [ rewrite e; apply gss | apply gso; auto ]. + Qed. + + (* Not derivable from the Map interface *) + Theorem gsident: + forall (A:Set)(i: positive) (m: t A) (v: A), + find i m = Some v -> add i v m = m. + Proof. + induction i; intros; destruct m; simpl; simpl in H; try congruence. + rewrite (IHi m2 v H); congruence. + rewrite (IHi m1 v H); congruence. + Qed. + + Lemma xmap2_lr : + forall (A B : Set)(f g: option A -> option A -> option B)(m : t A), + (forall (i j : option A), f i j = g j i) -> + xmap2_l f m = xmap2_r g m. + Proof. + induction m; intros; simpl; auto. + rewrite IHm1; auto. + rewrite IHm2; auto. + rewrite H; auto. + Qed. + + Theorem map2_commut: + forall (A B: Set) (f g: option A -> option A -> option B), + (forall (i j: option A), f i j = g j i) -> + forall (m1 m2: t A), + _map2 f m1 m2 = _map2 g m2 m1. + Proof. + intros A B f g Eq1. + assert (Eq2: forall (i j: option A), g i j = f j i). + intros; auto. + induction m1; intros; destruct m2; simpl; + try rewrite Eq1; + repeat rewrite (xmap2_lr f g); + repeat rewrite (xmap2_lr g f); + auto. + rewrite IHm1_1. + rewrite IHm1_2. + auto. + Qed. + +End PositiveMapAdditionalFacts. + diff --git a/theories/FSets/FMaps.v b/theories/FSets/FMaps.v index dac1b4396..d7b29547a 100644 --- a/theories/FSets/FMaps.v +++ b/theories/FSets/FMaps.v @@ -8,5 +8,10 @@ (* $Id$ *) +Require Export OrderedType. +Require Export OrderedTypeEx. +Require Export OrderedTypeAlt. Require Export FMapInterface. Require Export FMapList. +Require Export FMapPositive. +Require Export FMapIntMap. diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v new file mode 100644 index 000000000..cdc5e8d33 --- /dev/null +++ b/theories/FSets/FSetAVL.v @@ -0,0 +1,2883 @@ + +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +(** This module implements sets using AVL trees. + It follows the implementation from Ocaml's standard library. *) + +Require Import FSetInterface. +Require Import FSetList. +Require Import ZArith. +Require Import Int. + +Set Firstorder Depth 3. + +Module Raw (I:Int)(X:OrderedType). +Import I. +Module II:=MoreInt(I). +Import II. +Open Scope Int_scope. + +Module E := X. +Module MX := OrderedTypeFacts X. + +Definition elt := X.t. + +(** * Trees *) + +Inductive tree : Set := + | Leaf : tree + | Node : tree -> X.t -> tree -> int -> tree. + +Notation t := tree. + +(** The fourth field of [Node] is the height of the tree *) + +(** 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 (Node _ _ _ _) |- _ => inversion_clear H; inv f + | H:f _ (Node _ _ _ _) |- _ => inversion_clear H; inv f + | _ => idtac + end. + +(** Same, but with a backup of the original hypothesis. *) + +Ltac safe_inv f := match goal with + | H:f (Node _ _ _ _) |- _ => + generalize H; inversion_clear H; safe_inv f + | _ => intros + end. + +(** * Occurrence in a tree *) + +Inductive In (x : elt) : tree -> Prop := + | IsRoot : + forall (l r : tree) (h : int) (y : elt), + X.eq x y -> In x (Node l y r h) + | InLeft : + forall (l r : tree) (h : int) (y : elt), + In x l -> In x (Node l y r h) + | InRight : + forall (l r : tree) (h : int) (y : elt), + In x r -> In x (Node l y r h). + +Hint Constructors In. + +Ltac intuition_in := repeat progress (intuition; inv In). + +(** [In] is compatible with [X.eq] *) + +Lemma In_1 : + forall s x y, X.eq x y -> In x s -> In y s. +Proof. + induction s; simpl; intuition_in; eauto. +Qed. +Hint Immediate In_1. + +(** * Binary search trees *) + +(** [lt_tree x s]: all elements in [s] are smaller than [x] + (resp. greater for [gt_tree]) *) + +Definition lt_tree (x : elt) (s : tree) := + forall y:elt, In y s -> X.lt y x. +Definition gt_tree (x : elt) (s : tree) := + forall y:elt, In y s -> X.lt x y. + +Hint Unfold lt_tree gt_tree. + +Ltac order := match goal with + | H: lt_tree ?x ?s, H1: In ?y ?s |- _ => generalize (H _ H1); clear H; order + | H: gt_tree ?x ?s, H1: In ?y ?s |- _ => generalize (H _ H1); clear H; order + | _ => MX.order +end. + +(** Results about [lt_tree] and [gt_tree] *) + +Lemma lt_leaf : forall x : elt, lt_tree x Leaf. +Proof. + unfold lt_tree in |- *; intros; inversion H. +Qed. + +Lemma gt_leaf : forall x : elt, gt_tree x Leaf. +Proof. + unfold gt_tree in |- *; intros; inversion H. +Qed. + +Lemma lt_tree_node : + forall (x y : elt) (l r : tree) (h : int), + lt_tree x l -> lt_tree x r -> X.lt y x -> lt_tree x (Node l y r h). +Proof. + unfold lt_tree in *; intuition_in; order. +Qed. + +Lemma gt_tree_node : + forall (x y : elt) (l r : tree) (h : int), + gt_tree x l -> gt_tree x r -> X.lt x y -> gt_tree x (Node l y r h). +Proof. + unfold gt_tree in *; intuition_in; order. +Qed. + +Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. + +Lemma lt_tree_not_in : + forall (x : elt) (t : tree), lt_tree x t -> ~ In x t. +Proof. + intros; intro; order. +Qed. + +Lemma lt_tree_trans : + forall x y, X.lt x y -> forall t, lt_tree x t -> lt_tree y t. +Proof. + firstorder eauto. +Qed. + +Lemma gt_tree_not_in : + forall (x : elt) (t : tree), gt_tree x t -> ~ In x t. +Proof. + intros; intro; order. +Qed. + +Lemma gt_tree_trans : + forall x y, X.lt y x -> forall t, gt_tree x t -> gt_tree y t. +Proof. + firstorder eauto. +Qed. + +Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. + +(** [bst t] : [t] is a binary search tree *) + +Inductive bst : tree -> Prop := + | BSLeaf : bst Leaf + | BSNode : + forall (x : elt) (l r : tree) (h : int), + bst l -> bst r -> lt_tree x l -> gt_tree x r -> bst (Node l x r h). + +Hint Constructors bst. + +(** * 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 *) + +Definition height (s : tree) : int := + match s with + | Leaf => 0 + | Node _ _ _ h => h + end. + +Inductive avl : tree -> Prop := + | RBLeaf : avl Leaf + | RBNode : + forall (x : elt) (l r : tree) (h : int), + avl l -> + avl r -> + -(2) <= height l - height r <= 2 -> + h = max (height l) (height r) + 1 -> + avl (Node l x r h). + +Hint Constructors avl. + +(** Results about [avl] *) + +Lemma avl_node : + forall (x : elt) (l r : tree), + avl l -> + avl r -> + -(2) <= height l - height r <= 2 -> + avl (Node l x r (max (height l) (height r) + 1)). +Proof. + intros; auto. +Qed. +Hint Resolve avl_node. + +(** The tactics *) + +Lemma height_non_negative : forall s : tree, avl s -> height s >= 0. +Proof. + induction s; simpl; intros; auto with zarith. + inv avl; intuition; omega_max. +Qed. +Implicit Arguments height_non_negative. + +(** When [H:avl r], typing [avl_nn H] or [avl_nn r] adds [height r>=0] *) + +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. + +(** * Some shortcuts. *) + +Definition Equal s s' := forall a : elt, In a s <-> In a s'. +Definition Subset s s' := forall a : elt, In a s -> In a s'. +Definition Empty s := forall a : elt, ~ In a s. +Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x. +Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x. + +(** * Empty set *) + +Definition empty := Leaf. + +Lemma empty_bst : bst empty. +Proof. + auto. +Qed. + +Lemma empty_avl : avl empty. +Proof. + auto. +Qed. + +Lemma empty_1 : Empty empty. +Proof. + intro; intro. + inversion H. +Qed. + +(** * Emptyness test *) + +Definition is_empty (s:t) := match s with Leaf => true | _ => false end. + +Lemma is_empty_1 : forall s, Empty s -> is_empty s = true. +Proof. + destruct s as [|r x l h]; simpl; auto. + intro H; elim (H x); auto. +Qed. + +Lemma is_empty_2 : forall s, is_empty s = true -> Empty s. +Proof. + destruct s; simpl; intros; try discriminate; red; auto. +Qed. + +(** * Appartness *) + +(** The [mem] function is deciding appartness. It exploits the [bst] property + to achieve logarithmic complexity. *) + +Fixpoint mem (x:elt)(s:t) { struct s } : bool := + match s 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. + +Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true. +Proof. + intros s x. + functional induction mem x s; inversion_clear 1; auto. + inversion_clear 1. + inversion_clear 1; auto; absurd (X.lt x y); eauto. + inversion_clear 1; auto; absurd (X.lt y x); eauto. +Qed. + +Lemma mem_2 : forall s x, mem x s = true -> In x s. +Proof. + intros s x. + functional induction mem x s; auto; intros; try discriminate. +Qed. + +(** * Singleton set *) + +Definition singleton (x : elt) := Node Leaf x Leaf 1. + +Lemma singleton_bst : forall x : elt, bst (singleton x). +Proof. + unfold singleton; auto. +Qed. + +Lemma singleton_avl : forall x : elt, avl (singleton x). +Proof. + unfold singleton; intro. + constructor; auto; try red; simpl; omega_max. +Qed. + +Lemma singleton_1 : forall x y, In y (singleton x) -> X.eq x y. +Proof. + unfold singleton; inversion_clear 1; auto; inversion_clear H0. +Qed. + +Lemma singleton_2 : forall x y, X.eq x y -> In y (singleton x). +Proof. + unfold singleton; auto. +Qed. + +(** * Helper functions *) + +(** [create l x r] creates a node, assuming [l] and [r] + to be balanced and [|height l - height r| <= 2]. *) + +Definition create l x r := + Node l x r (max (height l) (height r) + 1). + +Lemma create_bst : + forall l x r, bst l -> bst r -> lt_tree x l -> gt_tree x r -> + bst (create l x r). +Proof. + unfold create; auto. +Qed. +Hint Resolve create_bst. + +Lemma create_avl : + forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> + avl (create l x r). +Proof. + unfold create; auto. +Qed. + +Lemma create_height : + forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> + height (create l x r) = max (height l) (height r) + 1. +Proof. + unfold create; intros; auto. +Qed. + +Lemma create_in : + forall l x r y, In y (create l x r) <-> X.eq y x \/ In y l \/ In y r. +Proof. + unfold create; split; [ inversion_clear 1 | ]; intuition. +Qed. + +(** trick for emulating [assert false] in Coq *) + +Definition assert_false := Leaf. + +(** [bal l x r] acts as [create], but performs one step of + rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *) + +Definition bal l x 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 + | Node ll lx lr _ => + if ge_lt_dec (height ll) (height lr) then + create ll lx (create lr x r) + else + match lr with + | Leaf => assert_false + | Node lrl lrx lrr _ => + create (create ll lx lrl) lrx (create lrr x r) + end + end + else + if gt_le_dec hr (hl+2) then + match r with + | Leaf => assert_false + | Node rl rx rr _ => + if ge_lt_dec (height rr) (height rl) then + create (create l x rl) rx rr + else + match rl with + | Leaf => assert_false + | Node rll rlx rlr _ => + create (create l x rll) rlx (create rlr rx rr) + end + end + else + create l x r. + +Ltac bal_tac := + intros l x r; + unfold bal; + destruct (gt_le_dec (height l) (height r + 2)); + [ destruct l as [ |ll lx lr lh]; + [ | destruct (ge_lt_dec (height ll) (height lr)); + [ | destruct lr ] ] + | destruct (gt_le_dec (height r) (height l + 2)); + [ destruct r as [ |rl rx rr rh]; + [ | destruct (ge_lt_dec (height rr) (height rl)); + [ | destruct rl ] ] + | ] ]; intros. + +Lemma bal_bst : forall l x r, bst l -> bst r -> + lt_tree x l -> gt_tree x r -> bst (bal l x r). +Proof. + (* intros l x r; functional induction bal l x r. MARCHE PAS !*) + bal_tac; + inv bst; repeat apply create_bst; auto; unfold create; + apply lt_tree_node || apply gt_tree_node; auto; + eapply lt_tree_trans || eapply gt_tree_trans || eauto; eauto. +Qed. + +Lemma bal_avl : forall l x r, avl l -> avl r -> + -(3) <= height l - height r <= 3 -> avl (bal l x r). +Proof. + bal_tac; inv avl; repeat apply create_avl; simpl in *; auto; omega_max. +Qed. + +Lemma bal_height_1 : forall l x r, avl l -> avl r -> + -(3) <= height l - height r <= 3 -> + 0 <= height (bal l x r) - max (height l) (height r) <= 1. +Proof. + bal_tac; inv avl; avl_nns; simpl in *; omega_max. +Qed. + +Lemma bal_height_2 : + forall l x r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> + height (bal l x r) == max (height l) (height r) +1. +Proof. + bal_tac; inv avl; simpl in *; omega_max. +Qed. + +Lemma bal_in : forall l x r y, avl l -> avl r -> + (In y (bal l x r) <-> X.eq y x \/ In y l \/ In y r). +Proof. + bal_tac; + solve [repeat rewrite create_in; intuition_in + |inv avl; avl_nns; simpl in *; false_omega]. +Qed. + +Ltac omega_bal := match goal with + | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?r ] => + generalize (bal_height_1 l x r H H') (bal_height_2 l x r H H'); + omega_max + end. + +(** * Insertion *) + +Fixpoint add (x:elt)(s:t) { struct s } : t := match s with + | Leaf => Node Leaf x Leaf 1 + | Node l y r h => + match X.compare x y with + | LT _ => bal (add x l) y r + | EQ _ => Node l y r h + | GT _ => bal l y (add x r) + end + end. + +Lemma add_avl_1 : forall s x, avl s -> + avl (add x s) /\ 0 <= height (add x s) - height s <= 1. +Proof. + intros s x; functional induction add x s; intros; inv avl; simpl in *. + intuition; try constructor; simpl; auto; try omega_max. + (* LT *) + destruct H; auto. + split. + apply bal_avl; auto; omega_max. + omega_bal. + (* EQ *) + intuition; omega_max. + (* GT *) + destruct H; auto. + split. + apply bal_avl; auto; omega_max. + omega_bal. +Qed. + +Lemma add_avl : forall s x, avl s -> avl (add x s). +Proof. + intros; generalize (add_avl_1 s x H); intuition. +Qed. +Hint Resolve add_avl. + +Lemma add_in : forall s x y, avl s -> + (In y (add x s) <-> X.eq y x \/ In y s). +Proof. + intros s x; functional induction add x s; auto; intros. + intuition_in. + (* LT *) + inv avl. + rewrite bal_in; auto. + rewrite (H y0 H1); intuition_in. + (* EQ *) + inv avl. + intuition. + eapply In_1; eauto. + (* GT *) + inv avl. + rewrite bal_in; auto. + rewrite (H y0 H2); intuition_in. +Qed. + +Lemma add_bst : forall s x, bst s -> avl s -> bst (add x s). +Proof. + intros s x; functional induction add x s; auto; intros. + inv bst; inv avl; apply bal_bst; auto. + (* lt_tree -> lt_tree (add ...) *) + red; red in H4. + intros. + rewrite (add_in l x y0 H0) in H1. + intuition. + eauto. + inv bst; inv avl; apply bal_bst; auto. + (* gt_tree -> gt_tree (add ...) *) + red; red in H4. + intros. + rewrite (add_in r x y0 H6) in H1. + intuition. + apply MX.lt_eq with x; auto. +Qed. + +(** * Join + + Same as [bal] but does not assume anything regarding heights + of [l] and [r]. +*) + +Fixpoint join (l:t) : elt -> t -> t := + match l with + | Leaf => add + | Node ll lx lr lh => fun x => + fix join_aux (r:t) : t := match r with + | Leaf => add x l + | Node rl rx rr rh => + if gt_le_dec lh (rh+2) then bal ll lx (join lr x r) + else if gt_le_dec rh (lh+2) then bal (join_aux rl) rx rr + else create l x r + end + end. + +Ltac join_tac := + intro l; induction l as [| ll _ lx lr Hlr lh]; + [ | intros x r; induction r as [| rl Hrl rx rr _ rh]; unfold join; + [ | destruct (gt_le_dec lh (rh+2)); + [ match goal with |- context b [ bal ?a ?b ?c] => + replace (bal a b c) + with (bal ll lx (join lr x (Node rl rx rr rh))); [ | auto] + end + | destruct (gt_le_dec rh (lh+2)); + [ match goal with |- context b [ bal ?a ?b ?c] => + replace (bal a b c) + with (bal (join (Node ll lx lr lh) x rl) rx rr); [ | auto] + end + | ] ] ] ]; intros. + +Lemma join_avl_1 : forall l x r, avl l -> avl r -> avl (join l x r) /\ + 0<= height (join l x r) - max (height l) (height r) <= 1. +Proof. + (* intros l x r; functional induction join l x r. AUTRE PROBLEME! *) + join_tac. + + split; simpl; auto. + destruct (add_avl_1 r x H0). + avl_nns; omega_max. + split; auto. + set (l:=Node ll lx lr lh) in *. + destruct (add_avl_1 l x H). + simpl (height Leaf). + avl_nns; omega_max. + + inversion_clear H. + assert (height (Node rl rx rr rh) = rh); auto. + set (r := Node rl rx rr rh) in *; clearbody r. + destruct (Hlr x r H2 H0); clear Hrl Hlr. + set (j := join lr x r) in *; clearbody j. + simpl. + assert (-(3) <= height ll - height j <= 3) by omega_max. + split. + apply bal_avl; auto. + omega_bal. + + inversion_clear H0. + assert (height (Node ll lx lr lh) = lh); auto. + set (l := Node ll lx lr lh) in *; clearbody l. + destruct (Hrl H H1); clear Hrl Hlr. + set (j := join l x rl) in *; clearbody j. + simpl. + assert (-(3) <= height j - height rr <= 3) by omega_max. + split. + apply bal_avl; auto. + omega_bal. + + clear Hrl Hlr. + assert (height (Node ll lx lr lh) = lh); auto. + assert (height (Node rl rx rr rh) = rh); auto. + set (l := Node ll lx lr lh) in *; clearbody l. + set (r := Node rl rx rr rh) in *; clearbody r. + assert (-(2) <= height l - height r <= 2) by omega_max. + split. + apply create_avl; auto. + rewrite create_height; auto; omega_max. +Qed. + +Lemma join_avl : forall l x r, avl l -> avl r -> avl (join l x r). +Proof. + intros; generalize (join_avl_1 l x r H H0); intuition. +Qed. +Hint Resolve join_avl. + +Lemma join_in : forall l x r y, avl l -> avl r -> + (In y (join l x r) <-> X.eq y x \/ In y l \/ In y r). +Proof. + join_tac. + simpl. + rewrite add_in; intuition_in. + + rewrite add_in; intuition_in. + + inv avl. + rewrite bal_in; auto. + rewrite Hlr; clear Hlr Hrl; intuition_in. + + inv avl. + rewrite bal_in; auto. + rewrite Hrl; clear Hlr Hrl; intuition_in. + + apply create_in. +Qed. + +Lemma join_bst : forall l x r, bst l -> avl l -> bst r -> avl r -> + lt_tree x l -> gt_tree x r -> bst (join l x r). +Proof. + join_tac. + apply add_bst; auto. + apply add_bst; auto. + + inv bst; safe_inv avl. + apply bal_bst; auto. + clear Hrl Hlr H13 H14 H16 H17 z; intro; intros. + set (r:=Node rl rx rr rh) in *; clearbody r. + rewrite (join_in lr x r y) in H13; auto. + intuition. + apply MX.lt_eq with x; eauto. + eauto. + + inv bst; safe_inv avl. + apply bal_bst; auto. + clear Hrl Hlr H13 H14 H16 H17 z; intro; intros. + set (l:=Node ll lx lr lh) in *; clearbody l. + rewrite (join_in l x rl y) in H13; auto. + intuition. + apply MX.eq_lt with x; eauto. + eauto. + + apply create_bst; auto. +Qed. + +(** * Extraction of minimum element + + morally, [remove_min] is to be applied to a non-empty tree + [t = Node l x r h]. Since we can't deal here with [assert false] + for [t=Leaf], we pre-unpack [t] (and forget about [h]). +*) + +Fixpoint remove_min (l:t)(x:elt)(r:t) { struct l } : t*elt := + match l with + | Leaf => (r,x) + | Node ll lx lr lh => let (l',m) := remove_min ll lx lr in (bal l' x r, m) + end. + +Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) -> + avl (fst (remove_min l x r)) /\ + 0 <= height (Node l x r h) - height (fst (remove_min l x r)) <= 1. +Proof. + intros l x r; functional induction remove_min l x r; simpl in *; intros. + inv avl; simpl in *; split; auto. + avl_nns; omega_max. + (* l = Node *) + inversion_clear H0. + destruct (H lh); auto. + split; simpl in *. + apply bal_avl; auto; omega_max. + omega_bal. +Qed. + +Lemma remove_min_avl : forall l x r h, avl (Node l x r h) -> + avl (fst (remove_min l x r)). +Proof. + intros; generalize (remove_min_avl_1 l x r h H); intuition. +Qed. + +Lemma remove_min_in : forall l x r h y, avl (Node l x r h) -> + (In y (Node l x r h) <-> + X.eq y (snd (remove_min l x r)) \/ In y (fst (remove_min l x r))). +Proof. + intros l x r; functional induction remove_min l x r; simpl in *; intros. + intuition_in. + (* l = Node *) + inversion_clear H0. + generalize (remove_min_avl ll lx lr lh H1). + rewrite H_eq_0; simpl; intros. + rewrite bal_in; auto. + generalize (H lh y H1). + intuition. + inversion_clear H8; intuition. +Qed. + +Lemma remove_min_bst : forall l x r h, + bst (Node l x r h) -> avl (Node l x r h) -> bst (fst (remove_min l x r)). +Proof. + intros l x r; functional induction remove_min l x r; simpl in *; intros. + inv bst; auto. + inversion_clear H0; inversion_clear H1. + apply bal_bst; auto. + firstorder. + intro; intros. + generalize (remove_min_in ll lx lr lh y H0). + rewrite H_eq_0; simpl. + destruct 1. + apply H4; intuition. +Qed. + +Lemma remove_min_gt_tree : forall l x r h, + bst (Node l x r h) -> avl (Node l x r h) -> + gt_tree (snd (remove_min l x r)) (fst (remove_min l x r)). +Proof. + intros l x r; functional induction remove_min l x r; simpl in *; intros. + inv bst; auto. + inversion_clear H0; inversion_clear H1. + intro; intro. + generalize (H lh H2 H0); clear H8 H7 H. + generalize (remove_min_avl ll lx lr lh H0). + generalize (remove_min_in ll lx lr lh m H0). + rewrite H_eq_0; simpl; intros. + rewrite (bal_in l' x r y H7 H6) in H1. + destruct H. + firstorder. + apply MX.lt_eq with x; auto. + apply X.lt_trans with x; auto. +Qed. + +(** * Merging two trees + + [merge t1 t2] builds the union of [t1] and [t2] assuming all elements + of [t1] to be smaller than all elements of [t2], and + [|height t1 - height t2| <= 2]. +*) + +Definition merge s1 s2 := match s1,s2 with + | Leaf, _ => s2 + | _, Leaf => s1 + | _, Node l2 x2 r2 h2 => + let (s2',m) := remove_min l2 x2 r2 in bal s1 m s2' +end. + +Lemma merge_avl_1 : forall s1 s2, avl s1 -> avl s2 -> + -(2) <= height s1 - height s2 <= 2 -> + avl (merge s1 s2) /\ + 0<= height (merge s1 s2) - max (height s1) (height s2) <=1. +Proof. + intros s1 s2; functional induction merge s1 s2; simpl in *; intros. + split; auto; avl_nns; omega_max. + split; auto; avl_nns; simpl in *; omega_max. + generalize (remove_min_avl_1 l2 x2 r2 h2 H0). + rewrite H_eq_1; simpl; destruct 1. + split. + apply bal_avl; auto. + simpl; omega_max. + omega_bal. +Qed. + +Lemma merge_avl : forall s1 s2, avl s1 -> avl s2 -> + -(2) <= height s1 - height s2 <= 2 -> avl (merge s1 s2). +Proof. + intros; generalize (merge_avl_1 s1 s2 H H0 H1); intuition. +Qed. + +Lemma merge_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (In y (merge s1 s2) <-> In y s1 \/ In y s2). +Proof. + intros s1 s2; functional induction merge s1 s2; simpl in *; intros. + intuition_in. + intuition_in. + replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite H_eq_1; auto]. + rewrite bal_in; auto. + generalize (remove_min_avl l2 x2 r2 h2); rewrite H_eq_1; simpl; auto. + generalize (remove_min_in l2 x2 r2 h2 y); rewrite H_eq_1; simpl; intro. + rewrite H3; intuition. +Qed. + +Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> + bst (merge s1 s2). +Proof. + intros s1 s2; functional induction merge s1 s2; simpl in *; intros; auto. + apply bal_bst; auto. + generalize (remove_min_bst l2 x2 r2 h2); rewrite H_eq_1; simpl in *; auto. + intro; intro. + apply H3; auto. + generalize (remove_min_in l2 x2 r2 h2 m); rewrite H_eq_1; simpl; intuition. + generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite H_eq_1; simpl; auto. +Qed. + +(** * Deletion *) + +Fixpoint remove (x:elt)(s:tree) { struct s } : t := match s with + | Leaf => Leaf + | Node l y r h => + match X.compare x y with + | LT _ => bal (remove x l) y r + | EQ _ => merge l r + | GT _ => bal l y (remove x r) + end + end. + +Lemma remove_avl_1 : forall s x, avl s -> + avl (remove x s) /\ 0 <= height s - height (remove x s) <= 1. +Proof. + intros s x; functional induction remove x s; simpl; intros. + intuition; omega_max. + (* LT *) + inv avl. + destruct (H H1). + split. + apply bal_avl; auto. + omega_max. + omega_bal. + (* EQ *) + inv avl. + generalize (merge_avl_1 l r H0 H1 H2). + intuition omega_max. + (* GT *) + inv avl. + destruct (H H2). + split. + apply bal_avl; auto. + omega_max. + omega_bal. +Qed. + +Lemma remove_avl : forall s x, avl s -> avl (remove x s). +Proof. + intros; generalize (remove_avl_1 s x H); intuition. +Qed. +Hint Resolve remove_avl. + +Lemma remove_in : forall s x y, bst s -> avl s -> + (In y (remove x s) <-> ~ X.eq y x /\ In y s). +Proof. + intros s x; functional induction remove x s; simpl; intros. + intuition_in. + (* LT *) + inv avl; inv bst; clear H_eq_0. + rewrite bal_in; auto. + generalize (H y0 H1); intuition; [ order | order | intuition_in ]. + (* EQ *) + inv avl; inv bst; clear H_eq_0. + rewrite merge_in; intuition; [ order | order | intuition_in ]. + elim H9; eauto. + (* GT *) + inv avl; inv bst; clear H_eq_0. + rewrite bal_in; auto. + generalize (H y0 H6); intuition; [ order | order | intuition_in ]. +Qed. + +Lemma remove_bst : forall s x, bst s -> avl s -> bst (remove x s). +Proof. + intros s x; functional induction remove x s; simpl; intros. + auto. + (* LT *) + inv avl; inv bst. + apply bal_bst; auto. + intro; intro. + rewrite (remove_in l x y0) in H0; auto. + destruct H0; eauto. + (* EQ *) + inv avl; inv bst. + apply merge_bst; eauto. + (* GT *) + inv avl; inv bst. + apply bal_bst; auto. + intro; intro. + rewrite (remove_in r x y0) in H0; auto. + destruct H0; eauto. +Qed. + + (** * Minimum element *) + +Fixpoint min_elt (s:t) : option elt := match s with + | Leaf => None + | Node Leaf y _ _ => Some y + | Node l _ _ _ => min_elt l +end. + +Lemma min_elt_1 : forall s x, min_elt s = Some x -> In x s. +Proof. + intro s; functional induction min_elt s; simpl. + inversion 1. + inversion 1; auto. + intros. + destruct t0; auto. +Qed. + +Lemma min_elt_2 : forall s x y, bst s -> + min_elt s = Some x -> In y s -> ~ X.lt y x. +Proof. + intro s; functional induction min_elt s; simpl. + inversion_clear 2. + inversion_clear 1. + inversion 1; subst. + inversion_clear 1; auto. + inversion_clear H5. + inversion_clear 1. + destruct t0. + inversion 1; subst. + assert (X.lt x y) by apply H3; auto. + inversion_clear 1; auto; order. + assert (X.lt t1 y) by auto. + inversion_clear 2; auto; + (assert (~ X.lt t1 x) by auto); order. +Qed. + +Lemma min_elt_3 : forall s, min_elt s = None -> Empty s. +Proof. + intro s; functional induction min_elt s; simpl. + red; auto. + inversion 1. + destruct t0. + inversion 1. + intros H0; destruct (H H0 t1); auto. +Qed. + + +(** * Maximum element *) + +Fixpoint max_elt (s:t) : option elt := match s with + | Leaf => None + | Node _ y Leaf _ => Some y + | Node _ _ r _ => max_elt r +end. + +Lemma max_elt_1 : forall s x, max_elt s = Some x -> In x s. +Proof. + intro s; functional induction max_elt s; simpl. + inversion 1. + inversion 1; auto. + intros. + destruct t2; auto. +Qed. + +Lemma max_elt_2 : forall s x y, bst s -> + max_elt s = Some x -> In y s -> ~ X.lt x y. +Proof. + intro s; functional induction max_elt s; simpl. + inversion_clear 2. + inversion_clear 1. + inversion 1; subst. + inversion_clear 1; auto. + inversion_clear H5. + inversion_clear 1. + destruct t2. + inversion 1; subst. + assert (X.lt y x) by apply H4; auto. + inversion_clear 1; auto; order. + assert (X.lt y t1) by auto. + inversion_clear 2; auto; + (assert (~ X.lt x t1) by auto); order. +Qed. + +Lemma max_elt_3 : forall s, max_elt s = None -> Empty s. +Proof. + intro s; functional induction max_elt s; simpl. + red; auto. + inversion 1. + destruct t2. + inversion 1. + intros H0; destruct (H H0 t1); auto. +Qed. + +(** * Any element *) + +Definition choose := min_elt. + +Lemma choose_1 : forall s x, choose s = Some x -> In x s. +Proof. + exact min_elt_1. +Qed. + +Lemma choose_2 : forall s, choose s = None -> Empty s. +Proof. + exact min_elt_3. +Qed. + +(** * Concatenation + + Same as [merge] but does not assume anything about heights. +*) + +Definition concat s1 s2 := + match s1, s2 with + | Leaf, _ => s2 + | _, Leaf => s1 + | _, Node l2 x2 r2 h2 => + let (s2',m) := remove_min l2 x2 r2 in + join s1 m s2' + end. + +Lemma concat_avl : forall s1 s2, avl s1 -> avl s2 -> avl (concat s1 s2). +Proof. + intros s1 s2; functional induction concat s1 s2; auto. + intros; change (avl (join (Node t t0 t1 i) m s2')). + rewrite <- H_eq_ in H; rewrite <- H_eq_. + apply join_avl; auto. + generalize (remove_min_avl l2 x2 r2 h2 H0); rewrite H_eq_1; simpl; auto. +Qed. + +Lemma concat_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> + bst (concat s1 s2). +Proof. + intros s1 s2; functional induction concat s1 s2; auto. + intros; change (bst (join (Node t t0 t1 i) m s2')). + rewrite <- H_eq_ in H; rewrite <- H_eq_ in H0; + rewrite <- H_eq_ in H3; rewrite <- H_eq_. + apply join_bst; auto. + generalize (remove_min_bst l2 x2 r2 h2 H1 H2); rewrite H_eq_1; simpl; auto. + generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite H_eq_1; simpl; auto. + generalize (remove_min_in l2 x2 r2 h2 m H2); rewrite H_eq_1; simpl; auto. + destruct 1; intuition. + generalize (remove_min_gt_tree l2 x2 r2 h2 H1 H2); rewrite H_eq_1; simpl; auto. +Qed. + +Lemma concat_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (forall y1 y2 : elt, In y1 s1 -> In y2 s2 -> X.lt y1 y2) -> + (In y (concat s1 s2) <-> In y s1 \/ In y s2). +Proof. + intros s1 s2; functional induction concat s1 s2. + intuition. + inversion_clear H5. + intuition. + inversion_clear H5. + intros. + change (In y (join (Node t t0 t1 i) m s2') <-> + In y (Node t t0 t1 i) \/ In y (Node l2 x2 r2 h2)). + rewrite <- H_eq_ in H; rewrite <- H_eq_ in H0; + rewrite <- H_eq_ in H3; rewrite <- H_eq_. + rewrite (join_in s1 m s2' y H0). + generalize (remove_min_avl l2 x2 r2 h2 H2); rewrite H_eq_1; simpl; auto. + generalize (remove_min_in l2 x2 r2 h2 y H2); rewrite H_eq_1; simpl. + intro EQ; rewrite EQ; intuition. +Qed. + +(** * Splitting + + [split x s] returns a triple [(l, present, r)] where + - [l] is the set of elements of [s] that are [< x] + - [r] is the set of elements of [s] that are [> x] + - [present] is [true] if and only if [s] contains [x]. +*) + +Fixpoint split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with + | Leaf => (Leaf, (false, Leaf)) + | Node l y r h => + match X.compare x y with + | LT _ => match split x l with + | (ll,(pres,rl)) => (ll, (pres, join rl y r)) + end + | EQ _ => (l, (true, r)) + | GT _ => match split x r with + | (rl,(pres,rr)) => (join l y rl, (pres, rr)) + end + end + end. + +Lemma split_avl : forall s x, avl s -> + avl (fst (split x s)) /\ avl (snd (snd (split x s))). +Proof. + intros s x; functional induction split x s. + auto. + destruct p; simpl in *. + inversion_clear 1; intuition. + simpl; inversion_clear 1; auto. + destruct p; simpl in *. + inversion_clear 1; intuition. +Qed. + +Lemma split_in_1 : forall s x y, bst s -> avl s -> + (In y (fst (split x s)) <-> In y s /\ X.lt y x). +Proof. + intros s x; functional induction split x s. + intuition; try inversion_clear H1. + (* LT *) + destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. + rewrite (H y0 H1 H5); clear H H_eq_0. + intuition. + inversion_clear H0; auto; order. + (* EQ *) + simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H7 H_eq_0. + intuition. + order. + intuition_in; order. + (* GT *) + destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. + rewrite join_in; auto. + generalize (split_avl r x H6); rewrite H_eq_1; simpl; intuition. + rewrite (H y0 H2 H6); clear H. + intuition; [ eauto | eauto | intuition_in ]. +Qed. + +Lemma split_in_2 : forall s x y, bst s -> avl s -> + (In y (snd (snd (split x s))) <-> In y s /\ X.lt x y). +Proof. + intros s x; functional induction split x s. + intuition; try inversion_clear H1. + (* LT *) + destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. + rewrite join_in; auto. + generalize (split_avl l x H5); rewrite H_eq_1; simpl; intuition. + rewrite (H y0 H1 H5); clear H H_eq_0. + intuition; [ order | order | intuition_in ]. + (* EQ *) + simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H7 H_eq_0. + intuition; [ order | intuition_in; order ]. + (* GT *) + destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. + rewrite (H y0 H2 H6); clear H H_eq_0. + intuition; intuition_in; order. +Qed. + +Lemma split_in_3 : forall s x, bst s -> avl s -> + (fst (snd (split x s)) = true <-> In x s). +Proof. + intros s x; functional induction split x s. + intuition; try inversion_clear H1. + (* LT *) + destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. + rewrite H; auto. + intuition_in; absurd (X.lt x y); eauto. + (* EQ *) + simpl in *; inversion_clear 1; inversion_clear 1; intuition. + (* GT *) + destruct p; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H8. + rewrite H; auto. + intuition_in; absurd (X.lt y x); eauto. +Qed. + +Lemma split_bst : forall s x, bst s -> avl s -> + bst (fst (split x s)) /\ bst (snd (snd (split x s))). +Proof. + intros s x; functional induction split x s. + intuition. + (* LT *) + destruct p; simpl in *; inversion_clear 1; inversion_clear 1. + intuition. + apply join_bst; auto. + generalize (split_avl l x H5); rewrite H_eq_1; simpl; intuition. + intro; intro. + generalize (split_in_2 l x y0 H1 H5); rewrite H_eq_1; simpl; intuition. + (* EQ *) + simpl in *; inversion_clear 1; inversion_clear 1; intuition. + (* GT *) + destruct p; simpl in *; inversion_clear 1; inversion_clear 1. + intuition. + apply join_bst; auto. + generalize (split_avl r x H6); rewrite H_eq_1; simpl; intuition. + intro; intro. + generalize (split_in_1 r x y0 H2 H6); rewrite H_eq_1; simpl; intuition. +Qed. + +(** * Intersection *) + + Fixpoint inter (s1 s2 : t) {struct s1} : t := match s1, s2 with + | Leaf,_ => Leaf + | _,Leaf => Leaf + | Node l1 x1 r1 h1, _ => + match split x1 s2 with + | (l2',(true,r2')) => join (inter l1 l2') x1 (inter r1 r2') + | (l2',(false,r2')) => concat (inter l1 l2') (inter r1 r2') + end + end. + +Lemma inter_avl : forall s1 s2, avl s1 -> avl s2 -> avl (inter s1 s2). +Proof. + (* intros s1 s2; functional induction inter s1 s2; auto. BOF BOF *) + induction s1 as [ | l1 Hl1 x1 r1 Hr1 h1]; simpl; auto. + destruct s2 as [ | l2 x2 r2 h2]; intros; auto. + generalize H0; inv avl. + set (r:=Node l2 x2 r2 h2) in *; clearbody r; intros. + destruct (split_avl r x1 H8). + destruct (split x1 r) as [l2' (b,r2')]; simpl in *. + destruct b; [ apply join_avl | apply concat_avl ]; auto. +Qed. + +Lemma inter_bst_in : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + bst (inter s1 s2) /\ (forall y, In y (inter s1 s2) <-> In y s1 /\ In y s2). +Proof. + induction s1 as [ | l1 Hl1 x1 r1 Hr1 h1]; simpl; auto. + intuition; inversion_clear H3. + destruct s2 as [ | l2 x2 r2 h2]; intros. + simpl; intuition; inversion_clear H3. + generalize H1 H2; inv avl; inv bst. + set (r:=Node l2 x2 r2 h2) in *; clearbody r; intros. + destruct (split_avl r x1 H17). + destruct (split_bst r x1 H16 H17). + split. + (* bst *) + destruct (split x1 r) as [l2' (b,r2')]; simpl in *. + destruct (Hl1 l2'); auto. + destruct (Hr1 r2'); auto. + destruct b. + (* bst join *) + apply join_bst; try apply inter_avl; firstorder. + (* bst concat *) + apply concat_bst; try apply inter_avl; auto. + intros; generalize (H22 y1) (H24 y2); intuition eauto. + (* in *) + intros. + destruct (split_in_1 r x1 y H16 H17). + destruct (split_in_2 r x1 y H16 H17). + destruct (split_in_3 r x1 H16 H17). + destruct (split x1 r) as [l2' (b,r2')]; simpl in *. + destruct (Hl1 l2'); auto. + destruct (Hr1 r2'); auto. + destruct b. + (* in join *) + rewrite join_in; try apply inter_avl; auto. + rewrite H30. + rewrite H28. + intuition_in. + apply In_1 with x1; auto. + (* in concat *) + rewrite concat_in; try apply inter_avl; auto. + intros. + intros; generalize (H28 y1) (H30 y2); intuition eauto. + rewrite H30. + rewrite H28. + intuition_in. + generalize (H26 (In_1 _ _ _ H22 H35)); intro; discriminate. +Qed. + +Lemma inter_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + bst (inter s1 s2). +Proof. + intros; generalize (inter_bst_in s1 s2); intuition. +Qed. + +Lemma inter_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (In y (inter s1 s2) <-> In y s1 /\ In y s2). +Proof. + intros; generalize (inter_bst_in s1 s2); firstorder. +Qed. + +(** * Difference *) + +Fixpoint diff (s1 s2 : t) { struct s1 } : t := match s1, s2 with + | Leaf, _ => Leaf + | _, Leaf => s1 + | Node l1 x1 r1 h1, _ => + match split x1 s2 with + | (l2',(true,r2')) => concat (diff l1 l2') (diff r1 r2') + | (l2',(false,r2')) => join (diff l1 l2') x1 (diff r1 r2') + end +end. + +Lemma diff_avl : forall s1 s2, avl s1 -> avl s2 -> avl (diff s1 s2). +Proof. + (* intros s1 s2; functional induction diff s1 s2; auto. BOF BOF *) + induction s1 as [ | l1 Hl1 x1 r1 Hr1 h1]; simpl; auto. + destruct s2 as [ | l2 x2 r2 h2]; intros; auto. + generalize H0; inv avl. + set (r:=Node l2 x2 r2 h2) in *; clearbody r; intros. + destruct (split_avl r x1 H8). + destruct (split x1 r) as [l2' (b,r2')]; simpl in *. + destruct b; [ apply concat_avl | apply join_avl ]; auto. +Qed. + +Lemma diff_bst_in : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + bst (diff s1 s2) /\ (forall y, In y (diff s1 s2) <-> In y s1 /\ ~In y s2). +Proof. + induction s1 as [ | l1 Hl1 x1 r1 Hr1 h1]; simpl; auto. + intuition; inversion_clear H3. + destruct s2 as [ | l2 x2 r2 h2]; intros; auto. + intuition; inversion_clear H4. + generalize H1 H2; inv avl; inv bst. + set (r:=Node l2 x2 r2 h2) in *; clearbody r; intros. + destruct (split_avl r x1 H17). + destruct (split_bst r x1 H16 H17). + split. + (* bst *) + destruct (split x1 r) as [l2' (b,r2')]; simpl in *. + destruct (Hl1 l2'); auto. + destruct (Hr1 r2'); auto. + destruct b. + (* bst concat *) + apply concat_bst; try apply diff_avl; auto. + intros; generalize (H22 y1) (H24 y2); intuition eauto. + (* bst join *) + apply join_bst; try apply diff_avl; firstorder. + (* in *) + intros. + destruct (split_in_1 r x1 y H16 H17). + destruct (split_in_2 r x1 y H16 H17). + destruct (split_in_3 r x1 H16 H17). + destruct (split x1 r) as [l2' (b,r2')]; simpl in *. + destruct (Hl1 l2'); auto. + destruct (Hr1 r2'); auto. + destruct b. + (* in concat *) + rewrite concat_in; try apply diff_avl; auto. + intros. + intros; generalize (H28 y1) (H30 y2); intuition eauto. + rewrite H30. + rewrite H28. + intuition_in. + elim H35; apply In_1 with x1; auto. + (* in join *) + rewrite join_in; try apply diff_avl; auto. + rewrite H30. + rewrite H28. + intuition_in. + generalize (H26 (In_1 _ _ _ H34 H24)); intro; discriminate. +Qed. + +Lemma diff_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + bst (diff s1 s2). +Proof. + intros; generalize (diff_bst_in s1 s2); intuition. +Qed. + +Lemma diff_in : forall s1 s2 y, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + (In y (diff s1 s2) <-> In y s1 /\ ~In y s2). +Proof. + intros; generalize (diff_bst_in s1 s2); firstorder. +Qed. + +(** * Elements *) + +(** [elements_tree_aux acc t] catenates the elements of [t] in infix + order to the list [acc] *) + +Fixpoint elements_aux (acc : list X.t) (t : tree) {struct t} : list X.t := + match t with + | Leaf => acc + | Node l x r _ => elements_aux (x :: elements_aux acc r) l + end. + +(** then [elements] is an instanciation with an empty [acc] *) + +Definition elements := elements_aux nil. + +Lemma elements_aux_in : forall s acc x, + InA X.eq x (elements_aux acc s) <-> In x s \/ InA X.eq x acc. +Proof. + induction s as [ | l Hl x r Hr h ]; simpl; auto. + intuition. + inversion H0. + intros. + rewrite Hl. + destruct (Hr acc x0); clear Hl Hr. + intuition; inversion_clear H3; intuition. +Qed. + +Lemma elements_in : forall s x, InA X.eq x (elements s) <-> In x s. +Proof. + intros; generalize (elements_aux_in s nil x); intuition. + inversion_clear H0. +Qed. + +Lemma elements_aux_sort : forall s acc, bst s -> sort X.lt acc -> + (forall x y : elt, InA X.eq x acc -> In y s -> X.lt y x) -> + sort X.lt (elements_aux acc s). +Proof. + induction s as [ | l Hl y r Hr h]; simpl; intuition. + inv bst. + apply Hl; auto. + constructor. + apply Hr; auto. + apply MX.In_Inf; intros. + destruct (elements_aux_in r acc y0); intuition. + intros. + inversion_clear H. + order. + destruct (elements_aux_in r acc x); intuition eauto. +Qed. + +Lemma elements_sort : forall s : tree, bst s -> sort X.lt (elements s). +Proof. + intros; unfold elements; apply elements_aux_sort; auto. + intros; inversion H0. +Qed. +Hint Resolve elements_sort. + +(** * Filter *) + +Section F. +Variable f : elt -> bool. + +Fixpoint filter_acc (acc:t)(s:t) { struct s } : t := match s with + | Leaf => acc + | Node l x r h => + filter_acc (filter_acc (if f x then add x acc else acc) l) r + end. + +Definition filter := filter_acc Leaf. + +Lemma filter_acc_avl : forall s acc, avl s -> avl acc -> + avl (filter_acc acc s). +Proof. + induction s; simpl; auto. + intros. + inv avl. + apply IHs2; auto. + apply IHs1; auto. + destruct (f t); auto. +Qed. +Hint Resolve filter_acc_avl. + +Lemma filter_acc_bst : forall s acc, bst s -> avl s -> bst acc -> avl acc -> + bst (filter_acc acc s). +Proof. + induction s; simpl; auto. + intros. + inv avl; inv bst. + destruct (f t); auto. + apply IHs2; auto. + apply IHs1; auto. + apply add_bst; auto. +Qed. + +Lemma filter_acc_in : forall s acc, avl s -> avl acc -> + compat_bool X.eq f -> forall x : elt, + In x (filter_acc acc s) <-> In x acc \/ In x s /\ f x = true. +Proof. + induction s; simpl; intros. + intuition_in. + inv bst; inv avl. + rewrite IHs2; auto. + destruct (f t); auto. + rewrite IHs1; auto. + destruct (f t); auto. + case_eq (f t); intros. + rewrite (add_in); auto. + intuition_in. + rewrite (H1 _ _ H8). + intuition. + intuition_in. + rewrite (H1 _ _ H8) in H9. + rewrite H in H9; discriminate. +Qed. + +Lemma filter_avl : forall s, avl s -> avl (filter s). +Proof. + unfold filter; intros; apply filter_acc_avl; auto. +Qed. + +Lemma filter_bst : forall s, bst s -> avl s -> bst (filter s). +Proof. + unfold filter; intros; apply filter_acc_bst; auto. +Qed. + +Lemma filter_in : forall s, avl s -> + compat_bool X.eq f -> forall x : elt, + In x (filter s) <-> In x s /\ f x = true. +Proof. + unfold filter; intros; rewrite filter_acc_in; intuition_in. +Qed. + +(** * Partition *) + +Fixpoint partition_acc (acc : t*t)(s : t) { struct s } : t*t := + match s with + | Leaf => acc + | Node l x r _ => + let (acct,accf) := acc in + partition_acc + (partition_acc + (if f x then (add x acct, accf) else (acct, add x accf)) l) r + end. + +Definition partition := partition_acc (Leaf,Leaf). + +Lemma partition_acc_avl_1 : forall s acc, avl s -> + avl (fst acc) -> avl (fst (partition_acc acc s)). +Proof. + induction s; simpl; auto. + destruct acc as [acct accf]; simpl in *. + intros. + inv avl. + apply IHs2; auto. + apply IHs1; auto. + destruct (f t); simpl; auto. +Qed. + +Lemma partition_acc_avl_2 : forall s acc, avl s -> + avl (snd acc) -> avl (snd (partition_acc acc s)). +Proof. + induction s; simpl; auto. + destruct acc as [acct accf]; simpl in *. + intros. + inv avl. + apply IHs2; auto. + apply IHs1; auto. + destruct (f t); simpl; auto. +Qed. +Hint Resolve partition_acc_avl_1 partition_acc_avl_2. + +Lemma partition_acc_bst_1 : forall s acc, bst s -> avl s -> + bst (fst acc) -> avl (fst acc) -> + bst (fst (partition_acc acc s)). +Proof. + induction s; simpl; auto. + destruct acc as [acct accf]; simpl in *. + intros. + inv avl; inv bst. + destruct (f t); auto. + apply IHs2; simpl; auto. + apply IHs1; simpl; auto. + apply add_bst; auto. + apply partition_acc_avl_1; simpl; auto. +Qed. + +Lemma partition_acc_bst_2 : forall s acc, bst s -> avl s -> + bst (snd acc) -> avl (snd acc) -> + bst (snd (partition_acc acc s)). +Proof. + induction s; simpl; auto. + destruct acc as [acct accf]; simpl in *. + intros. + inv avl; inv bst. + destruct (f t); auto. + apply IHs2; simpl; auto. + apply IHs1; simpl; auto. + apply add_bst; auto. + apply partition_acc_avl_2; simpl; auto. +Qed. + +Lemma partition_acc_in_1 : forall s acc, avl s -> avl (fst acc) -> + compat_bool X.eq f -> forall x : elt, + In x (fst (partition_acc acc s)) <-> + In x (fst acc) \/ In x s /\ f x = true. +Proof. + induction s; simpl; intros. + intuition_in. + destruct acc as [acct accf]; simpl in *. + inv bst; inv avl. + rewrite IHs2; auto. + destruct (f t); auto. + apply partition_acc_avl_1; simpl; auto. + rewrite IHs1; auto. + destruct (f t); simpl; auto. + case_eq (f t); simpl; intros. + rewrite (add_in); auto. + intuition_in. + rewrite (H1 _ _ H8). + intuition. + intuition_in. + rewrite (H1 _ _ H8) in H9. + rewrite H in H9; discriminate. +Qed. + +Lemma partition_acc_in_2 : forall s acc, avl s -> avl (snd acc) -> + compat_bool X.eq f -> forall x : elt, + In x (snd (partition_acc acc s)) <-> + In x (snd acc) \/ In x s /\ f x = false. +Proof. + induction s; simpl; intros. + intuition_in. + destruct acc as [acct accf]; simpl in *. + inv bst; inv avl. + rewrite IHs2; auto. + destruct (f t); auto. + apply partition_acc_avl_2; simpl; auto. + rewrite IHs1; auto. + destruct (f t); simpl; auto. + case_eq (f t); simpl; intros. + intuition. + intuition_in. + rewrite (H1 _ _ H8) in H9. + rewrite H in H9; discriminate. + rewrite (add_in); auto. + intuition_in. + rewrite (H1 _ _ H8). + intuition. +Qed. + +Lemma partition_avl_1 : forall s, avl s -> avl (fst (partition s)). +Proof. + unfold partition; intros; apply partition_acc_avl_1; auto. +Qed. + +Lemma partition_avl_2 : forall s, avl s -> avl (snd (partition s)). +Proof. + unfold partition; intros; apply partition_acc_avl_2; auto. +Qed. + +Lemma partition_bst_1 : forall s, bst s -> avl s -> + bst (fst (partition s)). +Proof. + unfold partition; intros; apply partition_acc_bst_1; auto. +Qed. + +Lemma partition_bst_2 : forall s, bst s -> avl s -> + bst (snd (partition s)). +Proof. + unfold partition; intros; apply partition_acc_bst_2; auto. +Qed. + +Lemma partition_in_1 : forall s, avl s -> + compat_bool X.eq f -> forall x : elt, + In x (fst (partition s)) <-> In x s /\ f x = true. +Proof. + unfold partition; intros; rewrite partition_acc_in_1; + simpl in *; intuition_in. +Qed. + +Lemma partition_in_2 : forall s, avl s -> + compat_bool X.eq f -> forall x : elt, + In x (snd (partition s)) <-> In x s /\ f x = false. +Proof. + unfold partition; intros; rewrite partition_acc_in_2; + simpl in *; intuition_in. +Qed. + +(** [for_all] and [exists] *) + +Fixpoint for_all (s:t) : bool := match s with + | Leaf => true + | Node l x r _ => f x && for_all l && for_all r +end. + +Lemma for_all_1 : forall s, compat_bool E.eq f -> + For_all (fun x => f x = true) s -> for_all s = true. +Proof. + induction s; simpl; auto. + intros. + rewrite IHs1; try red; auto. + rewrite IHs2; try red; auto. + generalize (H0 t). + destruct (f t); simpl; auto. +Qed. + +Lemma for_all_2 : forall s, compat_bool E.eq f -> + for_all s = true -> For_all (fun x => f x = true) s. +Proof. + induction s; simpl; auto; intros; red; intros; inv In. + destruct (andb_prop _ _ H0); auto. + destruct (andb_prop _ _ H1); eauto. + apply IHs1; auto. + destruct (andb_prop _ _ H0); auto. + destruct (andb_prop _ _ H1); auto. + apply IHs2; auto. + destruct (andb_prop _ _ H0); auto. +Qed. + +Fixpoint exists_ (s:t) : bool := match s with + | Leaf => false + | Node l x r _ => f x || exists_ l || exists_ r +end. + +Lemma exists_1 : forall s, compat_bool E.eq f -> + Exists (fun x => f x = true) s -> exists_ s = true. +Proof. + induction s; simpl; destruct 2 as (x,(U,V)); inv In. + rewrite (H _ _ (X.eq_sym H0)); rewrite V; auto. + apply orb_true_intro; left. + apply orb_true_intro; right; apply IHs1; firstorder. + apply orb_true_intro; right; apply IHs2; firstorder. +Qed. + +Lemma exists_2 : forall s, compat_bool E.eq f -> + exists_ s = true -> Exists (fun x => f x = true) s. +Proof. + induction s; simpl; intros. + discriminate. + destruct (orb_true_elim _ _ H0) as [H1|H1]. + destruct (orb_true_elim _ _ H1) as [H2|H2]. + exists t; auto. + destruct (IHs1 H H2); firstorder. + destruct (IHs2 H H1); firstorder. +Qed. + +End F. + +(** * Fold *) + +Module L := FSetList.Raw X. + +Fixpoint fold (A : Set) (f : elt -> A -> A)(s : tree) {struct s} : A -> A := + fun a => match s with + | Leaf => a + | Node l x r _ => fold A f r (f x (fold A f l a)) + end. +Implicit Arguments fold [A]. + +Definition fold' (A : Set) (f : elt -> A -> A)(s : tree) := + L.fold f (elements s). +Implicit Arguments fold' [A]. + +Lemma fold_equiv_aux : + forall (A : Set) (s : tree) (f : elt -> A -> A) (a : A) (acc : list elt), + L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a). +Proof. + simple induction s. + simpl in |- *; intuition. + simpl in |- *; intros. + rewrite H. + simpl. + apply H0. +Qed. + +Lemma fold_equiv : + forall (A : Set) (s : tree) (f : elt -> A -> A) (a : A), + fold f s a = fold' f s a. +Proof. + unfold fold', elements in |- *. + simple induction s; simpl in |- *; auto; intros. + rewrite fold_equiv_aux. + rewrite H0. + simpl in |- *; auto. +Qed. + +Lemma fold_1 : + forall (s:t)(Hs:bst s)(A : Set)(f : elt -> A -> A)(i : A), + fold f s i = fold_left (fun a e => f e a) (elements s) i. +Proof. + intros. + rewrite fold_equiv. + unfold fold'. + rewrite L.fold_1. + unfold L.elements; auto. + apply elements_sort; auto. +Qed. + +(** * Cardinal *) + +Fixpoint cardinal (s : tree) : nat := + match s with + | Leaf => 0%nat + | Node l _ r _ => S (cardinal l + cardinal r) + end. + +Lemma cardinal_elements_aux_1 : + forall s acc, (length acc + cardinal s)%nat = length (elements_aux acc s). +Proof. + simple induction s; simpl in |- *; intuition. + rewrite <- H. + simpl in |- *. + rewrite <- H0; omega. +Qed. + +Lemma cardinal_elements_1 : forall s : tree, cardinal s = length (elements s). +Proof. + exact (fun s => cardinal_elements_aux_1 s nil). +Qed. + +(** NB: the remaining functions (union, subset, compare) are still defined + in a dependent style, due to the use of well-founded induction. *) + +(** Induction over cardinals *) + +Lemma sorted_subset_cardinal : forall l' l : list X.t, + MX.Sort l -> MX.Sort l' -> + (forall x : elt, MX.In x l -> MX.In x l') -> (length l <= length l')%nat. +Proof. + simple induction l'; simpl in |- *; intuition. + destruct l; trivial; intros. + absurd (MX.In t nil); intuition. + inversion_clear H2. + inversion_clear H1. + destruct l0; simpl in |- *; intuition. + inversion_clear H0. + apply le_n_S. + case (X.compare t a); intro. + absurd (MX.In t (a :: l)). + intro. + inversion_clear H0. + order. + assert (X.lt a t). + apply MX.Sort_Inf_In with l; auto. + order. + firstorder. + apply H; auto. + intros. + assert (MX.In x (a :: l)). + apply H2; auto. + inversion_clear H6; auto. + assert (X.lt t x). + apply MX.Sort_Inf_In with l0; auto. + order. + apply le_trans with (length (t :: l0)). + simpl in |- *; omega. + apply (H (t :: l0)); auto. + intros. + assert (MX.In x (a :: l)); firstorder. + inversion_clear H6; auto. + assert (X.lt a x). + apply MX.Sort_Inf_In with (t :: l0); auto. + elim (X.lt_not_eq (x:=a) (y:=x)); auto. +Qed. + +Lemma cardinal_subset : forall a b : tree, bst a -> bst b -> + (forall y : elt, In y a -> In y b) -> + (cardinal a <= cardinal b)%nat. +Proof. + intros. + do 2 rewrite cardinal_elements_1. + apply sorted_subset_cardinal; auto. + intros. + generalize (elements_in a x) (elements_in b x). + intuition. +Qed. + +Lemma cardinal_left : forall (l r : tree) (x : elt) (h : int), + (cardinal l < cardinal (Node l x r h))%nat. +Proof. + simpl in |- *; intuition. +Qed. + +Lemma cardinal_right : + forall (l r : tree) (x : elt) (h : int), + (cardinal r < cardinal (Node l x r h))%nat. +Proof. + simpl in |- *; intuition. +Qed. + +Lemma cardinal_rec2 : forall P : tree -> tree -> Set, + (forall s1 s2 : tree, + (forall t1 t2 : tree, + (cardinal t1 + cardinal t2 < cardinal s1 + cardinal s2)%nat -> P t1 t2) + -> P s1 s2) -> + forall s1 s2 : tree, P s1 s2. +Proof. + intros P H s1 s2. + apply well_founded_induction_type_2 + with (R := fun yy' xx' : tree * tree => + (cardinal (fst yy') + cardinal (snd yy') < + cardinal (fst xx') + cardinal (snd xx'))%nat); auto. + apply (Wf_nat.well_founded_ltof _ + (fun xx' : tree * tree => (cardinal (fst xx') + cardinal (snd xx'))%nat)). +Qed. + +Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf. +Proof. + destruct 1; intuition; simpl in *. + avl_nns; simpl in *; false_omega_max. +Qed. + +(** * Union + + [union s1 s2] does an induction over the sum of the cardinals of + [s1] and [s2]. Code is +<< + let rec union s1 s2 = + match (s1, s2) with + (Empty, t2) -> t2 + | (t1, Empty) -> t1 + | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> + if h1 >= h2 then + if h2 = 1 then add v2 s1 else begin + let (l2', _, r2') = split v1 s2 in + join (union l1 l2') v1 (union r1 r2') + end + else + if h1 = 1 then add v1 s2 else begin + let (l1', _, r1') = split v2 s1 in + join (union l1' l2) v2 (union r1' r2) + end +>> +*) + +Definition union : + forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> + {s' : t | bst s' /\ avl s' /\ forall x : elt, In x s' <-> In x s1 \/ In x s2}. +Proof. + intros s1 s2; pattern s1, s2; apply cardinal_rec2; clear s1 s2. + destruct s1 as [| l1 x1 r1 h1]; intros. + (* s = Leaf *) + clear H. + exists s2; intuition_in. + (* s1 = Node l1 x1 r1 *) + destruct s2 as [| l2 x2 r2 h2]; simpl in |- *. + (* s2 = Leaf *) + clear H. + exists (Node l1 x1 r1 h1); simpl; intuition_in. + (* x' = Node l2 x2 r2 *) + case (ge_lt_dec h1 h2); intro. + (* h1 >= h2 *) + case (eq_dec h2 1); intro. + (* h2 = 1 *) + clear H. + exists (add x2 (Node l1 x1 r1 h1)); auto. + inv avl; inv bst. + avl_nn l2; avl_nn r2. + rewrite (height_0 _ H); [ | omega_max]. + rewrite (height_0 _ H4); [ | omega_max]. + split; [apply add_bst; auto|]. + split; [apply add_avl; auto|]. + intros. + rewrite (add_in (Node l1 x1 r1 h1) x2 x); intuition_in. + (* h2 <> 1 *) + (* split x1 s2 = l2',_,r2' *) + case_eq (split x1 (Node l2 x2 r2 h2)); intros l2' (b,r2') EqSplit. + set (s2 := Node l2 x2 r2 h2) in *; clearbody s2. + generalize (split_avl s2 x1 H3); rewrite EqSplit; simpl in *; intros (A,B). + generalize (split_bst s2 x1 H2 H3); rewrite EqSplit; simpl in *; intros (C,D). + generalize (split_in_1 s2 x1); rewrite EqSplit; simpl in *; intros. + generalize (split_in_2 s2 x1); rewrite EqSplit; simpl in *; intros. + (* union l1 l2' = l0 *) + destruct (H l1 l2') as [l0 (H7,(H8,H9))]; inv avl; inv bst; auto. + assert (cardinal l2' <= cardinal s2)%nat. + apply cardinal_subset; trivial. + intros y; rewrite (H4 y); intuition. + omega. + (* union r1 r2' = r0 *) + destruct (H r1 r2') as [r0 (H10,(H11,H12))]; inv avl; inv bst; auto. + assert (cardinal r2' <= cardinal s2)%nat. + apply cardinal_subset; trivial. + intros y; rewrite (H5 y); intuition. + omega. + exists (join l0 x1 r0). + inv avl; inv bst; clear H. + split. + apply join_bst; auto. + red; intros. + rewrite (H9 y) in H. + destruct H; auto. + rewrite (H4 y) in H; intuition. + red; intros. + rewrite (H12 y) in H. + destruct H; auto. + rewrite (H5 y) in H; intuition. + split. + apply join_avl; auto. + intros. + rewrite join_in; auto. + rewrite H9. + rewrite H12. + rewrite H4; auto. + rewrite H5; auto. + intuition_in. + case (X.compare x x1); intuition. + (* h1 < h2 *) + case (eq_dec h1 1); intro. + (* h1 = 1 *) + exists (add x1 (Node l2 x2 r2 h2)); auto. + inv avl; inv bst. + avl_nn l1; avl_nn r1. + rewrite (height_0 _ H3); [ | omega_max]. + rewrite (height_0 _ H8); [ | omega_max]. + split; [apply add_bst; auto|]. + split; [apply add_avl; auto|]. + intros. + rewrite (add_in (Node l2 x2 r2 h2) x1 x); intuition_in. + (* h1 <> 1 *) + (* split x2 s1 = l1',_,r1' *) + case_eq (split x2 (Node l1 x1 r1 h1)); intros l1' (b,r1') EqSplit. + set (s1 := Node l1 x1 r1 h1) in *; clearbody s1. + generalize (split_avl s1 x2 H1); rewrite EqSplit; simpl in *; intros (A,B). + generalize (split_bst s1 x2 H0 H1); rewrite EqSplit; simpl in *; intros (C,D). + generalize (split_in_1 s1 x2); rewrite EqSplit; simpl in *; intros. + generalize (split_in_2 s1 x2); rewrite EqSplit; simpl in *; intros. + (* union l1' l2 = l0 *) + destruct (H l1' l2) as [l0 (H7,(H8,H9))]; inv avl; inv bst; auto. + assert (cardinal l1' <= cardinal s1)%nat. + apply cardinal_subset; trivial. + intros y; rewrite (H4 y); intuition. + omega. + (* union r1' r2 = r0 *) + destruct (H r1' r2) as [r0 (H10,(H11,H12))]; inv avl; inv bst; auto. + assert (cardinal r1' <= cardinal s1)%nat. + apply cardinal_subset; trivial. + intros y; rewrite (H5 y); intuition. + omega. + exists (join l0 x2 r0). + inv avl; inv bst; clear H. + split. + apply join_bst; auto. + red; intros. + rewrite (H9 y) in H. + destruct H; auto. + rewrite (H4 y) in H; intuition. + red; intros. + rewrite (H12 y) in H. + destruct H; auto. + rewrite (H5 y) in H; intuition. + split. + apply join_avl; auto. + intros. + rewrite join_in; auto. + rewrite H9. + rewrite H12. + rewrite H4; auto. + rewrite H5; auto. + intuition_in. + case (X.compare x x2); intuition. +Qed. + + +(** * Subset +<< + let rec subset s1 s2 = + match (s1, s2) with + Empty, _ -> true + | _, Empty -> false + | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) -> + let c = Ord.compare v1 v2 in + if c = 0 then + subset l1 l2 && subset r1 r2 + else if c < 0 then + subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2 + else + subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2 +>> +*) + +Definition subset : forall s1 s2 : t, bst s1 -> bst s2 -> + {Subset s1 s2} + {~ Subset s1 s2}. +Proof. + intros s1 s2; pattern s1, s2; apply cardinal_rec2; clear s1 s2. + destruct s1 as [| l1 x1 r1 h1]; intros. + (* s1 = Leaf *) + left; red; intros; inv In. + (* s1 = Node l1 x1 r1 h1 *) + destruct s2 as [| l2 x2 r2 h2]. + (* s2 = Leaf *) + right; intros; intro. + assert (In x1 Leaf); auto. + inversion_clear H3. + (* s2 = Node l2 x2 r2 h2 *) + case (X.compare x1 x2); intro. + (* x1 < x2 *) + case (H (Node l1 x1 Leaf 0) l2); inv bst; auto; intros. + simpl in |- *; omega. + case (H r1 (Node l2 x2 r2 h2)); inv bst; auto; intros. + simpl in |- *; omega. + clear H; left; red; intuition. + generalize (s a) (s0 a); clear s s0; intuition_in. + clear H; right; red; firstorder. + clear H; right; red; inv bst; intuition. + apply n; red; intros. + assert (In a (Node l2 x2 r2 h2)) by inv In; auto. + intuition_in; order. + (* x1 = x2 *) + case (H l1 l2); inv bst; auto; intros. + simpl in |- *; omega. + case (H r1 r2); inv bst; auto; intros. + simpl in |- *; omega. + clear H; left; red; intuition_in; eauto. + clear H; right; red; inv bst; intuition. + apply n; red; intros. + assert (In a (Node l2 x2 r2 h2)) by auto. + intuition_in; order. + clear H; right; red; inv bst; intuition. + apply n; red; intros. + assert (In a (Node l2 x2 r2 h2)) by auto. + intuition_in; order. + (* x1 > x2 *) + case (H (Node Leaf x1 r1 0) r2); inv bst; auto; intros. + simpl in |- *; omega. + intros; case (H l1 (Node l2 x2 r2 h2)); inv bst; auto; intros. + simpl in |- *; omega. + clear H; left; red; intuition. + generalize (s a) (s0 a); clear s s0; intuition_in. + clear H; right; red; firstorder. + clear H; right; red; inv bst; intuition. + apply n; red; intros. + assert (In a (Node l2 x2 r2 h2)) by inv In; auto. + intuition_in; order. +Qed. + +(** * Comparison *) + +(** ** Relations [eq] and [lt] over trees *) + +Definition eq : t -> t -> Prop := Equal. + +Lemma eq_refl : forall s : t, eq s s. +Proof. + unfold eq, Equal in |- *; intuition. +Qed. + +Lemma eq_sym : forall s s' : t, eq s s' -> eq s' s. +Proof. + unfold eq, Equal in |- *; firstorder. +Qed. + +Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''. +Proof. + unfold eq, Equal in |- *; firstorder. +Qed. + +Lemma eq_L_eq : + forall s s' : t, eq s s' -> L.eq (elements s) (elements s'). +Proof. + unfold eq, Equal, L.eq, L.Equal in |- *; intros. + generalize (elements_in s a) (elements_in s' a). + firstorder. +Qed. + +Lemma L_eq_eq : + forall s s' : t, L.eq (elements s) (elements s') -> eq s s'. +Proof. + unfold eq, Equal, L.eq, L.Equal in |- *; intros. + generalize (elements_in s a) (elements_in s' a). + firstorder. +Qed. +Hint Resolve eq_L_eq L_eq_eq. + +Definition lt (s1 s2 : t) : Prop := L.lt (elements s1) (elements s2). + +Definition lt_trans (s s' s'' : t) (h : lt s s') + (h' : lt s' s'') : lt s s'' := L.lt_trans h h'. + +Lemma lt_not_eq : forall s s' : t, bst s -> bst s' -> lt s s' -> ~ eq s s'. +Proof. + unfold lt in |- *; intros; intro. + apply L.lt_not_eq with (s := elements s) (s' := elements s'); auto. +Qed. + +(** A new comparison algorithm suggested by Xavier Leroy: + +type enumeration = End | More of elt * t * enumeration + +let rec cons s e = match s with + | Empty -> e + | Node(l, v, r, _) -> cons l (More(v, r, e)) + +let rec compare_aux e1 e2 = match (e1, e2) with + | (End, End) -> 0 + | (End, More _) -> -1 + | (More _, End) -> 1 + | (More(v1, r1, k1), More(v2, r2, k2)) -> + let c = Ord.compare v1 v2 in + if c <> 0 then c else compare_aux (cons r1 k1) (cons r2 k2) + +let compare s1 s2 = compare_aux (cons s1 End) (cons s2 End) +*) + +(** ** Enumeration of the elements of a tree *) + +Inductive enumeration : Set := + | End : enumeration + | More : elt -> tree -> enumeration -> enumeration. + +(** [flatten_e e] returns the list of elements of [e] i.e. the list + of elements actually compared *) + +Fixpoint flatten_e (e : enumeration) : list elt := match e with + | End => nil + | More x t r => x :: elements t ++ flatten_e r + end. + +(** [sorted_e e] expresses that elements in the enumeration [e] are + sorted, and that all trees in [e] are binary search trees. *) + +Inductive In_e (x:elt) : enumeration -> Prop := + | InEHd1 : + forall (y : elt) (s : tree) (e : enumeration), + X.eq x y -> In_e x (More y s e) + | InEHd2 : + forall (y : elt) (s : tree) (e : enumeration), + In x s -> In_e x (More y s e) + | InETl : + forall (y : elt) (s : tree) (e : enumeration), + In_e x e -> In_e x (More y s e). + +Hint Constructors In_e. + +Inductive sorted_e : enumeration -> Prop := + | SortedEEnd : sorted_e End + | SortedEMore : + forall (x : elt) (s : tree) (e : enumeration), + bst s -> + (gt_tree x s) -> + sorted_e e -> + (forall y : elt, In_e y e -> X.lt x y) -> + (forall y : elt, + In y s -> forall z : elt, In_e z e -> X.lt y z) -> + sorted_e (More x s e). + +Hint Constructors sorted_e. + +Lemma in_app : + forall (x : elt) (l1 l2 : list elt), + L.MX.In x (l1 ++ l2) -> L.MX.In x l1 \/ L.MX.In x l2. +Proof. + simple induction l1; simpl in |- *; intuition. + inversion_clear H0; auto. + elim (H l2 H1); auto. +Qed. + +Lemma in_flatten_e : + forall (x : elt) (e : enumeration), L.MX.In x (flatten_e e) -> In_e x e. +Proof. + simple induction e; simpl in |- *; intuition. + inversion_clear H. + inversion_clear H0; auto. + elim (in_app x _ _ H1); auto. + destruct (elements_in t x); auto. +Qed. + +Lemma sort_app : + forall l1 l2 : list elt, L.MX.Sort l1 -> L.MX.Sort l2 -> + (forall x y : elt, L.MX.In x l1 -> L.MX.In y l2 -> X.lt x y) -> + L.MX.Sort (l1 ++ l2). +Proof. + simple induction l1; simpl in |- *; intuition. + apply cons_sort; auto. + apply H; auto. + inversion_clear H0; trivial. + induction l as [| a0 l Hrecl]; simpl in |- *; intuition. + induction l2 as [| a0 l2 Hrecl2]; simpl in |- *; intuition. + inversion_clear H0; inversion_clear H4; auto. +Qed. + +Lemma sorted_flatten_e : + forall e : enumeration, sorted_e e -> L.MX.Sort (flatten_e e). +Proof. + simple induction e; simpl in |- *; intuition. + apply cons_sort. + apply sort_app; inversion H0; auto. + intros; apply H8; auto. + destruct (elements_in t x0); auto. + apply in_flatten_e; auto. + apply L.MX.ListIn_Inf. + inversion_clear H0. + intros; elim (in_app_or _ _ _ H0); intuition. + destruct (elements_in t y); auto. + apply H4; apply in_flatten_e; auto. +Qed. + +Lemma elements_app : + forall (s : tree) (acc : list elt), elements_aux acc s = elements s ++ acc. +Proof. + simple induction s; simpl in |- *; intuition. + rewrite H0. + rewrite H. + unfold elements; simpl. + do 2 rewrite H. + rewrite H0. + repeat rewrite <- app_nil_end. + repeat rewrite app_ass; auto. +Qed. + +Lemma compare_flatten_1 : + forall (t0 t2 : tree) (t1 : elt) (z : int) (l : list elt), + elements t0 ++ t1 :: elements t2 ++ l = + elements (Node t0 t1 t2 z) ++ l. +Proof. + simpl in |- *; unfold elements in |- *; simpl in |- *; intuition. + repeat rewrite elements_app. + repeat rewrite <- app_nil_end. + repeat rewrite app_ass; auto. +Qed. + +(** key lemma for correctness *) + +Lemma flatten_e_elements : + forall (x : elt) (l r : tree) (z : int) (e : enumeration), + elements l ++ flatten_e (More x r e) = elements (Node l x r z) ++ flatten_e e. +Proof. + intros; simpl. + apply compare_flatten_1. +Qed. + +(** termination of [compare_aux] *) + +Open Scope Z_scope. + +Fixpoint measure_e_t (s : tree) : Z := match s with + | Leaf => 0 + | Node l _ r _ => 1 + measure_e_t l + measure_e_t r + end. + +Fixpoint measure_e (e : enumeration) : Z := match e with + | End => 0 + | More _ s r => 1 + measure_e_t s + measure_e r + end. + +Ltac Measure_e_t := unfold measure_e_t in |- *; fold measure_e_t in |- *. +Ltac Measure_e := unfold measure_e in |- *; fold measure_e in |- *. + +Lemma measure_e_t_0 : forall s : tree, measure_e_t s >= 0. +Proof. + simple induction s. + simpl in |- *; omega. + intros. + Measure_e_t; omega. (* BUG Simpl! *) +Qed. + +Ltac Measure_e_t_0 s := generalize (measure_e_t_0 s); intro. + +Lemma measure_e_0 : forall e : enumeration, measure_e e >= 0. +Proof. + simple induction e. + simpl in |- *; omega. + intros. + Measure_e; Measure_e_t_0 t; omega. +Qed. + +Ltac Measure_e_0 e := generalize (measure_e_0 e); intro. + +(** Induction principle over the sum of the measures for two lists *) + +Definition compare_rec2 : + forall P : enumeration -> enumeration -> Set, + (forall x x' : enumeration, + (forall y y' : enumeration, + measure_e y + measure_e y' < measure_e x + measure_e x' -> P y y') -> + P x x') -> + forall x x' : enumeration, P x x'. +Proof. + intros P H x x'. + apply well_founded_induction_type_2 + with (R := fun yy' xx' : enumeration * enumeration => + measure_e (fst yy') + measure_e (snd yy') < + measure_e (fst xx') + measure_e (snd xx')); auto. + apply Wf_nat.well_founded_lt_compat + with (f := fun xx' : enumeration * enumeration => + Zabs_nat (measure_e (fst xx') + measure_e (snd xx'))). + intros; apply Zabs.Zabs_nat_lt. + Measure_e_0 (fst x0); Measure_e_0 (snd x0); Measure_e_0 (fst y); + Measure_e_0 (snd y); intros; omega. +Qed. + +(** [cons t e] adds the elements of tree [t] on the head of + enumeration [e]. Code: + +let rec cons s e = match s with + | Empty -> e + | Node(l, v, r, _) -> cons l (More(v, r, e)) +*) + +Definition cons : forall (s : tree) (e : enumeration), bst s -> sorted_e e -> + (forall (x y : elt), In x s -> In_e y e -> X.lt x y) -> + { r : enumeration + | sorted_e r /\ + measure_e r = measure_e_t s + measure_e e /\ + flatten_e r = elements s ++ flatten_e e + }. +Proof. + simple induction s; intuition. + (* s = Leaf *) + exists e; intuition. + (* s = Node t t0 t1 z *) + clear H0. + case (H (More t0 t1 e)); clear H; intuition. + inv bst; auto. + constructor; inversion_clear H1; auto. + inversion_clear H0; inv bst; intuition; order. + exists x; intuition. + generalize H4; Measure_e; intros; Measure_e_t; omega. + rewrite H5. + apply flatten_e_elements. +Qed. + +Lemma l_eq_cons : + forall (l1 l2 : list elt) (x y : elt), + X.eq x y -> L.eq l1 l2 -> L.eq (x :: l1) (y :: l2). +Proof. + unfold L.eq, L.Equal in |- *; intuition. + inversion_clear H1; generalize (H0 a); clear H0; intuition. + apply InA_eqA with x; eauto. + inversion_clear H1; generalize (H0 a); clear H0; intuition. + apply InA_eqA with y; eauto. +Qed. + +Definition compare_aux : + forall e1 e2 : enumeration, sorted_e e1 -> sorted_e e2 -> + Compare L.lt L.eq (flatten_e e1) (flatten_e e2). +Proof. + intros e1 e2; pattern e1, e2 in |- *; apply compare_rec2. + simple destruct x; simple destruct x'; intuition. + (* x = x' = End *) + constructor 2; unfold L.eq, L.Equal in |- *; intuition. + (* x = End x' = More *) + constructor 1; simpl in |- *; auto. + (* x = More x' = End *) + constructor 3; simpl in |- *; auto. + (* x = More e t e0, x' = More e3 t0 e4 *) + case (X.compare e e3); intro. + (* e < e3 *) + constructor 1; simpl; auto. + (* e = e3 *) + destruct (cons t e0) as [c1 (H2,(H3,H4))]; try inversion_clear H0; auto. + destruct (cons t0 e4) as [c2 (H5,(H6,H7))]; try inversion_clear H1; auto. + destruct (H c1 c2); clear H; intuition. + Measure_e; omega. + constructor 1; simpl. + apply L.lt_cons_eq; auto. + rewrite H4 in l; rewrite H7 in l; auto. + constructor 2; simpl. + apply l_eq_cons; auto. + rewrite H4 in e6; rewrite H7 in e6; auto. + constructor 3; simpl. + apply L.lt_cons_eq; auto. + rewrite H4 in l; rewrite H7 in l; auto. + (* e > e3 *) + constructor 3; simpl; auto. +Qed. + +Definition compare : forall s1 s2, bst s1 -> bst s2 -> Compare lt eq s1 s2. +Proof. + intros s1 s2 s1_bst s2_bst; unfold lt, eq; simpl. + destruct (cons s1 End); intuition. + inversion_clear H0. + destruct (cons s2 End); intuition. + inversion_clear H3. + simpl in H2; rewrite <- app_nil_end in H2. + simpl in H5; rewrite <- app_nil_end in H5. + destruct (compare_aux x x0); intuition. + constructor 1; simpl in |- *. + rewrite H2 in l; rewrite H5 in l; auto. + constructor 2; apply L_eq_eq; simpl in |- *. + rewrite H2 in e; rewrite H5 in e; auto. + constructor 3; simpl in |- *. + rewrite H2 in l; rewrite H5 in l; auto. +Qed. + +(** * Equality test *) + +Definition equal : forall s s' : t, bst s -> bst s' -> {Equal s s'} + {~ Equal s s'}. +Proof. + intros s s' Hs Hs'; case (compare s s'); auto; intros. + right; apply lt_not_eq; auto. + right; intro; apply (lt_not_eq s' s); auto; apply eq_sym; auto. +Qed. + +(** We provide additionally a different implementation for union, subset and + equal, which is less efficient, but uses structural induction, hence computes + within Coq. *) + +(** Alternative union based on fold. + Complexity : [min(|s|,|s'|)*log(max(|s|,|s'|))] *) + +Definition union' s s' := + if ge_lt_dec (height s) (height s') then fold add s' s else fold add s s'. + +Lemma fold_add_avl : forall s s', avl s -> avl s' -> avl (fold add s s'). +Proof. + induction s; simpl; intros; inv avl; auto. +Qed. +Hint Resolve fold_add_avl. + +Lemma union'_avl : forall s s', avl s -> avl s' -> avl (union' s s'). +Proof. + unfold union'; intros; destruct (ge_lt_dec (height s) (height s')); auto. +Qed. + +Lemma fold_add_bst : forall s s', bst s -> avl s -> bst s' -> avl s' -> + bst (fold add s s'). +Proof. + induction s; simpl; intros; inv avl; inv bst; auto. + apply IHs2; auto. + apply add_bst; auto. +Qed. + +Lemma union'_bst : forall s s', bst s -> avl s -> bst s' -> avl s' -> + bst (union' s s'). +Proof. + unfold union'; intros; destruct (ge_lt_dec (height s) (height s')); + apply fold_add_bst; auto. +Qed. + +Lemma fold_add_in : forall s s' y, bst s -> avl s -> bst s' -> avl s' -> + (In y (fold add s s') <-> In y s \/ In y s'). +Proof. + induction s; simpl; intros; inv avl; inv bst; auto. + intuition_in. + rewrite IHs2; auto. + apply add_bst; auto. + apply fold_add_bst; auto. + rewrite add_in; auto. + rewrite IHs1; auto. + intuition_in. +Qed. + +Lemma union'_in : forall s s' y, bst s -> avl s -> bst s' -> avl s' -> + (In y (union' s s') <-> In y s \/ In y s'). +Proof. + unfold union'; intros; destruct (ge_lt_dec (height s) (height s')). + rewrite fold_add_in; intuition. + apply fold_add_in; auto. +Qed. + +(** Alternative subset based on diff. *) + +Definition subset' s s' := is_empty (diff s s'). + +Lemma subset'_1 : forall s s', bst s -> avl s -> bst s' -> avl s' -> + Subset s s' -> subset' s s' = true. +Proof. + unfold subset', Subset; intros; apply is_empty_1; red; intros. + rewrite (diff_in); intuition. +Qed. + +Lemma subset'_2 : forall s s', bst s -> avl s -> bst s' -> avl s' -> + subset' s s' = true -> Subset s s'. +Proof. + unfold subset', Subset; intros; generalize (is_empty_2 _ H3 a); unfold Empty. + rewrite (diff_in); intuition. + generalize (mem_2 s' a) (mem_1 s' a); destruct (mem a s'); intuition. +Qed. + +(** Alternative equal based on subset *) + +Definition equal' s s' := subset' s s' && subset' s' s. + +Lemma equal'_1 : forall s s', bst s -> avl s -> bst s' -> avl s' -> + Equal s s' -> equal' s s' = true. +Proof. + unfold equal', Equal; intros. + rewrite subset'_1; firstorder; simpl. + apply subset'_1; firstorder. +Qed. + +Lemma equal'_2 : forall s s', bst s -> avl s -> bst s' -> avl s' -> + equal' s s' = true -> Equal s s'. +Proof. + unfold equal', Equal; intros; destruct (andb_prop _ _ H3); split; + apply subset'_2; auto. +Qed. + +End Raw. + +(** * Encapsulation + + Now, in order to really provide a functor implementing [S], we + need to encapsulate everything into a type of balanced binary search trees. *) + +Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. + + Module E := X. + Module Raw := Raw I X. + Import Raw. + + Record bbst : Set := Bbst {this :> t; is_bst : bst this; is_avl: avl this}. + Definition t := bbst. + Definition elt := X.t. + + Definition In (x : elt) (s : t) := In x s. + Definition Equal s s' := forall a : elt, In a s <-> In a s'. + Definition Subset s s' := forall a : elt, In a s -> In a s'. + Definition Empty s := forall a : elt, ~ In a s. + Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x. + Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x. + + Implicit Types s : t. + Implicit Types x y : elt. + + Definition In_1 s := In_1 s. + + Definition mem x s := mem x s. + + Definition empty := Bbst _ empty_bst empty_avl. + Definition is_empty s := is_empty s. + Definition singleton x := Bbst _ (singleton_bst x) (singleton_avl x). + Definition add x s := + Bbst _ (add_bst s x (is_bst s) (is_avl s)) + (add_avl s x (is_avl s)). + Definition remove x s := + Bbst _ (remove_bst s x (is_bst s) (is_avl s)) + (remove_avl s x (is_avl s)). + Definition inter s s' := + Bbst _ (inter_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + (inter_avl _ _ (is_avl s) (is_avl s')). + Definition diff s s' := + Bbst _ (diff_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + (diff_avl _ _ (is_avl s) (is_avl s')). + Definition elements s := elements s. + Definition min_elt s := min_elt s. + Definition max_elt s := max_elt s. + Definition choose s := choose s. + Definition fold (B : Set) (f : elt -> B -> B) s := fold f s. + Definition cardinal s := cardinal s. + Definition filter (f : elt -> bool) s := + Bbst _ (filter_bst f _ (is_bst s) (is_avl s)) + (filter_avl f _ (is_avl s)). + Definition for_all (f : elt -> bool) s := for_all f s. + Definition exists_ (f : elt -> bool) s := exists_ f s. + Definition partition (f : elt -> bool) s := + let p := partition f s in + (Bbst (fst p) (partition_bst_1 f _ (is_bst s) (is_avl s)) + (partition_avl_1 f _ (is_avl s)), + Bbst (snd p) (partition_bst_2 f _ (is_bst s) (is_avl s)) + (partition_avl_2 f _ (is_avl s))). + + Definition union s s' := + let (u,p) := union _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s') in + let (b,p) := p in + let (a,_) := p in + Bbst u b a. + + Definition union' s s' := + Bbst _ (union'_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + (union'_avl _ _ (is_avl s) (is_avl s')). + + Definition equal s s':= if equal _ _ (is_bst s) (is_bst s') then true else false. + Definition equal' s s' := equal' s s'. + + Definition subset s s':= if subset _ _ (is_bst s) (is_bst s') then true else false. + Definition subset' s s' := subset' s s'. + + Definition eq s s' := eq s s'. + Definition lt s s' := lt s s'. + + Definition compare s s' : Compare lt eq s s'. + Proof. + intros; elim (compare _ _ (is_bst s) (is_bst s')); + [ constructor 1 | constructor 2 | constructor 3 ]; + auto. + Defined. + + (* specs *) + Section Specs. + Variable s s' : t. + Variable x y : elt. + + Hint Resolve is_bst is_avl. + + Definition mem_1 := mem_1 s x (is_bst s). + Definition mem_2 := mem_2 s x. + + Lemma equal_1 : Equal s s' -> equal s s' = true. + Proof. + unfold equal; destruct (Raw.equal s s'); simpl; auto. + Qed. + + Lemma equal_2 : equal s s' = true -> Equal s s'. + Proof. + unfold equal; destruct (Raw.equal s s'); simpl; intuition; discriminate. + Qed. + + Definition equal'_1 s s' := + equal'_1 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'). + Definition equal'_2 s s' := + equal'_2 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'). + + Lemma subset_1 : Subset s s' -> subset s s' = true. + Proof. + unfold subset; destruct (Raw.subset s s'); simpl; intuition. + Qed. + + Lemma subset_2 : subset s s' = true -> Subset s s'. + Proof. + unfold subset; destruct (Raw.subset s s'); simpl; intuition discriminate. + Qed. + + Definition subset'_1 s s' := + subset'_1 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'). + Definition subset'_2 s s' := + subset'_2 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s'). + + Definition empty_1 : Empty empty := empty_1. + + Definition is_empty_1 : Empty s -> is_empty s = true := is_empty_1 s. + Definition is_empty_2 : is_empty s = true -> Empty s := is_empty_2 s. + + Lemma add_1 : X.eq x y -> In y (add x s). + Proof. + unfold add, In; simpl; rewrite add_in; auto. + Qed. + + Lemma add_2 : In y s -> In y (add x s). + Proof. + unfold add, In; simpl; rewrite add_in; auto. + Qed. + + Lemma add_3 : ~ X.eq x y -> In y (add x s) -> In y s. + Proof. + unfold add, In; simpl; rewrite add_in; intuition. + elim H; auto. + Qed. + + Lemma remove_1 : E.eq x y -> ~ In y (remove x s). + Proof. + unfold remove, In; simpl; rewrite remove_in; intuition. + Qed. + + Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). + Proof. + unfold remove, In; simpl; rewrite remove_in; intuition. + Qed. + + Lemma remove_3 : In y (remove x s) -> In y s. + Proof. + unfold remove, In; simpl; rewrite remove_in; intuition. + Qed. + + Definition singleton_1 := singleton_1 x y. + Definition singleton_2 := singleton_2 x y. + + Lemma union_1 : In x (union s s') -> In x s \/ In x s'. + Proof. + unfold union, In; simpl. + destruct (Raw.union s s' (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + as (u,(b,(a,i))). + simpl in *; rewrite i; auto. + Qed. + + Lemma union_2 : In x s -> In x (union s s'). + Proof. + unfold union, In; simpl. + destruct (Raw.union s s' (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + as (u,(b,(a,i))). + simpl in *; rewrite i; auto. + Qed. + + Lemma union_3 : In x s' -> In x (union s s'). + Proof. + unfold union, In; simpl. + destruct (Raw.union s s' (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + as (u,(b,(a,i))). + simpl in *; rewrite i; auto. + Qed. + + Lemma union'_1 : In x (union' s s') -> In x s \/ In x s'. + Proof. + unfold union', In; simpl; rewrite union'_in; intuition. + Qed. + + Lemma union'_2 : In x s -> In x (union' s s'). + Proof. + unfold union', In; simpl; rewrite union'_in; intuition. + Qed. + + Lemma union'_3 : In x s' -> In x (union' s s'). + Proof. + unfold union', In; simpl; rewrite union'_in; intuition. + Qed. + + Lemma inter_1 : In x (inter s s') -> In x s. + Proof. + unfold inter, In; simpl; rewrite inter_in; intuition. + Qed. + + Lemma inter_2 : In x (inter s s') -> In x s'. + Proof. + unfold inter, In; simpl; rewrite inter_in; intuition. + Qed. + + Lemma inter_3 : In x s -> In x s' -> In x (inter s s'). + Proof. + unfold inter, In; simpl; rewrite inter_in; intuition. + Qed. + + Lemma diff_1 : In x (diff s s') -> In x s. + Proof. + unfold diff, In; simpl; rewrite diff_in; intuition. + Qed. + + Lemma diff_2 : In x (diff s s') -> ~ In x s'. + Proof. + unfold diff, In; simpl; rewrite diff_in; intuition. + Qed. + + Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s'). + Proof. + unfold diff, In; simpl; rewrite diff_in; intuition. + Qed. + + Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A), + fold A f s i = fold_left (fun a e => f e a) (elements s) i. + Proof. + unfold fold, elements; intros; apply fold_1; auto. + Qed. + + Lemma cardinal_1 : cardinal s = length (elements s). + Proof. + unfold cardinal, elements; intros; apply cardinal_elements_1; auto. + Qed. + + Section Filter. + Variable f : elt -> bool. + + Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. + Proof. + intro; unfold filter, In; simpl; rewrite filter_in; intuition. + Qed. + + Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. + Proof. + intro; unfold filter, In; simpl; rewrite filter_in; intuition. + Qed. + + Lemma filter_3 : compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). + Proof. + intro; unfold filter, In; simpl; rewrite filter_in; intuition. + Qed. + + Definition for_all_1 := for_all_1 f s. + Definition for_all_2 := for_all_2 f s. + + Definition exists_1 := exists_1 f s. + Definition exists_2 := exists_2 f s. + + Lemma partition_1 : compat_bool E.eq f -> + Equal (fst (partition f s)) (filter f s). + Proof. + unfold partition, filter, Equal, In; simpl ;intros H a. + rewrite partition_in_1; auto. + rewrite filter_in; intuition. + Qed. + + Lemma partition_2 : compat_bool E.eq f -> + Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). + Proof. + unfold partition, filter, Equal, In; simpl ;intros H a. + rewrite partition_in_2; auto. + rewrite filter_in; intuition. + red; intros. + f_equal; auto. + destruct (f a); auto. + destruct (f a); auto. + Qed. + + End Filter. + + Lemma elements_1 : In x s -> InA E.eq x (elements s). + Proof. + unfold elements, In; rewrite elements_in; auto. + Qed. + + Lemma elements_2 : InA E.eq x (elements s) -> In x s. + Proof. + unfold elements, In; rewrite elements_in; auto. + Qed. + + Definition elements_3 : sort E.lt (elements s) := elements_sort _ (is_bst s). + + Definition min_elt_1 := min_elt_1 s x. + Definition min_elt_2 := min_elt_2 s x y (is_bst s). + Definition min_elt_3 := min_elt_3 s. + + Definition max_elt_1 := max_elt_1 s x. + Definition max_elt_2 := max_elt_2 s x y (is_bst s). + Definition max_elt_3 := max_elt_3 s. + + Definition choose_1 := choose_1 s x. + Definition choose_2 := choose_2 s. + + Definition eq_refl s := eq_refl s. + Definition eq_sym s s' := eq_sym s s'. + Definition eq_trans s s' s'' := eq_trans s s' s''. + + Definition lt_trans s s' s'' := lt_trans s s' s''. + Definition lt_not_eq s s' := lt_not_eq _ _ (is_bst s) (is_bst s'). + + End Specs. +End IntMake. + +(* 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). + + diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v new file mode 100644 index 000000000..9dd5f2739 --- /dev/null +++ b/theories/FSets/FSetToFiniteSet.v @@ -0,0 +1,139 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +Require Import Ensembles Finite_sets. +Require Import FSetInterface FSetProperties OrderedTypeEx. + +(** * Going from [FSets] with usual equality + to the old [Ensembles] and [Finite_sets] theory. *) + +Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). + Module MP:= Properties(M). + Import M MP FM Ensembles Finite_sets. + + Definition mkEns : M.t -> Ensemble M.elt := + fun s x => M.In x s. + + Notation " !! " := mkEns. + + Lemma In_In : forall s x, M.In x s <-> In _ (!!s) x. + Proof. + unfold In; compute; auto. + Qed. + + Lemma Subset_Included : forall s s', s[<=]s' <-> Included _ (!!s) (!!s'). + Proof. + unfold Subset, Included, In, mkEns; intuition. + Qed. + + Notation " a === b " := (Same_set M.elt a b) (at level 70, no associativity). + + Lemma Equal_Same_set : forall s s', s[=]s' <-> !!s === !!s'. + Proof. + intros. + rewrite double_inclusion. + unfold Subset, Included, Same_set, In, mkEns; intuition. + Qed. + + Lemma empty_Empty_Set : !!M.empty === Empty_set _. + Proof. + unfold Same_set, Included, mkEns, In. + split; intro; set_iff; inversion 1. + Qed. + + Lemma Empty_Empty_set : forall s, Empty s -> !!s === Empty_set _. + Proof. + unfold Same_set, Included, mkEns, In. + split; intros. + destruct(H x H0). + inversion H0. + Qed. + + Lemma singleton_Singleton : forall x, !!(M.singleton x) === Singleton _ x . + Proof. + unfold Same_set, Included, mkEns, In. + split; intro; set_iff; inversion 1; try constructor; auto. + Qed. + + Lemma union_Union : forall s s', !!(union s s') === Union _ (!!s) (!!s'). + Proof. + unfold Same_set, Included, mkEns, In. + split; intro; set_iff; inversion 1; [ constructor 1 | constructor 2 | | ]; auto. + Qed. + + Lemma inter_Intersection : forall s s', !!(inter s s') === Intersection _ (!!s) (!!s'). + Proof. + unfold Same_set, Included, mkEns, In. + split; intro; set_iff; inversion 1; try constructor; auto. + Qed. + + Lemma add_Add : forall x s, !!(add x s) === Add _ (!!s) x. + Proof. + unfold Same_set, Included, mkEns, In. + split; intro; set_iff; inversion 1; auto with sets. + inversion H0. + constructor 2; constructor. + constructor 1; auto. + Qed. + + Lemma Add_Add : forall x s s', MP.Add x s s' -> !!s' === Add _ (!!s) x. + Proof. + unfold Same_set, Included, mkEns, In. + split; intros. + red in H; rewrite H in H0. + destruct H0. + inversion H0. + constructor 2; constructor. + constructor 1; auto. + red in H; rewrite H. + inversion H0; auto. + inversion H1; auto. + Qed. + + Lemma remove_Subtract : forall x s, !!(remove x s) === Subtract _ (!!s) x. + Proof. + unfold Same_set, Included, mkEns, In. + split; intro; set_iff; inversion 1; auto with sets. + split; auto. + swap H1. + inversion H2; auto. + Qed. + + Lemma mkEns_Finite : forall s, Finite _ (!!s). + Proof. + intro s; pattern s; apply set_induction; clear s; intros. + intros; replace (!!s) with (Empty_set elt); auto with sets. + symmetry; apply Extensionality_Ensembles. + apply Empty_Empty_set; auto. + replace (!!s') with (Add _ (!!s) x). + constructor 2; auto. + symmetry; apply Extensionality_Ensembles. + apply Add_Add; auto. + Qed. + + Lemma mkEns_cardinal : forall s, cardinal _ (!!s) (M.cardinal s). + Proof. + intro s; pattern s; apply set_induction; clear s; intros. + intros; replace (!!s) with (Empty_set elt); auto with sets. + rewrite cardinal_1; auto with sets. + symmetry; apply Extensionality_Ensembles. + apply Empty_Empty_set; auto. + replace (!!s') with (Add _ (!!s) x). + rewrite (cardinal_2 H0 H1); auto with sets. + symmetry; apply Extensionality_Ensembles. + apply Add_Add; auto. + Qed. + +End S_to_Finite_set. diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v index 51cd23c12..8b4123ebd 100644 --- a/theories/FSets/FSets.v +++ b/theories/FSets/FSets.v @@ -9,8 +9,11 @@ (* $Id$ *) Require Export OrderedType. +Require Export OrderedTypeEx. +Require Export OrderedTypeAlt. Require Export FSetInterface. Require Export FSetBridge. Require Export FSetProperties. Require Export FSetEqProperties. Require Export FSetList. +Require Export FSetToFiniteSet.
\ No newline at end of file diff --git a/theories/FSets/Int.v b/theories/FSets/Int.v new file mode 100644 index 000000000..534934a70 --- /dev/null +++ b/theories/FSets/Int.v @@ -0,0 +1,421 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +(** * An axiomatization of integers. *) + +(** We define a signature for an integer datatype based on [Z]. + The goal is to allow a switch after extraction to ocaml's + [big_int] or even [int] when finiteness isn't a problem + (typically : when mesuring the height of an AVL tree). +*) + +Require Import ZArith. +Require Import ROmega. + +Module Type Int. + + Delimit Scope Int_scope with I. + Open Scope Int_scope. + + Parameter int : Set. + + Parameter i2z : int -> Z. + Arguments Scope i2z [ Int_scope ]. + + Parameter _0 : int. + Parameter _1 : int. + Parameter _2 : int. + Parameter _3 : int. + Parameter plus : int -> int -> int. + Parameter opp : int -> int. + Parameter minus : int -> int -> int. + Parameter mult : int -> int -> int. + Parameter max : int -> int -> int. + + Notation "0" := _0 : Int_scope. + Notation "1" := _1 : Int_scope. + Notation "2" := _2 : Int_scope. + Notation "3" := _3 : Int_scope. + Infix "+" := plus : Int_scope. + Infix "-" := minus : Int_scope. + Infix "*" := mult : Int_scope. + Notation "- x" := (opp x) : Int_scope. + +(** For logical relations, we can rely on their counterparts in Z, + since they don't appear after extraction. Moreover, using tactics + like omega is easier this way. *) + + Notation "x == y" := (i2z x = i2z y) + (at level 70, y at next level, no associativity) : Int_scope. + Notation "x <= y" := (Zle (i2z x) (i2z y)): Int_scope. + Notation "x < y" := (Zlt (i2z x) (i2z y)) : Int_scope. + Notation "x >= y" := (Zge (i2z x) (i2z y)) : Int_scope. + Notation "x > y" := (Zgt (i2z x) (i2z y)): Int_scope. + Notation "x <= y <= z" := (x <= y /\ y <= z) : Int_scope. + Notation "x <= y < z" := (x <= y /\ y < z) : Int_scope. + Notation "x < y < z" := (x < y /\ y < z) : Int_scope. + Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope. + + (** Some decidability fonctions (informative). *) + + Axiom gt_le_dec : forall x y: int, {x > y} + {x <= y}. + Axiom ge_lt_dec : forall x y : int, {x >= y} + {x < y}. + Axiom eq_dec : forall x y : int, { x == y } + {~ x==y }. + + (** Specifications *) + + (** First, we ask [i2z] to be injective. Said otherwise, our ad-hoc equality + [==] and the generic [=] are in fact equivalent. We define [==] + nonetheless since the translation to [Z] for using automatic tactic is easier. *) + + Axiom i2z_eq : forall n p : int, n == p -> n = p. + + (** Then, we express the specifications of the above parameters using their + Z counterparts. *) + + Open Scope Z_scope. + Axiom i2z_0 : i2z _0 = 0. + Axiom i2z_1 : i2z _1 = 1. + Axiom i2z_2 : i2z _2 = 2. + Axiom i2z_3 : i2z _3 = 3. + Axiom i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. + Axiom i2z_opp : forall n, i2z (-n) = -i2z n. + Axiom i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. + Axiom i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. + Axiom i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). + +End Int. + +Module MoreInt (I:Int). + Import I. + + Open Scope Int_scope. + + (** A magic (but costly) tactic that goes from [int] back to the [Z] + friendly world ... *) + + Hint Rewrite -> + i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z. + + Ltac i2z := match goal with + | H : (eq (A:=int) ?a ?b) |- _ => + generalize (f_equal i2z H); + try autorewrite with i2z; clear H; intro H; i2z + | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); try autorewrite with i2z; i2z + | H : _ |- _ => progress autorewrite with i2z in H; i2z + | _ => try autorewrite with i2z + end. + + (** A reflexive version of the [i2z] tactic *) + + (** this [i2z_refl] is actually weaker than [i2z]. For instance, if a + [i2z] is buried deep inside a subterm, [i2z_refl] may miss it. + See also the limitation about [Set] or [Type] part below. + Anyhow, [i2z_refl] is enough for applying [romega]. *) + + Ltac i2z_gen := match goal with + | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen + | H : (eq (A:=int) ?a ?b) |- _ => + generalize (f_equal i2z H); clear H; i2z_gen + | H : (eq (A:=Z) ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zlt ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zle ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zgt ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zge ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : _ -> ?X |- _ => + (* A [Set] or [Type] part cannot be dealt with easily + using the [ExprP] datatype. So we forget it, leaving + a goal that can be weaker than the original. *) + match type of X with + | Type => clear H; i2z_gen + | Prop => generalize H; clear H; i2z_gen + end + | H : _ <-> _ |- _ => generalize H; clear H; i2z_gen + | H : _ /\ _ |- _ => generalize H; clear H; i2z_gen + | H : _ \/ _ |- _ => generalize H; clear H; i2z_gen + | H : ~ _ |- _ => generalize H; clear H; i2z_gen + | _ => idtac + end. + + Inductive ExprI : Set := + | EI0 : ExprI + | EI1 : ExprI + | EI2 : ExprI + | EI3 : ExprI + | EIplus : ExprI -> ExprI -> ExprI + | EIopp : ExprI -> ExprI + | EIminus : ExprI -> ExprI -> ExprI + | EImult : ExprI -> ExprI -> ExprI + | EImax : ExprI -> ExprI -> ExprI + | EIraw : int -> ExprI. + + Inductive ExprZ : Set := + | EZplus : ExprZ -> ExprZ -> ExprZ + | EZopp : ExprZ -> ExprZ + | EZminus : ExprZ -> ExprZ -> ExprZ + | EZmult : ExprZ -> ExprZ -> ExprZ + | EZmax : ExprZ -> ExprZ -> ExprZ + | EZofI : ExprI -> ExprZ + | EZraw : Z -> ExprZ. + + Inductive ExprP : Type := + | EPeq : ExprZ -> ExprZ -> ExprP + | EPlt : ExprZ -> ExprZ -> ExprP + | EPle : ExprZ -> ExprZ -> ExprP + | EPgt : ExprZ -> ExprZ -> ExprP + | EPge : ExprZ -> ExprZ -> ExprP + | EPimpl : ExprP -> ExprP -> ExprP + | EPequiv : ExprP -> ExprP -> ExprP + | EPand : ExprP -> ExprP -> ExprP + | EPor : ExprP -> ExprP -> ExprP + | EPneg : ExprP -> ExprP + | EPraw : Prop -> ExprP. + + (** [int] to [ExprI] *) + + Ltac i2ei trm := + match constr:trm with + | 0 => constr:EI0 + | 1 => constr:EI1 + | 2 => constr:EI2 + | 3 => constr:EI3 + | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIplus ex ey) + | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIminus ex ey) + | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImult ex ey) + | max ?x ?y => let ex := i2ei x with ey := i2ei y in constr:(EImax ex ey) + | - ?x => let ex := i2ei x in constr:(EIopp ex) + | ?x => constr:(EIraw x) + end + + (** [Z] to [ExprZ] *) + + with z2ez trm := + match constr:trm with + | (?x+?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey) + | (?x-?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey) + | (?x*?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey) + | (Zmax ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey) + | (-?x)%Z => let ex := z2ez x in constr:(EZopp ex) + | i2z ?x => let ex := i2ei x in constr:(EZofI ex) + | ?x => constr:(EZraw x) + end. + + (** [Prop] to [ExprP] *) + + Ltac p2ep trm := + match constr:trm with + | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey) + | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey) + | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey) + | (?x \/ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPor ex ey) + | (~ ?x) => let ex := p2ep x in constr:(EPneg ex) + | (eq (A:=Z) ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EPeq ex ey) + | (?x<?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey) + | (?x<=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey) + | (?x>?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey) + | (?x>=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey) + | ?x => constr:(EPraw x) + end. + + (** [ExprI] to [int] *) + + Fixpoint ei2i (e:ExprI) : int := + match e with + | EI0 => 0 + | EI1 => 1 + | EI2 => 2 + | EI3 => 3 + | EIplus e1 e2 => (ei2i e1)+(ei2i e2) + | EIminus e1 e2 => (ei2i e1)-(ei2i e2) + | EImult e1 e2 => (ei2i e1)*(ei2i e2) + | EImax e1 e2 => max (ei2i e1) (ei2i e2) + | EIopp e => -(ei2i e) + | EIraw i => i + end. + + (** [ExprZ] to [Z] *) + + Fixpoint ez2z (e:ExprZ) : Z := + match e with + | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z + | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z + | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z + | EZmax e1 e2 => Zmax (ez2z e1) (ez2z e2) + | EZopp e => (-(ez2z e))%Z + | EZofI e => i2z (ei2i e) + | EZraw z => z + end. + + (** [ExprP] to [Prop] *) + + Fixpoint ep2p (e:ExprP) : Prop := + match e with + | EPeq e1 e2 => (ez2z e1) = (ez2z e2) + | EPlt e1 e2 => ((ez2z e1)<(ez2z e2))%Z + | EPle e1 e2 => ((ez2z e1)<=(ez2z e2))%Z + | EPgt e1 e2 => ((ez2z e1)>(ez2z e2))%Z + | EPge e1 e2 => ((ez2z e1)>=(ez2z e2))%Z + | EPimpl e1 e2 => (ep2p e1) -> (ep2p e2) + | EPequiv e1 e2 => (ep2p e1) <-> (ep2p e2) + | EPand e1 e2 => (ep2p e1) /\ (ep2p e2) + | EPor e1 e2 => (ep2p e1) \/ (ep2p e2) + | EPneg e => ~ (ep2p e) + | EPraw p => p + end. + + (** [ExprI] (supposed under a [i2z]) to a simplified [ExprZ] *) + + Fixpoint norm_ei (e:ExprI) : ExprZ := + match e with + | EI0 => EZraw (0%Z) + | EI1 => EZraw (1%Z) + | EI2 => EZraw (2%Z) + | EI3 => EZraw (3%Z) + | EIplus e1 e2 => EZplus (norm_ei e1) (norm_ei e2) + | EIminus e1 e2 => EZminus (norm_ei e1) (norm_ei e2) + | EImult e1 e2 => EZmult (norm_ei e1) (norm_ei e2) + | EImax e1 e2 => EZmax (norm_ei e1) (norm_ei e2) + | EIopp e => EZopp (norm_ei e) + | EIraw i => EZofI (EIraw i) + end. + + (** [ExprZ] to a simplified [ExprZ] *) + + Fixpoint norm_ez (e:ExprZ) : ExprZ := + match e with + | EZplus e1 e2 => EZplus (norm_ez e1) (norm_ez e2) + | EZminus e1 e2 => EZminus (norm_ez e1) (norm_ez e2) + | EZmult e1 e2 => EZmult (norm_ez e1) (norm_ez e2) + | EZmax e1 e2 => EZmax (norm_ez e1) (norm_ez e2) + | EZopp e => EZopp (norm_ez e) + | EZofI e => norm_ei e + | EZraw z => EZraw z + end. + + (** [ExprP] to a simplified [ExprP] *) + + Fixpoint norm_ep (e:ExprP) : ExprP := + match e with + | EPeq e1 e2 => EPeq (norm_ez e1) (norm_ez e2) + | EPlt e1 e2 => EPlt (norm_ez e1) (norm_ez e2) + | EPle e1 e2 => EPle (norm_ez e1) (norm_ez e2) + | EPgt e1 e2 => EPgt (norm_ez e1) (norm_ez e2) + | EPge e1 e2 => EPge (norm_ez e1) (norm_ez e2) + | EPimpl e1 e2 => EPimpl (norm_ep e1) (norm_ep e2) + | EPequiv e1 e2 => EPequiv (norm_ep e1) (norm_ep e2) + | EPand e1 e2 => EPand (norm_ep e1) (norm_ep e2) + | EPor e1 e2 => EPor (norm_ep e1) (norm_ep e2) + | EPneg e => EPneg (norm_ep e) + | EPraw p => EPraw p + end. + + Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e). + Proof. + induction e; simpl; intros; i2z; auto; try congruence. + Qed. + + Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e. + Proof. + induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct. + Qed. + + Lemma norm_ep_correct : + forall e:ExprP, ep2p (norm_ep e) <-> ep2p e. + Proof. + induction e; simpl; repeat (rewrite norm_ez_correct); intuition. + Qed. + + Lemma norm_ep_correct2 : + forall e:ExprP, ep2p (norm_ep e) -> ep2p e. + Proof. + intros; destruct (norm_ep_correct e); auto. + Qed. + + Ltac i2z_refl := + i2z_gen; + match goal with |- ?t => + let e := p2ep t + in + (change (ep2p e); + apply norm_ep_correct2; + simpl) + end. + + Ltac iauto := i2z_refl; auto. + Ltac iomega := i2z_refl; intros; romega. + + Open Scope Z_scope. + + Lemma max_spec : forall (x y:Z), + x >= y /\ Zmax x y = x \/ + x < y /\ Zmax x y = y. + Proof. + intros; unfold Zmax, Zlt, Zge. + destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate. + Qed. + + Ltac omega_max_genspec x y := + generalize (max_spec x y); + let z := fresh "z" in let Hz := fresh "Hz" in + (set (z:=Zmax x y); clearbody z). + + Ltac omega_max_loop := + match goal with + (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *) + | |- context [ i2z (?f ?x) ] => + let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop + | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop + | _ => intros + end. + + Ltac omega_max := i2z_refl; omega_max_loop; try romega. + + Ltac false_omega := i2z_refl; intros; romega. + Ltac false_omega_max := elimtype False; omega_max. + + Open Scope Int_scope. +End MoreInt. + + +(** It's always nice to know that our [Int] interface is realizable :-) *) + +Module Z_as_Int <: Int. + Open Scope Z_scope. + Definition int := Z. + Definition _0 := 0. + Definition _1 := 1. + Definition _2 := 2. + Definition _3 := 3. + Definition plus := Zplus. + Definition opp := Zopp. + Definition minus := Zminus. + Definition mult := Zmult. + Definition max := Zmax. + Definition gt_le_dec := Z_gt_le_dec. + Definition ge_lt_dec := Z_ge_lt_dec. + Definition eq_dec := Z_eq_dec. + Definition i2z : int -> Z := fun n => n. + Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed. + Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed. + Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed. + Lemma i2z_2 : i2z _2 = 2. Proof. auto. Qed. + Lemma i2z_3 : i2z _3 = 3. Proof. auto. Qed. + Lemma i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. Proof. auto. Qed. + Lemma i2z_opp : forall n, i2z (- n) = - i2z n. Proof. auto. Qed. + Lemma i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. Proof. auto. Qed. + Lemma i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. Proof. auto. Qed. + Lemma i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed. +End Z_as_Int. + diff --git a/theories/FSets/OrderedTypeAlt.v b/theories/FSets/OrderedTypeAlt.v new file mode 100644 index 000000000..4eaaca403 --- /dev/null +++ b/theories/FSets/OrderedTypeAlt.v @@ -0,0 +1,129 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +Require Import OrderedType. + +(** * An alternative (but equivalent) presentation for an Ordered Type inferface. *) + +(** NB: [comparison], defined in [theories/Init/datatypes.v] is [Eq|Lt|Gt] +whereas [compare], defined in [theories/FSets/OrderedType.v] is [EQ _ | LT _ | GT _ ] +*) + +Module Type OrderedTypeAlt. + + Parameter t : Set. + + Parameter compare : t -> t -> comparison. + + Infix "?=" := compare (at level 70, no associativity). + + Parameter compare_sym : + forall x y, (y?=x) = CompOpp (x?=y). + Parameter compare_trans : + forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + +End OrderedTypeAlt. + +(** From this new presentation to the original one. *) + +Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType. + Import O. + + Definition t := t. + + Definition eq x y := (x?=y) = Eq. + Definition lt x y := (x?=y) = Lt. + + Lemma eq_refl : forall x, eq x x. + Proof. + intro x. + unfold eq. + assert (H:=compare_sym x x). + destruct (x ?= x); simpl in *; try discriminate; auto. + Qed. + + Lemma eq_sym : forall x y, eq x y -> eq y x. + Proof. + unfold eq; intros. + rewrite compare_sym. + rewrite H; simpl; auto. + Qed. + + Definition eq_trans := (compare_trans Eq). + + Definition lt_trans := (compare_trans Lt). + + Lemma lt_not_eq : forall x y, lt x y -> ~eq x y. + Proof. + unfold eq, lt; intros. + rewrite H; discriminate. + Qed. + + Definition compare : forall x y, Compare lt eq x y. + Proof. + intros. + case_eq (x ?= y); intros. + apply EQ; auto. + apply LT; auto. + apply GT; red. + rewrite compare_sym; rewrite H; auto. + Defined. + +End OrderedType_from_Alt. + +(** From the original presentation to this alternative one. *) + +Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt. + Import O. + Module MO:=OrderedTypeFacts(O). + Import MO. + + Definition t := t. + + Definition compare x y := match compare x y with + | LT _ => Lt + | EQ _ => Eq + | GT _ => Gt + end. + + Infix "?=" := compare (at level 70, no associativity). + + Lemma compare_sym : + forall x y, (y?=x) = CompOpp (x?=y). + Proof. + intros x y. + unfold compare. + destruct (O.compare y x); elim_comp; simpl; auto. + Qed. + + Lemma compare_trans : + forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + Proof. + intros c x y z. + destruct c; unfold compare. + destruct (O.compare x y); intros; try discriminate. + destruct (O.compare y z); intros; try discriminate. + elim_comp; auto. + destruct (O.compare x y); intros; try discriminate. + destruct (O.compare y z); intros; try discriminate. + elim_comp; auto. + destruct (O.compare x y); intros; try discriminate. + destruct (O.compare y z); intros; try discriminate. + elim_comp; auto. + Qed. + +End OrderedType_to_Alt. + + diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v new file mode 100644 index 000000000..cee0413b1 --- /dev/null +++ b/theories/FSets/OrderedTypeEx.v @@ -0,0 +1,248 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id$ *) + +Require Import OrderedType. +Require Import ZArith. +Require Import NArith Ndec. +Require Import Compare_dec. + +(** * Examples of Ordered Type structures. *) + +(** First, a particular case of [OrderedType] where + the equality is the usual one of Coq. *) + +Module Type UsualOrderedType. + Parameter t : Set. + Definition eq := @eq t. + Parameter lt : t -> t -> Prop. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Parameter compare : forall x y : t, Compare lt eq x y. +End UsualOrderedType. + +(** a [UsualOrderedType] is in particular an [OrderedType]. *) + +Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U. + +(** [nat] is an ordered type with respect to the usual order on natural numbers. *) + +Module Nat_as_OT <: UsualOrderedType. + + Definition t := nat. + + Definition eq := @eq nat. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt := lt. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. unfold lt in |- *; intros; apply lt_trans with y; auto. Qed. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. unfold lt, eq in |- *; intros; omega. Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + intros; case (lt_eq_lt_dec x y). + simple destruct 1; intro. + constructor 1; auto. + constructor 2; auto. + intro; constructor 3; auto. + Qed. + +End Nat_as_OT. + + +(** [Z] is an ordered type with respect to the usual order on integers. *) + +Open Scope Z_scope. + +Module Z_as_OT <: UsualOrderedType. + + Definition t := Z. + Definition eq := @eq Z. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt (x y:Z) := (x<y). + + Lemma lt_trans : forall x y z, x<y -> y<z -> x<z. + Proof. auto with zarith. Qed. + + Lemma lt_not_eq : forall x y, x<y -> ~ x=y. + Proof. auto with zarith. Qed. + + Definition compare : forall x y, Compare lt eq x y. + Proof. + intros x y; case_eq (x ?= y); intros. + apply EQ; unfold eq; apply Zcompare_Eq_eq; auto. + apply LT; unfold lt, Zlt; auto. + apply GT; unfold lt, Zlt; rewrite <- Zcompare_Gt_Lt_antisym; auto. + Defined. + +End Z_as_OT. + + +(** [positive] is an ordered type with respect to the usual order on natural numbers. *) + +Open Scope positive_scope. + +Module Positive_as_OT <: UsualOrderedType. + Definition t:=positive. + Definition eq:=@eq positive. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt p q:= (p ?= q) Eq = Lt. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. + unfold lt; intros x y z. + change ((Zpos x < Zpos y)%Z -> (Zpos y < Zpos z)%Z -> (Zpos x < Zpos z)%Z). + auto with zarith. + Qed. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + intros; intro. + rewrite H0 in H. + unfold lt in H. + rewrite Pcompare_refl in H; discriminate. + Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + intros x y. + case_eq ((x ?= y) Eq); intros. + apply EQ; apply Pcompare_Eq_eq; auto. + apply LT; unfold lt; auto. + apply GT; unfold lt. + replace Eq with (CompOpp Eq); auto. + rewrite <- Pcompare_antisym; rewrite H; auto. + Qed. + +End Positive_as_OT. + + +(** [N] is an ordered type with respect to the usual order on natural numbers. *) + +Open Scope positive_scope. + +Module N_as_OT <: UsualOrderedType. + Definition t:=N. + Definition eq:=@eq N. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + + Definition lt p q:= Nle q p = false. + + Definition lt_trans := Nlt_trans. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + intros; intro. + rewrite H0 in H. + unfold lt in H. + rewrite Nle_refl in H; discriminate. + Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + Proof. + intros x y. + case_eq ((x ?= y)%N); intros. + apply EQ; apply Ncompare_Eq_eq; auto. + apply LT; unfold lt; auto. + generalize (Nle_Ncompare y x). + destruct (Nle y x); auto. + rewrite <- Ncompare_antisym. + destruct (x ?= y)%N; simpl; try discriminate. + intros (H0,_); elim H0; auto. + apply GT; unfold lt. + generalize (Nle_Ncompare x y). + destruct (Nle x y); auto. + destruct (x ?= y)%N; simpl; try discriminate. + intros (H0,_); elim H0; auto. + Qed. + +End N_as_OT. + + +(** From two ordered types, we can build a new OrderedType + over their cartesian product, using the lexicographic order. *) + +Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. + Module MO1:=OrderedTypeFacts(O1). + Module MO2:=OrderedTypeFacts(O2). + + Definition t := prod O1.t O2.t. + + Definition eq x y := O1.eq (fst x) (fst y) /\ O2.eq (snd x) (snd y). + + Definition lt x y := + O1.lt (fst x) (fst y) \/ + (O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)). + + Lemma eq_refl : forall x : t, eq x x. + Proof. + intros (x1,x2); red; simpl; auto. + Qed. + + Lemma eq_sym : forall x y : t, eq x y -> eq y x. + Proof. + intros (x1,x2) (y1,y2); unfold eq; simpl; intuition. + Qed. + + Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. + Proof. + intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. + Qed. + + Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. + Proof. + intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition. + left; eauto. + left; eapply MO1.lt_eq; eauto. + left; eapply MO1.eq_lt; eauto. + right; split; eauto. + Qed. + + Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. + Proof. + intros (x1,x2) (y1,y2); unfold eq, lt; simpl; intuition. + apply (O1.lt_not_eq H0 H1). + apply (O2.lt_not_eq H3 H2). + Qed. + + Definition compare : forall x y : t, Compare lt eq x y. + intros (x1,x2) (y1,y2). + destruct (O1.compare x1 y1). + apply LT; unfold lt; auto. + destruct (O2.compare x2 y2). + apply LT; unfold lt; auto. + apply EQ; unfold eq; auto. + apply GT; unfold lt; auto. + apply GT; unfold lt; auto. + Qed. + +End PairOrderedType. + |