diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-20 11:49:19 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-20 11:49:19 +0000 |
| commit | efc09aa417b49315aa9e1fea1a13987241d3752a (patch) | |
| tree | 83a259efb5c67b94dd46af9b64546377f2975a91 /theories/FSets | |
| parent | b2f8c34af642840ea80f14986cac285af1900767 (diff) | |
FSetCompat: a compatibility wrapper between FSets and MSets
Thanks to the functors in FSetCompat, the three implementations
of FSets (FSetWeakList, FSetList, FSetAVL) are just made of a few
lines adapting the corresponding MSets implementation to the old
interface.
This approach breaks FSetFullAVL. Since this file is of little use
for stdlib users, we migrate it into contrib Orsay/FSets.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12402 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FSetAVL.v | 2017 | ||||
| -rw-r--r-- | theories/FSets/FSetCompat.v | 413 | ||||
| -rw-r--r-- | theories/FSets/FSetFullAVL.v | 1126 | ||||
| -rw-r--r-- | theories/FSets/FSetList.v | 1259 | ||||
| -rw-r--r-- | theories/FSets/FSetWeakList.v | 941 |
5 files changed, 433 insertions, 5323 deletions
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 08071ec56..e2953f333 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -33,2023 +33,20 @@ code after extraction. *) -Require Import FSetInterface FSetList ZArith Int. +Require Import FSetInterface ZArith Int. Set Implicit Arguments. Unset Strict Implicit. -(** Notations and helper lemma about pairs *) +(** This is just a compatibility layer, the real implementation + is now in [MSetAVL] *) -Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. -Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. - -(** * Raw - - Functor of pure functions + a posteriori proofs of invariant - preservation *) - -Module Raw (Import I:Int)(X:OrderedType). -Open Local Scope pair_scope. -Open Local Scope lazy_bool_scope. -Open Local Scope Int_scope. - -Definition elt := X.t. - -(** * Trees - - The fourth field of [Node] is the height of the tree *) - -Inductive tree := - | Leaf : tree - | Node : tree -> X.t -> tree -> int -> tree. - -Notation t := 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. - -(** * Empty Set *) - -Definition empty := Leaf. - -(** * Emptyness test *) - -Definition is_empty s := - match s with Leaf => true | _ => false end. - -(** * Appartness *) - -(** The [mem] function is deciding appartness. It exploits the - binary search tree invariant to achieve logarithmic complexity. *) - -Fixpoint mem x s := - 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. - -(** * Singleton set *) - -Definition singleton x := Node Leaf x Leaf 1. - -(** * 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). - -(** [bal l x r] acts as [create], but performs one step of - rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *) - -Definition assert_false := create. - -Definition bal l x r := - let hl := height l in - let hr := height r in - if gt_le_dec hl (hr+2) then - match l with - | Leaf => assert_false l x r - | 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 l x r - | 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 l x r - | 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 l x r - | Node rll rlx rlr _ => - create (create l x rll) rlx (create rlr rx rr) - end - end - else - create l x r. - -(** * Insertion *) - -Fixpoint add x s := 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. - -(** * Join - - Same as [bal] but does not assume anything regarding heights - of [l] and [r]. -*) - -Fixpoint join l : 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. - -(** * 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 x r : 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. - -(** * 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. - -(** * Deletion *) - -Fixpoint remove x s := 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. - -(** * Minimum element *) - -Fixpoint min_elt s := match s with - | Leaf => None - | Node Leaf y _ _ => Some y - | Node l _ _ _ => min_elt l -end. - -(** * Maximum element *) - -Fixpoint max_elt s := match s with - | Leaf => None - | Node _ y Leaf _ => Some y - | Node _ _ r _ => max_elt r -end. - -(** * Any element *) - -Definition choose := min_elt. - -(** * 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 _ => - let (s2',m) := remove_min l2 x2 r2 in - join s1 m s2' - end. - -(** * 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]. -*) - -Record triple := mktriple { t_left:t; t_in:bool; t_right:t }. -Notation "<< l , b , r >>" := (mktriple l b r) (at level 9). -Notation "t #l" := (t_left t) (at level 9, format "t '#l'"). -Notation "t #b" := (t_in t) (at level 9, format "t '#b'"). -Notation "t #r" := (t_right t) (at level 9, format "t '#r'"). - -Fixpoint split x s : triple := match s with - | Leaf => << Leaf, false, Leaf >> - | Node l y r h => - match X.compare x y with - | LT _ => let (ll,b,rl) := split x l in << ll, b, join rl y r >> - | EQ _ => << l, true, r >> - | GT _ => let (rl,b,rr) := split x r in << join l y rl, b, rr >> - end - end. - -(** * Intersection *) - -Fixpoint inter s1 s2 := match s1, s2 with - | Leaf, _ => Leaf - | _, Leaf => Leaf - | Node l1 x1 r1 h1, _ => - let (l2',pres,r2') := split x1 s2 in - if pres then join (inter l1 l2') x1 (inter r1 r2') - else concat (inter l1 l2') (inter r1 r2') - end. - -(** * Difference *) - -Fixpoint diff s1 s2 := match s1, s2 with - | Leaf, _ => Leaf - | _, Leaf => s1 - | Node l1 x1 r1 h1, _ => - let (l2',pres,r2') := split x1 s2 in - if pres then concat (diff l1 l2') (diff r1 r2') - else join (diff l1 l2') x1 (diff r1 r2') -end. - -(** * Union *) - -(** In ocaml, heights of [s1] and [s2] are compared each time in order - to recursively perform the split on the smaller set. - Unfortunately, this leads to a non-structural algorithm. The - following code is a simplification of the ocaml version: no - comparison of heights. It might be slightly slower, but - experimentally all the tests I've made in ocaml have shown this - potential slowdown to be non-significant. Anyway, the exact code - of ocaml has also been formalized thanks to Function+measure, see - [ocaml_union] in [FSetFullAVL]. -*) - -Fixpoint union s1 s2 := - match s1, s2 with - | Leaf, _ => s2 - | _, Leaf => s1 - | Node l1 x1 r1 h1, _ => - let (l2',_,r2') := split x1 s2 in - join (union l1 l2') x1 (union r1 r2') - end. - -(** * 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) : 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. - -(** * Filter *) - -Fixpoint filter_acc (f:elt->bool) acc s := match s with - | Leaf => acc - | Node l x r h => - filter_acc f (filter_acc f (if f x then add x acc else acc) l) r - end. - -Definition filter f := filter_acc f Leaf. - - -(** * Partition *) - -Fixpoint partition_acc (f:elt->bool)(acc : t*t)(s : t) : t*t := - match s with - | Leaf => acc - | Node l x r _ => - let (acct,accf) := acc in - partition_acc f - (partition_acc f - (if f x then (add x acct, accf) else (acct, add x accf)) l) r - end. - -Definition partition f := partition_acc f (Leaf,Leaf). - -(** * [for_all] and [exists] *) - -Fixpoint for_all (f:elt->bool) s := match s with - | Leaf => true - | Node l x r _ => f x &&& for_all f l &&& for_all f r -end. - -Fixpoint exists_ (f:elt->bool) s := match s with - | Leaf => false - | Node l x r _ => f x ||| exists_ f l ||| exists_ f r -end. - -(** * Fold *) - -Fixpoint fold (A : Type) (f : elt -> A -> A)(s : tree) : A -> A := - fun a => match s with - | Leaf => a - | Node l x r _ => fold f r (f x (fold f l a)) - end. -Implicit Arguments fold [A]. - - -(** * Subset *) - -(** In ocaml, recursive calls are made on "half-trees" such as - (Node l1 x1 Leaf _) and (Node Leaf x1 r1 _). Instead of these - non-structural calls, we propose here two specialized functions for - these situations. This version should be almost as efficient as - the one of ocaml (closures as arguments may slow things a bit), - it is simply less compact. The exact ocaml version has also been - formalized (thanks to Function+measure), see [ocaml_subset] in - [FSetFullAVL]. - *) - -Fixpoint subsetl (subset_l1:t->bool) x1 s2 : bool := - match s2 with - | Leaf => false - | Node l2 x2 r2 h2 => - match X.compare x1 x2 with - | EQ _ => subset_l1 l2 - | LT _ => subsetl subset_l1 x1 l2 - | GT _ => mem x1 r2 &&& subset_l1 s2 - end - end. - -Fixpoint subsetr (subset_r1:t->bool) x1 s2 : bool := - match s2 with - | Leaf => false - | Node l2 x2 r2 h2 => - match X.compare x1 x2 with - | EQ _ => subset_r1 r2 - | LT _ => mem x1 l2 &&& subset_r1 s2 - | GT _ => subsetr subset_r1 x1 r2 - end - end. - -Fixpoint subset s1 s2 : bool := match s1, s2 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 _ => subsetl (subset l1) x1 l2 &&& subset r1 s2 - | GT _ => subsetr (subset r1) x1 r2 &&& subset l1 s2 - end - end. - -(** * A new comparison algorithm suggested by Xavier Leroy - - Transformation in C.P.S. suggested by Benjamin Grégoire. - The original ocaml code (with non-structural recursive calls) - has also been formalized (thanks to Function+measure), see - [ocaml_compare] in [FSetFullAVL]. The following code with - continuations computes dramatically faster in Coq, and - should be almost as efficient after extraction. -*) - -(** Enumeration of the elements of a tree *) - -Inductive enumeration := - | End : enumeration - | More : elt -> tree -> enumeration -> enumeration. - - -(** [cons t e] adds the elements of tree [t] on the head of - enumeration [e]. *) - -Fixpoint cons s e : enumeration := - match s with - | Leaf => e - | Node l x r h => cons l (More x r e) - end. - -(** One step of comparison of elements *) - -Definition compare_more x1 (cont:enumeration->comparison) e2 := - match e2 with - | End => Gt - | More x2 r2 e2 => - match X.compare x1 x2 with - | EQ _ => cont (cons r2 e2) - | LT _ => Lt - | GT _ => Gt - end - end. - -(** Comparison of left tree, middle element, then right tree *) - -Fixpoint compare_cont s1 (cont:enumeration->comparison) e2 := - match s1 with - | Leaf => cont e2 - | Node l1 x1 r1 _ => - compare_cont l1 (compare_more x1 (compare_cont r1 cont)) e2 - end. - -(** Initial continuation *) - -Definition compare_end e2 := - match e2 with End => Eq | _ => Lt end. - -(** The complete comparison *) - -Definition compare s1 s2 := compare_cont s1 compare_end (cons s2 End). - -(** * Equality test *) - -Definition equal s1 s2 : bool := - match compare s1 s2 with - | Eq => true - | _ => false - end. - - - - -(** * Invariants *) - -(** ** 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). - - - - -(** * 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. - - - -(** * Correctness proofs, isolated in a sub-module *) - -Module Proofs. - Module MX := OrderedTypeFacts X. - Module L := FSetList.Raw X. - -(** * Automation and dedicated tactics *) - -Hint Constructors In bst. -Hint Unfold lt_tree gt_tree. - -Tactic Notation "factornode" ident(l) ident(x) ident(r) ident(h) - "as" ident(s) := - set (s:=Node l x r h) in *; clearbody s; clear l x r h. - -(** 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. - -Ltac intuition_in := repeat progress (intuition; inv In). - -(** Helper tactic concerning order of elements. *) - -Ltac order := match goal with - | U: lt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order - | U: gt_tree _ ?s, V: In _ ?s |- _ => generalize (U _ V); clear U; order - | _ => MX.order -end. - - -(** * Basic results about [In], [lt_tree], [gt_tree], [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. - -Lemma In_node_iff : - forall l x r h y, - In y (Node l x r h) <-> In y l \/ X.eq y x \/ In y r. -Proof. - intuition_in. -Qed. - -(** Results about [lt_tree] and [gt_tree] *) - -Lemma lt_leaf : forall x : elt, lt_tree x Leaf. -Proof. - red; inversion 1. -Qed. - -Lemma gt_leaf : forall x : elt, gt_tree x Leaf. -Proof. - 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; 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; 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. - 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. - eauto. -Qed. - -Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans. - -(** * Inductions principles *) - -Functional Scheme mem_ind := Induction for mem Sort Prop. -Functional Scheme bal_ind := Induction for bal Sort Prop. -Functional Scheme add_ind := Induction for add Sort Prop. -Functional Scheme remove_min_ind := Induction for remove_min Sort Prop. -Functional Scheme merge_ind := Induction for merge Sort Prop. -Functional Scheme remove_ind := Induction for remove Sort Prop. -Functional Scheme min_elt_ind := Induction for min_elt Sort Prop. -Functional Scheme max_elt_ind := Induction for max_elt Sort Prop. -Functional Scheme concat_ind := Induction for concat Sort Prop. -Functional Scheme split_ind := Induction for split Sort Prop. -Functional Scheme inter_ind := Induction for inter Sort Prop. -Functional Scheme diff_ind := Induction for diff Sort Prop. -Functional Scheme union_ind := Induction for union Sort Prop. - - -(** * Empty set *) - -Lemma empty_1 : Empty empty. -Proof. - intro; intro. - inversion H. -Qed. - -Lemma empty_bst : bst empty. -Proof. - auto. -Qed. - -(** * Emptyness test *) - -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 *) - -Lemma mem_1 : forall s x, bst s -> In x s -> mem x s = true. -Proof. - intros s x; functional induction mem x s; auto; intros; try clear e0; - 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; discriminate. -Qed. - - - -(** * Singleton set *) - -Lemma singleton_1 : forall x y, In y (singleton x) -> X.eq x y. -Proof. - unfold singleton; intros; inv In; order. -Qed. - -Lemma singleton_2 : forall x y, X.eq x y -> In y (singleton x). -Proof. - unfold singleton; auto. -Qed. - -Lemma singleton_bst : forall x : elt, bst (singleton x). -Proof. - unfold singleton; auto. -Qed. - - - -(** * Helper functions *) - -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. - -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 bal_in : forall l x r y, - In y (bal l x r) <-> X.eq y x \/ In y l \/ In y r. -Proof. - intros l x r; functional induction bal l x r; intros; try clear e0; - rewrite !create_in; intuition_in. -Qed. - -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; 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. -Hint Resolve bal_bst. - - - -(** * Insertion *) - -Lemma add_in : forall s x y, - In y (add x s) <-> X.eq y x \/ In y s. -Proof. - intros s x; functional induction (add x s); auto; intros; - try rewrite bal_in, IHt; intuition_in. - eapply In_1; eauto. -Qed. - -Lemma add_bst : forall s x, bst s -> bst (add x s). -Proof. - intros s x; functional induction (add x s); auto; intros; - inv bst; apply bal_bst; auto. - (* lt_tree -> lt_tree (add ...) *) - red; red in H3. - intros. - rewrite add_in in H. - intuition. - eauto. - inv bst; auto using bal_bst. - (* gt_tree -> gt_tree (add ...) *) - red; red in H3. - intros. - rewrite add_in in H. - intuition. - apply MX.lt_eq with x; auto. -Qed. -Hint Resolve add_bst. - - - -(** * Join *) - -(* Function/Functional Scheme can't deal with internal fix. - Let's do its job by hand: *) - -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_in : forall l x r y, - 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. - rewrite bal_in, Hlr; clear Hlr Hrl; intuition_in. - rewrite bal_in, Hrl; clear Hlr Hrl; intuition_in. - apply create_in. -Qed. - -Lemma join_bst : forall l x r, bst l -> bst r -> - lt_tree x l -> gt_tree x r -> bst (join l x r). -Proof. - join_tac; auto; inv bst; apply bal_bst; auto; - clear Hrl Hlr z; intro; intros; rewrite join_in in *. - intuition; [ apply MX.lt_eq with x | ]; eauto. - intuition; [ apply MX.eq_lt with x | ]; eauto. -Qed. -Hint Resolve join_bst. - - - -(** * Extraction of minimum element *) - -Lemma remove_min_in : forall l x r h y, - In y (Node l x r h) <-> - 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. - rewrite bal_in, In_node_iff, IHp, e0; simpl; intuition. -Qed. - -Lemma remove_min_bst : forall l x r h, - bst (Node l x r h) -> bst (remove_min l x r)#1. -Proof. - intros l x r; functional induction (remove_min l x r); simpl; intros. - inv bst; auto. - inversion_clear H. - specialize IHp with (1:=H0); rewrite e0 in IHp; auto. - apply bal_bst; auto. - intro y; specialize (H2 y). - rewrite remove_min_in, e0 in H2; simpl in H2; intuition. -Qed. - -Lemma remove_min_gt_tree : forall l x r h, - bst (Node l x r h) -> - 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); simpl; intros. - inv bst; auto. - inversion_clear H. - specialize IHp with (1:=H0); rewrite e0 in IHp; simpl in IHp. - intro y; rewrite bal_in; intuition; - specialize (H2 m); rewrite remove_min_in, e0 in H2; simpl in H2; - [ apply MX.lt_eq with x | ]; eauto. -Qed. -Hint Resolve remove_min_bst remove_min_gt_tree. - - - -(** * Merging two trees *) - -Lemma merge_in : forall s1 s2 y, - In y (merge s1 s2) <-> In y s1 \/ In y s2. -Proof. - intros s1 s2; functional induction (merge s1 s2); intros; - try factornode _x _x0 _x1 _x2 as s1. - intuition_in. - intuition_in. - rewrite bal_in, remove_min_in, e1; simpl; intuition. -Qed. - -Lemma merge_bst : forall s1 s2, bst s1 -> bst 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); intros; auto; - try factornode _x _x0 _x1 _x2 as s1. - apply bal_bst; auto. - change s2' with ((s2',m)#1); rewrite <-e1; eauto. - intros y Hy. - apply H1; auto. - rewrite remove_min_in, e1; simpl; auto. - change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto. -Qed. -Hint Resolve merge_bst. - - - -(** * Deletion *) - -Lemma remove_in : forall s x y, bst s -> - (In y (remove x s) <-> ~ X.eq y x /\ In y s). -Proof. - intros s x; functional induction (remove x s); intros; inv bst. - intuition_in. - rewrite bal_in, IHt; clear e0 IHt; intuition; [order|order|intuition_in]. - rewrite merge_in; clear e0; intuition; [order|order|intuition_in]. - elim H4; eauto. - rewrite bal_in, IHt; clear e0 IHt; intuition; [order|order|intuition_in]. -Qed. - -Lemma remove_bst : forall s x, bst s -> bst (remove x s). -Proof. - intros s x; functional induction (remove x s); intros; inv bst. - auto. - (* LT *) - apply bal_bst; auto. - intro z; rewrite remove_in; auto; destruct 1; eauto. - (* EQ *) - eauto. - (* GT *) - apply bal_bst; auto. - intro z; rewrite remove_in; auto; destruct 1; eauto. -Qed. -Hint Resolve remove_bst. - - -(** * Minimum element *) - -Lemma min_elt_1 : forall s x, min_elt s = Some x -> In x s. -Proof. - intro s; functional induction (min_elt s); auto; inversion 1; 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); - try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1. - inversion_clear 2. - inversion_clear 1. - inversion 1; subst. - inversion_clear 1; auto. - inversion_clear H5. - inversion_clear 1. - simpl. - destruct l1. - inversion 1; subst. - assert (X.lt x y) by (apply H2; auto). - inversion_clear 1; auto; order. - assert (X.lt x1 y) by auto. - inversion_clear 2; auto; - (assert (~ X.lt x1 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). - red; red; inversion 2. - inversion 1. - intro H0. - destruct (IHo H0 _x2); auto. -Qed. - - - -(** * Maximum element *) - -Lemma max_elt_1 : forall s x, max_elt s = Some x -> In x s. -Proof. - intro s; functional induction (max_elt s); auto; inversion 1; 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); - try rename _x1 into l1, _x2 into x1, _x3 into r1, _x4 into h1. - inversion_clear 2. - inversion_clear 1. - inversion 1; subst. - inversion_clear 1; auto. - inversion_clear H5. - inversion_clear 1. - assert (X.lt y x1) by auto. - inversion_clear 2; auto; - (assert (~ X.lt x x1) by auto); order. -Qed. - -Lemma max_elt_3 : forall s, max_elt s = None -> Empty s. -Proof. - intro s; functional induction (max_elt s). - red; auto. - inversion 1. - intros H0; destruct (IHo H0 _x2); auto. -Qed. - - - -(** * Any element *) - -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. - -Lemma choose_3 : forall s s', bst s -> bst s' -> - forall x x', choose s = Some x -> choose s' = Some x' -> - Equal s s' -> X.eq x x'. -Proof. - unfold choose, Equal; intros s s' Hb Hb' x x' Hx Hx' H. - assert (~X.lt x x'). - apply min_elt_2 with s'; auto. - rewrite <-H; auto using min_elt_1. - assert (~X.lt x' x). - apply min_elt_2 with s; auto. - rewrite H; auto using min_elt_1. - destruct (X.compare x x'); intuition. -Qed. - - -(** * Concatenation *) - -Lemma concat_in : forall s1 s2 y, - In y (concat s1 s2) <-> In y s1 \/ In y s2. -Proof. - intros s1 s2; functional induction (concat s1 s2); intros; - try factornode _x _x0 _x1 _x2 as s1. - intuition_in. - intuition_in. - rewrite join_in, remove_min_in, e1; simpl; intuition. -Qed. - -Lemma concat_bst : forall s1 s2, bst s1 -> bst 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); intros; auto; - try factornode _x _x0 _x1 _x2 as s1. - apply join_bst; auto. - change (bst (s2',m)#1); rewrite <-e1; eauto. - intros y Hy. - apply H1; auto. - rewrite remove_min_in, e1; simpl; auto. - change (gt_tree (s2',m)#2 (s2',m)#1); rewrite <-e1; eauto. -Qed. -Hint Resolve concat_bst. - - -(** * Splitting *) - -Lemma split_in_1 : forall s x y, bst s -> - (In y (split x s)#l <-> In y s /\ X.lt y x). -Proof. - intros s x; functional induction (split x s); simpl; intros; - inv bst; try clear e0. - intuition_in. - rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. - intuition_in; order. - rewrite join_in. - rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. -Qed. - -Lemma split_in_2 : forall s x y, bst s -> - (In y (split x s)#r <-> In y s /\ X.lt x y). -Proof. - intros s x; functional induction (split x s); subst; simpl; intros; - inv bst; try clear e0. - intuition_in. - rewrite join_in. - rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. - intuition_in; order. - rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. -Qed. - -Lemma split_in_3 : forall s x, bst s -> - ((split x s)#b = true <-> In x s). -Proof. - intros s x; functional induction (split x s); subst; simpl; intros; - inv bst; try clear e0. - intuition_in; try discriminate. - rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. - intuition. - rewrite e1 in IHt; simpl in IHt; rewrite IHt; intuition_in; order. -Qed. - -Lemma split_bst : forall s x, bst s -> - bst (split x s)#l /\ bst (split x s)#r. -Proof. - intros s x; functional induction (split x s); subst; simpl; intros; - inv bst; try clear e0; try rewrite e1 in *; simpl in *; intuition; - apply join_bst; auto. - intros y0. - generalize (split_in_2 x y0 H0); rewrite e1; simpl; intuition. - intros y0. - generalize (split_in_1 x y0 H1); rewrite e1; simpl; intuition. -Qed. - - - -(** * Intersection *) - -Lemma inter_bst_in : forall s1 s2, bst s1 -> bst s2 -> - bst (inter s1 s2) /\ (forall y, In y (inter s1 s2) <-> In y s1 /\ In y s2). -Proof. - intros s1 s2; functional induction inter s1 s2; intros B1 B2; - [intuition_in|intuition_in | | ]; - factornode _x0 _x1 _x2 _x3 as s2; - generalize (split_bst x1 B2); - rewrite e1; simpl; destruct 1; inv bst; - destruct IHt as (IHb1,IHi1); auto; - destruct IHt0 as (IHb2,IHi2); auto; - generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1) - (split_in_3 x1 B2)(split_bst x1 B2); - rewrite e1; simpl; split; intros. - (* bst join *) - apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *) - rewrite join_in, IHi1, IHi2, H5, H6; intuition_in. - apply In_1 with x1; auto. - (* bst concat *) - apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. - (* In concat *) - rewrite concat_in, IHi1, IHi2, H5, H6; auto. - assert (~In x1 s2) by (rewrite <- H7; auto). - intuition_in. - elim H9. - apply In_1 with y; auto. -Qed. - -Lemma inter_in : forall s1 s2 y, bst s1 -> bst s2 -> - (In y (inter s1 s2) <-> In y s1 /\ In y s2). -Proof. - intros s1 s2 y B1 B2; destruct (inter_bst_in B1 B2); auto. -Qed. - -Lemma inter_bst : forall s1 s2, bst s1 -> bst s2 -> bst (inter s1 s2). -Proof. - intros s1 s2 B1 B2; destruct (inter_bst_in B1 B2); auto. -Qed. - - -(** * Difference *) - -Lemma diff_bst_in : forall s1 s2, bst s1 -> bst s2 -> - bst (diff s1 s2) /\ (forall y, In y (diff s1 s2) <-> In y s1 /\ ~In y s2). -Proof. - intros s1 s2; functional induction diff s1 s2; intros B1 B2; - [intuition_in|intuition_in | | ]; - factornode _x0 _x1 _x2 _x3 as s2; - generalize (split_bst x1 B2); - rewrite e1; simpl; destruct 1; - inv avl; inv bst; - destruct IHt as (IHb1,IHi1); auto; - destruct IHt0 as (IHb2,IHi2); auto; - generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1) - (split_in_3 x1 B2)(split_bst x1 B2); - rewrite e1; simpl; split; intros. - (* bst concat *) - apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order. - (* In concat *) - rewrite concat_in, IHi1, IHi2, H5, H6; intuition_in. - elim H13. - apply In_1 with x1; auto. - (* bst join *) - apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition. (* In join *) - rewrite join_in, IHi1, IHi2, H5, H6; auto. - assert (~In x1 s2) by (rewrite <- H7; auto). - intuition_in. - elim H9. - apply In_1 with y; auto. -Qed. - -Lemma diff_in : forall s1 s2 y, bst s1 -> bst s2 -> - (In y (diff s1 s2) <-> In y s1 /\ ~In y s2). -Proof. - intros s1 s2 y B1 B2; destruct (diff_bst_in B1 B2); auto. -Qed. - -Lemma diff_bst : forall s1 s2, bst s1 -> bst s2 -> bst (diff s1 s2). -Proof. - intros s1 s2 B1 B2; destruct (diff_bst_in B1 B2); auto. -Qed. - - -(** * Union *) - -Lemma union_in : forall s1 s2 y, bst s1 -> bst s2 -> - (In y (union s1 s2) <-> In y s1 \/ In y s2). -Proof. - intros s1 s2; functional induction union s1 s2; intros y B1 B2. - intuition_in. - intuition_in. - factornode _x0 _x1 _x2 _x3 as s2. - generalize (split_in_1 x1 y B2)(split_in_2 x1 y B2)(split_bst x1 B2). - rewrite e1; simpl. - destruct 3; inv bst. - rewrite join_in, IHt, IHt0, H, H0; auto. - case (X.compare y x1); intuition_in. -Qed. - -Lemma union_bst : forall s1 s2, bst s1 -> bst s2 -> - bst (union s1 s2). -Proof. - intros s1 s2; functional induction union s1 s2; intros B1 B2; auto. - factornode _x0 _x1 _x2 _x3 as s2. - generalize (@split_in_1 s2 x1)(@split_in_2 s2 x1)(split_bst x1 B2). - rewrite e1; simpl; destruct 3. - inv bst. - apply join_bst; auto. - intro y; rewrite union_in, H; intuition_in. - intro y; rewrite union_in, H0; intuition_in. -Qed. - - -(** * Elements *) - -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. - -Lemma elements_nodup : forall s : tree, bst s -> NoDupA X.eq (elements s). -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. - -Lemma elements_app : - forall s acc, elements_aux acc s = elements s ++ acc. -Proof. - induction s; simpl; intros; auto. - rewrite IHs1, IHs2. - unfold elements; simpl. - rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto. -Qed. - -Lemma elements_node : - forall l x r h acc, - elements l ++ x :: elements r ++ acc = - elements (Node l x r h) ++ acc. -Proof. - unfold elements; simpl; intros; auto. - rewrite !elements_app, <- !app_nil_end, !app_ass; auto. -Qed. - - -(** * Filter *) - -Section F. -Variable f : elt -> bool. - -Lemma filter_acc_in : forall s acc, - compat_bool X.eq f -> forall x : elt, - In x (filter_acc f acc s) <-> In x acc \/ In x s /\ f x = true. -Proof. - induction s; simpl; intros. - intuition_in. - rewrite IHs2, IHs1 by (destruct (f t); auto). - case_eq (f t); intros. - rewrite (add_in); auto. - intuition_in. - rewrite (H _ _ H2). - intuition. - intuition_in. - rewrite (H _ _ H2) in H3. - rewrite H0 in H3; discriminate. -Qed. - -Lemma filter_acc_bst : forall s acc, bst s -> bst acc -> - bst (filter_acc f acc s). -Proof. - induction s; simpl; auto. - intros. - inv bst. - destruct (f t); auto. -Qed. - -Lemma filter_in : forall s, - compat_bool X.eq f -> forall x : elt, - In x (filter f s) <-> In x s /\ f x = true. -Proof. - unfold filter; intros; rewrite filter_acc_in; intuition_in. -Qed. - -Lemma filter_bst : forall s, bst s -> bst (filter f s). -Proof. - unfold filter; intros; apply filter_acc_bst; auto. -Qed. - - - -(** * Partition *) - -Lemma partition_acc_in_1 : forall s acc, - compat_bool X.eq f -> forall x : elt, - In x (partition_acc f acc s)#1 <-> - In x acc#1 \/ In x s /\ f x = true. -Proof. - induction s; simpl; intros. - intuition_in. - destruct acc as [acct accf]; simpl in *. - rewrite IHs2 by - (destruct (f t); auto; apply partition_acc_avl_1; simpl; auto). - rewrite IHs1 by (destruct (f t); simpl; auto). - case_eq (f t); simpl; intros. - rewrite (add_in); auto. - intuition_in. - rewrite (H _ _ H2). - intuition. - intuition_in. - rewrite (H _ _ H2) in H3. - rewrite H0 in H3; discriminate. -Qed. - -Lemma partition_acc_in_2 : forall s acc, - compat_bool X.eq f -> forall x : elt, - In x (partition_acc f acc s)#2 <-> - In x acc#2 \/ In x s /\ f x = false. -Proof. - induction s; simpl; intros. - intuition_in. - destruct acc as [acct accf]; simpl in *. - rewrite IHs2 by - (destruct (f t); auto; apply partition_acc_avl_2; simpl; auto). - rewrite IHs1 by (destruct (f t); simpl; auto). - case_eq (f t); simpl; intros. - intuition. - intuition_in. - rewrite (H _ _ H2) in H3. - rewrite H0 in H3; discriminate. - rewrite (add_in); auto. - intuition_in. - rewrite (H _ _ H2). - intuition. -Qed. - -Lemma partition_in_1 : forall s, - compat_bool X.eq f -> forall x : elt, - In x (partition f s)#1 <-> 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, - compat_bool X.eq f -> forall x : elt, - In x (partition f s)#2 <-> In x s /\ f x = false. -Proof. - unfold partition; intros; rewrite partition_acc_in_2; - simpl in *; intuition_in. -Qed. - -Lemma partition_acc_bst_1 : forall s acc, bst s -> bst acc#1 -> - bst (partition_acc f acc s)#1. -Proof. - induction s; simpl; auto. - destruct acc as [acct accf]; simpl in *. - intros. - inv bst. - destruct (f t); auto. - apply IHs2; simpl; auto. - apply IHs1; simpl; auto. -Qed. - -Lemma partition_acc_bst_2 : forall s acc, bst s -> bst acc#2 -> - bst (partition_acc f acc s)#2. -Proof. - induction s; simpl; auto. - destruct acc as [acct accf]; simpl in *. - intros. - inv bst. - destruct (f t); auto. - apply IHs2; simpl; auto. - apply IHs1; simpl; auto. -Qed. - -Lemma partition_bst_1 : forall s, bst s -> bst (partition f s)#1. -Proof. - unfold partition; intros; apply partition_acc_bst_1; auto. -Qed. - -Lemma partition_bst_2 : forall s, bst s -> bst (partition f s)#2. -Proof. - unfold partition; intros; apply partition_acc_bst_2; auto. -Qed. - - - -(** * [for_all] and [exists] *) - -Lemma for_all_1 : forall s, compat_bool X.eq f -> - For_all (fun x => f x = true) s -> for_all f 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 X.eq f -> - for_all f 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. - -Lemma exists_1 : forall s, compat_bool X.eq f -> - Exists (fun x => f x = true) s -> exists_ f s = true. -Proof. - induction s; simpl; destruct 2 as (x,(U,V)); inv In; rewrite <- ?orb_lazy_alt. - rewrite (H _ _ (X.eq_sym H0)); rewrite V; auto. - apply orb_true_intro; left. - 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 -> - exists_ f s = true -> Exists (fun x => f x = true) s. -Proof. - induction s; simpl; intros; rewrite <- ?orb_lazy_alt in *. - discriminate. - destruct (orb_true_elim _ _ H0) as [H1|H1]. - destruct (orb_true_elim _ _ H1) as [H2|H2]. - exists t; auto. - destruct (IHs1 H H2); auto; exists x; intuition. - destruct (IHs2 H H1); auto; exists x; intuition. -Qed. - -End F. - - - -(** * Fold *) - -Definition fold' (A : Type) (f : elt -> A -> A)(s : tree) := - L.fold f (elements s). -Implicit Arguments fold' [A]. - -Lemma fold_equiv_aux : - forall (A : Type) (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 : Type) (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 : Type)(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. - -(** * Subset *) - -Lemma subsetl_12 : forall subset_l1 l1 x1 h1 s2, - bst (Node l1 x1 Leaf h1) -> bst s2 -> - (forall s, bst s -> (subset_l1 s = true <-> Subset l1 s)) -> - (subsetl subset_l1 x1 s2 = true <-> Subset (Node l1 x1 Leaf h1) s2 ). -Proof. - induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros. - unfold Subset; intuition; try discriminate. - assert (H': In x1 Leaf) by auto; inversion H'. - inversion_clear H0. - specialize (IHl2 H H2 H1). - specialize (IHr2 H H3 H1). - inv bst. clear H8. - destruct X.compare. - - rewrite IHl2; clear H1 IHl2 IHr2. - 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. - - rewrite H1 by auto; clear H1 IHl2 IHr2. - unfold Subset. intuition_in. - assert (X.eq a x2) by order; intuition_in. - assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. - - rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2. - unfold Subset. intuition_in. - assert (H':=mem_2 H6); apply In_1 with x1; auto. - apply mem_1; auto. - assert (In x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order. -Qed. - - -Lemma subsetr_12 : forall subset_r1 r1 x1 h1 s2, - bst (Node Leaf x1 r1 h1) -> bst s2 -> - (forall s, bst s -> (subset_r1 s = true <-> Subset r1 s)) -> - (subsetr subset_r1 x1 s2 = true <-> Subset (Node Leaf x1 r1 h1) s2). -Proof. - induction s2 as [|l2 IHl2 x2 r2 IHr2 h2]; simpl; intros. - unfold Subset; intuition; try discriminate. - assert (H': In x1 Leaf) by auto; inversion H'. - inversion_clear H0. - specialize (IHl2 H H2 H1). - specialize (IHr2 H H3 H1). - inv bst. clear H7. - destruct X.compare. - - rewrite <-andb_lazy_alt, andb_true_iff, H1 by auto; clear H1 IHl2 IHr2. - unfold Subset. intuition_in. - assert (H':=mem_2 H1); apply In_1 with x1; auto. - apply mem_1; auto. - assert (In x1 (Node l2 x2 r2 h2)) by auto; intuition_in; order. - - rewrite H1 by auto; clear H1 IHl2 IHr2. - unfold Subset. intuition_in. - assert (X.eq a x2) by order; intuition_in. - assert (In a (Node l2 x2 r2 h2)) by auto; intuition_in; order. - - rewrite IHr2; clear H1 IHl2 IHr2. - 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 subset_12 : forall s1 s2, bst s1 -> bst s2 -> - (subset s1 s2 = true <-> Subset s1 s2). -Proof. - induction s1 as [|l1 IHl1 x1 r1 IHr1 h1]; simpl; intros. - unfold Subset; intuition_in. - destruct s2 as [|l2 x2 r2 h2]; simpl; intros. - unfold Subset; intuition_in; try discriminate. - assert (H': In x1 Leaf) by auto; inversion H'. - inv bst. - destruct X.compare. - - rewrite <-andb_lazy_alt, andb_true_iff, IHr1 by auto. - rewrite (@subsetl_12 (subset l1) l1 x1 h1) by auto. - clear IHl1 IHr1. - 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. - - rewrite <-andb_lazy_alt, andb_true_iff, IHl1, IHr1 by auto. - clear IHl1 IHr1. - unfold Subset; intuition_in. - assert (X.eq a x2) by order; 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. - - rewrite <-andb_lazy_alt, andb_true_iff, IHl1 by auto. - rewrite (@subsetr_12 (subset r1) r1 x1 h1) by auto. - clear IHl1 IHr1. - 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. - - - -(** * Comparison *) - -(** ** Relations [eq] and [lt] over trees *) - -Definition eq := Equal. -Definition lt (s1 s2 : t) : Prop := L.lt (elements s1) (elements s2). - -Lemma eq_refl : forall s : t, Equal s s. -Proof. - unfold Equal; intuition. -Qed. - -Lemma eq_sym : forall s s' : t, Equal s s' -> Equal s' s. -Proof. - unfold Equal; intros s s' H x; destruct (H x); split; auto. -Qed. - -Lemma eq_trans : forall s s' s'' : t, - Equal s s' -> Equal s' s'' -> Equal s s''. -Proof. - 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, Equal s s' -> L.eq (elements s) (elements s'). -Proof. - 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') -> Equal s s'. -Proof. - unfold Equal, L.eq, L.Equal; intros; do 2 rewrite <-elements_in; auto. -Qed. -Hint Resolve eq_L_eq L_eq_eq. - -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' -> ~ Equal s s'. -Proof. - unfold lt in |- *; intros; intro. - apply L.lt_not_eq with (s := elements s) (s' := elements s'); auto. -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 with *. - inversion_clear H1; generalize (H0 a); clear H0; intuition. - apply InA_eqA with y; eauto with *. -Qed. -Hint Resolve L_eq_cons. - - -(** * A new comparison algorithm suggested by Xavier Leroy *) - -(** [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. - -Lemma flatten_e_elements : - forall l x r h e, - elements l ++ flatten_e (More x r e) = elements (Node l x r h) ++ flatten_e e. -Proof. - intros; simpl; apply elements_node. -Qed. - -Lemma cons_1 : forall s e, - flatten_e (cons s e) = elements s ++ flatten_e e. -Proof. - induction s; simpl; auto; intros. - rewrite IHs1; apply flatten_e_elements. -Qed. - -(** Correctness of this comparison *) - -Definition Cmp c := - match c with - | Eq => L.eq - | Lt => L.lt - | Gt => (fun l1 l2 => L.lt l2 l1) - end. - -Lemma cons_Cmp : forall c x1 x2 l1 l2, X.eq x1 x2 -> - Cmp c l1 l2 -> Cmp c (x1::l1) (x2::l2). -Proof. - destruct c; simpl; auto. -Qed. -Hint Resolve cons_Cmp. - -Lemma compare_end_Cmp : - forall e2, Cmp (compare_end e2) nil (flatten_e e2). -Proof. - destruct e2; simpl; auto. - apply L.eq_refl. -Qed. - -Lemma compare_more_Cmp : forall x1 cont x2 r2 e2 l, - Cmp (cont (cons r2 e2)) l (elements r2 ++ flatten_e e2) -> - Cmp (compare_more x1 cont (More x2 r2 e2)) (x1::l) - (flatten_e (More x2 r2 e2)). -Proof. - simpl; intros; destruct X.compare; simpl; auto. -Qed. - -Lemma compare_cont_Cmp : forall s1 cont e2 l, - (forall e, Cmp (cont e) l (flatten_e e)) -> - Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2). -Proof. - induction s1 as [|l1 Hl1 x1 r1 Hr1 h1]; simpl; intros; auto. - rewrite <- elements_node; simpl. - apply Hl1; auto. clear e2. intros [|x2 r2 e2]. - simpl; auto. - apply compare_more_Cmp. - rewrite <- cons_1; auto. -Qed. - -Lemma compare_Cmp : forall s1 s2, - Cmp (compare s1 s2) (elements s1) (elements s2). -Proof. - intros; unfold compare. - rewrite (app_nil_end (elements s1)). - replace (elements s2) with (flatten_e (cons s2 End)) by - (rewrite cons_1; simpl; rewrite <- app_nil_end; auto). - apply compare_cont_Cmp; auto. - intros. - apply compare_end_Cmp; auto. -Qed. - -(** * Equality test *) - -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_Cmp s1 s2). -destruct (compare s1 s2); simpl in *; auto; intros. -elim (lt_not_eq B1 B2 H E); auto. -elim (lt_not_eq B2 B1 H (eq_sym E)); auto. -Qed. - -Lemma equal_2 : forall s1 s2, - equal s1 s2 = true -> Equal s1 s2. -Proof. -unfold equal; intros s1 s2 E. -generalize (compare_Cmp s1 s2); - destruct compare; auto; discriminate. -Qed. - -End Proofs. - -End Raw. - - - -(** * Encapsulation - - Now, in order to really provide a functor implementing [S], we - need to encapsulate everything into a type of binary search trees. - They also happen to be well-balanced, but this has no influence - on the correctness of operations, so we won't state this here, - see [FSetFullAVL] if you need more than just the FSet interface. -*) +Require FSetCompat MSetAVL OrderedType2 OrderedType2Alt. Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. - - Module E := X. - Module Raw := Raw I X. - Import Raw.Proofs. - - Record bst := Bst {this :> Raw.t; is_bst : Raw.bst this}. - Definition t := bst. - Definition elt := E.t. - - Definition In (x : elt) (s : t) := Raw.In x s. - Definition Equal (s s':t) := forall a : elt, In a s <-> In a s'. - Definition Subset (s s':t) := forall a : elt, In a s -> In a s'. - Definition Empty (s:t) := forall a : elt, ~ In a s. - Definition For_all (P : elt -> Prop) (s:t) := forall x, In x s -> P x. - Definition Exists (P : elt -> Prop) (s:t) := exists x, In x s /\ P x. - - Lemma In_1 : forall (s:t)(x y:elt), E.eq x y -> In x s -> In y s. - Proof. intro s; exact (@In_1 s). Qed. - - Definition mem (x:elt)(s:t) : bool := Raw.mem x s. - - Definition empty : t := Bst empty_bst. - Definition is_empty (s:t) : bool := Raw.is_empty s. - Definition singleton (x:elt) : t := Bst (singleton_bst x). - Definition add (x:elt)(s:t) : t := Bst (add_bst x (is_bst s)). - Definition remove (x:elt)(s:t) : t := Bst (remove_bst x (is_bst s)). - Definition inter (s s':t) : t := Bst (inter_bst (is_bst s) (is_bst s')). - Definition union (s s':t) : t := Bst (union_bst (is_bst s) (is_bst s')). - Definition diff (s s':t) : t := Bst (diff_bst (is_bst s) (is_bst 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. - Definition choose (s:t) : option elt := Raw.choose s. - 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 := - Bst (filter_bst f (is_bst 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 - (@Bst (fst p) (partition_bst_1 f (is_bst s)), - @Bst (snd p) (partition_bst_2 f (is_bst s))). - - Definition equal (s s':t) : bool := Raw.equal s s'. - Definition subset (s s':t) : bool := Raw.subset s s'. - - Definition eq (s s':t) : Prop := Raw.Equal s s'. - Definition lt (s s':t) : Prop := Raw.Proofs.lt s s'. - - Definition compare (s s':t) : Compare lt eq s s'. - Proof. - intros (s,b) (s',b'). - generalize (compare_Cmp s s'). - destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto. - Defined. - - Definition eq_dec (s s':t) : { eq s s' } + { ~ eq s s' }. - Proof. - intros (s,b) (s',b'); unfold eq; simpl. - case_eq (Raw.equal s s'); intro H; [left|right]. - apply equal_2; auto. - intro H'; rewrite equal_1 in H; auto; discriminate. - Defined. - - (* specs *) - Section Specs. - Variable s s' s'': t. - Variable x y : elt. - - Hint Resolve is_bst. - - Lemma mem_1 : In x s -> mem x s = true. - Proof. exact (mem_1 (is_bst s)). Qed. - Lemma mem_2 : mem x s = true -> In x s. - Proof. exact (@mem_2 s x). Qed. - - Lemma equal_1 : Equal s s' -> equal s s' = true. - Proof. exact (equal_1 (is_bst s) (is_bst s')). Qed. - Lemma equal_2 : equal s s' = true -> Equal s s'. - Proof. exact (@equal_2 s s'). Qed. - - Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition. - - Lemma subset_1 : Subset s s' -> subset s s' = true. - Proof. wrap subset subset_12. Qed. - Lemma subset_2 : subset s s' = true -> Subset s s'. - Proof. wrap subset subset_12. Qed. - - Lemma empty_1 : Empty empty. - Proof. exact empty_1. Qed. - - Lemma is_empty_1 : Empty s -> is_empty s = true. - Proof. exact (@is_empty_1 s). Qed. - Lemma is_empty_2 : is_empty s = true -> Empty s. - Proof. exact (@is_empty_2 s). Qed. - - Lemma add_1 : E.eq x y -> In y (add x s). - Proof. wrap add add_in. Qed. - Lemma add_2 : In y s -> In y (add x s). - Proof. wrap add add_in. Qed. - Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. - Proof. wrap add add_in. elim H; auto. Qed. - - Lemma remove_1 : E.eq x y -> ~ In y (remove x s). - Proof. wrap remove remove_in. Qed. - Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). - Proof. wrap remove remove_in. Qed. - Lemma remove_3 : In y (remove x s) -> In y s. - Proof. wrap remove remove_in. Qed. - - Lemma singleton_1 : In y (singleton x) -> E.eq x y. - Proof. exact (@singleton_1 x y). Qed. - Lemma singleton_2 : E.eq x y -> In y (singleton x). - Proof. exact (@singleton_2 x y). Qed. - - Lemma union_1 : In x (union s s') -> In x s \/ In x s'. - Proof. wrap union union_in. Qed. - Lemma union_2 : In x s -> In x (union s s'). - Proof. wrap union union_in. Qed. - Lemma union_3 : In x s' -> In x (union s s'). - Proof. wrap union union_in. Qed. - - Lemma inter_1 : In x (inter s s') -> In x s. - Proof. wrap inter inter_in. Qed. - Lemma inter_2 : In x (inter s s') -> In x s'. - Proof. wrap inter inter_in. Qed. - Lemma inter_3 : In x s -> In x s' -> In x (inter s s'). - Proof. wrap inter inter_in. Qed. - - Lemma diff_1 : In x (diff s s') -> In x s. - Proof. wrap diff diff_in. Qed. - Lemma diff_2 : In x (diff s s') -> ~ In x s'. - Proof. wrap diff diff_in. Qed. - Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s'). - Proof. wrap diff diff_in. 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. - Proof. unfold fold, elements; intros; apply fold_1; auto. Qed. - - Lemma cardinal_1 : cardinal s = length (elements s). - Proof. - unfold cardinal, elements; intros; apply elements_cardinal; 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. wrap filter filter_in. Qed. - Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. - Proof. intro. wrap filter filter_in. Qed. - Lemma filter_3 : compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). - Proof. intro. wrap filter filter_in. Qed. - - Lemma for_all_1 : compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true. - Proof. exact (@for_all_1 f s). Qed. - Lemma for_all_2 : compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s. - Proof. exact (@for_all_2 f s). Qed. - - Lemma exists_1 : compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. - Proof. exact (@exists_1 f s). Qed. - Lemma exists_2 : compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. - Proof. exact (@exists_2 f s). Qed. - - 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, 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, filter_in; intuition. - rewrite H2; auto. - destruct (f a); auto. - repeat red; intros; f_equal. - rewrite (H _ _ H0); auto. - Qed. - - End Filter. - - Lemma elements_1 : In x s -> InA E.eq x (elements s). - Proof. wrap elements elements_in. Qed. - Lemma elements_2 : InA E.eq x (elements s) -> In x s. - Proof. wrap elements elements_in. Qed. - Lemma elements_3 : sort E.lt (elements s). - Proof. exact (elements_sort (is_bst s)). Qed. - Lemma elements_3w : NoDupA E.eq (elements s). - Proof. exact (elements_nodup (is_bst s)). Qed. - - Lemma min_elt_1 : min_elt s = Some x -> In x s. - Proof. exact (@min_elt_1 s x). Qed. - Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. - Proof. exact (@min_elt_2 s x y (is_bst s)). Qed. - Lemma min_elt_3 : min_elt s = None -> Empty s. - Proof. exact (@min_elt_3 s). Qed. - - Lemma max_elt_1 : max_elt s = Some x -> In x s. - Proof. exact (@max_elt_1 s x). Qed. - Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. - Proof. exact (@max_elt_2 s x y (is_bst s)). Qed. - Lemma max_elt_3 : max_elt s = None -> Empty s. - Proof. exact (@max_elt_3 s). Qed. - - Lemma choose_1 : choose s = Some x -> In x s. - Proof. exact (@choose_1 s x). Qed. - Lemma choose_2 : choose s = None -> Empty s. - Proof. exact (@choose_2 s). Qed. - Lemma choose_3 : choose s = Some x -> choose s' = Some y -> - Equal s s' -> E.eq x y. - Proof. exact (@choose_3 _ _ (is_bst s) (is_bst s') x y). Qed. - - Lemma eq_refl : eq s s. - Proof. exact (eq_refl s). Qed. - Lemma eq_sym : eq s s' -> eq s' s. - Proof. exact (@eq_sym s s'). Qed. - Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''. - Proof. exact (@eq_trans s s' s''). Qed. - - Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''. - Proof. exact (@lt_trans s s' s''). Qed. - Lemma lt_not_eq : lt s s' -> ~eq s s'. - Proof. exact (@lt_not_eq _ _ (is_bst s) (is_bst s')). Qed. - - End Specs. + Module X' := OrderedType2Alt.Update_OT X. + Module MSet := MSetAVL.IntMake I X'. + Include FSetCompat.Backport_Sets X MSet. End IntMake. (* For concrete use inside Coq, we propose an instantiation of [Int] by [Z]. *) diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v new file mode 100644 index 000000000..487b4fc32 --- /dev/null +++ b/theories/FSets/FSetCompat.v @@ -0,0 +1,413 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(** * Compatibility functors between FSetInterface and MSetInterface. *) + +Require Import FSetInterface FSetFacts MSetInterface MSetFacts. +Set Implicit Arguments. +Unset Strict Implicit. + +(** * From new Weak Sets to old ones *) + +Module Backport_WSets + (E:DecidableType.DecidableType) + (M:MSetInterface.WSets with Definition E.t := E.t + with Definition E.eq := E.eq) + <: FSetInterface.WSfun E. + + Definition elt := E.t. + Definition t := M.t. + + Implicit Type s : t. + Implicit Type x y : elt. + Implicit Type f : elt -> bool. + + Definition In : elt -> t -> Prop := M.In. + 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. + Definition empty : t := M.empty. + Definition is_empty : t -> bool := M.is_empty. + Definition mem : elt -> t -> bool := M.mem. + Definition add : elt -> t -> t := M.add. + Definition singleton : elt -> t := M.singleton. + Definition remove : elt -> t -> t := M.remove. + Definition union : t -> t -> t := M.union. + Definition inter : t -> t -> t := M.inter. + Definition diff : t -> t -> t := M.diff. + Definition eq : t -> t -> Prop := M.eq. + Definition eq_dec : forall s s', {eq s s'}+{~eq s s'}:= M.eq_dec. + Definition equal : t -> t -> bool := M.equal. + Definition subset : t -> t -> bool := M.subset. + Definition fold : forall A : Type, (elt -> A -> A) -> t -> A -> A := M.fold. + Definition for_all : (elt -> bool) -> t -> bool := M.for_all. + Definition exists_ : (elt -> bool) -> t -> bool := M.exists_. + Definition filter : (elt -> bool) -> t -> t := M.filter. + Definition partition : (elt -> bool) -> t -> t * t:= M.partition. + Definition cardinal : t -> nat := M.cardinal. + Definition elements : t -> list elt := M.elements. + Definition choose : t -> option elt := M.choose. + + Module MF := MSetFacts.WFacts M. + + Definition In_1 : forall s x y, E.eq x y -> In x s -> In y s + := MF.In_1. + Definition eq_refl : forall s, eq s s + := @Equivalence_Reflexive _ _ M.eq_equiv. + Definition eq_sym : forall s s', eq s s' -> eq s' s + := @Equivalence_Symmetric _ _ M.eq_equiv. + Definition eq_trans : forall s s' s'', eq s s' -> eq s' s'' -> eq s s'' + := @Equivalence_Transitive _ _ M.eq_equiv. + Definition mem_1 : forall s x, In x s -> mem x s = true + := MF.mem_1. + Definition mem_2 : forall s x, mem x s = true -> In x s + := MF.mem_2. + Definition equal_1 : forall s s', Equal s s' -> equal s s' = true + := MF.equal_1. + Definition equal_2 : forall s s', equal s s' = true -> Equal s s' + := MF.equal_2. + Definition subset_1 : forall s s', Subset s s' -> subset s s' = true + := MF.subset_1. + Definition subset_2 : forall s s', subset s s' = true -> Subset s s' + := MF.subset_2. + Definition empty_1 : Empty empty := MF.empty_1. + Definition is_empty_1 : forall s, Empty s -> is_empty s = true + := MF.is_empty_1. + Definition is_empty_2 : forall s, is_empty s = true -> Empty s + := MF.is_empty_2. + Definition add_1 : forall s x y, E.eq x y -> In y (add x s) + := MF.add_1. + Definition add_2 : forall s x y, In y s -> In y (add x s) + := MF.add_2. + Definition add_3 : forall s x y, ~ E.eq x y -> In y (add x s) -> In y s + := MF.add_3. + Definition remove_1 : forall s x y, E.eq x y -> ~ In y (remove x s) + := MF.remove_1. + Definition remove_2 : forall s x y, ~ E.eq x y -> In y s -> In y (remove x s) + := MF.remove_2. + Definition remove_3 : forall s x y, In y (remove x s) -> In y s + := MF.remove_3. + Definition union_1 : forall s s' x, In x (union s s') -> In x s \/ In x s' + := MF.union_1. + Definition union_2 : forall s s' x, In x s -> In x (union s s') + := MF.union_2. + Definition union_3 : forall s s' x, In x s' -> In x (union s s') + := MF.union_3. + Definition inter_1 : forall s s' x, In x (inter s s') -> In x s + := MF.inter_1. + Definition inter_2 : forall s s' x, In x (inter s s') -> In x s' + := MF.inter_2. + Definition inter_3 : forall s s' x, In x s -> In x s' -> In x (inter s s') + := MF.inter_3. + Definition diff_1 : forall s s' x, In x (diff s s') -> In x s + := MF.diff_1. + Definition diff_2 : forall s s' x, In x (diff s s') -> ~ In x s' + := MF.diff_2. + Definition diff_3 : forall s s' x, In x s -> ~ In x s' -> In x (diff s s') + := MF.diff_3. + Definition singleton_1 : forall x y, In y (singleton x) -> E.eq x y + := MF.singleton_1. + Definition singleton_2 : forall x y, E.eq x y -> In y (singleton x) + := MF.singleton_2. + Definition fold_1 : forall s (A : Type) (i : A) (f : elt -> A -> A), + fold f s i = fold_left (fun a e => f e a) (elements s) i + := MF.fold_1. + Definition cardinal_1 : forall s, cardinal s = length (elements s) + := MF.cardinal_1. + Definition filter_1 : forall s x f, compat_bool E.eq f -> + In x (filter f s) -> In x s + := MF.filter_1. + Definition filter_2 : forall s x f, compat_bool E.eq f -> + In x (filter f s) -> f x = true + := MF.filter_2. + Definition filter_3 : forall s x f, compat_bool E.eq f -> + In x s -> f x = true -> In x (filter f s) + := MF.filter_3. + Definition for_all_1 : forall s f, compat_bool E.eq f -> + For_all (fun x => f x = true) s -> for_all f s = true + := MF.for_all_1. + Definition for_all_2 : forall s f, compat_bool E.eq f -> + for_all f s = true -> For_all (fun x => f x = true) s + := MF.for_all_2. + Definition exists_1 : forall s f, compat_bool E.eq f -> + Exists (fun x => f x = true) s -> exists_ f s = true + := MF.exists_1. + Definition exists_2 : forall s f, compat_bool E.eq f -> + exists_ f s = true -> Exists (fun x => f x = true) s + := MF.exists_2. + Definition partition_1 : forall s f, compat_bool E.eq f -> + Equal (fst (partition f s)) (filter f s) + := MF.partition_1. + Definition partition_2 : forall s f, compat_bool E.eq f -> + Equal (snd (partition f s)) (filter (fun x => negb (f x)) s) + := MF.partition_2. + Definition choose_1 : forall s x, choose s = Some x -> In x s + := MF.choose_1. + Definition choose_2 : forall s, choose s = None -> Empty s + := MF.choose_2. + Definition elements_1 : forall s x, In x s -> InA E.eq x (elements s) + := MF.elements_1. + Definition elements_2 : forall s x, InA E.eq x (elements s) -> In x s + := MF.elements_2. + Definition elements_3w : forall s, NoDupA E.eq (elements s) + := MF.elements_3w. + +End Backport_WSets. + + +(** * From new Sets to new ones *) + +Module Backport_Sets + (E:OrderedType.OrderedType) + (M:MSetInterface.Sets with Definition E.t := E.t + with Definition E.eq := E.eq + with Definition E.lt := E.lt) + <: FSetInterface.S with Module E:=E. + + Include Backport_WSets E M. + + Module E := E. + + Implicit Type s : t. + Implicit Type x y : elt. + + Definition lt : t -> t -> Prop := M.lt. + Definition min_elt : t -> option elt := M.min_elt. + Definition max_elt : t -> option elt := M.max_elt. + Definition min_elt_1 : forall s x, min_elt s = Some x -> In x s + := M.min_elt_spec1. + Definition min_elt_2 : forall s x y, + min_elt s = Some x -> In y s -> ~ E.lt y x + := M.min_elt_spec2. + Definition min_elt_3 : forall s, min_elt s = None -> Empty s + := M.min_elt_spec3. + Definition max_elt_1 : forall s x, max_elt s = Some x -> In x s + := M.max_elt_spec1. + Definition max_elt_2 : forall s x y, + max_elt s = Some x -> In y s -> ~ E.lt x y + := M.max_elt_spec2. + Definition max_elt_3 : forall s, max_elt s = None -> Empty s + := M.max_elt_spec3. + Definition elements_3 : forall s, sort E.lt (elements s) + := M.elements_spec2. + Definition choose_3 : forall s s' x y, + choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y + := M.choose_spec3. + Definition lt_trans : forall s s' s'', lt s s' -> lt s' s'' -> lt s s'' + := @StrictOrder_Transitive _ _ M.lt_strorder. + Lemma lt_not_eq : forall s s', lt s s' -> ~ eq s s'. + Proof. + unfold lt, eq. intros s s' Hlt Heq. rewrite Heq in Hlt. + apply (StrictOrder_Irreflexive s'); auto. + Qed. + Definition compare : forall s s', Compare lt eq s s'. + Proof. + intros s s'. generalize (M.compare_spec s s'). + destruct (M.compare s s'); simpl; intros. + constructor 2; auto. + constructor 1; auto. + constructor 3; auto. + Defined. + +End Backport_Sets. + + +(** * From old Weak Sets to new ones. *) + +Module Update_WSets + (E:DecidableType2.DecidableType) + (M:FSetInterface.WS with Definition E.t := E.t + with Definition E.eq := E.eq) + <: MSetInterface.WSetsOn E. + + Definition elt := E.t. + Definition t := M.t. + + Implicit Type s : t. + Implicit Type x y : elt. + Implicit Type f : elt -> bool. + + Definition In : elt -> t -> Prop := M.In. + 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. + Definition empty : t := M.empty. + Definition is_empty : t -> bool := M.is_empty. + Definition mem : elt -> t -> bool := M.mem. + Definition add : elt -> t -> t := M.add. + Definition singleton : elt -> t := M.singleton. + Definition remove : elt -> t -> t := M.remove. + Definition union : t -> t -> t := M.union. + Definition inter : t -> t -> t := M.inter. + Definition diff : t -> t -> t := M.diff. + Definition eq : t -> t -> Prop := M.eq. + Definition eq_dec : forall s s', {eq s s'}+{~eq s s'}:= M.eq_dec. + Definition equal : t -> t -> bool := M.equal. + Definition subset : t -> t -> bool := M.subset. + Definition fold : forall A : Type, (elt -> A -> A) -> t -> A -> A := M.fold. + Definition for_all : (elt -> bool) -> t -> bool := M.for_all. + Definition exists_ : (elt -> bool) -> t -> bool := M.exists_. + Definition filter : (elt -> bool) -> t -> t := M.filter. + Definition partition : (elt -> bool) -> t -> t * t:= M.partition. + Definition cardinal : t -> nat := M.cardinal. + Definition elements : t -> list elt := M.elements. + Definition choose : t -> option elt := M.choose. + + Module MF := FSetFacts.WFacts M. + + Instance In_compat : Proper (E.eq==>Logic.eq==>iff) In. + Proof. intros x x' Hx s s' Hs. subst. apply MF.In_eq_iff; auto. Qed. + + Instance eq_equiv : Equivalence eq. + + Section Spec. + Variable s s': t. + Variable x y : elt. + + Lemma mem_spec : mem x s = true <-> In x s. + Proof. intros; symmetry; apply MF.mem_iff. Qed. + + Lemma equal_spec : equal s s' = true <-> Equal s s'. + Proof. intros; symmetry; apply MF.equal_iff. Qed. + + Lemma subset_spec : subset s s' = true <-> Subset s s'. + Proof. intros; symmetry; apply MF.subset_iff. Qed. + + Definition empty_spec : Empty empty := M.empty_1. + + Lemma is_empty_spec : is_empty s = true <-> Empty s. + Proof. intros; symmetry; apply MF.is_empty_iff. Qed. + + Lemma add_spec : In y (add x s) <-> E.eq y x \/ In y s. + Proof. intros. rewrite MF.add_iff. intuition. Qed. + + Lemma remove_spec : In y (remove x s) <-> In y s /\ ~E.eq y x. + Proof. intros. rewrite MF.remove_iff. intuition. Qed. + + Lemma singleton_spec : In y (singleton x) <-> E.eq y x. + Proof. intros; rewrite MF.singleton_iff. intuition. Qed. + + Definition union_spec : In x (union s s') <-> In x s \/ In x s' + := @MF.union_iff s s' x. + Definition inter_spec : In x (inter s s') <-> In x s /\ In x s' + := @MF.inter_iff s s' x. + Definition diff_spec : In x (diff s s') <-> In x s /\ ~In x s' + := @MF.diff_iff s s' x. + Definition fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A), + fold f s i = fold_left (flip f) (elements s) i + := @M.fold_1 s. + Definition cardinal_spec : cardinal s = length (elements s) + := @M.cardinal_1 s. + + Lemma elements_spec1 : InA E.eq x (elements s) <-> In x s. + Proof. intros; symmetry; apply MF.elements_iff. Qed. + + Definition elements_spec2w : NoDupA E.eq (elements s) + := @M.elements_3w s. + Definition choose_spec1 : choose s = Some x -> In x s + := @M.choose_1 s x. + Definition choose_spec2 : choose s = None -> Empty s + := @M.choose_2 s. + Definition filter_spec : forall f, Proper (E.eq==>Logic.eq) f -> + (In x (filter f s) <-> In x s /\ f x = true) + := @MF.filter_iff s x. + Definition partition_spec1 : forall f, Proper (E.eq==>Logic.eq) f -> + Equal (fst (partition f s)) (filter f s) + := @M.partition_1 s. + Definition partition_spec2 : forall f, Proper (E.eq==>Logic.eq) f -> + Equal (snd (partition f s)) (filter (fun x => negb (f x)) s) + := @M.partition_2 s. + + Lemma for_all_spec : forall f, Proper (E.eq==>Logic.eq) f -> + (for_all f s = true <-> For_all (fun x => f x = true) s). + Proof. intros; symmetry; apply MF.for_all_iff; auto. Qed. + + Lemma exists_spec : forall f, Proper (E.eq==>Logic.eq) f -> + (exists_ f s = true <-> Exists (fun x => f x = true) s). + Proof. intros; symmetry; apply MF.exists_iff; auto. Qed. + + End Spec. + +End Update_WSets. + + +(** * From old Sets to new ones. *) + +Module Update_Sets + (E:OrderedType2.OrderedType) + (M:FSetInterface.S with Definition E.t := E.t + with Definition E.eq := E.eq + with Definition E.lt := E.lt) + <: MSetInterface.Sets with Module E:=E. + + Module E := E. + + Include Update_WSets E M. + + Implicit Type s : t. + Implicit Type x y : elt. + + Definition lt : t -> t -> Prop := M.lt. + Definition min_elt : t -> option elt := M.min_elt. + Definition max_elt : t -> option elt := M.max_elt. + Definition min_elt_spec1 : forall s x, min_elt s = Some x -> In x s + := M.min_elt_1. + Definition min_elt_spec2 : forall s x y, + min_elt s = Some x -> In y s -> ~ E.lt y x + := M.min_elt_2. + Definition min_elt_spec3 : forall s, min_elt s = None -> Empty s + := M.min_elt_3. + Definition max_elt_spec1 : forall s x, max_elt s = Some x -> In x s + := M.max_elt_1. + Definition max_elt_spec2 : forall s x y, + max_elt s = Some x -> In y s -> ~ E.lt x y + := M.max_elt_2. + Definition max_elt_spec3 : forall s, max_elt s = None -> Empty s + := M.max_elt_3. + Definition elements_spec2 : forall s, sort E.lt (elements s) + := M.elements_3. + Definition choose_spec3 : forall s s' x y, + choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y + := M.choose_3. + + Instance lt_strorder : StrictOrder lt. + Proof. + split. + intros x Hx. apply (M.lt_not_eq Hx); auto with *. + exact M.lt_trans. + Qed. + + Instance lt_compat : Proper (eq==>eq==>iff) lt. + Proof. + apply proper_sym_impl_iff_2; auto with *. + intros s s' Hs u u' Hu H. + assert (H0 : lt s' u). + destruct (M.compare s' u) as [H'|H'|H']; auto. + elim (M.lt_not_eq H). transitivity s'; auto with *. + elim (M.lt_not_eq (M.lt_trans H H')); auto. + destruct (M.compare s' u') as [H'|H'|H']; auto. + elim (M.lt_not_eq H). + transitivity u'; auto with *. transitivity s'; auto with *. + elim (M.lt_not_eq (M.lt_trans H' H0)); auto with *. + Qed. + + Definition compare s s' := + match M.compare s s' with + | EQ _ => Eq + | LT _ => Lt + | GT _ => Gt + end. + + Lemma compare_spec : forall s s', Cmp eq lt (compare s s') s s'. + Proof. intros; unfold compare; destruct M.compare; auto. Qed. + +End Update_Sets. diff --git a/theories/FSets/FSetFullAVL.v b/theories/FSets/FSetFullAVL.v deleted file mode 100644 index 782dccae3..000000000 --- a/theories/FSets/FSetFullAVL.v +++ /dev/null @@ -1,1126 +0,0 @@ -(***********************************************************************) -(* 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 *) -(***********************************************************************) - -(* $Id$ *) - -(** * FSetFullAVL : some complements to FSetAVL - - - Functor [AvlProofs] proves that trees of [FSetAVL] are not only - binary search trees, but moreover well-balanced ones. This is done - by proving that all operations preserve the balancing. - - - Functor [OcamlOps] contains variants of [union], [subset], - [compare] and [equal] that are faithful to the original ocaml codes, - while the versions in FSetAVL have been adapted to perform only - structural recursive code. - - - Finally, we pack the previous elements in a [Make] functor - similar to the one of [FSetAVL], but richer. -*) - -Require Import Recdef FSetInterface FSetList ZArith Int FSetAVL ROmega. - -Set Implicit Arguments. -Unset Strict Implicit. - -Module AvlProofs (Import I:Int)(X:OrderedType). -Module Import Raw := Raw I X. -Import Raw.Proofs. -Module Import II := MoreInt I. -Open Local Scope pair_scope. -Open Local Scope Int_scope. - -Ltac omega_max := i2z_refl; romega with Z. - -(** * 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 avl. - -(** 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. - -(** Tactics about [avl] *) - -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. - -(** Results about [height] *) - -Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf. -Proof. - destruct 1; intuition; simpl in *. - avl_nns; simpl in *; exfalso; omega_max. -Qed. - -(** * Results about [avl] *) - -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. - intros; auto. -Qed. -Hint Resolve avl_node. - - -(** empty *) - -Lemma empty_avl : avl empty. -Proof. - auto. -Qed. - -(** singleton *) - -Lemma singleton_avl : forall x : elt, avl (singleton x). -Proof. - unfold singleton; intro. - constructor; auto; try red; simpl; omega_max. -Qed. - -(** create *) - -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; auto. -Qed. - -(** bal *) - -Lemma bal_avl : forall l x r, avl l -> avl r -> - -(3) <= height l - height r <= 3 -> avl (bal l x r). -Proof. - intros l x r; functional induction bal l x r; intros; clearf; - inv avl; simpl in *; - match goal with |- avl (assert_false _ _ _) => avl_nns - | _ => repeat apply create_avl; simpl in *; auto - end; omega_max. -Qed. - -Lemma bal_height_1 : forall l x r, avl l -> avl r -> - -(3) <= height l - height r <= 3 -> - 0 <= height (bal l x r) - max (height l) (height r) <= 1. -Proof. - 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. - intros l x r; functional induction bal l x r; intros; clearf; - inv avl; simpl in *; omega_max. -Qed. - -Ltac omega_bal := match goal with - | H:avl ?l, H':avl ?r |- context [ bal ?l ?x ?r ] => - generalize (bal_height_1 x H H') (bal_height_2 x H H'); - omega_max - end. - -(** add *) - -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); subst;intros; inv avl; simpl in *. - intuition; try constructor; simpl; auto; try omega_max. - (* LT *) - destruct IHt; auto. - split. - apply bal_avl; auto; omega_max. - omega_bal. - (* EQ *) - intuition; omega_max. - (* GT *) - destruct IHt; 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; destruct (add_avl_1 x H); auto. -Qed. -Hint Resolve add_avl. - -(** join *) - -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. - join_tac. - - split; simpl; auto. - destruct (add_avl_1 x H0). - avl_nns; omega_max. - set (l:=Node ll lx lr lh) in *. - split; auto. - destruct (add_avl_1 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; destruct (join_avl_1 x H H0); auto. -Qed. -Hint Resolve join_avl. - -(** remove_min *) - -Lemma remove_min_avl_1 : forall l x r h, avl (Node l x r h) -> - 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. - avl_nns; omega_max. - inversion_clear H. - rewrite e0 in IHp;simpl in IHp;destruct (IHp _x); 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 (remove_min l x r)#1. -Proof. - intros; destruct (remove_min_avl_1 H); auto. -Qed. - -(** merge *) - -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); intros; - try factornode _x _x0 _x1 _x2 as s1. - simpl; split; auto; avl_nns; omega_max. - simpl; split; auto; avl_nns; simpl in *; omega_max. - generalize (remove_min_avl_1 H0). - rewrite e1; destruct 1. - split. - apply bal_avl; auto. - simpl; omega_max. - simpl in *; 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; destruct (merge_avl_1 H H0 H1); auto. -Qed. - - -(** remove *) - -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); intros. - intuition; omega_max. - (* LT *) - inv avl. - destruct (IHt H0). - 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 (IHt H1). - split. - apply bal_avl; auto. - omega_max. - omega_bal. -Qed. - -Lemma remove_avl : forall s x, avl s -> avl (remove x s). -Proof. - intros; destruct (remove_avl_1 x H); auto. -Qed. -Hint Resolve remove_avl. - -(** concat *) - -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; apply join_avl; auto. - generalize (remove_min_avl H0); rewrite e1; simpl; auto. -Qed. -Hint Resolve concat_avl. - -(** split *) - -Lemma split_avl : forall s x, avl s -> - avl (split x s)#l /\ avl (split x s)#r. -Proof. - intros s x; functional induction (split x s); simpl; auto. - rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition. - simpl; inversion_clear 1; auto. - rewrite e1 in IHt;simpl in IHt;inversion_clear 1; intuition. -Qed. - -(** inter *) - -Lemma inter_avl : forall s1 s2, avl s1 -> avl s2 -> avl (inter s1 s2). -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. - -(** diff *) - -Lemma diff_avl : forall s1 s2, avl s1 -> avl s2 -> avl (diff s1 s2). -Proof. - 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. - -(** union *) - -Lemma union_avl : forall s1 s2, avl s1 -> avl s2 -> avl (union s1 s2). -Proof. - intros s1 s2; functional induction union s1 s2; auto; intros A1 A2; - generalize (split_avl x1 A2); rewrite e1; simpl; destruct 1; - inv avl; auto. -Qed. - -(** filter *) - -Lemma filter_acc_avl : forall f s acc, avl s -> avl acc -> - avl (filter_acc f acc s). -Proof. - induction s; simpl; auto. - intros. - inv avl. - destruct (f t); auto. -Qed. -Hint Resolve filter_acc_avl. - -Lemma filter_avl : forall f s, avl s -> avl (filter f s). -Proof. - unfold filter; intros; apply filter_acc_avl; auto. -Qed. - -(** partition *) - -Lemma partition_acc_avl_1 : forall f s acc, avl s -> - avl acc#1 -> avl (partition_acc f acc s)#1. -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 f s acc, avl s -> - avl acc#2 -> avl (partition_acc f acc s)#2. -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_avl_1 : forall f s, avl s -> avl (partition f s)#1. -Proof. - unfold partition; intros; apply partition_acc_avl_1; auto. -Qed. - -Lemma partition_avl_2 : forall f s, avl s -> avl (partition f s)#2. -Proof. - unfold partition; intros; apply partition_acc_avl_2; auto. -Qed. - -End AvlProofs. - - -Module OcamlOps (Import I:Int)(X:OrderedType). -Module Import AvlProofs := AvlProofs I X. -Import Raw. -Import Raw.Proofs. -Import II. -Open Local Scope pair_scope. -Open Local Scope nat_scope. - -(** Properties of cardinal *) - -Lemma bal_cardinal : forall l x r, - cardinal (bal l x r) = S (cardinal l + cardinal r). -Proof. - intros l x r; functional induction bal l x r; intros; clearf; - simpl; auto with arith; romega with *. -Qed. - -Lemma add_cardinal : forall x s, - cardinal (add x s) <= S (cardinal s). -Proof. - intros; functional induction add x s; simpl; auto with arith; - rewrite bal_cardinal; romega with *. -Qed. - -Lemma join_cardinal : forall l x r, - cardinal (join l x r) <= S (cardinal l + cardinal r). -Proof. - join_tac; auto with arith. - simpl; apply add_cardinal. - simpl; 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 *. - simpl S in *; generalize (bal_cardinal (join (Node ll lx lr lh) x rl) rx rr). - romega with *. -Qed. - -Lemma split_cardinal_1 : forall x s, - (cardinal (split x s)#l <= cardinal s)%nat. -Proof. - intros x s; functional induction split x s; simpl; auto. - rewrite e1 in IHt; simpl in *. - romega with *. - romega with *. - rewrite e1 in IHt; simpl in *. - generalize (@join_cardinal l y rl); romega with *. -Qed. - -Lemma split_cardinal_2 : forall x s, - (cardinal (split x s)#r <= cardinal s)%nat. -Proof. - intros x s; functional induction split x s; simpl; auto. - rewrite e1 in IHt; simpl in *. - generalize (@join_cardinal rl y r); romega with *. - romega with *. - rewrite e1 in IHt; simpl in *; romega with *. -Qed. - -(** * [ocaml_union], an union faithful to the original ocaml code *) - -Definition cardinal2 (s:t*t) := (cardinal s#1 + cardinal s#2)%nat. - -Ltac ocaml_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 ocaml_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%I then add x2 s#1 else - let (l2',_,r2') := split x1 s#2 in - join (ocaml_union (l1,l2')) x1 (ocaml_union (r1,r2')) - else - if eq_dec h1 1%I then add x1 s#2 else - let (l1',_,r1') := split x2 s#1 in - join (ocaml_union (l1',l2)) x2 (ocaml_union (r1',r2)) - end. -Proof. -abstract ocaml_union_tac. -abstract ocaml_union_tac. -abstract ocaml_union_tac. -abstract ocaml_union_tac. -Defined. - -Lemma ocaml_union_in : forall s y, - bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> - (In y (ocaml_union s) <-> In y s#1 \/ In y s#2). -Proof. - intros s; functional induction ocaml_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; intuition_in. - (* join (union (l1,l2')) x1 (union (r1,r2')) *) - generalize - (split_avl x1 A2) (split_bst x1 B2) - (split_in_1 x1 y B2) (split_in_2 x1 y B2). - rewrite e2; simpl. - destruct 1; destruct 1; inv avl; inv bst. - rewrite join_in, IHt, 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',r2)) *) - generalize - (split_avl x2 A1) (split_bst x2 B1) - (split_in_1 x2 y B1) (split_in_2 x2 y B1). - rewrite e2; simpl. - destruct 1; destruct 1; inv avl; inv bst. - rewrite join_in, IHt, IHt0; auto. - do 2 (intro Eq; rewrite Eq; clear Eq). - case (X.compare y x2); intuition_in. -Qed. - -Lemma ocaml_union_bst : forall s, - bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> bst (ocaml_union s). -Proof. - intros s; functional induction ocaml_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')) *) - clear _x _x0; factornode l2 x2 r2 h2 as s2. - generalize (split_avl x1 A2) (split_bst x1 B2) - (@split_in_1 s2 x1)(@split_in_2 s2 x1). - rewrite e2; simpl. - destruct 1; destruct 1; intros. - inv bst; inv avl. - apply join_bst; auto. - intro y; rewrite ocaml_union_in, H3; intuition_in. - intro y; rewrite ocaml_union_in, H4; intuition_in. - (* join (union (l1',l2)) x1 (union (r1',r2)) *) - clear _x _x0; factornode l1 x1 r1 h1 as s1. - generalize (split_avl x2 A1) (split_bst x2 B1) - (@split_in_1 s1 x2)(@split_in_2 s1 x2). - rewrite e2; simpl. - destruct 1; destruct 1; intros. - inv bst; inv avl. - apply join_bst; auto. - intro y; rewrite ocaml_union_in, H3; intuition_in. - intro y; rewrite ocaml_union_in, H4; intuition_in. -Qed. - -Lemma ocaml_union_avl : forall s, - avl s#1 -> avl s#2 -> avl (ocaml_union s). -Proof. - intros s; functional induction ocaml_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. - -Lemma ocaml_union_alt : forall s, bst s#1 -> avl s#1 -> bst s#2 -> avl s#2 -> - Equal (ocaml_union s) (union s#1 s#2). -Proof. - red; intros; rewrite ocaml_union_in, union_in; simpl; intuition. -Qed. - - -(** * [ocaml_subset], a subset faithful to the original ocaml code *) - -Function ocaml_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 _ => ocaml_subset (l1,l2) && ocaml_subset (r1,r2) - | LT _ => ocaml_subset (Node l1 x1 Leaf 0%I, l2) && ocaml_subset (r1,s#2) - | GT _ => ocaml_subset (Node Leaf x1 r1 0%I, r2) && ocaml_subset (l1,s#2) - end - end. - -Proof. - 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 ocaml_subset_12 : forall s, - bst s#1 -> bst s#2 -> - (ocaml_subset s = true <-> Subset s#1 s#2). -Proof. - intros s; functional induction ocaml_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, IHb, IHb0; auto; clear IHb IHb0. - unfold Subset; intuition_in. - assert (X.eq a x2) by order; 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, IHb, 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, IHb, 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 ocaml_subset_alt : forall s, bst s#1 -> bst s#2 -> - ocaml_subset s = subset s#1 s#2. -Proof. - intros. - generalize (ocaml_subset_12 H H0); rewrite <-subset_12 by auto. - destruct ocaml_subset; destruct subset; intuition. -Qed. - - - -(** [ocaml_compare], a compare faithful to the original ocaml code *) - -(** termination of [compare_aux] *) - -Fixpoint cardinal_e e := match e with - | End => 0 - | More _ s r => S (cardinal s + cardinal_e r) - end. - -Lemma cons_cardinal_e : forall s e, - cardinal_e (cons s e) = cardinal s + cardinal_e e. -Proof. - induction s; simpl; intros; auto. - rewrite IHs1; simpl; rewrite <- plus_n_Sm; auto with arith. -Qed. - -Definition cardinal_e_2 e := cardinal_e e#1 + cardinal_e e#2. - -Function ocaml_compare_aux - (e:enumeration*enumeration) { measure cardinal_e_2 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 _ => ocaml_compare_aux (cons r1 e1, cons r2 e2) - | LT _ => Lt - | GT _ => Gt - end - end. - -Proof. -intros; unfold cardinal_e_2; simpl; -abstract (do 2 rewrite cons_cardinal_e; romega with *). -Defined. - -Definition ocaml_compare s1 s2 := - ocaml_compare_aux (cons s1 End, cons s2 End). - -Lemma ocaml_compare_aux_Cmp : forall e, - Cmp (ocaml_compare_aux e) (flatten_e e#1) (flatten_e e#2). -Proof. - intros e; functional induction ocaml_compare_aux e; simpl; intros; - auto; try discriminate. - apply L.eq_refl. - simpl in *. - apply cons_Cmp; auto. - rewrite <- 2 cons_1; auto. -Qed. - -Lemma ocaml_compare_Cmp : forall s1 s2, - Cmp (ocaml_compare s1 s2) (elements s1) (elements s2). -Proof. - unfold ocaml_compare; intros. - assert (H1:=cons_1 s1 End). - assert (H2:=cons_1 s2 End). - simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2. - apply (@ocaml_compare_aux_Cmp (cons s1 End, cons s2 End)). -Qed. - -Lemma ocaml_compare_alt : forall s1 s2, bst s1 -> bst s2 -> - ocaml_compare s1 s2 = compare s1 s2. -Proof. - intros s1 s2 B1 B2. - generalize (ocaml_compare_Cmp s1 s2)(compare_Cmp s1 s2). - unfold Cmp. - destruct ocaml_compare; destruct compare; auto; intros; exfalso. - elim (lt_not_eq B1 B2 H0); auto. - elim (lt_not_eq B2 B1 H0); auto. - apply eq_sym; auto. - elim (lt_not_eq B1 B2 H); auto. - elim (lt_not_eq B1 B1). - red; eapply L.lt_trans; eauto. - apply eq_refl. - elim (lt_not_eq B2 B1 H); auto. - apply eq_sym; auto. - elim (lt_not_eq B1 B2 H0); auto. - elim (lt_not_eq B1 B1). - red; eapply L.lt_trans; eauto. - apply eq_refl. -Qed. - - -(** * Equality test *) - -Definition ocaml_equal s1 s2 : bool := - match ocaml_compare s1 s2 with - | Eq => true - | _ => false - end. - -Lemma ocaml_equal_1 : forall s1 s2, bst s1 -> bst s2 -> - Equal s1 s2 -> ocaml_equal s1 s2 = true. -Proof. -unfold ocaml_equal; intros s1 s2 B1 B2 E. -generalize (ocaml_compare_Cmp s1 s2). -destruct (ocaml_compare s1 s2); auto; intros. -elim (lt_not_eq B1 B2 H E); auto. -elim (lt_not_eq B2 B1 H (eq_sym E)); auto. -Qed. - -Lemma ocaml_equal_2 : forall s1 s2, - ocaml_equal s1 s2 = true -> Equal s1 s2. -Proof. -unfold ocaml_equal; intros s1 s2 E. -generalize (ocaml_compare_Cmp s1 s2); - destruct ocaml_compare; auto; discriminate. -Qed. - -Lemma ocaml_equal_alt : forall s1 s2, bst s1 -> bst s2 -> - ocaml_equal s1 s2 = equal s1 s2. -Proof. -intros; unfold ocaml_equal, equal; rewrite ocaml_compare_alt; auto. -Qed. - -End OcamlOps. - - - -(** * Encapsulation - - We can implement [S] with balanced binary search trees. - When compared to [FSetAVL], we maintain here two invariants - (bst and avl) instead of only bst, which is enough for fulfilling - the FSet interface. - - This encapsulation propose the non-structural variants - [ocaml_union], [ocaml_subset], [ocaml_compare], [ocaml_equal]. -*) - -Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. - - Module E := X. - Module Import OcamlOps := OcamlOps I X. - Import AvlProofs. - Import Raw. - Import Raw.Proofs. - - Record bbst := Bbst {this :> Raw.t; is_bst : bst this; is_avl : avl this}. - Definition t := bbst. - Definition elt := E.t. - - Definition In (x : elt) (s : t) : Prop := In x s. - Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'. - Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'. - Definition Empty (s:t) : Prop := forall a : elt, ~ In a s. - Definition For_all (P : elt -> Prop) (s:t) : Prop := forall x, In x s -> P x. - Definition Exists (P : elt -> Prop) (s:t) : Prop := exists x, In x s /\ P x. - - Lemma In_1 : forall (s:t)(x y:elt), E.eq x y -> In x s -> In y s. - Proof. intro s; exact (@In_1 s). Qed. - - Definition mem (x:elt)(s:t) : bool := mem x s. - - Definition empty : t := Bbst empty_bst empty_avl. - Definition is_empty (s:t) : bool := is_empty s. - Definition singleton (x:elt) : t := - Bbst (singleton_bst x) (singleton_avl x). - Definition add (x:elt)(s:t) : t := - Bbst (add_bst x (is_bst s)) (add_avl x (is_avl s)). - Definition remove (x:elt)(s:t) : t := - Bbst (remove_bst x (is_bst s)) (remove_avl x (is_avl s)). - Definition inter (s s':t) : t := - Bbst (inter_bst (is_bst s) (is_bst s')) - (inter_avl (is_avl s) (is_avl s')). - Definition union (s s':t) : t := - Bbst (union_bst (is_bst s) (is_bst s')) - (union_avl (is_avl s) (is_avl s')). - Definition ocaml_union (s s':t) : t := - Bbst (@ocaml_union_bst (s.(this),s'.(this)) - (is_bst s) (is_avl s) (is_bst s') (is_avl s')) - (@ocaml_union_avl (s.(this),s'.(this)) (is_avl s) (is_avl s')). - Definition diff (s s':t) : t := - Bbst (diff_bst (is_bst s) (is_bst s')) - (diff_avl (is_avl s) (is_avl s')). - Definition elements (s:t) : list elt := elements s. - Definition min_elt (s:t) : option elt := min_elt s. - Definition max_elt (s:t) : option elt := max_elt s. - Definition choose (s:t) : option elt := choose s. - Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := fold f s. - Definition cardinal (s:t) : nat := cardinal s. - Definition filter (f : elt -> bool) (s:t) : t := - Bbst (filter_bst f (is_bst s)) (filter_avl f (is_avl s)). - Definition for_all (f : elt -> bool) (s:t) : bool := for_all f s. - Definition exists_ (f : elt -> bool) (s:t) : bool := exists_ f s. - Definition partition (f : elt -> bool) (s:t) : t * t := - let p := partition f s in - (@Bbst (fst p) (partition_bst_1 f (is_bst s)) - (partition_avl_1 f (is_avl s)), - @Bbst (snd p) (partition_bst_2 f (is_bst s)) - (partition_avl_2 f (is_avl s))). - - Definition equal (s s':t) : bool := equal s s'. - Definition ocaml_equal (s s':t) : bool := ocaml_equal s s'. - Definition subset (s s':t) : bool := subset s s'. - Definition ocaml_subset (s s':t) : bool := - ocaml_subset (s.(this),s'.(this)). - - Definition eq (s s':t) : Prop := Equal s s'. - Definition lt (s s':t) : Prop := lt s s'. - - Definition compare (s s':t) : Compare lt eq s s'. - Proof. - intros (s,b,a) (s',b',a'). - generalize (compare_Cmp s s'). - destruct Raw.compare; intros; [apply EQ|apply LT|apply GT]; red; auto. - change (Raw.Equal s s'); auto. - Defined. - - Definition ocaml_compare (s s':t) : Compare lt eq s s'. - Proof. - intros (s,b,a) (s',b',a'). - generalize (ocaml_compare_Cmp s s'). - destruct ocaml_compare; intros; [apply EQ|apply LT|apply GT]; red; auto. - change (Raw.Equal s s'); auto. - Defined. - - Definition eq_dec (s s':t) : { eq s s' } + { ~ eq s s' }. - Proof. - intros (s,b,a) (s',b',a'); unfold eq; simpl. - case_eq (Raw.equal s s'); intro H; [left|right]. - apply equal_2; auto. - intro H'; rewrite equal_1 in H; auto; discriminate. - Defined. - - (* specs *) - Section Specs. - Variable s s' s'': t. - Variable x y : elt. - - Hint Resolve is_bst is_avl. - - Lemma mem_1 : In x s -> mem x s = true. - Proof. exact (mem_1 (is_bst s)). Qed. - Lemma mem_2 : mem x s = true -> In x s. - Proof. exact (@mem_2 s x). Qed. - - Lemma equal_1 : Equal s s' -> equal s s' = true. - Proof. exact (equal_1 (is_bst s) (is_bst s')). Qed. - Lemma equal_2 : equal s s' = true -> Equal s s'. - Proof. exact (@equal_2 s s'). Qed. - - Lemma ocaml_equal_alt : ocaml_equal s s' = equal s s'. - Proof. - destruct s; destruct s'; unfold ocaml_equal, equal; simpl. - apply ocaml_equal_alt; auto. - Qed. - - Lemma ocaml_equal_1 : Equal s s' -> ocaml_equal s s' = true. - Proof. exact (ocaml_equal_1 (is_bst s) (is_bst s')). Qed. - Lemma ocaml_equal_2 : ocaml_equal s s' = true -> Equal s s'. - Proof. exact (@ocaml_equal_2 s s'). Qed. - - Ltac wrap t H := unfold t, In; simpl; rewrite H; auto; intuition. - - Lemma subset_1 : Subset s s' -> subset s s' = true. - Proof. wrap subset subset_12. Qed. - Lemma subset_2 : subset s s' = true -> Subset s s'. - Proof. wrap subset subset_12. Qed. - - Lemma ocaml_subset_alt : ocaml_subset s s' = subset s s'. - Proof. - destruct s; destruct s'; unfold ocaml_subset, subset; simpl. - rewrite ocaml_subset_alt; auto. - Qed. - - Lemma ocaml_subset_1 : Subset s s' -> ocaml_subset s s' = true. - Proof. wrap ocaml_subset ocaml_subset_12; simpl; auto. Qed. - Lemma ocaml_subset_2 : ocaml_subset s s' = true -> Subset s s'. - Proof. wrap ocaml_subset ocaml_subset_12; simpl; auto. Qed. - - Lemma empty_1 : Empty empty. - Proof. exact empty_1. Qed. - - Lemma is_empty_1 : Empty s -> is_empty s = true. - Proof. exact (@is_empty_1 s). Qed. - Lemma is_empty_2 : is_empty s = true -> Empty s. - Proof. exact (@is_empty_2 s). Qed. - - Lemma add_1 : E.eq x y -> In y (add x s). - Proof. wrap add add_in. Qed. - Lemma add_2 : In y s -> In y (add x s). - Proof. wrap add add_in. Qed. - Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. - Proof. wrap add add_in. elim H; auto. Qed. - - Lemma remove_1 : E.eq x y -> ~ In y (remove x s). - Proof. wrap remove remove_in. Qed. - Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). - Proof. wrap remove remove_in. Qed. - Lemma remove_3 : In y (remove x s) -> In y s. - Proof. wrap remove remove_in. Qed. - - Lemma singleton_1 : In y (singleton x) -> E.eq x y. - Proof. exact (@singleton_1 x y). Qed. - Lemma singleton_2 : E.eq x y -> In y (singleton x). - Proof. exact (@singleton_2 x y). Qed. - - Lemma union_1 : In x (union s s') -> In x s \/ In x s'. - Proof. wrap union union_in. Qed. - Lemma union_2 : In x s -> In x (union s s'). - Proof. wrap union union_in. Qed. - Lemma union_3 : In x s' -> In x (union s s'). - Proof. wrap union union_in. Qed. - - Lemma ocaml_union_alt : Equal (ocaml_union s s') (union s s'). - Proof. - unfold ocaml_union, union, Equal, In. - destruct s as (s0,b,a); destruct s' as (s0',b',a'); simpl. - exact (@ocaml_union_alt (s0,s0') b a b' a'). - Qed. - - Lemma ocaml_union_1 : In x (ocaml_union s s') -> In x s \/ In x s'. - Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed. - Lemma ocaml_union_2 : In x s -> In x (ocaml_union s s'). - Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed. - Lemma ocaml_union_3 : In x s' -> In x (ocaml_union s s'). - Proof. wrap ocaml_union ocaml_union_in; simpl; auto. Qed. - - Lemma inter_1 : In x (inter s s') -> In x s. - Proof. wrap inter inter_in. Qed. - Lemma inter_2 : In x (inter s s') -> In x s'. - Proof. wrap inter inter_in. Qed. - Lemma inter_3 : In x s -> In x s' -> In x (inter s s'). - Proof. wrap inter inter_in. Qed. - - Lemma diff_1 : In x (diff s s') -> In x s. - Proof. wrap diff diff_in. Qed. - Lemma diff_2 : In x (diff s s') -> ~ In x s'. - Proof. wrap diff diff_in. Qed. - Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s'). - Proof. wrap diff diff_in. 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. - Proof. - unfold fold, elements; intros; apply fold_1; auto. - Qed. - - Lemma cardinal_1 : cardinal s = length (elements s). - Proof. - unfold cardinal, elements; intros; apply elements_cardinal; 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. wrap filter filter_in. Qed. - Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. - Proof. intro. wrap filter filter_in. Qed. - Lemma filter_3 : compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). - Proof. intro. wrap filter filter_in. Qed. - - Lemma for_all_1 : compat_bool E.eq f -> For_all (fun x => f x = true) s -> for_all f s = true. - Proof. exact (@for_all_1 f s). Qed. - Lemma for_all_2 : compat_bool E.eq f -> for_all f s = true -> For_all (fun x => f x = true) s. - Proof. exact (@for_all_2 f s). Qed. - - Lemma exists_1 : compat_bool E.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. - Proof. exact (@exists_1 f s). Qed. - Lemma exists_2 : compat_bool E.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. - Proof. exact (@exists_2 f s). Qed. - - 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, 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, filter_in; intuition. - rewrite H2; auto. - destruct (f a); auto. - repeat red; intros; f_equal. - rewrite (H _ _ H0); auto. - Qed. - - End Filter. - - Lemma elements_1 : In x s -> InA E.eq x (elements s). - Proof. wrap elements elements_in. Qed. - Lemma elements_2 : InA E.eq x (elements s) -> In x s. - Proof. wrap elements elements_in. Qed. - Lemma elements_3 : sort E.lt (elements s). - Proof. exact (elements_sort (is_bst s)). Qed. - Lemma elements_3w : NoDupA E.eq (elements s). - Proof. exact (elements_nodup (is_bst s)). Qed. - - Lemma min_elt_1 : min_elt s = Some x -> In x s. - Proof. exact (@min_elt_1 s x). Qed. - Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. - Proof. exact (@min_elt_2 s x y (is_bst s)). Qed. - Lemma min_elt_3 : min_elt s = None -> Empty s. - Proof. exact (@min_elt_3 s). Qed. - - Lemma max_elt_1 : max_elt s = Some x -> In x s. - Proof. exact (@max_elt_1 s x). Qed. - Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. - Proof. exact (@max_elt_2 s x y (is_bst s)). Qed. - Lemma max_elt_3 : max_elt s = None -> Empty s. - Proof. exact (@max_elt_3 s). Qed. - - Lemma choose_1 : choose s = Some x -> In x s. - Proof. exact (@choose_1 s x). Qed. - Lemma choose_2 : choose s = None -> Empty s. - Proof. exact (@choose_2 s). Qed. - Lemma choose_3 : choose s = Some x -> choose s' = Some y -> - Equal s s' -> E.eq x y. - Proof. exact (@choose_3 _ _ (is_bst s) (is_bst s') x y). Qed. - - Lemma eq_refl : eq s s. - Proof. exact (eq_refl s). Qed. - Lemma eq_sym : eq s s' -> eq s' s. - Proof. exact (@eq_sym s s'). Qed. - Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''. - Proof. exact (@eq_trans s s' s''). Qed. - - Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''. - Proof. exact (@lt_trans s s' s''). Qed. - Lemma lt_not_eq : lt s s' -> ~eq s s'. - Proof. exact (@lt_not_eq _ _ (is_bst s) (is_bst s')). Qed. - - 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/FSetList.v b/theories/FSets/FSetList.v index eb6f7b222..950f48a90 100644 --- a/theories/FSets/FSetList.v +++ b/theories/FSets/FSetList.v @@ -17,1260 +17,13 @@ Require Export FSetInterface. Set Implicit Arguments. Unset Strict Implicit. -(** * Functions over lists +(** This is just a compatibility layer, the real implementation + is now in [MSetList] *) - First, we provide sets as lists which are not necessarily sorted. - The specs are proved under the additional condition of being sorted. - And the functions returning sets are proved to preserve this invariant. *) - -Module Raw (X: OrderedType). - - Module MX := OrderedTypeFacts X. - Import MX. - - Definition elt := X.t. - Definition t := list elt. - - Definition empty : t := nil. - - Definition is_empty (l : t) : bool := if l then true else false. - - (** ** The set operations. *) - - Fixpoint mem (x : elt) (s : t) {struct s} : bool := - match s with - | nil => false - | y :: l => - match X.compare x y with - | LT _ => false - | EQ _ => true - | GT _ => mem x l - end - end. - - Fixpoint add (x : elt) (s : t) {struct s} : t := - match s with - | nil => x :: nil - | y :: l => - match X.compare x y with - | LT _ => x :: s - | EQ _ => s - | GT _ => y :: add x l - end - end. - - Definition singleton (x : elt) : t := x :: nil. - - Fixpoint remove (x : elt) (s : t) {struct s} : t := - match s with - | nil => nil - | y :: l => - match X.compare x y with - | LT _ => s - | EQ _ => l - | GT _ => y :: remove x l - end - end. - - Fixpoint union (s : t) : t -> t := - match s with - | nil => fun s' => s' - | x :: l => - (fix union_aux (s' : t) : t := - match s' with - | nil => s - | x' :: l' => - match X.compare x x' with - | LT _ => x :: union l s' - | EQ _ => x :: union l l' - | GT _ => x' :: union_aux l' - end - end) - end. - - Fixpoint inter (s : t) : t -> t := - match s with - | nil => fun _ => nil - | x :: l => - (fix inter_aux (s' : t) : t := - match s' with - | nil => nil - | x' :: l' => - match X.compare x x' with - | LT _ => inter l s' - | EQ _ => x :: inter l l' - | GT _ => inter_aux l' - end - end) - end. - - Fixpoint diff (s : t) : t -> t := - match s with - | nil => fun _ => nil - | x :: l => - (fix diff_aux (s' : t) : t := - match s' with - | nil => s - | x' :: l' => - match X.compare x x' with - | LT _ => x :: diff l s' - | EQ _ => diff l l' - | GT _ => diff_aux l' - end - end) - end. - - Fixpoint equal (s : t) : t -> bool := - fun s' : t => - match s, s' with - | nil, nil => true - | x :: l, x' :: l' => - match X.compare x x' with - | EQ _ => equal l l' - | _ => false - end - | _, _ => false - end. - - Fixpoint subset (s s' : t) {struct s'} : bool := - match s, s' with - | nil, _ => true - | x :: l, x' :: l' => - match X.compare x x' with - | LT _ => false - | EQ _ => subset l l' - | GT _ => subset s l' - end - | _, _ => false - end. - - Fixpoint fold (B : Type) (f : elt -> B -> B) (s : t) {struct s} : - B -> B := fun i => match s with - | nil => i - | x :: l => fold f l (f x i) - end. - - Fixpoint filter (f : elt -> bool) (s : t) {struct s} : t := - match s with - | nil => nil - | x :: l => if f x then x :: filter f l else filter f l - end. - - Fixpoint for_all (f : elt -> bool) (s : t) {struct s} : bool := - match s with - | nil => true - | x :: l => if f x then for_all f l else false - end. - - Fixpoint exists_ (f : elt -> bool) (s : t) {struct s} : bool := - match s with - | nil => false - | x :: l => if f x then true else exists_ f l - end. - - Fixpoint partition (f : elt -> bool) (s : t) {struct s} : - t * t := - match s with - | nil => (nil, nil) - | x :: l => - let (s1, s2) := partition f l in - if f x then (x :: s1, s2) else (s1, x :: s2) - end. - - Definition cardinal (s : t) : nat := length s. - - Definition elements (x : t) : list elt := x. - - Definition min_elt (s : t) : option elt := - match s with - | nil => None - | x :: _ => Some x - end. - - Fixpoint max_elt (s : t) : option elt := - match s with - | nil => None - | x :: nil => Some x - | _ :: l => max_elt l - end. - - Definition choose := min_elt. - - (** ** Proofs of set operation specifications. *) - - Section ForNotations. - - Notation Sort := (sort X.lt). - Notation Inf := (lelistA X.lt). - Notation In := (InA X.eq). - - 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 : t) := exists x, In x s /\ P x. - - Lemma mem_1 : - forall (s : t) (Hs : Sort s) (x : elt), In x s -> mem x s = true. - Proof. - simple induction s; intros. - inversion H. - inversion_clear Hs. - inversion_clear H0. - simpl; elim_comp; trivial. - simpl; elim_comp_gt x a; auto. - apply Sort_Inf_In with l; trivial. - Qed. - - Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s. - Proof. - simple induction s. - intros; inversion H. - intros a l Hrec x. - simpl. - case (X.compare x a); intros; try discriminate; auto. - Qed. - - Lemma add_Inf : - forall (s : t) (x a : elt), Inf a s -> X.lt a x -> Inf a (add x s). - Proof. - simple induction s. - simpl; intuition. - simpl; intros; case (X.compare x a); intuition; inversion H0; - intuition. - Qed. - Hint Resolve add_Inf. - - Lemma add_sort : forall (s : t) (Hs : Sort s) (x : elt), Sort (add x s). - Proof. - simple induction s. - simpl; intuition. - simpl; intros; case (X.compare x a); intuition; inversion_clear Hs; - auto. - Qed. - - Lemma add_1 : - forall (s : t) (Hs : Sort s) (x y : elt), X.eq x y -> In y (add x s). - Proof. - simple induction s. - simpl; intuition. - simpl; intros; case (X.compare x a); inversion_clear Hs; auto. - constructor; apply X.eq_trans with x; auto. - Qed. - - Lemma add_2 : - forall (s : t) (Hs : Sort s) (x y : elt), In y s -> In y (add x s). - Proof. - simple induction s. - simpl; intuition. - simpl; intros; case (X.compare x a); intuition. - inversion_clear Hs; inversion_clear H0; auto. - Qed. - - Lemma add_3 : - forall (s : t) (Hs : Sort s) (x y : elt), - ~ X.eq x y -> In y (add x s) -> In y s. - Proof. - simple induction s. - simpl; inversion_clear 3; auto; order. - simpl; intros a l Hrec Hs x y; case (X.compare x a); intros; - inversion_clear H0; inversion_clear Hs; auto. - order. - constructor 2; apply Hrec with x; auto. - Qed. - - Lemma remove_Inf : - forall (s : t) (Hs : Sort s) (x a : elt), Inf a s -> Inf a (remove x s). - Proof. - simple induction s. - simpl; intuition. - simpl; intros; case (X.compare x a); intuition; inversion_clear H0; auto. - inversion_clear Hs; apply Inf_lt with a; auto. - Qed. - Hint Resolve remove_Inf. - - Lemma remove_sort : - forall (s : t) (Hs : Sort s) (x : elt), Sort (remove x s). - Proof. - simple induction s. - simpl; intuition. - simpl; intros; case (X.compare x a); intuition; inversion_clear Hs; auto. - Qed. - - Lemma remove_1 : - forall (s : t) (Hs : Sort s) (x y : elt), X.eq x y -> ~ In y (remove x s). - Proof. - simple induction s. - simpl; red; intros; inversion H0. - simpl; intros; case (X.compare x a); intuition; inversion_clear Hs. - inversion_clear H1. - order. - generalize (Sort_Inf_In H2 H3 H4); order. - generalize (Sort_Inf_In H2 H3 H1); order. - inversion_clear H1. - order. - apply (H H2 _ _ H0 H4). - Qed. - - Lemma remove_2 : - forall (s : t) (Hs : Sort s) (x y : elt), - ~ X.eq x y -> In y s -> In y (remove x s). - Proof. - simple induction s. - simpl; intuition. - simpl; intros; case (X.compare x a); intuition; inversion_clear Hs; - inversion_clear H1; auto. - destruct H0; apply X.eq_trans with a; auto. - Qed. - - Lemma remove_3 : - forall (s : t) (Hs : Sort s) (x y : elt), In y (remove x s) -> In y s. - Proof. - simple induction s. - simpl; intuition. - simpl; intros a l Hrec Hs x y; case (X.compare x a); intuition. - inversion_clear Hs; inversion_clear H; auto. - constructor 2; apply Hrec with x; auto. - Qed. - - Lemma singleton_sort : forall x : elt, Sort (singleton x). - Proof. - unfold singleton; simpl; auto. - Qed. - - Lemma singleton_1 : forall x y : elt, In y (singleton x) -> X.eq x y. - Proof. - unfold singleton; simpl; intuition. - inversion_clear H; auto; inversion H0. - Qed. - - Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x). - Proof. - unfold singleton; simpl; auto. - Qed. - - Ltac DoubleInd := - simple induction s; - [ simpl; auto; try solve [ intros; inversion H ] - | intros x l Hrec; simple induction s'; - [ simpl; auto; try solve [ intros; inversion H ] - | intros x' l' Hrec' Hs Hs'; inversion Hs; inversion Hs'; subst; - simpl ] ]. - - Lemma union_Inf : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (a : elt), - Inf a s -> Inf a s' -> Inf a (union s s'). - Proof. - DoubleInd. - intros i His His'; inversion_clear His; inversion_clear His'. - case (X.compare x x'); auto. - Qed. - Hint Resolve union_Inf. - - Lemma union_sort : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (union s s'). - Proof. - DoubleInd; case (X.compare x x'); intuition; constructor; auto. - apply Inf_eq with x'; trivial; apply union_Inf; trivial; apply Inf_eq with x; auto. - change (Inf x' (union (x :: l) l')); auto. - Qed. - - Lemma union_1 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt), - In x (union s s') -> In x s \/ In x s'. - Proof. - DoubleInd; case (X.compare x x'); intuition; inversion_clear H; intuition. - elim (Hrec (x' :: l') H1 Hs' x0); intuition. - elim (Hrec l' H1 H5 x0); intuition. - elim (H0 x0); intuition. - Qed. - - Lemma union_2 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt), - In x s -> In x (union s s'). - Proof. - DoubleInd. - intros i Hi; case (X.compare x x'); intuition; inversion_clear Hi; auto. - Qed. - - Lemma union_3 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt), - In x s' -> In x (union s s'). - Proof. - DoubleInd. - intros i Hi; case (X.compare x x'); inversion_clear Hi; intuition. - constructor; apply X.eq_trans with x'; auto. - Qed. - - Lemma inter_Inf : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (a : elt), - Inf a s -> Inf a s' -> Inf a (inter s s'). - Proof. - DoubleInd. - intros i His His'; inversion His; inversion His'; subst. - case (X.compare x x'); intuition. - apply Inf_lt with x; auto. - apply H3; auto. - apply Inf_lt with x'; auto. - Qed. - Hint Resolve inter_Inf. - - Lemma inter_sort : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (inter s s'). - Proof. - DoubleInd; case (X.compare x x'); auto. - constructor; auto. - apply Inf_eq with x'; trivial; apply inter_Inf; trivial; apply Inf_eq with x; auto. - Qed. - - Lemma inter_1 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt), - In x (inter s s') -> In x s. - Proof. - DoubleInd; case (X.compare x x'); intuition. - constructor 2; apply Hrec with (x'::l'); auto. - inversion_clear H; auto. - constructor 2; apply Hrec with l'; auto. - Qed. - - Lemma inter_2 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt), - In x (inter s s') -> In x s'. - Proof. - DoubleInd; case (X.compare x x'); intuition; inversion_clear H. - constructor 1; apply X.eq_trans with x; auto. - constructor 2; auto. - Qed. - - Lemma inter_3 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt), - In x s -> In x s' -> In x (inter s s'). - Proof. - DoubleInd. - intros i His His'; elim (X.compare x x'); intuition. - - inversion_clear His; auto. - generalize (Sort_Inf_In Hs' (cons_leA _ _ _ _ l0) His'); order. - - inversion_clear His; auto; inversion_clear His'; auto. - constructor; apply X.eq_trans with x'; auto. - - change (In i (inter (x :: l) l')). - inversion_clear His'; auto. - generalize (Sort_Inf_In Hs (cons_leA _ _ _ _ l0) His); order. - Qed. - - Lemma diff_Inf : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (a : elt), - Inf a s -> Inf a s' -> Inf a (diff s s'). - Proof. - DoubleInd. - intros i His His'; inversion His; inversion His'. - case (X.compare x x'); intuition. - apply Hrec; trivial. - apply Inf_lt with x; auto. - apply Inf_lt with x'; auto. - apply H10; trivial. - apply Inf_lt with x'; auto. - Qed. - Hint Resolve diff_Inf. - - Lemma diff_sort : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Sort (diff s s'). - Proof. - DoubleInd; case (X.compare x x'); auto. - Qed. - - Lemma diff_1 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt), - In x (diff s s') -> In x s. - Proof. - DoubleInd; case (X.compare x x'); intuition. - inversion_clear H; auto. - constructor 2; apply Hrec with (x'::l'); auto. - constructor 2; apply Hrec with l'; auto. - Qed. - - Lemma diff_2 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt), - In x (diff s s') -> ~ In x s'. - Proof. - DoubleInd. - intros; intro Abs; inversion Abs. - case (X.compare x x'); intuition. - - inversion_clear H. - generalize (Sort_Inf_In Hs' (cons_leA _ _ _ _ l0) H3); order. - apply Hrec with (x'::l') x0; auto. - - inversion_clear H3. - generalize (Sort_Inf_In H1 H2 (diff_1 H1 H5 H)); order. - apply Hrec with l' x0; auto. - - inversion_clear H3. - generalize (Sort_Inf_In Hs (cons_leA _ _ _ _ l0) (diff_1 Hs H5 H)); order. - apply H0 with x0; auto. - Qed. - - Lemma diff_3 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s') (x : elt), - In x s -> ~ In x s' -> In x (diff s s'). - Proof. - DoubleInd. - intros i His His'; elim (X.compare x x'); intuition; inversion_clear His; auto. - elim His'; constructor; apply X.eq_trans with x; auto. - Qed. - - Lemma equal_1 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), - Equal s s' -> equal s s' = true. - Proof. - simple induction s; unfold Equal. - intro s'; case s'; auto. - simpl; intuition. - elim (H e); intros; assert (A : In e nil); auto; inversion A. - intros x l Hrec s'. - case s'. - intros; elim (H x); intros; assert (A : In x nil); auto; inversion A. - intros x' l' Hs Hs'; inversion Hs; inversion Hs'; subst. - simpl; case (X.compare x); intros; auto. - - elim (H x); intros. - assert (A : In x (x' :: l')); auto; inversion_clear A. - order. - generalize (Sort_Inf_In H5 H6 H4); order. - - apply Hrec; intuition; elim (H a); intros. - assert (A : In a (x' :: l')); auto; inversion_clear A; auto. - generalize (Sort_Inf_In H1 H2 H0); order. - assert (A : In a (x :: l)); auto; inversion_clear A; auto. - generalize (Sort_Inf_In H5 H6 H0); order. - - elim (H x'); intros. - assert (A : In x' (x :: l)); auto; inversion_clear A. - order. - generalize (Sort_Inf_In H1 H2 H4); order. - Qed. - - Lemma equal_2 : forall s s' : t, equal s s' = true -> Equal s s'. - Proof. - simple induction s; unfold Equal. - intro s'; case s'; intros. - intuition. - simpl in H; discriminate H. - intros x l Hrec s'. - case s'. - intros; simpl in H; discriminate. - intros x' l'; simpl; case (X.compare x); intros; auto; try discriminate. - elim (Hrec l' H a); intuition; inversion_clear H2; auto. - constructor; apply X.eq_trans with x; auto. - constructor; apply X.eq_trans with x'; auto. - Qed. - - Lemma subset_1 : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), - Subset s s' -> subset s s' = true. - Proof. - intros s s'; generalize s' s; clear s s'. - simple induction s'; unfold Subset. - intro s; case s; auto. - intros; elim (H e); intros; assert (A : In e nil); auto; inversion A. - intros x' l' Hrec s; case s. - simpl; auto. - intros x l Hs Hs'; inversion Hs; inversion Hs'; subst. - simpl; case (X.compare x); intros; auto. - - assert (A : In x (x' :: l')); auto; inversion_clear A. - order. - generalize (Sort_Inf_In H5 H6 H0); order. - - apply Hrec; intuition. - assert (A : In a (x' :: l')); auto; inversion_clear A; auto. - generalize (Sort_Inf_In H1 H2 H0); order. - - apply Hrec; intuition. - assert (A : In a (x' :: l')); auto; inversion_clear A; auto. - inversion_clear H0. - order. - generalize (Sort_Inf_In H1 H2 H4); order. - Qed. - - Lemma subset_2 : forall s s' : t, subset s s' = true -> Subset s s'. - Proof. - intros s s'; generalize s' s; clear s s'. - simple induction s'; unfold Subset. - intro s; case s; auto. - simpl; intros; discriminate H. - intros x' l' Hrec s; case s. - intros; inversion H0. - intros x l; simpl; case (X.compare x); intros; auto. - discriminate H. - inversion_clear H0. - constructor; apply X.eq_trans with x; auto. - constructor 2; apply Hrec with l; auto. - constructor 2; apply Hrec with (x::l); auto. - Qed. - - Lemma empty_sort : Sort empty. - Proof. - unfold empty; constructor. - Qed. - - Lemma empty_1 : Empty empty. - Proof. - unfold Empty, empty; intuition; inversion H. - Qed. - - Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true. - Proof. - unfold Empty; intro s; case s; simpl; intuition. - elim (H e); auto. - Qed. - - Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s. - Proof. - unfold Empty; intro s; case s; simpl; intuition; - inversion H0. - Qed. - - Lemma elements_1 : forall (s : t) (x : elt), In x s -> In x (elements s). - Proof. - unfold elements; auto. - Qed. - - Lemma elements_2 : forall (s : t) (x : elt), In x (elements s) -> In x s. - Proof. - unfold elements; auto. - Qed. - - Lemma elements_3 : forall (s : t) (Hs : Sort s), Sort (elements s). - Proof. - unfold elements; auto. - Qed. - - Lemma elements_3w : forall (s : t) (Hs : Sort s), NoDupA X.eq (elements s). - Proof. - unfold elements; auto. - Qed. - - Lemma min_elt_1 : forall (s : t) (x : elt), min_elt s = Some x -> In x s. - Proof. - intro s; case s; simpl; intros; inversion H; auto. - Qed. - - Lemma min_elt_2 : - forall (s : t) (Hs : Sort s) (x y : elt), - min_elt s = Some x -> In y s -> ~ X.lt y x. - Proof. - simple induction s; simpl. - intros; inversion H. - intros a l; case l; intros; inversion H0; inversion_clear H1; subst. - order. - inversion H2. - order. - inversion_clear Hs. - inversion_clear H3. - generalize (H H1 e y (refl_equal (Some e)) H2); order. - Qed. - - Lemma min_elt_3 : forall s : t, min_elt s = None -> Empty s. - Proof. - unfold Empty; intro s; case s; simpl; intuition; - inversion H; inversion H0. - Qed. - - Lemma max_elt_1 : forall (s : t) (x : elt), max_elt s = Some x -> In x s. - Proof. - simple induction s; simpl. - intros; inversion H. - intros x l; case l; simpl. - intuition. - inversion H0; auto. - intros. - constructor 2; apply (H _ H0). - Qed. - - Lemma max_elt_2 : - forall (s : t) (Hs : Sort s) (x y : elt), - max_elt s = Some x -> In y s -> ~ X.lt x y. - Proof. - simple induction s; simpl. - intros; inversion H. - intros x l; case l; simpl. - intuition. - inversion H0; subst. - inversion_clear H1. - order. - inversion H3. - intros; inversion_clear Hs; inversion_clear H3; inversion_clear H1. - assert (In e (e::l0)) by auto. - generalize (H H2 x0 e H0 H1); order. - generalize (H H2 x0 y H0 H3); order. - Qed. - - Lemma max_elt_3 : forall s : t, max_elt s = None -> Empty s. - Proof. - unfold Empty; simple induction s; simpl. - red; intros; inversion H0. - intros x l; case l; simpl; intros. - inversion H0. - elim (H H0 e); auto. - Qed. - - Definition choose_1 : - forall (s : t) (x : elt), choose s = Some x -> In x s := min_elt_1. - - Definition choose_2 : forall s : t, choose s = None -> Empty s := min_elt_3. - - Lemma choose_3: forall s s', Sort s -> Sort s' -> forall x x', - choose s = Some x -> choose s' = Some x' -> Equal s s' -> X.eq x x'. - Proof. - unfold choose, Equal; intros s s' Hs Hs' x x' Hx Hx' H. - assert (~X.lt x x'). - apply min_elt_2 with s'; auto. - rewrite <-H; auto using min_elt_1. - assert (~X.lt x' x). - apply min_elt_2 with s; auto. - rewrite H; auto using min_elt_1. - destruct (X.compare x x'); intuition. - Qed. - - Lemma fold_1 : - forall (s : t) (Hs : Sort s) (A : Type) (i : A) (f : elt -> A -> A), - fold f s i = fold_left (fun a e => f e a) (elements s) i. - Proof. - induction s. - simpl; trivial. - intros. - inversion_clear Hs. - simpl; auto. - Qed. - - Lemma cardinal_1 : - forall (s : t) (Hs : Sort s), - cardinal s = length (elements s). - Proof. - auto. - Qed. - - Lemma filter_Inf : - forall (s : t) (Hs : Sort s) (x : elt) (f : elt -> bool), - Inf x s -> Inf x (filter f s). - Proof. - simple induction s; simpl. - intuition. - intros x l Hrec Hs a f Ha; inversion_clear Hs; inversion_clear Ha. - case (f x). - constructor; auto. - apply Hrec; auto. - apply Inf_lt with x; auto. - Qed. - - Lemma filter_sort : - forall (s : t) (Hs : Sort s) (f : elt -> bool), Sort (filter f s). - Proof. - simple induction s; simpl. - auto. - intros x l Hrec Hs f; inversion_clear Hs. - case (f x); auto. - constructor; auto. - apply filter_Inf; auto. - Qed. - - Lemma filter_1 : - forall (s : t) (x : elt) (f : elt -> bool), - compat_bool X.eq f -> In x (filter f s) -> In x s. - Proof. - simple induction s; simpl. - intros; inversion H0. - intros x l Hrec a f Hf. - case (f x); simpl. - inversion_clear 1. - constructor; auto. - constructor 2; apply (Hrec a f Hf); trivial. - constructor 2; apply (Hrec a f Hf); trivial. - Qed. - - Lemma filter_2 : - forall (s : t) (x : elt) (f : elt -> bool), - compat_bool X.eq f -> In x (filter f s) -> f x = true. - Proof. - simple induction s; simpl. - intros; inversion H0. - intros x l Hrec a f Hf. - generalize (Hf x); case (f x); simpl; auto. - inversion_clear 2; auto. - symmetry; auto. - Qed. - - Lemma filter_3 : - forall (s : t) (x : elt) (f : elt -> bool), - compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s). - Proof. - simple induction s; simpl. - intros; inversion H0. - intros x l Hrec a f Hf. - generalize (Hf x); case (f x); simpl. - inversion_clear 2; auto. - inversion_clear 2; auto. - rewrite <- (H a (X.eq_sym H1)); intros; discriminate. - Qed. - - Lemma for_all_1 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> - For_all (fun x => f x = true) s -> for_all f s = true. - Proof. - simple induction s; simpl; auto; unfold For_all. - intros x l Hrec f Hf. - generalize (Hf x); case (f x); simpl. - auto. - intros; rewrite (H x); auto. - Qed. - - Lemma for_all_2 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> - for_all f s = true -> For_all (fun x => f x = true) s. - Proof. - simple induction s; simpl; auto; unfold For_all. - intros; inversion H1. - intros x l Hrec f Hf. - intros A a; intros. - assert (f x = true). - generalize A; case (f x); auto. - rewrite H0 in A; simpl in A. - inversion_clear H; auto. - rewrite (Hf a x); auto. - Qed. - - Lemma exists_1 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. - Proof. - simple induction s; simpl; auto; unfold Exists. - intros. - elim H0; intuition. - inversion H2. - intros x l Hrec f Hf. - generalize (Hf x); case (f x); simpl. - auto. - destruct 2 as [a (A1,A2)]. - inversion_clear A1. - rewrite <- (H a (X.eq_sym H0)) in A2; discriminate. - apply Hrec; auto. - exists a; auto. - Qed. - - Lemma exists_2 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. - Proof. - simple induction s; simpl; auto; unfold Exists. - intros; discriminate. - intros x l Hrec f Hf. - case_eq (f x); intros. - exists x; auto. - destruct (Hrec f Hf H0) as [a (A1,A2)]. - exists a; auto. - Qed. - - Lemma partition_Inf_1 : - forall (s : t) (Hs : Sort s) (f : elt -> bool) (x : elt), - Inf x s -> Inf x (fst (partition f s)). - Proof. - simple induction s; simpl. - intuition. - intros x l Hrec Hs f a Ha; inversion_clear Hs; inversion_clear Ha. - generalize (Hrec H f a). - case (f x); case (partition f l); simpl. - auto. - intros; apply H2; apply Inf_lt with x; auto. - Qed. - - Lemma partition_Inf_2 : - forall (s : t) (Hs : Sort s) (f : elt -> bool) (x : elt), - Inf x s -> Inf x (snd (partition f s)). - Proof. - simple induction s; simpl. - intuition. - intros x l Hrec Hs f a Ha; inversion_clear Hs; inversion_clear Ha. - generalize (Hrec H f a). - case (f x); case (partition f l); simpl. - intros; apply H2; apply Inf_lt with x; auto. - auto. - Qed. - - Lemma partition_sort_1 : - forall (s : t) (Hs : Sort s) (f : elt -> bool), Sort (fst (partition f s)). - Proof. - simple induction s; simpl. - auto. - intros x l Hrec Hs f; inversion_clear Hs. - generalize (Hrec H f); generalize (partition_Inf_1 H f). - case (f x); case (partition f l); simpl; auto. - Qed. - - Lemma partition_sort_2 : - forall (s : t) (Hs : Sort s) (f : elt -> bool), Sort (snd (partition f s)). - Proof. - simple induction s; simpl. - auto. - intros x l Hrec Hs f; inversion_clear Hs. - generalize (Hrec H f); generalize (partition_Inf_2 H f). - case (f x); case (partition f l); simpl; auto. - Qed. - - Lemma partition_1 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s). - Proof. - simple induction s; simpl; auto; unfold Equal. - split; auto. - intros x l Hrec f Hf. - generalize (Hrec f Hf); clear Hrec. - destruct (partition f l) as [s1 s2]; simpl; intros. - case (f x); simpl; auto. - split; inversion_clear 1; auto. - constructor 2; rewrite <- H; auto. - constructor 2; rewrite H; auto. - Qed. - - Lemma partition_2 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> - Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). - Proof. - simple induction s; simpl; auto; unfold Equal. - split; auto. - intros x l Hrec f Hf. - generalize (Hrec f Hf); clear Hrec. - destruct (partition f l) as [s1 s2]; simpl; intros. - case (f x); simpl; auto. - split; inversion_clear 1; auto. - constructor 2; rewrite <- H; auto. - constructor 2; rewrite H; auto. - Qed. - - Definition eq : t -> t -> Prop := Equal. - - Lemma eq_refl : forall s : t, eq s s. - Proof. - unfold eq, Equal; intuition. - Qed. - - Lemma eq_sym : forall s s' : t, eq s s' -> eq s' s. - Proof. - unfold eq, Equal; intros; destruct (H a); intuition. - Qed. - - Lemma eq_trans : forall s s' s'' : t, eq s s' -> eq s' s'' -> eq s s''. - Proof. - unfold eq, Equal; intros; destruct (H a); destruct (H0 a); intuition. - Qed. - - Inductive lt : t -> t -> Prop := - | lt_nil : forall (x : elt) (s : t), lt nil (x :: s) - | lt_cons_lt : - forall (x y : elt) (s s' : t), X.lt x y -> lt (x :: s) (y :: s') - | lt_cons_eq : - forall (x y : elt) (s s' : t), - X.eq x y -> lt s s' -> lt (x :: s) (y :: s'). - Hint Constructors lt. - - Lemma lt_trans : forall s s' s'' : t, lt s s' -> lt s' s'' -> lt s s''. - Proof. - intros s s' s'' H; generalize s''; clear s''; elim H. - intros x l s'' H'; inversion_clear H'; auto. - intros x x' l l' E s'' H'; inversion_clear H'; auto. - constructor; apply X.lt_trans with x'; auto. - constructor; apply lt_eq with x'; auto. - intros. - inversion_clear H3. - constructor; apply eq_lt with y; auto. - constructor 3; auto; apply X.eq_trans with y; auto. - Qed. - - Lemma lt_not_eq : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), lt s s' -> ~ eq s s'. - Proof. - unfold eq, Equal. - intros s s' Hs Hs' H; generalize Hs Hs'; clear Hs Hs'; elim H; intros; intro. - elim (H0 x); intros. - assert (X : In x nil); auto; inversion X. - inversion_clear Hs; inversion_clear Hs'. - elim (H1 x); intros. - assert (X : In x (y :: s'0)); auto; inversion_clear X. - order. - generalize (Sort_Inf_In H4 H5 H8); order. - inversion_clear Hs; inversion_clear Hs'. - elim H2; auto; split; intros. - generalize (Sort_Inf_In H4 H5 H8); intros. - elim (H3 a); intros. - assert (X : In a (y :: s'0)); auto; inversion_clear X; auto. - order. - generalize (Sort_Inf_In H6 H7 H8); intros. - elim (H3 a); intros. - assert (X : In a (x :: s0)); auto; inversion_clear X; auto. - order. - Qed. - - Definition compare : - forall (s s' : t) (Hs : Sort s) (Hs' : Sort s'), Compare lt eq s s'. - Proof. - simple induction s. - intros; case s'. - constructor 2; apply eq_refl. - constructor 1; auto. - intros a l Hrec s'; case s'. - constructor 3; auto. - intros a' l' Hs Hs'. - case (X.compare a a'); [ constructor 1 | idtac | constructor 3 ]; auto. - elim (Hrec l'); - [ constructor 1 - | constructor 2 - | constructor 3 - | inversion Hs - | inversion Hs' ]; auto. - generalize e; unfold eq, Equal; intuition; inversion_clear H. - constructor; apply X.eq_trans with a; auto. - destruct (e1 a0); auto. - constructor; apply X.eq_trans with a'; auto. - destruct (e1 a0); auto. - Defined. - - End ForNotations. - Hint Constructors lt. - -End Raw. - -(** * Encapsulation - - Now, in order to really provide a functor implementing [S], we - need to encapsulate everything into a type of strictly ordered lists. *) +Require FSetCompat MSetList OrderedType2 OrderedType2Alt. Module Make (X: OrderedType) <: S with Module E := X. - - Module Raw := Raw X. - Module E := X. - - Record slist := {this :> Raw.t; sorted : sort E.lt this}. - Definition t := slist. - Definition elt := E.t. - - Definition In (x : elt) (s : t) : Prop := InA E.eq x s.(this). - Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'. - Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'. - Definition Empty (s:t) : Prop := forall a : elt, ~ In a s. - Definition For_all (P : elt -> Prop)(s:t) : Prop := forall x, In x s -> P x. - Definition Exists (P : elt -> Prop)(s:t) : Prop := exists x, In x s /\ P x. - - Definition mem (x : elt) (s : t) : bool := Raw.mem x s. - Definition add (x : elt)(s : t) : t := Build_slist (Raw.add_sort (sorted s) x). - Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_sort (sorted s) x). - Definition singleton (x : elt) : t := Build_slist (Raw.singleton_sort x). - Definition union (s s' : t) : t := - Build_slist (Raw.union_sort (sorted s) (sorted s')). - Definition inter (s s' : t) : t := - Build_slist (Raw.inter_sort (sorted s) (sorted s')). - Definition diff (s s' : t) : t := - Build_slist (Raw.diff_sort (sorted s) (sorted s')). - Definition equal (s s' : t) : bool := Raw.equal s s'. - Definition subset (s s' : t) : bool := Raw.subset s s'. - Definition empty : t := Build_slist Raw.empty_sort. - Definition is_empty (s : t) : bool := Raw.is_empty 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. - Definition choose (s : t) : option elt := Raw.choose s. - Definition fold (B : Type) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. - Definition cardinal (s : t) : nat := Raw.cardinal s. - Definition filter (f : elt -> bool) (s : t) : t := - Build_slist (Raw.filter_sort (sorted s) f). - 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 - (Build_slist (this:=fst p) (Raw.partition_sort_1 (sorted s) f), - Build_slist (this:=snd p) (Raw.partition_sort_2 (sorted s) f)). - Definition eq (s s' : t) : Prop := Raw.eq s s'. - Definition lt (s s' : t) : Prop := Raw.lt s s'. - - Section Spec. - Variable s s' s'': t. - Variable x y : elt. - - Lemma In_1 : E.eq x y -> In x s -> In y s. - Proof. exact (fun H H' => Raw.MX.In_eq H H'). Qed. - - Lemma mem_1 : In x s -> mem x s = true. - Proof. exact (fun H => Raw.mem_1 s.(sorted) H). Qed. - Lemma mem_2 : mem x s = true -> In x s. - Proof. exact (fun H => Raw.mem_2 H). Qed. - - Lemma equal_1 : Equal s s' -> equal s s' = true. - Proof. exact (Raw.equal_1 s.(sorted) s'.(sorted)). Qed. - Lemma equal_2 : equal s s' = true -> Equal s s'. - Proof. exact (fun H => Raw.equal_2 H). Qed. - - Lemma subset_1 : Subset s s' -> subset s s' = true. - Proof. exact (Raw.subset_1 s.(sorted) s'.(sorted)). Qed. - Lemma subset_2 : subset s s' = true -> Subset s s'. - Proof. exact (fun H => Raw.subset_2 H). Qed. - - Lemma empty_1 : Empty empty. - Proof. exact Raw.empty_1. Qed. - - Lemma is_empty_1 : Empty s -> is_empty s = true. - Proof. exact (fun H => Raw.is_empty_1 H). Qed. - Lemma is_empty_2 : is_empty s = true -> Empty s. - Proof. exact (fun H => Raw.is_empty_2 H). Qed. - - Lemma add_1 : E.eq x y -> In y (add x s). - Proof. exact (fun H => Raw.add_1 s.(sorted) H). Qed. - Lemma add_2 : In y s -> In y (add x s). - Proof. exact (fun H => Raw.add_2 s.(sorted) x H). Qed. - Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. - Proof. exact (fun H => Raw.add_3 s.(sorted) H). Qed. - - Lemma remove_1 : E.eq x y -> ~ In y (remove x s). - Proof. exact (fun H => Raw.remove_1 s.(sorted) H). Qed. - Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). - Proof. exact (fun H H' => Raw.remove_2 s.(sorted) H H'). Qed. - Lemma remove_3 : In y (remove x s) -> In y s. - Proof. exact (fun H => Raw.remove_3 s.(sorted) H). Qed. - - Lemma singleton_1 : In y (singleton x) -> E.eq x y. - Proof. exact (fun H => Raw.singleton_1 H). Qed. - Lemma singleton_2 : E.eq x y -> In y (singleton x). - Proof. exact (fun H => Raw.singleton_2 H). Qed. - - Lemma union_1 : In x (union s s') -> In x s \/ In x s'. - Proof. exact (fun H => Raw.union_1 s.(sorted) s'.(sorted) H). Qed. - Lemma union_2 : In x s -> In x (union s s'). - Proof. exact (fun H => Raw.union_2 s.(sorted) s'.(sorted) H). Qed. - Lemma union_3 : In x s' -> In x (union s s'). - Proof. exact (fun H => Raw.union_3 s.(sorted) s'.(sorted) H). Qed. - - Lemma inter_1 : In x (inter s s') -> In x s. - Proof. exact (fun H => Raw.inter_1 s.(sorted) s'.(sorted) H). Qed. - Lemma inter_2 : In x (inter s s') -> In x s'. - Proof. exact (fun H => Raw.inter_2 s.(sorted) s'.(sorted) H). Qed. - Lemma inter_3 : In x s -> In x s' -> In x (inter s s'). - Proof. exact (fun H => Raw.inter_3 s.(sorted) s'.(sorted) H). Qed. - - Lemma diff_1 : In x (diff s s') -> In x s. - Proof. exact (fun H => Raw.diff_1 s.(sorted) s'.(sorted) H). Qed. - Lemma diff_2 : In x (diff s s') -> ~ In x s'. - Proof. exact (fun H => Raw.diff_2 s.(sorted) s'.(sorted) H). Qed. - Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s'). - Proof. exact (fun H => Raw.diff_3 s.(sorted) s'.(sorted) H). 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. - Proof. exact (Raw.fold_1 s.(sorted)). Qed. - - Lemma cardinal_1 : cardinal s = length (elements s). - Proof. exact (Raw.cardinal_1 s.(sorted)). Qed. - - Section Filter. - - Variable f : elt -> bool. - - Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. - Proof. exact (@Raw.filter_1 s x f). Qed. - Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. - Proof. exact (@Raw.filter_2 s x f). Qed. - Lemma filter_3 : - compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). - Proof. exact (@Raw.filter_3 s x f). Qed. - - Lemma for_all_1 : - compat_bool E.eq f -> - For_all (fun x => f x = true) s -> for_all f s = true. - Proof. exact (@Raw.for_all_1 s f). Qed. - Lemma for_all_2 : - compat_bool E.eq f -> - for_all f s = true -> For_all (fun x => f x = true) s. - Proof. exact (@Raw.for_all_2 s f). Qed. - - Lemma exists_1 : - compat_bool E.eq f -> - Exists (fun x => f x = true) s -> exists_ f s = true. - Proof. exact (@Raw.exists_1 s f). Qed. - Lemma exists_2 : - compat_bool E.eq f -> - exists_ f s = true -> Exists (fun x => f x = true) s. - Proof. exact (@Raw.exists_2 s f). Qed. - - Lemma partition_1 : - compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s). - Proof. exact (@Raw.partition_1 s f). Qed. - Lemma partition_2 : - compat_bool E.eq f -> - Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). - Proof. exact (@Raw.partition_2 s f). Qed. - - End Filter. - - Lemma elements_1 : In x s -> InA E.eq x (elements s). - Proof. exact (fun H => Raw.elements_1 H). Qed. - Lemma elements_2 : InA E.eq x (elements s) -> In x s. - Proof. exact (fun H => Raw.elements_2 H). Qed. - Lemma elements_3 : sort E.lt (elements s). - Proof. exact (Raw.elements_3 s.(sorted)). Qed. - Lemma elements_3w : NoDupA E.eq (elements s). - Proof. exact (Raw.elements_3w s.(sorted)). Qed. - - Lemma min_elt_1 : min_elt s = Some x -> In x s. - Proof. exact (fun H => Raw.min_elt_1 H). Qed. - Lemma min_elt_2 : min_elt s = Some x -> In y s -> ~ E.lt y x. - Proof. exact (fun H => Raw.min_elt_2 s.(sorted) H). Qed. - Lemma min_elt_3 : min_elt s = None -> Empty s. - Proof. exact (fun H => Raw.min_elt_3 H). Qed. - - Lemma max_elt_1 : max_elt s = Some x -> In x s. - Proof. exact (fun H => Raw.max_elt_1 H). Qed. - Lemma max_elt_2 : max_elt s = Some x -> In y s -> ~ E.lt x y. - Proof. exact (fun H => Raw.max_elt_2 s.(sorted) H). Qed. - Lemma max_elt_3 : max_elt s = None -> Empty s. - Proof. exact (fun H => Raw.max_elt_3 H). Qed. - - Lemma choose_1 : choose s = Some x -> In x s. - Proof. exact (fun H => Raw.choose_1 H). Qed. - Lemma choose_2 : choose s = None -> Empty s. - Proof. exact (fun H => Raw.choose_2 H). Qed. - Lemma choose_3 : choose s = Some x -> choose s' = Some y -> - Equal s s' -> E.eq x y. - Proof. exact (@Raw.choose_3 _ _ s.(sorted) s'.(sorted) x y). Qed. - - Lemma eq_refl : eq s s. - Proof. exact (Raw.eq_refl s). Qed. - Lemma eq_sym : eq s s' -> eq s' s. - Proof. exact (@Raw.eq_sym s s'). Qed. - Lemma eq_trans : eq s s' -> eq s' s'' -> eq s s''. - Proof. exact (@Raw.eq_trans s s' s''). Qed. - - Lemma lt_trans : lt s s' -> lt s' s'' -> lt s s''. - Proof. exact (@Raw.lt_trans s s' s''). Qed. - Lemma lt_not_eq : lt s s' -> ~ eq s s'. - Proof. exact (Raw.lt_not_eq s.(sorted) s'.(sorted)). Qed. - - Definition compare : Compare lt eq s s'. - Proof. - elim (Raw.compare s.(sorted) s'.(sorted)); - [ constructor 1 | constructor 2 | constructor 3 ]; - auto. - Defined. - - Definition eq_dec : { eq s s' } + { ~ eq s s' }. - Proof. - change eq with Equal. - case_eq (equal s s'); intro H; [left | right]. - apply equal_2; auto. - intro H'; rewrite equal_1 in H; auto; discriminate. - Defined. - - End Spec. - + Module X' := OrderedType2Alt.Update_OT X. + Module MSet := MSetList.Make X'. + Include FSetCompat.Backport_Sets X MSet. End Make. diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 7a3e60d38..6bf4ae989 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -11,947 +11,20 @@ (** * Finite sets library *) (** This file proposes an implementation of the non-dependant - interface [FSetWeakInterface.S] using lists without redundancy. *) + interface [FSetInterface.WS] using lists without redundancy. *) Require Import FSetInterface. Set Implicit Arguments. Unset Strict Implicit. -(** * Functions over lists +(** This is just a compatibility layer, the real implementation + is now in [MSetWeakList] *) - First, we provide sets as lists which are (morally) without redundancy. - The specs are proved under the additional condition of no redundancy. - And the functions returning sets are proved to preserve this invariant. *) - -Module Raw (X: DecidableType). - - Definition elt := X.t. - Definition t := list elt. - - Definition empty : t := nil. - - Definition is_empty (l : t) : bool := if l then true else false. - - (** ** The set operations. *) - - Fixpoint mem (x : elt) (s : t) {struct s} : bool := - match s with - | nil => false - | y :: l => - if X.eq_dec x y then true else mem x l - end. - - Fixpoint add (x : elt) (s : t) {struct s} : t := - match s with - | nil => x :: nil - | y :: l => - if X.eq_dec x y then s else y :: add x l - end. - - Definition singleton (x : elt) : t := x :: nil. - - Fixpoint remove (x : elt) (s : t) {struct s} : t := - match s with - | nil => nil - | y :: l => - if X.eq_dec x y then l else y :: remove x l - end. - - Fixpoint fold (B : Type) (f : elt -> B -> B) (s : t) {struct s} : - B -> B := fun i => match s with - | nil => i - | x :: l => fold f l (f x i) - end. - - Definition union (s : t) : t -> t := fold add s. - - Definition diff (s s' : t) : t := fold remove s' s. - - Definition inter (s s': t) : t := - fold (fun x s => if mem x s' then add x s else s) s nil. - - Definition subset (s s' : t) : bool := is_empty (diff s s'). - - Definition equal (s s' : t) : bool := andb (subset s s') (subset s' s). - - Fixpoint filter (f : elt -> bool) (s : t) {struct s} : t := - match s with - | nil => nil - | x :: l => if f x then x :: filter f l else filter f l - end. - - Fixpoint for_all (f : elt -> bool) (s : t) {struct s} : bool := - match s with - | nil => true - | x :: l => if f x then for_all f l else false - end. - - Fixpoint exists_ (f : elt -> bool) (s : t) {struct s} : bool := - match s with - | nil => false - | x :: l => if f x then true else exists_ f l - end. - - Fixpoint partition (f : elt -> bool) (s : t) {struct s} : - t * t := - match s with - | nil => (nil, nil) - | x :: l => - let (s1, s2) := partition f l in - if f x then (x :: s1, s2) else (s1, x :: s2) - end. - - Definition cardinal (s : t) : nat := length s. - - Definition elements (s : t) : list elt := s. - - Definition choose (s : t) : option elt := - match s with - | nil => None - | x::_ => Some x - end. - - (** ** Proofs of set operation specifications. *) - Section ForNotations. - Notation NoDup := (NoDupA X.eq). - Notation In := (InA X.eq). - - 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. - - Lemma In_eq : - forall (s : t) (x y : elt), X.eq x y -> In x s -> In y s. - Proof. - intros s x y; setoid_rewrite InA_alt; firstorder eauto. - Qed. - Hint Immediate In_eq. - - Lemma mem_1 : - forall (s : t)(x : elt), In x s -> mem x s = true. - Proof. - induction s; intros. - inversion H. - simpl; destruct (X.eq_dec x a); trivial. - inversion_clear H; auto. - Qed. - - Lemma mem_2 : forall (s : t) (x : elt), mem x s = true -> In x s. - Proof. - induction s. - intros; inversion H. - intros x; simpl. - destruct (X.eq_dec x a); firstorder; discriminate. - Qed. - - Lemma add_1 : - forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> In y (add x s). - Proof. - induction s. - simpl; intuition. - simpl; intros; case (X.eq_dec x a); intuition; inversion_clear Hs; - firstorder. - eauto. - Qed. - - Lemma add_2 : - forall (s : t) (Hs : NoDup s) (x y : elt), In y s -> In y (add x s). - Proof. - induction s. - simpl; intuition. - simpl; intros; case (X.eq_dec x a); intuition. - inversion_clear Hs; eauto; inversion_clear H; intuition. - Qed. - - Lemma add_3 : - forall (s : t) (Hs : NoDup s) (x y : elt), - ~ X.eq x y -> In y (add x s) -> In y s. - Proof. - induction s. - simpl; intuition. - inversion_clear H0; firstorder; absurd (X.eq x y); auto. - simpl; intros Hs x y; case (X.eq_dec x a); intros; - inversion_clear H0; inversion_clear Hs; firstorder; - absurd (X.eq x y); auto. - Qed. - - Lemma add_unique : - forall (s : t) (Hs : NoDup s)(x:elt), NoDup (add x s). - Proof. - induction s. - simpl; intuition. - constructor; auto. - intro H0; inversion H0. - intros. - inversion_clear Hs. - simpl. - destruct (X.eq_dec x a). - constructor; auto. - constructor; auto. - intro H1; apply H. - eapply add_3; eauto. - Qed. - - Lemma remove_1 : - forall (s : t) (Hs : NoDup s) (x y : elt), X.eq x y -> ~ In y (remove x s). - Proof. - simple induction s. - simpl; red; intros; inversion H0. - simpl; intros; case (X.eq_dec x a); intuition; inversion_clear Hs. - elim H2. - apply In_eq with y; eauto. - inversion_clear H1; eauto. - Qed. - - Lemma remove_2 : - forall (s : t) (Hs : NoDup s) (x y : elt), - ~ X.eq x y -> In y s -> In y (remove x s). - Proof. - simple induction s. - simpl; intuition. - simpl; intros; case (X.eq_dec x a); intuition; inversion_clear Hs; - inversion_clear H1; auto. - absurd (X.eq x y); eauto. - Qed. - - Lemma remove_3 : - forall (s : t) (Hs : NoDup s) (x y : elt), In y (remove x s) -> In y s. - Proof. - simple induction s. - simpl; intuition. - simpl; intros a l Hrec Hs x y; case (X.eq_dec x a); intuition. - inversion_clear Hs; inversion_clear H; firstorder. - Qed. - - Lemma remove_unique : - forall (s : t) (Hs : NoDup s) (x : elt), NoDup (remove x s). - Proof. - simple induction s. - simpl; intuition. - simpl; intros; case (X.eq_dec x a); intuition; inversion_clear Hs; - auto. - constructor; auto. - intro H2; elim H0. - eapply remove_3; eauto. - Qed. - - Lemma singleton_unique : forall x : elt, NoDup (singleton x). - Proof. - unfold singleton; simpl; constructor; auto; intro H; inversion H. - Qed. - - Lemma singleton_1 : forall x y : elt, In y (singleton x) -> X.eq x y. - Proof. - unfold singleton; simpl; intuition. - inversion_clear H; auto; inversion H0. - Qed. - - Lemma singleton_2 : forall x y : elt, X.eq x y -> In y (singleton x). - Proof. - unfold singleton; simpl; intuition. - Qed. - - Lemma empty_unique : NoDup empty. - Proof. - unfold empty; constructor. - Qed. - - Lemma empty_1 : Empty empty. - Proof. - unfold Empty, empty; intuition; inversion H. - Qed. - - Lemma is_empty_1 : forall s : t, Empty s -> is_empty s = true. - Proof. - unfold Empty; intro s; case s; simpl; intuition. - elim (H e); auto. - Qed. - - Lemma is_empty_2 : forall s : t, is_empty s = true -> Empty s. - Proof. - unfold Empty; intro s; case s; simpl; intuition; - inversion H0. - Qed. - - Lemma elements_1 : forall (s : t) (x : elt), In x s -> In x (elements s). - Proof. - unfold elements; auto. - Qed. - - Lemma elements_2 : forall (s : t) (x : elt), In x (elements s) -> In x s. - Proof. - unfold elements; auto. - Qed. - - Lemma elements_3w : forall (s : t) (Hs : NoDup s), NoDup (elements s). - Proof. - unfold elements; auto. - Qed. - - Lemma fold_1 : - forall (s : t) (Hs : NoDup s) (A : Type) (i : A) (f : elt -> A -> A), - fold f s i = fold_left (fun a e => f e a) (elements s) i. - Proof. - induction s; simpl; auto; intros. - inversion_clear Hs; auto. - Qed. - - Lemma union_unique : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (union s s'). - Proof. - unfold union; induction s; simpl; auto; intros. - inversion_clear Hs. - apply IHs; auto. - apply add_unique; auto. - Qed. - - Lemma union_1 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x (union s s') -> In x s \/ In x s'. - Proof. - unfold union; induction s; simpl; auto; intros. - inversion_clear Hs. - destruct (X.eq_dec x a). - left; auto. - destruct (IHs (add a s') H1 (add_unique Hs' a) x); intuition. - right; eapply add_3; eauto. - Qed. - - Lemma union_0 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x s \/ In x s' -> In x (union s s'). - Proof. - unfold union; induction s; simpl; auto; intros. - inversion_clear H; auto. - inversion_clear H0. - inversion_clear Hs. - apply IHs; auto. - apply add_unique; auto. - destruct H. - inversion_clear H; auto. - right; apply add_1; auto. - right; apply add_2; auto. - Qed. - - Lemma union_2 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x s -> In x (union s s'). - Proof. - intros; apply union_0; auto. - Qed. - - Lemma union_3 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x s' -> In x (union s s'). - Proof. - intros; apply union_0; auto. - Qed. - - Lemma inter_unique : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (inter s s'). - Proof. - unfold inter; intros s. - set (acc := nil (A:=elt)). - assert (NoDup acc) by (unfold acc; auto). - clearbody acc; generalize H; clear H; generalize acc; clear acc. - induction s; simpl; auto; intros. - inversion_clear Hs. - apply IHs; auto. - destruct (mem a s'); intros; auto. - apply add_unique; auto. - Qed. - - Lemma inter_0 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x (inter s s') -> In x s /\ In x s'. - Proof. - unfold inter; intros. - set (acc := nil (A:=elt)) in *. - assert (NoDup acc) by (unfold acc; auto). - cut ((In x s /\ In x s') \/ In x acc). - destruct 1; auto. - inversion H1. - clearbody acc. - generalize H0 H Hs' Hs; clear H0 H Hs Hs'. - generalize acc x s'; clear acc x s'. - induction s; simpl; auto; intros. - inversion_clear Hs. - case_eq (mem a s'); intros H3; rewrite H3 in H; simpl in H. - destruct (IHs _ _ _ (add_unique H0 a) H); auto. - left; intuition. - destruct (X.eq_dec x a); auto. - left; intuition. - apply In_eq with a; eauto. - apply mem_2; auto. - right; eapply add_3; eauto. - destruct (IHs _ _ _ H0 H); auto. - left; intuition. - Qed. - - Lemma inter_1 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x (inter s s') -> In x s. - Proof. - intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ]. - Qed. - - Lemma inter_2 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x (inter s s') -> In x s'. - Proof. - intros; cut (In x s /\ In x s'); [ intuition | apply inter_0; auto ]. - Qed. - - Lemma inter_3 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x s -> In x s' -> In x (inter s s'). - Proof. - intros s s' Hs Hs' x. - cut (((In x s /\ In x s')\/ In x (nil (A:=elt))) -> In x (inter s s')). - intuition. - unfold inter. - set (acc := nil (A:=elt)) in *. - assert (NoDup acc) by (unfold acc; auto). - clearbody acc. - generalize H Hs' Hs; clear H Hs Hs'. - generalize acc x s'; clear acc x s'. - induction s; simpl; auto; intros. - destruct H0; auto. - destruct H0; inversion H0. - inversion_clear Hs. - case_eq (mem a s'); intros H3; apply IHs; auto. - apply add_unique; auto. - destruct H0. - destruct H0. - inversion_clear H0. - right; apply add_1; auto. - left; auto. - right; apply add_2; auto. - destruct H0; auto. - destruct H0. - inversion_clear H0; auto. - absurd (In x s'); auto. - red; intros. - rewrite (mem_1 (In_eq H5 H0)) in H3. - discriminate. - Qed. - - Lemma diff_unique : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), NoDup (diff s s'). - Proof. - unfold diff; intros s s' Hs; generalize s Hs; clear Hs s. - induction s'; simpl; auto; intros. - inversion_clear Hs'. - apply IHs'; auto. - apply remove_unique; auto. - Qed. - - Lemma diff_0 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x (diff s s') -> In x s /\ ~ In x s'. - Proof. - unfold diff; intros s s' Hs; generalize s Hs; clear Hs s. - induction s'; simpl; auto; intros. - inversion_clear Hs'. - split; auto; intro H1; inversion H1. - inversion_clear Hs'. - destruct (IHs' (remove a s) (remove_unique Hs a) H1 x H). - split. - eapply remove_3; eauto. - red; intros. - inversion_clear H4; auto. - destruct (remove_1 Hs (X.eq_sym H5) H2). - Qed. - - Lemma diff_1 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x (diff s s') -> In x s. - Proof. - intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto]. - Qed. - - Lemma diff_2 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x (diff s s') -> ~ In x s'. - Proof. - intros; cut (In x s /\ ~ In x s'); [ intuition | apply diff_0; auto]. - Qed. - - Lemma diff_3 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s') (x : elt), - In x s -> ~ In x s' -> In x (diff s s'). - Proof. - unfold diff; intros s s' Hs; generalize s Hs; clear Hs s. - induction s'; simpl; auto; intros. - inversion_clear Hs'. - apply IHs'; auto. - apply remove_unique; auto. - apply remove_2; auto. - Qed. - - Lemma subset_1 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), - Subset s s' -> subset s s' = true. - Proof. - unfold subset, Subset; intros. - apply is_empty_1. - unfold Empty; intros. - intro. - destruct (diff_2 Hs Hs' H0). - apply H. - eapply diff_1; eauto. - Qed. - - Lemma subset_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'), - subset s s' = true -> Subset s s'. - Proof. - unfold subset, Subset; intros. - generalize (is_empty_2 H); clear H; unfold Empty; intros. - generalize (@mem_1 s' a) (@mem_2 s' a); destruct (mem a s'). - intuition. - intros. - destruct (H a). - apply diff_3; intuition. - Qed. - - Lemma equal_1 : - forall (s s' : t) (Hs : NoDup s) (Hs' : NoDup s'), - Equal s s' -> equal s s' = true. - Proof. - unfold Equal, equal; intros. - apply andb_true_intro; split; apply subset_1; firstorder. - Qed. - - Lemma equal_2 : forall (s s' : t)(Hs : NoDup s) (Hs' : NoDup s'), - equal s s' = true -> Equal s s'. - Proof. - unfold Equal, equal; intros. - destruct (andb_prop _ _ H); clear H. - split; apply subset_2; auto. - Qed. - - Definition choose_1 : - forall (s : t) (x : elt), choose s = Some x -> In x s. - Proof. - destruct s; simpl; intros; inversion H; auto. - Qed. - - Definition choose_2 : forall s : t, choose s = None -> Empty s. - Proof. - destruct s; simpl; intros. - intros x H0; inversion H0. - inversion H. - Qed. - - Lemma cardinal_1 : - forall (s : t) (Hs : NoDup s), cardinal s = length (elements s). - Proof. - auto. - Qed. - - Lemma filter_1 : - forall (s : t) (x : elt) (f : elt -> bool), - In x (filter f s) -> In x s. - Proof. - simple induction s; simpl. - intros; inversion H. - intros x l Hrec a f. - case (f x); simpl. - inversion_clear 1. - constructor; auto. - constructor 2; apply (Hrec a f); trivial. - constructor 2; apply (Hrec a f); trivial. - Qed. - - Lemma filter_2 : - forall (s : t) (x : elt) (f : elt -> bool), - compat_bool X.eq f -> In x (filter f s) -> f x = true. - Proof. - simple induction s; simpl. - intros; inversion H0. - intros x l Hrec a f Hf. - generalize (Hf x); case (f x); simpl; auto. - inversion_clear 2; auto. - symmetry; auto. - Qed. - - Lemma filter_3 : - forall (s : t) (x : elt) (f : elt -> bool), - compat_bool X.eq f -> In x s -> f x = true -> In x (filter f s). - Proof. - simple induction s; simpl. - intros; inversion H0. - intros x l Hrec a f Hf. - generalize (Hf x); case (f x); simpl. - inversion_clear 2; auto. - inversion_clear 2; auto. - rewrite <- (H a (X.eq_sym H1)); intros; discriminate. - Qed. - - Lemma filter_unique : - forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (filter f s). - Proof. - simple induction s; simpl. - auto. - intros x l Hrec Hs f; inversion_clear Hs. - case (f x); auto. - constructor; auto. - intro H1; apply H. - eapply filter_1; eauto. - Qed. - - - Lemma for_all_1 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> - For_all (fun x => f x = true) s -> for_all f s = true. - Proof. - simple induction s; simpl; auto; unfold For_all. - intros x l Hrec f Hf. - generalize (Hf x); case (f x); simpl. - auto. - intros; rewrite (H x); auto. - Qed. - - Lemma for_all_2 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> - for_all f s = true -> For_all (fun x => f x = true) s. - Proof. - simple induction s; simpl; auto; unfold For_all. - intros; inversion H1. - intros x l Hrec f Hf. - intros A a; intros. - assert (f x = true). - generalize A; case (f x); auto. - rewrite H0 in A; simpl in A. - inversion_clear H; auto. - rewrite (Hf a x); auto. - Qed. - - Lemma exists_1 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> Exists (fun x => f x = true) s -> exists_ f s = true. - Proof. - simple induction s; simpl; auto; unfold Exists. - intros. - elim H0; intuition. - inversion H2. - intros x l Hrec f Hf. - generalize (Hf x); case (f x); simpl. - auto. - destruct 2 as [a (A1,A2)]. - inversion_clear A1. - rewrite <- (H a (X.eq_sym H0)) in A2; discriminate. - apply Hrec; auto. - exists a; auto. - Qed. - - Lemma exists_2 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> exists_ f s = true -> Exists (fun x => f x = true) s. - Proof. - simple induction s; simpl; auto; unfold Exists. - intros; discriminate. - intros x l Hrec f Hf. - case_eq (f x); intros. - exists x; auto. - destruct (Hrec f Hf H0) as [a (A1,A2)]. - exists a; auto. - Qed. - - Lemma partition_1 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> Equal (fst (partition f s)) (filter f s). - Proof. - simple induction s; simpl; auto; unfold Equal. - firstorder. - intros x l Hrec f Hf. - generalize (Hrec f Hf); clear Hrec. - case (partition f l); intros s1 s2; simpl; intros. - case (f x); simpl; firstorder; inversion H0; intros; firstorder. - Qed. - - Lemma partition_2 : - forall (s : t) (f : elt -> bool), - compat_bool X.eq f -> - Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). - Proof. - simple induction s; simpl; auto; unfold Equal. - firstorder. - intros x l Hrec f Hf. - generalize (Hrec f Hf); clear Hrec. - case (partition f l); intros s1 s2; simpl; intros. - case (f x); simpl; firstorder; inversion H0; intros; firstorder. - Qed. - - Lemma partition_aux_1 : - forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt), - In x (fst (partition f s)) -> In x s. - Proof. - induction s; simpl; auto; intros. - inversion_clear Hs. - generalize (IHs H1 f x). - destruct (f a); destruct (partition f s); simpl in *; auto. - inversion_clear H; auto. - Qed. - - Lemma partition_aux_2 : - forall (s : t) (Hs : NoDup s) (f : elt -> bool)(x:elt), - In x (snd (partition f s)) -> In x s. - Proof. - induction s; simpl; auto; intros. - inversion_clear Hs. - generalize (IHs H1 f x). - destruct (f a); destruct (partition f s); simpl in *; auto. - inversion_clear H; auto. - Qed. - - Lemma partition_unique_1 : - forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (fst (partition f s)). - Proof. - simple induction s; simpl. - auto. - intros x l Hrec Hs f; inversion_clear Hs. - generalize (@partition_aux_1 _ H0 f x). - generalize (Hrec H0 f). - case (f x); case (partition f l); simpl; auto. - Qed. - - Lemma partition_unique_2 : - forall (s : t) (Hs : NoDup s) (f : elt -> bool), NoDup (snd (partition f s)). - Proof. - simple induction s; simpl. - auto. - intros x l Hrec Hs f; inversion_clear Hs. - generalize (@partition_aux_2 _ H0 f x). - generalize (Hrec H0 f). - case (f x); case (partition f l); simpl; auto. - Qed. - - Definition eq : t -> t -> Prop := Equal. - - Lemma eq_refl : forall s, eq s s. - Proof. firstorder. Qed. - - Lemma eq_sym : forall s s', eq s s' -> eq s' s. - Proof. firstorder. Qed. - - Lemma eq_trans : - forall s s' s'', eq s s' -> eq s' s'' -> eq s s''. - Proof. firstorder. Qed. - - Definition eq_dec : forall (s s':t)(Hs:NoDup s)(Hs':NoDup s'), - { eq s s' }+{ ~eq s s' }. - Proof. - intros. - change eq with Equal. - case_eq (equal s s'); intro H; [left | right]. - apply equal_2; auto. - intro H'; rewrite equal_1 in H; auto; discriminate. - Defined. - - End ForNotations. -End Raw. - -(** * Encapsulation - - Now, in order to really provide a functor implementing [S], we - need to encapsulate everything into a type of lists without redundancy. *) +Require DecidableType2 FSetCompat MSetWeakList. Module Make (X: DecidableType) <: WS with Module E := X. - - Module Raw := Raw X. Module E := X. - - Record slist := {this :> Raw.t; unique : NoDupA E.eq this}. - Definition t := slist. - Definition elt := E.t. - - Definition In (x : elt) (s : t) : Prop := InA E.eq x s.(this). - Definition Equal (s s':t) : Prop := forall a : elt, In a s <-> In a s'. - Definition Subset (s s':t) : Prop := forall a : elt, In a s -> In a s'. - Definition Empty (s:t) : Prop := forall a : elt, ~ In a s. - Definition For_all (P : elt -> Prop) (s : t) : Prop := - forall x : elt, In x s -> P x. - Definition Exists (P : elt -> Prop) (s : t) : Prop := exists x : elt, In x s /\ P x. - - Definition mem (x : elt) (s : t) : bool := Raw.mem x s. - Definition add (x : elt)(s : t) : t := Build_slist (Raw.add_unique (unique s) x). - Definition remove (x : elt)(s : t) : t := Build_slist (Raw.remove_unique (unique s) x). - Definition singleton (x : elt) : t := Build_slist (Raw.singleton_unique x). - Definition union (s s' : t) : t := - Build_slist (Raw.union_unique (unique s) (unique s')). - Definition inter (s s' : t) : t := - Build_slist (Raw.inter_unique (unique s) (unique s')). - Definition diff (s s' : t) : t := - Build_slist (Raw.diff_unique (unique s) (unique s')). - Definition equal (s s' : t) : bool := Raw.equal s s'. - Definition subset (s s' : t) : bool := Raw.subset s s'. - Definition empty : t := Build_slist Raw.empty_unique. - Definition is_empty (s : t) : bool := Raw.is_empty s. - Definition elements (s : t) : list elt := Raw.elements s. - Definition choose (s:t) : option elt := Raw.choose s. - Definition fold (B : Type) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. - Definition cardinal (s : t) : nat := Raw.cardinal s. - Definition filter (f : elt -> bool) (s : t) : t := - Build_slist (Raw.filter_unique (unique s) f). - 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 - (Build_slist (this:=fst p) (Raw.partition_unique_1 (unique s) f), - Build_slist (this:=snd p) (Raw.partition_unique_2 (unique s) f)). - - Section Spec. - Variable s s' : t. - Variable x y : elt. - - Lemma In_1 : E.eq x y -> In x s -> In y s. - Proof. exact (fun H H' => Raw.In_eq H H'). Qed. - - Lemma mem_1 : In x s -> mem x s = true. - Proof. exact (fun H => Raw.mem_1 H). Qed. - Lemma mem_2 : mem x s = true -> In x s. - Proof. exact (fun H => Raw.mem_2 H). Qed. - - Lemma equal_1 : Equal s s' -> equal s s' = true. - Proof. exact (Raw.equal_1 s.(unique) s'.(unique)). Qed. - Lemma equal_2 : equal s s' = true -> Equal s s'. - Proof. exact (Raw.equal_2 s.(unique) s'.(unique)). Qed. - - Lemma subset_1 : Subset s s' -> subset s s' = true. - Proof. exact (Raw.subset_1 s.(unique) s'.(unique)). Qed. - Lemma subset_2 : subset s s' = true -> Subset s s'. - Proof. exact (Raw.subset_2 s.(unique) s'.(unique)). Qed. - - Lemma empty_1 : Empty empty. - Proof. exact Raw.empty_1. Qed. - - Lemma is_empty_1 : Empty s -> is_empty s = true. - Proof. exact (fun H => Raw.is_empty_1 H). Qed. - Lemma is_empty_2 : is_empty s = true -> Empty s. - Proof. exact (fun H => Raw.is_empty_2 H). Qed. - - Lemma add_1 : E.eq x y -> In y (add x s). - Proof. exact (fun H => Raw.add_1 s.(unique) H). Qed. - Lemma add_2 : In y s -> In y (add x s). - Proof. exact (fun H => Raw.add_2 s.(unique) x H). Qed. - Lemma add_3 : ~ E.eq x y -> In y (add x s) -> In y s. - Proof. exact (fun H => Raw.add_3 s.(unique) H). Qed. - - Lemma remove_1 : E.eq x y -> ~ In y (remove x s). - Proof. exact (fun H => Raw.remove_1 s.(unique) H). Qed. - Lemma remove_2 : ~ E.eq x y -> In y s -> In y (remove x s). - Proof. exact (fun H H' => Raw.remove_2 s.(unique) H H'). Qed. - Lemma remove_3 : In y (remove x s) -> In y s. - Proof. exact (fun H => Raw.remove_3 s.(unique) H). Qed. - - Lemma singleton_1 : In y (singleton x) -> E.eq x y. - Proof. exact (fun H => Raw.singleton_1 H). Qed. - Lemma singleton_2 : E.eq x y -> In y (singleton x). - Proof. exact (fun H => Raw.singleton_2 H). Qed. - - Lemma union_1 : In x (union s s') -> In x s \/ In x s'. - Proof. exact (fun H => Raw.union_1 s.(unique) s'.(unique) H). Qed. - Lemma union_2 : In x s -> In x (union s s'). - Proof. exact (fun H => Raw.union_2 s.(unique) s'.(unique) H). Qed. - Lemma union_3 : In x s' -> In x (union s s'). - Proof. exact (fun H => Raw.union_3 s.(unique) s'.(unique) H). Qed. - - Lemma inter_1 : In x (inter s s') -> In x s. - Proof. exact (fun H => Raw.inter_1 s.(unique) s'.(unique) H). Qed. - Lemma inter_2 : In x (inter s s') -> In x s'. - Proof. exact (fun H => Raw.inter_2 s.(unique) s'.(unique) H). Qed. - Lemma inter_3 : In x s -> In x s' -> In x (inter s s'). - Proof. exact (fun H => Raw.inter_3 s.(unique) s'.(unique) H). Qed. - - Lemma diff_1 : In x (diff s s') -> In x s. - Proof. exact (fun H => Raw.diff_1 s.(unique) s'.(unique) H). Qed. - Lemma diff_2 : In x (diff s s') -> ~ In x s'. - Proof. exact (fun H => Raw.diff_2 s.(unique) s'.(unique) H). Qed. - Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s'). - Proof. exact (fun H => Raw.diff_3 s.(unique) s'.(unique) H). 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. - Proof. exact (Raw.fold_1 s.(unique)). Qed. - - Lemma cardinal_1 : cardinal s = length (elements s). - Proof. exact (Raw.cardinal_1 s.(unique)). Qed. - - Section Filter. - - Variable f : elt -> bool. - - Lemma filter_1 : compat_bool E.eq f -> In x (filter f s) -> In x s. - Proof. exact (fun H => @Raw.filter_1 s x f). Qed. - Lemma filter_2 : compat_bool E.eq f -> In x (filter f s) -> f x = true. - Proof. exact (@Raw.filter_2 s x f). Qed. - Lemma filter_3 : - compat_bool E.eq f -> In x s -> f x = true -> In x (filter f s). - Proof. exact (@Raw.filter_3 s x f). Qed. - - Lemma for_all_1 : - compat_bool E.eq f -> - For_all (fun x => f x = true) s -> for_all f s = true. - Proof. exact (@Raw.for_all_1 s f). Qed. - Lemma for_all_2 : - compat_bool E.eq f -> - for_all f s = true -> For_all (fun x => f x = true) s. - Proof. exact (@Raw.for_all_2 s f). Qed. - - Lemma exists_1 : - compat_bool E.eq f -> - Exists (fun x => f x = true) s -> exists_ f s = true. - Proof. exact (@Raw.exists_1 s f). Qed. - Lemma exists_2 : - compat_bool E.eq f -> - exists_ f s = true -> Exists (fun x => f x = true) s. - Proof. exact (@Raw.exists_2 s f). Qed. - - Lemma partition_1 : - compat_bool E.eq f -> Equal (fst (partition f s)) (filter f s). - Proof. exact (@Raw.partition_1 s f). Qed. - Lemma partition_2 : - compat_bool E.eq f -> - Equal (snd (partition f s)) (filter (fun x => negb (f x)) s). - Proof. exact (@Raw.partition_2 s f). Qed. - - End Filter. - - Lemma elements_1 : In x s -> InA E.eq x (elements s). - Proof. exact (fun H => Raw.elements_1 H). Qed. - Lemma elements_2 : InA E.eq x (elements s) -> In x s. - Proof. exact (fun H => Raw.elements_2 H). Qed. - Lemma elements_3w : NoDupA E.eq (elements s). - Proof. exact (Raw.elements_3w s.(unique)). Qed. - - Lemma choose_1 : choose s = Some x -> In x s. - Proof. exact (fun H => Raw.choose_1 H). Qed. - Lemma choose_2 : choose s = None -> Empty s. - Proof. exact (fun H => Raw.choose_2 H). Qed. - - End Spec. - - Definition eq : t -> t -> Prop := Equal. - - Lemma eq_refl : forall s, eq s s. - Proof. firstorder. Qed. - - Lemma eq_sym : forall s s', eq s s' -> eq s' s. - Proof. firstorder. Qed. - - Lemma eq_trans : - forall s s' s'', eq s s' -> eq s' s'' -> eq s s''. - Proof. firstorder. Qed. - - Definition eq_dec : forall (s s':t), - { eq s s' }+{ ~eq s s' }. - Proof. - intros s s'; exact (Raw.eq_dec s.(unique) s'.(unique)). - Defined. - + Module X' := DecidableType2.Update_DT X. + Module MSet := MSetWeakList.Make X'. + Include FSetCompat.Backport_WSets X MSet. End Make. |