diff options
| -rw-r--r-- | Makefile.common | 5 | ||||
| -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 | ||||
| -rw-r--r-- | theories/Structures/DecidableType2.v | 20 | ||||
| -rw-r--r-- | theories/Structures/OrderTac.v | 37 | ||||
| -rw-r--r-- | theories/Structures/OrderedType2Alt.v | 117 | ||||
| -rw-r--r-- | theories/theories.itarget | 2 |
10 files changed, 505 insertions, 5432 deletions
diff --git a/Makefile.common b/Makefile.common index 967f7b21e..06e5f3b4b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -379,7 +379,7 @@ FSETSBASEVO:=$(addprefix theories/FSets/, \ FSetInterface.vo FSetList.vo FSetBridge.vo \ FSetFacts.vo FSetProperties.vo FSetEqProperties.vo \ FSetWeakList.vo FSetAVL.vo FSetDecide.vo \ - FSets.vo \ + FSetCompat.vo FSets.vo \ FMapInterface.vo FMapList.vo FMapFacts.vo \ FMapWeakList.vo FMapPositive.vo FSetToFiniteSet.vo \ FMaps.vo ) @@ -387,7 +387,8 @@ FSETSBASEVO:=$(addprefix theories/FSets/, \ FSETS_basic:= FSETS_all:=$(addprefix theories/FSets/, \ - FSetFullAVL.vo FMapAVL.vo FMapFullAVL.vo ) + FMapAVL.vo FMapFullAVL.vo ) + FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS)) 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. diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index c6d16a6c5..61fd743dc 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -9,6 +9,8 @@ (* $Id$ *) Require Export SetoidList. +Require DecidableType. (* No Import here, this is on purpose *) + Set Implicit Arguments. Unset Strict Implicit. @@ -31,6 +33,24 @@ Module Type DecidableType. Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }. End DecidableType. +(** * Compatibility wrapper from/to the old version of [DecidableType] *) + +Module Type DecidableTypeOrig := DecidableType.DecidableType. + +Module Backport_DT (E:DecidableType) <: DecidableTypeOrig. + Include E. + Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv. + Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv. + Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv. +End Backport_DT. + +Module Update_DT (E:DecidableTypeOrig) <: DecidableType. + Include E. + Instance eq_equiv : Equivalence eq. + Proof. exact (Build_Equivalence _ _ eq_refl eq_sym eq_trans). Qed. +End Update_DT. + + (** * Additional notions about keys and datas used in FMap *) Module KeyDecidableType(D:DecidableType). diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v index c2990f283..31c9324f8 100644 --- a/theories/Structures/OrderTac.v +++ b/theories/Structures/OrderTac.v @@ -44,16 +44,17 @@ End OrderTacSig. (** An abstract vision of the predicates. This allows a one-line statement for interesting transitivity properties: for instance - [trans_ord LE LE = LE] will imply later [le x y -> le y z -> le x z]. - *) + [trans_ord OLE OLE = OLE] will imply later + [le x y -> le y z -> le x z]. +*) -Inductive ord := EQ | LT | LE. +Inductive ord := OEQ | OLT | OLE. Definition trans_ord o o' := match o, o' with - | EQ, _ => o' - | _, EQ => o - | LE, LE => LE - | _, _ => LT + | OEQ, _ => o' + | _, OEQ => o + | OLE, OLE => OLE + | _, _ => OLT end. Infix "+" := trans_ord : order. @@ -103,7 +104,7 @@ Ltac subst_eqns := end. Definition interp_ord o := - match o with EQ => eq | LT => lt | LE => le end. + match o with OEQ => eq | OLT => lt | OLE => le end. Notation "#" := interp_ord : order. Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. @@ -112,15 +113,15 @@ destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition; subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. Qed. -Definition eq_trans x y z : x==y -> y==z -> x==z := trans EQ EQ x y z. -Definition le_trans x y z : x<=y -> y<=z -> x<=z := trans LE LE x y z. -Definition lt_trans x y z : x<y -> y<z -> x<z := trans LT LT x y z. -Definition le_lt_trans x y z : x<=y -> y<z -> x<z := trans LE LT x y z. -Definition lt_le_trans x y z : x<y -> y<=z -> x<z := trans LT LE x y z. -Definition eq_lt x y z : x==y -> y<z -> x<z := trans EQ LT x y z. -Definition lt_eq x y z : x<y -> y==z -> x<z := trans LT EQ x y z. -Definition eq_le x y z : x==y -> y<=z -> x<=z := trans EQ LE x y z. -Definition le_eq x y z : x<=y -> y==z -> x<=z := trans LE EQ x y z. +Definition eq_trans x y z : x==y -> y==z -> x==z := trans OEQ OEQ x y z. +Definition le_trans x y z : x<=y -> y<=z -> x<=z := trans OLE OLE x y z. +Definition lt_trans x y z : x<y -> y<z -> x<z := trans OLT OLT x y z. +Definition le_lt_trans x y z : x<=y -> y<z -> x<z := trans OLE OLT x y z. +Definition lt_le_trans x y z : x<y -> y<=z -> x<z := trans OLT OLE x y z. +Definition eq_lt x y z : x==y -> y<z -> x<z := trans OEQ OLT x y z. +Definition lt_eq x y z : x<y -> y==z -> x<z := trans OLT OEQ x y z. +Definition eq_le x y z : x==y -> y<=z -> x<=z := trans OEQ OLE x y z. +Definition le_eq x y z : x<=y -> y==z -> x<=z := trans OLE OEQ x y z. Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z. Proof. eauto using eq_trans, eq_sym. Qed. @@ -176,7 +177,7 @@ end. Ltac order_eq x y eqn := match x with | y => clear eqn - | _ => change (#EQ x y) in eqn; order_rewr x eqn + | _ => change (#OEQ x y) in eqn; order_rewr x eqn end. (** Goal preparation : We turn all negative hyps into positive ones diff --git a/theories/Structures/OrderedType2Alt.v b/theories/Structures/OrderedType2Alt.v index 43b3d05f8..6c2fb0d3f 100644 --- a/theories/Structures/OrderedType2Alt.v +++ b/theories/Structures/OrderedType2Alt.v @@ -13,42 +13,15 @@ (* $Id$ *) -Require Import OrderedType2. +Require Import OrderedType OrderedType2. Set Implicit Arguments. -(** NB: Instead of [comparison], defined in [Datatypes.v] which is [Eq|Lt|Gt], - we used historically the dependent type [compare] which is - [EQ _ | LT _ | GT _ ] -*) - -Inductive Compare (X : Type) (lt eq : X -> X -> Prop) (x y : X) : Type := - | LT : lt x y -> Compare lt eq x y - | EQ : eq x y -> Compare lt eq x y - | GT : lt y x -> Compare lt eq x y. - (** * Some alternative (but equivalent) presentations for an Ordered Type inferface. *) (** ** The original interface *) -Module Type OrderedTypeOrig. - Parameter Inline t : Type. - - Parameter Inline eq : t -> t -> Prop. - Axiom eq_refl : forall x : t, eq x x. - Axiom eq_sym : forall x y : t, eq x y -> eq y x. - Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. - - Parameter Inline lt : t -> t -> Prop. - Axiom lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. - Axiom lt_not_eq : forall x y : t, lt x y -> ~ eq x y. - - Parameter compare : forall x y : t, Compare lt eq x y. - - Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans. - -End OrderedTypeOrig. +Module Type OrderedTypeOrig := OrderedType.OrderedType. (** ** An interface based on compare *) @@ -69,43 +42,31 @@ End OrderedTypeAlt. (** ** From OrderedTypeOrig to OrderedType. *) -Module OrderedType_from_Orig (O:OrderedTypeOrig) <: OrderedType. +Module Update_OT (O:OrderedTypeOrig) <: OrderedType. - Import O. - Definition t := O.t. - Definition eq := O.eq. - Instance eq_equiv : Equivalence eq. - Proof. - split; red; [ apply eq_refl | apply eq_sym | eapply eq_trans ]. - Qed. + Include Update_DT O. (* Provides : t eq eq_equiv eq_dec *) Definition lt := O.lt. - Instance lt_strorder : StrictOrder lt. - Proof. - split; repeat red; intros. - eapply lt_not_eq; eauto. - eapply lt_trans; eauto. - Qed. - Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z. - Proof. - intros; destruct (compare x z); auto. - elim (@lt_not_eq x y); eauto. - elim (@lt_not_eq z y); eauto using lt_trans. - Qed. - - Lemma eq_lt : forall x y z, eq x y -> lt y z -> lt x z. + Instance lt_strorder : StrictOrder lt. Proof. - intros; destruct (compare x z); auto. - elim (@lt_not_eq y z); eauto. - elim (@lt_not_eq y x); eauto using lt_trans. + split. + intros x Hx. apply (O.lt_not_eq Hx); auto with *. + exact O.lt_trans. Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. Proof. apply proper_sym_impl_iff_2; auto with *. - repeat red; intros. - eapply lt_eq; eauto. eapply eq_lt; eauto. symmetry; auto. + intros x x' Hx y y' Hy H. + assert (H0 : lt x' y). + destruct (O.compare x' y) as [H'|H'|H']; auto. + elim (O.lt_not_eq H). transitivity x'; auto with *. + elim (O.lt_not_eq (O.lt_trans H H')); auto. + destruct (O.compare x' y') as [H'|H'|H']; auto. + elim (O.lt_not_eq H). + transitivity x'; auto with *. transitivity y'; auto with *. + elim (O.lt_not_eq (O.lt_trans H' H0)); auto with *. Qed. Definition compare x y := @@ -120,31 +81,15 @@ Module OrderedType_from_Orig (O:OrderedTypeOrig) <: OrderedType. intros; unfold compare; destruct O.compare; auto. Qed. - Definition eq_dec : forall x y, { eq x y } + { ~eq x y }. - Proof. - intros; destruct (O.compare x y). - right. apply lt_not_eq; auto. - left; auto. - right. intro. apply (@lt_not_eq y x); auto. - Defined. - -End OrderedType_from_Orig. +End Update_OT. (** ** From OrderedType to OrderedTypeOrig. *) -Module OrderedType_to_Orig (O:OrderedType) <: OrderedTypeOrig. +Module Backport_OT (O:OrderedType) <: OrderedTypeOrig. - Import O. - Definition t := t. - Definition eq := eq. - Definition lt := lt. + Include Backport_DT O. (* Provides : t eq eq_refl eq_sym eq_trans eq_dec *) - Lemma eq_refl : Reflexive eq. - Proof. auto. Qed. - Lemma eq_sym : Symmetric eq. - Proof. apply eq_equiv. Qed. - Lemma eq_trans : Transitive eq. - Proof. apply eq_equiv. Qed. + Definition lt := O.lt. Lemma lt_not_eq : forall x y, lt x y -> ~eq x y. Proof. @@ -152,23 +97,20 @@ Module OrderedType_to_Orig (O:OrderedType) <: OrderedTypeOrig. Qed. Lemma lt_trans : Transitive lt. - Proof. apply lt_strorder. Qed. + Proof. apply O.lt_strorder. Qed. Definition compare : forall x y, Compare lt eq x y. Proof. - intros. generalize (compare_spec x y); unfold Cmp, flip. - destruct (compare x y); [apply EQ|apply LT|apply GT]; auto. + intros. generalize (O.compare_spec x y); unfold Cmp, flip. + destruct (O.compare x y); [apply EQ|apply LT|apply GT]; auto. Defined. - Definition eq_dec := eq_dec. - -End OrderedType_to_Orig. +End Backport_OT. (** ** From OrderedTypeAlt to OrderedType. *) -Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType. - Import O. +Module OT_from_Alt (Import O:OrderedTypeAlt) <: OrderedType. Definition t := t. @@ -239,12 +181,11 @@ Module OrderedType_from_Alt (O:OrderedTypeAlt) <: OrderedType. case (x ?= y); [ left | right | right ]; auto; discriminate. Defined. -End OrderedType_from_Alt. +End OT_from_Alt. (** From the original presentation to this alternative one. *) -Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt. - Import O. +Module OT_to_Alt (Import O:OrderedType) <: OrderedTypeAlt. Definition t := t. Definition compare := compare. @@ -294,4 +235,4 @@ Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt. intros; apply StrictOrder_Transitive with y; auto. Qed. -End OrderedType_to_Alt. +End OT_to_Alt. diff --git a/theories/theories.itarget b/theories/theories.itarget index 09aeac753..44c6feee7 100644 --- a/theories/theories.itarget +++ b/theories/theories.itarget @@ -49,12 +49,12 @@ FSets/FMapList.vo FSets/FMapPositive.vo FSets/FMaps.vo FSets/FMapWeakList.vo +FSets/FSetCompat.vo FSets/FSetAVL.vo FSets/FSetBridge.vo FSets/FSetDecide.vo FSets/FSetEqProperties.vo FSets/FSetFacts.vo -FSets/FSetFullAVL.vo FSets/FSetInterface.vo FSets/FSetList.vo FSets/FSetProperties.vo |