From 770a0e7a4b6df754ead90c51334898dec5df4ebc Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 9 Feb 2008 17:22:35 +0000 Subject: Major revision of FSetAVL: more Function, including some non-structural ones NB: this change adds about 10s of compile-time to a file that is already taking about 30s on my machine. If somebody strongly objects to this, contact me. I really think that the gain in uniformity, clarity, and computability (in Coq) worth the extra compile-time: no more function-by-tactic, everything (vm_)computes, and quite efficiently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10545 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bool.v | 6 + theories/FSets/FSetAVL.v | 1742 ++++++++++++++++++++-------------------------- 2 files changed, 749 insertions(+), 999 deletions(-) (limited to 'theories') diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0d674ebf9..652ac955e 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -308,6 +308,12 @@ Hint Resolve orb_comm orb_assoc: bool v62. (** * Properties of [andb] *) (*******************************) +Lemma andb_true_iff : + forall b1 b2:bool, b1 && b2 = true <-> b1 = true /\ b2 = true. +Proof. + destruct b1; destruct b2; intuition. +Qed. + Lemma andb_true_eq : forall a b:bool, true = a && b -> true = a /\ true = b. Proof. diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index b6bcb6fb4..6f0ea32a5 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -17,24 +17,30 @@ (** 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 Local Scope Int_scope. +Require Import Recdef FSetInterface FSetList ZArith Int. +Module Raw (Import I:Int)(X:OrderedType). +Module Import II:=MoreInt(I). +Open Scope Int_scope. Module MX := OrderedTypeFacts X. Definition elt := X.t. -(** * Trees *) +(** Notations and helper lemma about pairs *) + +Notation "s #1" := (fst s) (at level 9, format "s '#1'"). +Notation "s #2" := (snd s) (at level 9, format "s '#2'"). + +Lemma distr_pair : forall (A B:Set)(s:A*B)(a:A)(b:B), s = (a,b) -> + s#1 = a /\ s#2 = b. +Proof. + destruct s; simpl; injection 1; auto. +Qed. + + +(** * Trees + + The fourth field of [Node] is the height of the tree *) Inductive tree : Set := | Leaf : tree @@ -42,10 +48,74 @@ Inductive tree : Set := Notation t := tree. -(** The fourth field of [Node] is the height of the tree *) +(** * Basic functions on trees: height and cardinal *) + +Definition height (s : tree) : int := + match s with + | Leaf => 0 + | Node _ _ _ h => h + end. + +Fixpoint cardinal (s : tree) : nat := + match s with + | Leaf => 0%nat + | Node l _ r _ => S (cardinal l + cardinal r) + end. + +(** * Occurrence in a tree *) + +Inductive In (x : elt) : tree -> Prop := + | IsRoot : forall l r h y, X.eq x y -> In x (Node l y r h) + | InLeft : forall l r h y, In x l -> In x (Node l y r h) + | InRight : forall l r h y, In x r -> In x (Node l y r h). + +(** * 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, In y s -> X.lt y x. +Definition gt_tree x s := forall y, 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 l r h, bst l -> bst r -> + lt_tree x l -> gt_tree x r -> bst (Node l x 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 *) + +Inductive avl : tree -> Prop := + | RBLeaf : avl Leaf + | RBNode : forall x l r h, avl l -> avl r -> + -(2) <= height l - height r <= 2 -> + h = max (height l) (height r) + 1 -> + avl (Node l x r h). + + + +(** * Automation and dedicated tactics *) + +Hint Constructors In bst avl. +Hint Unfold lt_tree gt_tree. + +(** A tactic for cleaning hypothesis after use of functional induction. *) + +Ltac clearf := + match goal with + | H : (@Logic.eq (Compare _ _ _ _) _ _) |- _ => clear H; clearf + | H : (@Logic.eq (sumbool _ _) _ _) |- _ => clear H; clearf + | _ => idtac + end. (** A tactic to repeat [inversion_clear] on all hyps of the form [(f (Node _ _ _ _))] *) + Ltac inv f := match goal with | H:f Leaf |- _ => inversion_clear H; inv f @@ -63,74 +133,83 @@ Ltac safe_inv f := match goal with | _ => intros end. -(** * Occurrence in a tree *) +Ltac intuition_in := repeat progress (intuition; inv In). -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. +(** Helper tactic concerning order of elements. *) -Ltac intuition_in := repeat progress (intuition; inv In). +Ltac order := match goal with + | U: lt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order + | U: gt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order + | _ => MX.order +end. -(** [In] is compatible with [X.eq] *) +(** Tactics about [avl] *) -Lemma In_1 : - forall s x y, X.eq x y -> In x s -> In y s. +Lemma height_non_negative : forall s : tree, avl s -> height s >= 0. Proof. - induction s; simpl; intuition_in; eauto. + induction s; simpl; intros; auto with zarith. + inv avl; intuition; omega_max. Qed. -Hint Immediate In_1. +Implicit Arguments height_non_negative. -(** * Binary search trees *) +(** When [H:avl r], typing [avl_nn H] or [avl_nn r] adds [height r>=0] *) -(** [lt_tree x s]: all elements in [s] are smaller than [x] - (resp. greater for [gt_tree]) *) +Ltac avl_nn_hyp H := + let nz := fresh "nz" in assert (nz := height_non_negative H). -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. +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. -Hint Unfold lt_tree gt_tree. +(* Repeat the previous tactic. + Drawback: need to clear the [avl _] hyps ... Thank you Ltac *) -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 avl_nns := + match goal with + | H:avl _ |- _ => avl_nn_hyp H; clear H; avl_nns + | _ => idtac + end. + + + +(** * Basic results about [In], [lt_tree], [gt_tree], [avl], [height] *) + +(** [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. (** 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. + red; inversion 1. Qed. Lemma gt_leaf : forall x : elt, gt_tree x Leaf. Proof. - unfold gt_tree in |- *; intros; inversion H. + red; inversion 1. 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. + unfold lt_tree; 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. + unfold gt_tree; intuition_in; order. Qed. Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node. @@ -144,7 +223,7 @@ 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. + eauto. Qed. Lemma gt_tree_not_in : @@ -156,51 +235,15 @@ 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. + 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 -> +Lemma avl_node : + forall x l r, avl l -> avl r -> -(2) <= height l - height r <= 2 -> avl (Node l x r (max (height l) (height r) + 1)). Proof. @@ -208,35 +251,15 @@ Proof. Qed. Hint Resolve avl_node. -(** The tactics *) +(** Results about [height] *) -Lemma height_non_negative : forall s : tree, avl s -> height s >= 0. +Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf. Proof. - induction s; simpl; intros; auto with zarith. - inv avl; intuition; omega_max. + destruct 1; intuition; simpl in *. + avl_nns; simpl in *; elimtype False; 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. *) @@ -246,6 +269,17 @@ 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. + + +(** trick for emulating [assert false] in Coq. *) + +Definition assert_false := Leaf. +Lemma assert_false_cardinal : cardinal assert_false = 0%nat. +Proof. simpl; auto. Qed. +Opaque assert_false. + + + (** * Empty set *) Definition empty := Leaf. @@ -281,6 +315,8 @@ Proof. destruct s; simpl; intros; try discriminate; red; auto. Qed. + + (** * Appartness *) (** The [mem] function is deciding appartness. It exploits the [bst] property @@ -297,27 +333,25 @@ Function mem (x:elt)(s:t) { struct s } : bool := 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. +Proof. + intros s x; functional induction mem x s; auto; intros; clearf; + inv bst; intuition_in; order. 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. + intros s x; functional induction mem x s; auto; intros; 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. + unfold singleton; auto. Qed. Lemma singleton_avl : forall x : elt, avl (singleton x). @@ -328,7 +362,7 @@ 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. + unfold singleton; intros; inv In; order. Qed. Lemma singleton_2 : forall x y, X.eq x y -> In y (singleton x). @@ -336,6 +370,8 @@ Proof. unfold singleton; auto. Qed. + + (** * Helper functions *) (** [create l x r] creates a node, assuming [l] and [r] @@ -372,14 +408,11 @@ 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 := +Function bal (l:t)(x:elt)(r:t) : t := let hl := height l in let hr := height r in if gt_le_dec hl (hr+2) then @@ -412,55 +445,51 @@ Definition bal l x r := 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. + intros l x r; functional induction bal l x r; intros; + 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. 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. + intros l x r; functional induction bal l x r; intros; clearf; + 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. + intros l x r; functional induction bal l x r; intros; clearf; + 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. + intros l x r; functional induction bal l x r; intros; clearf; + 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; + intros l x r; functional induction bal l x r; intros; clearf; solve [repeat rewrite create_in; intuition_in - |inv avl; avl_nns; simpl in *; omega_max]. + |inv avl; avl_nns; simpl in *; omega_max ]. +Qed. + +Lemma bal_cardinal : forall l x r, + (cardinal (bal l x r) <= S (cardinal l + cardinal r))%nat. +Proof. + intros l x r; functional induction bal l x r; intros; clearf; + simpl; auto with arith; romega with *. Qed. Ltac omega_bal := match goal with @@ -469,6 +498,8 @@ Ltac omega_bal := match goal with omega_max end. + + (** * Insertion *) Function add (x:elt)(s:t) { struct s } : t := match s with @@ -544,6 +575,16 @@ Proof. apply MX.lt_eq with x; auto. Qed. +Lemma add_cardinal : forall x s, + (cardinal (add x s) <= S (cardinal s))%nat. +Proof. + intros; functional induction add x s; simpl; auto with arith. + generalize (bal_cardinal (add x l) y r); romega with *. + generalize (bal_cardinal l y (add x r)); romega with *. +Qed. + + + (** * Join Same as [bal] but does not assume anything regarding heights @@ -563,6 +604,8 @@ Fixpoint join (l:t) : elt -> t -> t := end end. +(* XXX: Comment utiliser Function pour definit join et eviter join_tac ? *) + 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; @@ -581,7 +624,6 @@ Ltac join_tac := 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. @@ -680,6 +722,24 @@ Proof. apply create_bst; auto. Qed. +Lemma join_cardinal : forall l x r, + (cardinal (join l x r) <= S (cardinal l + cardinal r))%nat. +Proof. + join_tac; simpl; auto with arith. + apply add_cardinal. + destruct X.compare; simpl; auto with arith. + generalize (bal_cardinal (add x ll) lx lr) (add_cardinal x ll); + romega with *. + generalize (bal_cardinal ll lx (add x lr)) (add_cardinal x lr); + romega with *. + generalize (bal_cardinal ll lx (join lr x (Node rl rx rr rh))) + (Hlr x (Node rl rx rr rh)); simpl; romega with *. + generalize (bal_cardinal (join (Node ll lx lr lh) x rl) rx rr). + simpl in *; romega with *. +Qed. + + + (** * Extraction of minimum element morally, [remove_min] is to be applied to a non-empty tree @@ -690,12 +750,13 @@ Qed. Function 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 : t*elt) in (bal l' x r, m) + | 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. + avl (remove_min l x r)#1 /\ + 0 <= height (Node l x r h) - height (remove_min l x r)#1 <= 1. Proof. intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv avl; simpl in *; split; auto. @@ -709,14 +770,14 @@ Proof. Qed. Lemma remove_min_avl : forall l x r h, avl (Node l x r h) -> - avl (fst (remove_min l x r)). + avl (remove_min l x r)#1. 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))). + X.eq y (remove_min l x r)#2 \/ In y (remove_min l x r)#1). Proof. intros l x r; functional induction (remove_min l x r); simpl in *; intros. intuition_in. @@ -731,14 +792,14 @@ Proof. 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)). + bst (Node l x r h) -> avl (Node l x r h) -> bst (remove_min l x r)#1. Proof. intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv bst; auto. inversion_clear H; inversion_clear H0. rewrite_all e0;simpl in *. apply bal_bst; auto. - firstorder. + apply (IHp lh); auto. intro; intros. generalize (remove_min_in ll lx lr lh y H). rewrite e0; simpl. @@ -748,7 +809,7 @@ 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)). + gt_tree (remove_min l x r)#2 (remove_min l x r)#1. Proof. intros l x r; functional induction (remove_min l x r); subst;simpl in *; intros. inv bst; auto. @@ -759,12 +820,13 @@ Proof. generalize (remove_min_in ll lx lr lh m H). rewrite e0; simpl; intros. rewrite (bal_in l' x r y H7 H5) in H0. - destruct H6. - firstorder. - apply MX.lt_eq with x; auto. - apply X.lt_trans with x; auto. + assert (In m (Node ll lx lr lh)) by (rewrite H6; auto); clear H6. + assert (X.lt m x) by order. + decompose [or] H0; order. Qed. + + (** * Merging two trees [merge t1 t2] builds the union of [t1] and [t2] assuming all elements @@ -809,7 +871,7 @@ Proof. intuition_in. intuition_in. destruct s1;try contradiction;clear y. - replace s2' with (fst (remove_min l2 x2 r2)); [|rewrite e1; auto]. + replace s2' with ((remove_min l2 x2 r2)#1); [|rewrite e1; auto]. rewrite bal_in; auto. generalize (remove_min_avl l2 x2 r2 h2); rewrite e1; simpl; auto. generalize (remove_min_in l2 x2 r2 h2 y0); rewrite e1; simpl; intro. @@ -830,9 +892,11 @@ Proof. generalize (remove_min_gt_tree l2 x2 r2 h2); rewrite e1; simpl; auto. Qed. + + (** * Deletion *) -Function remove (x:elt)(s:tree) { struct s } : t := match s with +Function remove (x:elt)(s:t) { struct s } : t := match s with | Leaf => Leaf | Node l y r h => match X.compare x y with @@ -913,7 +977,9 @@ Proof. destruct H; eauto. Qed. - (** * Minimum element *) + + +(** * Minimum element *) Function min_elt (s:t) : option elt := match s with | Leaf => None @@ -962,6 +1028,7 @@ Proof. Qed. + (** * Maximum element *) Function max_elt (s:t) : option elt := match s with @@ -989,9 +1056,6 @@ Proof. inversion_clear H5. destruct r;try contradiction. inversion_clear 1. -(* inversion 1; subst. *) -(* assert (X.lt y x) by (apply H4; auto). *) -(* inversion_clear 1; auto; order. *) assert (X.lt _x0 t) by auto. inversion_clear 2; auto; (assert (~ X.lt x t) by auto); order. @@ -1006,6 +1070,8 @@ Proof. intros H0; destruct (IHo H0 t); auto. Qed. + + (** * Any element *) Definition choose := min_elt. @@ -1020,6 +1086,8 @@ Proof. exact min_elt_3. Qed. + + (** * Concatenation Same as [merge] but does not assume anything about heights. @@ -1072,6 +1140,10 @@ Proof. intro EQ; rewrite EQ; intuition. Qed. +Hint Resolve concat_avl concat_bst. + + + (** * Splitting [split x s] returns a triple [(l, present, r)] where @@ -1080,7 +1152,7 @@ Qed. - [present] is [true] if and only if [s] contains [x]. *) -Function split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with +Function 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 @@ -1095,7 +1167,7 @@ Function split (x:elt)(s:t) {struct s} : t * (bool * t) := match s with end. Lemma split_avl : forall s x, avl s -> - avl (fst (split x s)) /\ avl (snd (snd (split x s))). + avl (split x s)#1 /\ avl (split x s)#2#2. Proof. intros s x; functional induction (split x s);subst;simpl in *. auto. @@ -1105,7 +1177,7 @@ Proof. 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). + (In y (split x s)#1 <-> In y s /\ X.lt y x). Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. @@ -1128,7 +1200,7 @@ Proof. 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). + (In y (split x s)#2#2 <-> In y s /\ X.lt x y). Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. @@ -1148,7 +1220,7 @@ Proof. Qed. Lemma split_in_3 : forall s x, bst s -> avl s -> - (fst (snd (split x s)) = true <-> In x s). + ((split x s)#2#1 = true <-> In x s). Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition; try inversion_clear H1. @@ -1165,7 +1237,7 @@ Proof. Qed. Lemma split_bst : forall s x, bst s -> avl s -> - bst (fst (split x s)) /\ bst (snd (snd (split x s))). + bst (split x s)#1 /\ bst (split x s)#2#2. Proof. intros s x; functional induction (split x s);subst;simpl in *. intuition. @@ -1187,12 +1259,35 @@ Proof. generalize (split_in_1 r x y0 H1 H5); rewrite e1; simpl; intuition. Qed. +Lemma split_cardinal_1 : forall x s, + (cardinal (split x s)#1 <= cardinal s)%nat. +Proof. + intros x s; functional induction split x s; simpl; auto. + rewrite e1 in IHp; simpl in *. + romega with *. + romega with *. + rewrite e1 in IHp; simpl in *. + generalize (join_cardinal l y rl); romega with *. +Qed. + +Lemma split_cardinal_2 : forall x s, + (cardinal (split x s)#2#2 <= cardinal s)%nat. +Proof. + intros x s; functional induction split x s; simpl; auto. + rewrite e1 in IHp; simpl in *. + generalize (join_cardinal rl y r); romega with *. + romega with *. + rewrite e1 in IHp; simpl in *; romega with *. +Qed. + + + (** * Intersection *) -Fixpoint inter (s1 s2 : t) {struct s1} : t := match s1, s2 with - | Leaf,_ => Leaf - | _,Leaf => Leaf - | Node l1 x1 r1 h1, _ => +Function inter (s1 s2 : t) { struct s1 } : t := match s1, s2 with + | Leaf, _ => Leaf + | _, Leaf => Leaf + | Node l1 x1 r1 h1, Node l2 x2 r2 h2 => match split x1 s2 with | (l2',(true,r2')) => join (inter l1 l2') x1 (inter r1 r2') | (l2',(false,r2')) => concat (inter l1 l2') (inter r1 r2') @@ -1200,58 +1295,44 @@ Fixpoint inter (s1 s2 : t) {struct s1} : t := match s1, s2 with 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. +Proof. + intros s1 s2; functional induction inter s1 s2; auto; intros A1 A2; + generalize (split_avl _ x1 A2); rewrite e1; simpl; destruct 1; + inv avl; auto. Qed. +Hint Resolve inter_avl. 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. +Proof. + intros s1 s2; functional induction inter s1 s2; intros B1 A1 B2 A2; + [intuition_in|intuition_in | | ]; + set (r:=Node l2 x2 r2 h2) in *; + generalize (split_avl _ x1 A2)(split_bst _ x1 B2 A2); + rewrite e1; simpl; destruct 1; destruct 1; + inv avl; inv bst; + destruct IHt as (IHb1,IHi1); auto; + destruct IHt0 as (IHb2,IHi2); auto; + destruct (distr_pair _ _ _ _ _ e1); clear e1; + destruct (distr_pair _ _ _ _ _ H12); clear H12; split. (* bst join *) - apply join_bst; try apply inter_avl; auto; - intro y; [rewrite (H22 y)|rewrite (H24 y)]; intuition. - (* bst concat *) - apply concat_bst; try apply inter_avl; auto. - intros y1 y2; rewrite (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, H28; intuition_in. + apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. + (* In join *) + intros; rewrite join_in; auto; rewrite IHi1; rewrite IHi2. + rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. + rewrite split_in_3 in H13; intuition_in. apply In_1 with x1; auto. - (* in concat *) - rewrite concat_in; try apply inter_avl; auto. - intros y1 y2; rewrite (H28 y1), (H30 y2); intuition eauto. - rewrite H30, H28; intuition_in. - generalize (H26 (In_1 _ _ _ H22 H35)); intro; discriminate. + (* bst concat *) + apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. + (* In concat *) + intros; rewrite concat_in; auto. + intros y1 y2; rewrite IHi1, IHi2; intuition; order. + rewrite IHi1; rewrite IHi2. + rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. + assert (~In x1 r) by (rewrite <- split_in_3; auto; rewrite H13; auto). + intuition_in. + elim H12. + apply In_1 with y; auto. Qed. Lemma inter_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -1266,72 +1347,60 @@ Proof. intros s1 s2 y B1 A1 B2 A2; destruct (inter_bst_in s1 s2 B1 A1 B2 A2); auto. Qed. + + (** * Difference *) -Fixpoint diff (s1 s2 : t) { struct s1 } : t := match s1, s2 with +Function diff (s1 s2 : t) { struct s1 } : t := match s1, s2 with | Leaf, _ => Leaf | _, Leaf => s1 - | Node l1 x1 r1 h1, _ => + | Node l1 x1 r1 h1, Node l2 x2 r2 h2 => match split x1 s2 with | (l2',(true,r2')) => concat (diff l1 l2') (diff r1 r2') | (l2',(false,r2')) => join (diff l1 l2') x1 (diff r1 r2') end -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. + intros s1 s2; functional induction diff s1 s2; auto; intros A1 A2; + generalize (split_avl _ x1 A2); rewrite e1; simpl; destruct 1; + inv avl; auto. Qed. +Hint Resolve diff_avl. 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. +Proof. + intros s1 s2; functional induction diff s1 s2; intros B1 A1 B2 A2; + [intuition_in|intuition_in | | ]; + set (r:=Node l2 x2 r2 h2) in *; + generalize (split_avl _ x1 A2)(split_bst _ x1 B2 A2); + rewrite e1; simpl; destruct 1; destruct 1; + inv avl; inv bst; + destruct IHt as (IHb1,IHi1); auto; + destruct IHt0 as (IHb2,IHi2); auto; + destruct (distr_pair _ _ _ _ _ e1); clear e1; + destruct (distr_pair _ _ _ _ _ H12); clear H12; split. (* bst concat *) - apply concat_bst; try apply diff_avl; auto. - intros y1 y2; rewrite (H22 y1), (H24 y2); intuition eauto. + apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. + (* In concat *) + intros; rewrite concat_in; auto. + intros y1 y2; rewrite IHi1, IHi2; intuition; order. + rewrite IHi1; rewrite IHi2. + rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. + rewrite split_in_3 in H13; intuition_in. + elim H17. + apply In_1 with x1; auto. (* bst join *) - apply join_bst; try apply diff_avl; auto; - intro y; [rewrite (H22 y)|rewrite (H24 y)]; intuition. - (* 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, H28; intuition_in. - elim H35; apply In_1 with x1; auto. - (* in join *) - rewrite join_in; try apply diff_avl; auto. - rewrite H30, H28; intuition_in. - generalize (H26 (In_1 _ _ _ H34 H24)); intro; discriminate. + apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. + (* In join *) + intros; rewrite join_in; auto; rewrite IHi1; rewrite IHi2. + rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto. + assert (~In x1 r) by (rewrite <- split_in_3; auto; rewrite H13; auto). + intuition_in. + elim H12. + apply In_1 with y; auto. Qed. Lemma diff_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> @@ -1346,6 +1415,128 @@ Proof. intros s1 s2 y B1 A1 B2 A2; destruct (diff_bst_in s1 s2 B1 A1 B2 A2); auto. Qed. + + +(** * Union *) + +Definition cardinal2 (s:t*t) := (cardinal s#1 + cardinal s#2)%nat. + +Ltac union_tac := + intros; unfold cardinal2; simpl fst in *; simpl snd in *; + match goal with H: split ?x ?s = _ |- _ => + generalize (split_cardinal_1 x s) (split_cardinal_2 x s); + rewrite H; simpl; romega with * + end. + +Function union (s : t * t) { measure cardinal2 s } : t := + match s with + | (Leaf, Leaf) => s#2 + | (Leaf, Node _ _ _ _) => s#2 + | (Node _ _ _ _, Leaf) => s#1 + | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) => + if ge_lt_dec h1 h2 then + if eq_dec h2 1 then add x2 s#1 else + let (l2',r2') := split x1 s#2 in + join (union (l1,l2')) x1 (union (r1,r2'#2)) + else + if eq_dec h1 1 then add x1 s#2 else + let (l1',r1') := split x2 s#1 in + join (union (l1',l2)) x2 (union (r1'#2,r2)) + end. +Proof. +abstract union_tac. +abstract union_tac. +abstract union_tac. +abstract union_tac. +Defined. + +Lemma union_avl : forall s, + avl s#1 -> avl s#2 -> avl (union s). +Proof. + intros s; functional induction union s; + simpl fst in *; simpl snd in *; auto. + intros A1 A2; generalize (split_avl _ x1 A2); rewrite e2; simpl. + inv avl; destruct 1; auto. + intros A1 A2; generalize (split_avl _ x2 A1); rewrite e2; simpl. + inv avl; destruct 1; auto. +Qed. +Hint Resolve union_avl. + +Lemma union_in : forall s y, + bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> + (In y (union s) <-> In y s#1 \/ In y s#2). +Proof. + intros s; functional induction union s; intros y B1 A1 B2 A2; + simpl fst in *; simpl snd in *; try clear e0 e1. + intuition_in. + intuition_in. + intuition_in. + (* add x2 s#1 *) + inv avl. + rewrite (height_0 _ H); [ | avl_nn l2; omega_max]. + rewrite (height_0 _ H0); [ | avl_nn r2; omega_max]. + rewrite add_in; auto; intuition_in. + (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *) + generalize + (split_avl _ x1 A2) (split_bst _ x1 B2 A2) + (split_in_1 _ x1 y B2 A2) (split_in_2 _ x1 y B2 A2). + rewrite e2; simpl. + destruct 1; destruct 1; inv avl; inv bst. + rewrite join_in; auto. + rewrite IHt; auto. + rewrite IHt0; auto. + do 2 (intro Eq; rewrite Eq; clear Eq). + case (X.compare y x1); intuition_in. + (* add x1 s#2 *) + inv avl. + rewrite (height_0 _ H3); [ | avl_nn l1; omega_max]. + rewrite (height_0 _ H4); [ | avl_nn r1; omega_max]. + rewrite add_in; auto; intuition_in. + (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *) + generalize + (split_avl _ x2 A1) (split_bst _ x2 B1 A1) + (split_in_1 _ x2 y B1 A1) (split_in_2 _ x2 y B1 A1). + rewrite e2; simpl. + destruct 1; destruct 1; inv avl; inv bst. + rewrite join_in; auto. + rewrite IHt; auto. + rewrite IHt0; auto. + do 2 (intro Eq; rewrite Eq; clear Eq). + case (X.compare y x2); intuition_in. +Qed. + +Lemma union_bst : forall s, + bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> bst (union s). +Proof. + intros s; functional induction union s; intros B1 A1 B2 A2; + simpl fst in *; simpl snd in *; try clear e0 e1; + try apply add_bst; auto. + (* join (union (l1,l2')) x1 (union (r1,r2'#2)) *) + generalize (split_avl _ x1 A2) (split_bst _ x1 B2 A2). + rewrite e2; simpl. + destruct 1; destruct 1. + destruct (distr_pair _ _ _ _ _ e2) as (L,R); clear e2. + inv bst; inv avl. + apply join_bst; auto. + intro y; rewrite union_in; auto; simpl. + rewrite <- L, split_in_1; auto; intuition_in. + intro y; rewrite union_in; auto; simpl. + rewrite <- R, split_in_2; auto; intuition_in. + (* join (union (l1',l2)) x1 (union (r1'#2,r2)) *) + generalize (split_avl _ x2 A1) (split_bst _ x2 B1 A1). + rewrite e2; simpl. + destruct 1; destruct 1. + destruct (distr_pair _ _ _ _ _ e2) as (L,R); clear e2. + inv bst; inv avl. + apply join_bst; auto. + intro y; rewrite union_in; auto; simpl. + rewrite <- L, split_in_1; auto; intuition_in. + intro y; rewrite union_in; auto; simpl. + rewrite <- R, split_in_2; auto; intuition_in. +Qed. + + + (** * Elements *) (** [elements_tree_aux acc t] catenates the elements of [t] in infix @@ -1408,6 +1599,22 @@ Proof. auto. Qed. +Lemma elements_aux_cardinal : + 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 elements_cardinal : forall s : tree, cardinal s = length (elements s). +Proof. + exact (fun s => elements_aux_cardinal s nil). +Qed. + + + (** * Filter *) Section F. @@ -1483,6 +1690,8 @@ Proof. unfold filter; intros; rewrite filter_acc_in; intuition_in. Qed. + + (** * Partition *) Fixpoint partition_acc (acc : t*t)(s : t) { struct s } : t*t := @@ -1498,7 +1707,7 @@ Fixpoint partition_acc (acc : t*t)(s : t) { struct s } : t*t := 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)). + avl acc#1 -> avl (partition_acc acc s)#1. Proof. induction s; simpl; auto. destruct acc as [acct accf]; simpl in *. @@ -1510,7 +1719,7 @@ Proof. Qed. Lemma partition_acc_avl_2 : forall s acc, avl s -> - avl (snd acc) -> avl (snd (partition_acc acc s)). + avl acc#2 -> avl (partition_acc acc s)#2. Proof. induction s; simpl; auto. destruct acc as [acct accf]; simpl in *. @@ -1523,8 +1732,8 @@ 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)). + bst acc#1 -> avl acc#1 -> + bst (partition_acc acc s)#1. Proof. induction s; simpl; auto. destruct acc as [acct accf]; simpl in *. @@ -1538,8 +1747,8 @@ Proof. 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)). + bst acc#2 -> avl acc#2 -> + bst (partition_acc acc s)#2. Proof. induction s; simpl; auto. destruct acc as [acct accf]; simpl in *. @@ -1552,10 +1761,10 @@ Proof. apply partition_acc_avl_2; simpl; auto. Qed. -Lemma partition_acc_in_1 : forall s acc, avl s -> avl (fst acc) -> +Lemma partition_acc_in_1 : forall s acc, avl s -> avl acc#1 -> 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. + In x (partition_acc acc s)#1 <-> + In x acc#1 \/ In x s /\ f x = true. Proof. induction s; simpl; intros. intuition_in. @@ -1576,10 +1785,10 @@ Proof. rewrite H in H9; discriminate. Qed. -Lemma partition_acc_in_2 : forall s acc, avl s -> avl (snd acc) -> +Lemma partition_acc_in_2 : forall s acc, avl s -> avl acc#2 -> 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. + In x (partition_acc acc s)#2 <-> + In x acc#2 \/ In x s /\ f x = false. Proof. induction s; simpl; intros. intuition_in. @@ -1601,31 +1810,31 @@ Proof. intuition. Qed. -Lemma partition_avl_1 : forall s, avl s -> avl (fst (partition s)). +Lemma partition_avl_1 : forall s, avl s -> avl (partition s)#1. Proof. unfold partition; intros; apply partition_acc_avl_1; auto. Qed. -Lemma partition_avl_2 : forall s, avl s -> avl (snd (partition s)). +Lemma partition_avl_2 : forall s, avl s -> avl (partition s)#2. 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)). + bst (partition s)#1. 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)). + bst (partition s)#2. 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. + In x (partition s)#1 <-> In x s /\ f x = true. Proof. unfold partition; intros; rewrite partition_acc_in_1; simpl in *; intuition_in. @@ -1633,13 +1842,15 @@ 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. + In x (partition s)#2 <-> In x s /\ f x = false. Proof. unfold partition; intros; rewrite partition_acc_in_2; simpl in *; intuition_in. Qed. -(** [for_all] and [exists] *) + + +(** * [for_all] and [exists] *) Fixpoint for_all (s:t) : bool := match s with | Leaf => true @@ -1681,8 +1892,8 @@ 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. + apply orb_true_intro; right; apply IHs1; auto; exists x; auto. + apply orb_true_intro; right; apply IHs2; auto; exists x; auto. Qed. Lemma exists_2 : forall s, compat_bool X.eq f -> @@ -1693,12 +1904,14 @@ Proof. 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. + destruct (IHs1 H H2); auto; exists x; intuition. + destruct (IHs2 H H1); auto; exists x; intuition. +Qed. End F. + + (** * Fold *) Module L := FSetList.Raw X. @@ -1749,378 +1962,100 @@ Proof. 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. +(** * Subset *) -(** 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 *) +Function subset (s:t*t) { measure cardinal2 s } : bool := + match s with + | (Leaf, _) => true + | (Node _ _ _ _, Leaf) => false + | (Node l1 x1 r1 h1, Node l2 x2 r2 h2) => + match X.compare x1 x2 with + | EQ _ => subset (l1,l2) && subset (r1,r2) + | LT _ => subset (Node l1 x1 Leaf 0, l2) && subset (r1,s#2) + | GT _ => subset (Node Leaf x1 r1 0, r2) && subset (l1,s#2) + end + end. -Lemma sorted_subset_cardinal : forall l' l : list X.t, - sort X.lt l -> sort X.lt l' -> - (forall x : elt, InA X.eq x l -> InA X.eq x l') -> (length l <= length l')%nat. Proof. - simple induction l'; simpl in |- *; intuition. - destruct l; trivial; intros. - absurd (InA X.eq 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 (InA X.eq 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 (InA X.eq 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 (InA X.eq 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. + intros; unfold cardinal2; simpl; abstract romega with *. + intros; unfold cardinal2; simpl; abstract romega with *. + intros; unfold cardinal2; simpl; abstract romega with *. + intros; unfold cardinal2; simpl; abstract romega with *. + intros; unfold cardinal2; simpl; abstract romega with *. + intros; unfold cardinal2; simpl; abstract romega with *. +Defined. -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. +Lemma subset_12 : forall s, + bst s#1 -> bst s#2 -> + (Subset s#1 s#2 <-> subset s = true). Proof. - intros. - do 2 rewrite cardinal_elements_1. - apply sorted_subset_cardinal; auto. - intros. - generalize (elements_in a x) (elements_in b x). + intros s; functional induction subset s; simpl; + intros B1 B2; try clear e0. intuition. + red; auto; inversion 1. + split; intros; try discriminate. + assert (H': In _x0 Leaf) by auto; inversion H'. + (**) + simpl in *; inv bst. + rewrite andb_true_iff. + rewrite <- IHb; auto; rewrite <- IHb0; auto; clear IHb IHb0. + unfold Subset; intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + assert (X.eq a x2) by order; intuition_in. + (**) + simpl in *; inv bst. + rewrite andb_true_iff. + rewrite <- IHb; auto; rewrite <- IHb0; auto; clear IHb IHb0. + unfold Subset; intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + (**) + simpl in *; inv bst. + rewrite andb_true_iff. + rewrite <- IHb; auto; rewrite <- IHb0; auto; clear IHb IHb0. + unfold Subset; intuition_in. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. + assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. 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 *; elimtype 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. +(* NB: Don't use name eq yet otherwise Function won't work *) -Lemma eq_refl : forall s : t, eq s s. +Lemma eq_refl : forall s : t, Equal s s. Proof. - unfold eq, Equal in |- *; intuition. + unfold Equal; intuition. Qed. -Lemma eq_sym : forall s s' : t, eq s s' -> eq s' s. +Lemma eq_sym : forall s s' : t, Equal s s' -> Equal s' s. Proof. - unfold eq, Equal in |- *; firstorder. + unfold Equal; intros s s' H x; destruct (H x); split; auto. Qed. -Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''. +Lemma eq_trans : forall s s' s'' : t, + Equal s s' -> Equal s' s'' -> Equal s s''. Proof. - unfold eq, Equal in |- *; firstorder. + unfold Equal; intros s s' s'' H1 H2 x; + destruct (H1 x); destruct (H2 x); split; auto. Qed. Lemma eq_L_eq : - forall s s' : t, eq s s' -> L.eq (elements s) (elements s'). + forall s s' : t, Equal 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. + unfold Equal, L.eq, L.Equal; intros; do 2 rewrite elements_in; auto. Qed. Lemma L_eq_eq : - forall s s' : t, L.eq (elements s) (elements s') -> eq s s'. + forall s s' : t, L.eq (elements s) (elements s') -> Equal s s'. Proof. - unfold eq, Equal, L.eq, L.Equal in |- *; intros. - generalize (elements_in s a) (elements_in s' a). - firstorder. + unfold Equal, L.eq, L.Equal; intros; do 2 rewrite <-elements_in; auto. Qed. Hint Resolve eq_L_eq L_eq_eq. @@ -2129,30 +2064,15 @@ 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'. +Lemma lt_not_eq : forall s s' : t, + bst s -> bst s' -> lt s s' -> ~ Equal 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) -*) +(** * A new comparison algorithm suggested by Xavier Leroy *) (** ** Enumeration of the elements of a tree *) @@ -2182,8 +2102,6 @@ Inductive In_e (x:elt) : enumeration -> Prop := 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 : @@ -2196,56 +2114,7 @@ Inductive sorted_e : enumeration -> Prop := 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), - InA X.eq x (l1 ++ l2) -> InA X.eq x l1 \/ InA X.eq 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), InA X.eq 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, sort X.lt l1 -> sort X.lt l2 -> - (forall x y : elt, InA X.eq x l1 -> InA X.eq y l2 -> X.lt x y) -> - sort X.lt (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 -> sort X.lt (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. +Hint Constructors In_e sorted_e. Lemma elements_app : forall (s : tree) (acc : list elt), elements_aux acc s = elements s ++ acc. @@ -2283,92 +2152,46 @@ Qed. (** termination of [compare_aux] *) -Open Local Scope Z_scope. +Open Scope nat_scope. -Fixpoint measure_e_t (s : tree) : Z := match s with +Fixpoint measure_e_t (s : tree) : nat := 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 +Fixpoint measure_e (e : enumeration) : nat := 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. +(** [cons t e] adds the elements of tree [t] on the head of + enumeration [e]. *) -(** Induction principle over the sum of the measures for two lists *) +Fixpoint cons s e {struct s} : enumeration := + match s with + | Leaf => e + | Node l x r h => cons l (More x r e) + end. -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'. +Lemma cons_measure_e : forall s e, + measure_e (cons s e) = measure_e_t s + measure_e e. 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. + induction s; simpl; intros; auto. + rewrite IHs1; simpl; rewrite <- plus_n_Sm; auto with arith. 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 -> +Lemma cons_1 : forall s e, + 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. + sorted_e (cons s e) /\ + flatten_e (cons s e) = elements s ++ flatten_e e. +Proof. + induction s; simpl; auto. + clear IHs2; intros. + inv bst. + destruct (IHs1 (More t s2 e)); clear IHs1; intuition. + inversion_clear H6; subst; auto; order. + rewrite H6. apply flatten_e_elements. Qed. @@ -2383,164 +2206,132 @@ Proof. 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 measure2 e := measure_e e#1 + measure_e e#2. + +Function compare_aux + (e:enumeration*enumeration) { measure measure2 e } : comparison := + match e with + | (End,End) => Eq + | (End,More _ _ _) => Lt + | (More _ _ _, End) => Gt + | (More x1 r1 e1, More x2 r2 e2) => + match X.compare x1 x2 with + | EQ _ => compare_aux (cons r1 e1, cons r2 e2) + | LT _ => Lt + | GT _ => Gt + end + end. -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. +intros; unfold measure2; simpl; +abstract (do 2 rewrite cons_measure_e; romega with *). +Defined. -(** * Equality test *) +Definition compare s1 s2 := compare_aux (cons s1 End, cons s2 End). -Definition equal : forall s s' : t, bst s -> bst s' -> {Equal s s'} + {~ Equal s s'}. +Lemma compare_aux_Eq : forall e, + sorted_e e#1 -> sorted_e e#2 -> + compare_aux e = Eq -> L.eq (flatten_e e#1) (flatten_e e#2). 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. + intros e; functional induction compare_aux e; simpl; intros; auto; + try discriminate. + apply L.eq_refl. + apply l_eq_cons; auto. + inversion H; subst; clear H. + inversion H0; subst; clear H0. + destruct (cons_1 r1 e1); destruct (cons_1 r2 e2); auto. + rewrite <- H0; rewrite <- H3; 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. +Lemma compare_aux_Lt : forall e, + sorted_e e#1 -> sorted_e e#2 -> + compare_aux e = Lt -> L.lt (flatten_e e#1) (flatten_e e#2). +Proof. + intros e; functional induction compare_aux e; simpl; intros; auto; + try discriminate. + apply L.lt_cons_eq; auto. + inversion H; subst; clear H. + inversion H0; subst; clear H0. + destruct (cons_1 r1 e1); destruct (cons_1 r2 e2); auto. + rewrite <- H0; rewrite <- H3; 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. +Lemma compare_aux_Gt : forall e, + sorted_e e#1 -> sorted_e e#2 -> + compare_aux e = Gt -> L.lt (flatten_e e#2) (flatten_e e#1). +Proof. + intros e; functional induction compare_aux e; simpl; intros; auto; + try discriminate. + apply L.lt_cons_eq; auto. + inversion H; subst; clear H. + inversion H0; subst; clear H0. + destruct (cons_1 r1 e1); destruct (cons_1 r2 e2); auto. + rewrite <- H0; rewrite <- H3; 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. +Lemma compare_Eq : forall s1 s2, bst s1 -> bst s2 -> + compare s1 s2 = Eq -> Equal s1 s2. +Proof. + unfold compare; intros. + destruct (cons_1 s1 End) as (S1,E1); auto; try inversion 2. + destruct (cons_1 s2 End) as (S2,E2); auto; try inversion 2. + simpl in *; rewrite <- app_nil_end in *. + apply L_eq_eq; rewrite <-E1, <-E2. + apply (compare_aux_Eq (cons s1 End, cons s2 End)); simpl; 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. +Lemma compare_Lt : forall s1 s2, bst s1 -> bst s2 -> + compare s1 s2 = Lt -> lt s1 s2. +Proof. + unfold compare; intros. + destruct (cons_1 s1 End) as (S1,E1); auto; try inversion 2. + destruct (cons_1 s2 End) as (S2,E2); auto; try inversion 2. + simpl in *; rewrite <- app_nil_end in *. + red; rewrite <- E1, <- E2. + apply (compare_aux_Lt (cons s1 End, cons s2 End)); simpl; auto. 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'). +Lemma compare_Gt : forall s1 s2, bst s1 -> bst s2 -> + compare s1 s2 = Gt -> lt s2 s1. Proof. - unfold union'; intros; destruct (ge_lt_dec (height s) (height s')). - rewrite fold_add_in; intuition. - apply fold_add_in; auto. + unfold compare; intros. + destruct (cons_1 s1 End) as (S1,E1); auto; try inversion 2. + destruct (cons_1 s2 End) as (S2,E2); auto; try inversion 2. + simpl in *; rewrite <- app_nil_end in *. + red; rewrite <- E1, <- E2. + apply (compare_aux_Gt (cons s1 End, cons s2 End)); simpl; auto. Qed. -(** Alternative subset based on diff. *) +Close Scope nat_scope. -Definition subset' s s' := is_empty (diff s s'). +(** * Equality test *) -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. +Definition equal s1 s2 : bool := + match compare s1 s2 with + | Eq => true + | _ => false + end. -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. +Lemma equal_1 : forall s1 s2, bst s1 -> bst s2 -> + Equal s1 s2 -> equal s1 s2 = true. +Proof. +unfold equal; intros s1 s2 B1 B2 E. +generalize (compare_Lt _ _ B1 B2)(compare_Gt _ _ B1 B2). +destruct (compare s1 s2); auto; intros. +elim (lt_not_eq _ _ B1 B2 (H (refl_equal Lt)) E); auto. +elim (lt_not_eq _ _ B2 B1 (H0 (refl_equal Gt)) (eq_sym _ _ E)); auto. 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. +Lemma equal_2 : forall s1 s2, bst s1 -> bst s2 -> + equal s1 s2 = true -> Equal s1 s2. +Proof. +unfold equal; intros s1 s2 B1 B2 E. +generalize (compare_Eq _ _ B1 B2); + destruct compare; auto; discriminate. 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. - Lemma choose_equal: forall s s', bst s -> avl s -> bst s' -> avl s' -> - (equal' s s')=true -> + Equal s s' -> match choose s, choose s' with | Some x, Some x' => X.eq x x' | None, None => True @@ -2548,7 +2339,6 @@ Lemma choose_equal: forall s s', bst s -> avl s -> bst s' -> avl s' -> end. Proof. unfold choose; intros s s' Hb Ha Hb' Ha' H. - generalize (equal'_2 s s' Hb Ha Hb' Ha' H); clear H; intros. generalize (@min_elt_1 s) (@min_elt_2 s) (@min_elt_3 s). generalize (@min_elt_1 s') (@min_elt_2 s') (@min_elt_3 s'). destruct (min_elt s) as [x|]; destruct (min_elt s') as [x'|]; auto. @@ -2569,12 +2359,11 @@ Proof. intros H1 _ _ _ _ H3'. destruct (H3' (refl_equal _) x'). rewrite (H x'); auto. -Qed. +Qed. End Raw. -Set Implicit Arguments. -Unset Strict Implicit. + (** * Encapsulation @@ -2602,21 +2391,25 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Definition mem (x:elt)(s:t) : bool := Raw.mem x s. - Definition empty : t := Bbst Raw.empty_bst Raw.empty_avl. + Definition empty : t := Bbst _ Raw.empty_bst Raw.empty_avl. Definition is_empty (s:t) : bool := Raw.is_empty s. - Definition singleton (x:elt) : t := Bbst (Raw.singleton_bst x) (Raw.singleton_avl x). + Definition singleton (x:elt) : t := Bbst _ (Raw.singleton_bst x) (Raw.singleton_avl x). Definition add (x:elt)(s:t) : t := - Bbst (Raw.add_bst s x (is_bst s) (is_avl s)) - (Raw.add_avl s x (is_avl s)). + Bbst _ (Raw.add_bst s x (is_bst s) (is_avl s)) + (Raw.add_avl s x (is_avl s)). Definition remove (x:elt)(s:t) : t := - Bbst (Raw.remove_bst s x (is_bst s) (is_avl s)) - (Raw.remove_avl s x (is_avl s)). + Bbst _ (Raw.remove_bst s x (is_bst s) (is_avl s)) + (Raw.remove_avl s x (is_avl s)). Definition inter (s s':t) : t := - Bbst (Raw.inter_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (Raw.inter_avl _ _ (is_avl s) (is_avl s')). + Bbst _ (Raw.inter_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + (Raw.inter_avl _ _ (is_avl s) (is_avl s')). + Definition union (s s':t) : t := + let (s,b,a) := s in let (s',b',a') := s' in + Bbst _ (Raw.union_bst (s,s') b a b' a') + (Raw.union_avl (s,s') a a'). Definition diff (s s':t) : t := - Bbst (Raw.diff_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (Raw.diff_avl _ _ (is_avl s) (is_avl s')). + Bbst _ (Raw.diff_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) + (Raw.diff_avl _ _ (is_avl s) (is_avl s')). Definition elements (s:t) : list elt := Raw.elements s. Definition min_elt (s:t) : option elt := Raw.min_elt s. Definition max_elt (s:t) : option elt := Raw.max_elt s. @@ -2624,41 +2417,29 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s. Definition cardinal (s:t) : nat := Raw.cardinal s. Definition filter (f : elt -> bool) (s:t) : t := - Bbst (Raw.filter_bst f _ (is_bst s) (is_avl s)) - (Raw.filter_avl f _ (is_avl s)). + Bbst _ (Raw.filter_bst f _ (is_bst s) (is_avl s)) + (Raw.filter_avl f _ (is_avl s)). Definition for_all (f : elt -> bool) (s:t) : bool := Raw.for_all f s. Definition exists_ (f : elt -> bool) (s:t) : bool := Raw.exists_ f s. Definition partition (f : elt -> bool) (s:t) : t * t := let p := Raw.partition f s in - (Bbst (Raw.partition_bst_1 f _ (is_bst s) (is_avl s)) - (Raw.partition_avl_1 f _ (is_avl s)), - Bbst (Raw.partition_bst_2 f _ (is_bst s) (is_avl s)) - (Raw.partition_avl_2 f _ (is_avl s))). + (Bbst (fst p) (Raw.partition_bst_1 f _ (is_bst s) (is_avl s)) + (Raw.partition_avl_1 f _ (is_avl s)), + Bbst (snd p) (Raw.partition_bst_2 f _ (is_bst s) (is_avl s)) + (Raw.partition_avl_2 f _ (is_avl s))). - Definition union (s s':t) : t := - let (u,p) := Raw.union _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s') in - let (b,p) := p in - let (a,_) := p in - Bbst b a. + Definition equal (s s':t) : bool := Raw.equal s s'. + Definition subset (s s':t) : bool := Raw.subset (s.(this),s'.(this)). - Definition union' (s s' : t) : t := - Bbst (Raw.union'_bst _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (Raw.union'_avl _ _ (is_avl s) (is_avl s')). - - Definition equal (s s': t) : bool := if Raw.equal _ _ (is_bst s) (is_bst s') then true else false. - Definition equal' (s s':t) : bool := Raw.equal' s s'. - - Definition subset (s s':t) : bool := if Raw.subset _ _ (is_bst s) (is_bst s') then true else false. - Definition subset' (s s':t) : bool := Raw.subset' s s'. - - Definition eq (s s':t) : Prop := Raw.eq s s'. + Definition eq (s s':t) : Prop := Raw.Equal s s'. Definition lt (s s':t) : Prop := Raw.lt s s'. - Definition compare (s s':t) : Compare lt eq s s'. - Proof. - intros; elim (Raw.compare _ _ (is_bst s) (is_bst s')); - [ constructor 1 | constructor 2 | constructor 3 ]; - auto. + Definition compare (s s':t) : Compare lt eq s s'. + Proof. + intros (s,b,a) (s',b',a'). + generalize (Raw.compare_Eq _ _ b b') (Raw.compare_Lt _ _ b b') + (Raw.compare_Gt _ _ b b'). + destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto. Defined. (* specs *) @@ -2674,35 +2455,20 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Proof. exact (Raw.mem_2 s x). Qed. Lemma equal_1 : Equal s s' -> equal s s' = true. - Proof. - unfold equal; destruct (Raw.equal s s'); simpl; auto. - Qed. - + Proof. exact (Raw.equal_1 s s' (is_bst s) (is_bst s')). Qed. Lemma equal_2 : equal s s' = true -> Equal s s'. - Proof. - unfold equal; destruct (Raw.equal s s'); simpl; intuition; discriminate. - Qed. - - Lemma equal'_1 : Equal s s' -> equal' s s' = true. - Proof. exact (Raw.equal'_1 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')). Qed. - Lemma equal'_2 : equal' s s' = true -> Equal s s'. - Proof. exact (Raw.equal'_2 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')). Qed. + Proof. exact (Raw.equal_2 s s' (is_bst s) (is_bst s')). Qed. Lemma subset_1 : Subset s s' -> subset s s' = true. Proof. - unfold subset; destruct (Raw.subset s s'); simpl; intuition. + unfold subset; rewrite <- Raw.subset_12; simpl; auto. Qed. Lemma subset_2 : subset s s' = true -> Subset s s'. Proof. - unfold subset; destruct (Raw.subset s s'); simpl; intuition discriminate. + unfold subset; rewrite <- Raw.subset_12; simpl; auto. Qed. - Lemma subset'_1 : Subset s s' -> subset' s s' = true. - Proof. exact (Raw.subset'_1 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')). Qed. - Lemma subset'_2 : subset' s s' = true -> Subset s s'. - Proof. exact (Raw.subset'_2 _ _ (is_bst s) (is_avl s) (is_bst s') (is_avl s')). Qed. - Lemma empty_1 : Empty empty. Proof. exact Raw.empty_1. Qed. @@ -2750,40 +2516,19 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. 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. + destruct s; destruct s'; simpl; rewrite Raw.union_in; simpl; 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. + destruct s; destruct s'; simpl; rewrite Raw.union_in; simpl; 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 Raw.union'_in; intuition. - Qed. - - Lemma union'_2 : In x s -> In x (union' s s'). - Proof. - unfold union', In; simpl; rewrite Raw.union'_in; intuition. - Qed. - - Lemma union'_3 : In x s' -> In x (union' s s'). - Proof. - unfold union', In; simpl; rewrite Raw.union'_in; intuition. + destruct s; destruct s'; simpl; rewrite Raw.union_in; simpl; auto. Qed. Lemma inter_1 : In x (inter s s') -> In x s. @@ -2817,14 +2562,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Qed. Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A), - fold f s i = fold_left (fun a e => f e a) (elements s) i. + fold A f s i = fold_left (fun a e => f e a) (elements s) i. Proof. unfold fold, elements; intros; apply Raw.fold_1; auto. Qed. Lemma cardinal_1 : cardinal s = length (elements s). Proof. - unfold cardinal, elements; intros; apply Raw.cardinal_elements_1; auto. + unfold cardinal, elements; intros; apply Raw.elements_cardinal; auto. Qed. Section Filter. @@ -2922,7 +2667,6 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. intros. unfold choose. apply Raw.choose_equal; auto. - apply Raw.equal'_1; auto. exact (equal_2 H). Qed. -- cgit v1.2.3