diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 40 | ||||
| -rw-r--r-- | theories/FSets/FMapFacts.v | 38 | ||||
| -rw-r--r-- | theories/FSets/FMapIntMap.v | 42 | ||||
| -rw-r--r-- | theories/FSets/FMapInterface.v | 23 | ||||
| -rw-r--r-- | theories/FSets/FMapList.v | 41 | ||||
| -rw-r--r-- | theories/FSets/FMapPositive.v | 50 | ||||
| -rw-r--r-- | theories/FSets/FMapWeakList.v | 38 | ||||
| -rw-r--r-- | theories/FSets/FSetAVL.v | 8 | ||||
| -rw-r--r-- | theories/FSets/FSetEqProperties.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FSetInterface.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FSetList.v | 2 | ||||
| -rw-r--r-- | theories/FSets/FSetProperties.v | 16 | ||||
| -rw-r--r-- | theories/FSets/FSetWeakList.v | 2 | ||||
| -rw-r--r-- | theories/FSets/OrderedType.v | 6 | ||||
| -rw-r--r-- | theories/FSets/OrderedTypeAlt.v | 2 | ||||
| -rw-r--r-- | theories/FSets/OrderedTypeEx.v | 2 |
16 files changed, 151 insertions, 167 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index af3cdb8018..a31a0fd849 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -33,7 +33,7 @@ Definition key := X.t. Notation "s #1" := (fst s) (at level 9, format "s '#1'"). Notation "s #2" := (snd s) (at level 9, format "s '#2'"). -Lemma distr_pair : forall (A B:Set)(s:A*B)(a:A)(b:B), s = (a,b) -> +Lemma distr_pair : forall (A B:Type)(s:A*B)(a:A)(b:B), s = (a,b) -> s#1 = a /\ s#2 = b. Proof. destruct s; simpl; injection 1; auto. @@ -44,13 +44,13 @@ Qed. Section Elt. -Variable elt : Set. +Variable elt : Type. (** * Trees The fifth field of [Node] is the height of the tree *) -Inductive tree : Set := +Inductive tree := | Leaf : tree | Node : tree -> key -> elt -> tree -> int -> tree. @@ -403,7 +403,7 @@ Qed. (** [bal l x e r] acts as [create], but performs one step of rebalancing if necessary, i.e. assumes [|height l - height r| <= 3]. *) -Function bal (elt:Set)(l: t elt)(x:key)(e:elt)(r:t elt) : t elt := +Function bal (elt:Type)(l: t elt)(x:key)(e:elt)(r:t elt) : t elt := let hl := height l in let hr := height r in if gt_le_dec hl (hr+2) then @@ -495,7 +495,7 @@ Ltac omega_bal := match goal with (** * Insertion *) -Function add (elt:Set)(x:key)(e:elt)(s:t elt) { struct s } : t elt := +Function add (elt:Type)(x:key)(e:elt)(s:t elt) { struct s } : t elt := match s with | Leaf => Node (Leaf _) x e (Leaf _) 1 | Node l y e' r h => @@ -602,7 +602,7 @@ Qed. for [t=Leaf], we pre-unpack [t] (and forget about [h]). *) -Function remove_min (elt:Set)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t elt*(key*elt) := +Function remove_min (elt:Type)(l:t elt)(x:key)(e:elt)(r:t elt) { struct l } : t elt*(key*elt) := match l with | Leaf => (r,(x,e)) | Node ll lx le lr lh => let (l',m) := (remove_min ll lx le lr : t elt*(key*elt)) in (bal l' x e r, m) @@ -709,7 +709,7 @@ Qed. [|height t1 - height t2| <= 2]. *) -Function merge (elt:Set) (s1 s2 : t elt) : tree elt := match s1,s2 with +Function merge (elt:Type) (s1 s2 : t elt) : tree elt := match s1,s2 with | Leaf, _ => s2 | _, Leaf => s1 | _, Node l2 x2 e2 r2 h2 => @@ -793,7 +793,7 @@ Qed. (** * Deletion *) -Function remove (elt:Set)(x:key)(s:t elt) { struct s } : t elt := match s with +Function remove (elt:Type)(x:key)(s:t elt) { struct s } : t elt := match s with | Leaf => Leaf _ | Node l y e r h => match X.compare x y with @@ -903,7 +903,7 @@ Qed. Section Elt2. -Variable elt:Set. +Variable elt:Type. Notation eqk := (PX.eqk (elt:= elt)). Notation eqke := (PX.eqke (elt:= elt)). @@ -1173,7 +1173,7 @@ Definition Equivb (cmp:elt->elt->bool) m m' := (** ** Enumeration of the elements of a tree *) -Inductive enumeration : Set := +Inductive enumeration := | End : enumeration | More : key -> elt -> t elt -> enumeration -> enumeration. @@ -1392,7 +1392,7 @@ End Elt2. Section Elts. -Variable elt elt' elt'' : Set. +Variable elt elt' elt'' : Type. Section Map. Variable f : elt -> elt'. @@ -1588,7 +1588,7 @@ Proof. unfold map2; intros; apply anti_elements_bst; auto. Qed. -Lemma find_elements : forall (elt:Set)(m: t elt) x, bst m -> +Lemma find_elements : forall (elt:Type)(m: t elt) x, bst m -> L.find x (elements m) = find x m. Proof. intros. @@ -1672,14 +1672,14 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Module E := X. Module Raw := Raw I X. - Record bbst (elt:Set) : Set := + Record bbst (elt:Type) := Bbst {this :> Raw.tree elt; is_bst : Raw.bst this; is_avl: Raw.avl this}. Definition t := bbst. Definition key := E.t. Section Elt. - Variable elt elt' elt'': Set. + Variable elt elt' elt'': Type. Implicit Types m : t elt. Implicit Types x y : key. @@ -1814,27 +1814,27 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. End Elt. - Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m). Proof. intros elt elt' m x e f; exact (@Raw.map_1 elt elt' f m.(this) x e). Qed. - Lemma map_2 : forall (elt elt':Set)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m. + Lemma map_2 : forall (elt elt':Type)(m:t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m. Proof. intros elt elt' m x f; do 2 unfold In in *; do 2 rewrite Raw.In_alt; simpl. apply Raw.map_2; auto. Qed. - Lemma mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt) (f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. intros elt elt' m x e f; exact (@Raw.mapi_1 elt elt' f m.(this) x e). Qed. - Lemma mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key) (f:key->elt->elt'), In x (mapi f m) -> In x m. Proof. intros elt elt' m x f; unfold In in *; do 2 rewrite Raw.In_alt; simpl; apply Raw.mapi_2; auto. Qed. - Lemma map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). @@ -1845,7 +1845,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. apply m'.(is_bst). Qed. - Lemma map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. Proof. diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 6bdff3d7b5..87111b1a75 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -32,7 +32,7 @@ Proof. destruct b; destruct b'; intuition. Qed. -Lemma MapsTo_fun : forall (elt:Set) m x (e e':elt), +Lemma MapsTo_fun : forall (elt:Type) m x (e e':elt), MapsTo x e m -> MapsTo x e' m -> e=e'. Proof. intros. @@ -43,7 +43,7 @@ Qed. (** ** Specifications written using equivalences *) Section IffSpec. -Variable elt elt' elt'': Set. +Variable elt elt' elt'': Type. Implicit Type m: t elt. Implicit Type x y z: key. Implicit Type e: elt. @@ -308,7 +308,7 @@ Ltac map_iff := Section BoolSpec. -Lemma mem_find_b : forall (elt:Set)(m:t elt)(x:key), mem x m = if find x m then true else false. +Lemma mem_find_b : forall (elt:Type)(m:t elt)(x:key), mem x m = if find x m then true else false. Proof. intros. generalize (find_mapsto_iff m x)(mem_in_iff m x); unfold In. @@ -320,7 +320,7 @@ destruct H0 as (e,H0). destruct (H e); intuition discriminate. Qed. -Variable elt elt' elt'' : Set. +Variable elt elt' elt'' : Type. Implicit Types m : t elt. Implicit Types x y z : key. Implicit Types e : elt. @@ -449,7 +449,7 @@ intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. destruct (eq_dec x y); auto. Qed. -Definition option_map (A:Set)(B:Set)(f:A->B)(o:option A) : option B := +Definition option_map (A B:Type)(f:A->B)(o:option A) : option B := match o with | Some a => Some (f a) | None => None @@ -570,7 +570,7 @@ End BoolSpec. Section Equalities. -Variable elt:Set. +Variable elt:Type. (** * Relations between [Equal], [Equiv] and [Equivb]. *) @@ -638,18 +638,18 @@ End Equalities. (** * [Equal] is a setoid equality. *) -Lemma Equal_refl : forall (elt:Set)(m : t elt), Equal m m. +Lemma Equal_refl : forall (elt:Type)(m : t elt), Equal m m. Proof. red; reflexivity. Qed. -Lemma Equal_sym : forall (elt:Set)(m m' : t elt), +Lemma Equal_sym : forall (elt:Type)(m m' : t elt), Equal m m' -> Equal m' m. Proof. unfold Equal; auto. Qed. -Lemma Equal_trans : forall (elt:Set)(m m' m'' : t elt), +Lemma Equal_trans : forall (elt:Type)(m m' m'' : t elt), Equal m m' -> Equal m' m'' -> Equal m m''. Proof. unfold Equal; congruence. Qed. -Definition Equal_ST : forall elt:Set, Setoid_Theory (t elt) (@Equal _). +Definition Equal_ST : forall elt:Type, Setoid_Theory (t elt) (@Equal _). Proof. constructor; [apply Equal_refl | apply Equal_sym | apply Equal_trans]. Qed. @@ -758,7 +758,7 @@ Module WProperties (E:DecidableType)(M:WSfun E). Import M. Section Elt. - Variable elt:Set. + Variable elt:Type. Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m). @@ -789,7 +789,7 @@ Module WProperties (E:DecidableType)(M:WSfun E). rewrite <-elements_Empty; apply empty_1. Qed. - Lemma fold_Empty : forall m (A:Set)(f:key->elt->A->A)(i:A), + Lemma fold_Empty : forall m (A:Type)(f:key->elt->A->A)(i:A), Empty m -> fold f m i = i. Proof. intros. @@ -807,7 +807,7 @@ Module WProperties (E:DecidableType)(M:WSfun E). exists (a,b); auto. Qed. - Lemma fold_Equal : forall m1 m2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) + Lemma fold_Equal : forall m1 m2 (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) (f:key->elt->A->A)(i:A), compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> transpose eqA (fun y => f (fst y) (snd y)) -> @@ -832,7 +832,7 @@ Module WProperties (E:DecidableType)(M:WSfun E). rewrite H1; split; auto. Qed. - Lemma fold_Add : forall m1 m2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) + Lemma fold_Add : forall m1 m2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) (f:key->elt->A->A)(i:A), compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> transpose eqA (fun y =>f (fst y) (snd y)) -> @@ -1124,7 +1124,7 @@ Module OrdProperties (M:S). Import M. Section Elt. - Variable elt:Set. + Variable elt:Type. Notation eqke := (@eqke elt). Notation eqk := (@eqk elt). @@ -1509,7 +1509,7 @@ Module OrdProperties (M:S). (** The following lemma has already been proved on Weak Maps, but with one additionnal hypothesis (some [transpose] fact). *) - Lemma fold_Equal : forall s1 s2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) + Lemma fold_Equal : forall s1 s2 (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) (f:key->elt->A->A)(i:A), compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> Equal s1 s2 -> @@ -1523,7 +1523,7 @@ Module OrdProperties (M:S). apply elements_Equal_eqlistA; auto. Qed. - Lemma fold_Add : forall s1 s2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) + Lemma fold_Add : forall s1 s2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) (f:key->elt->A->A)(i:A), compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> transpose eqA (fun y =>f (fst y) (snd y)) -> @@ -1546,7 +1546,7 @@ Module OrdProperties (M:S). apply fold_right_commutes with (eqA:=eqke) (eqB:=eqA); auto. Qed. - Lemma fold_Add_Above : forall s1 s2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) + Lemma fold_Add_Above : forall s1 s2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) (f:key->elt->A->A)(i:A), compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> Above x s1 -> Add x e s1 s2 -> @@ -1562,7 +1562,7 @@ Module OrdProperties (M:S). refl_st. Qed. - Lemma fold_Add_Below : forall s1 s2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) + Lemma fold_Add_Below : forall s1 s2 x e (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory A eqA) (f:key->elt->A->A)(i:A), compat_op eqke eqA (fun y =>f (fst y) (snd y)) -> Below x s1 -> Add x e s1 s2 -> diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v index 0c180fcbd1..26b892885b 100644 --- a/theories/FSets/FMapIntMap.v +++ b/theories/FSets/FMapIntMap.v @@ -77,7 +77,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. Definition t := Map. Section A. - Variable A:Set. + Variable A:Type. Definition empty : t A := M0 A. @@ -343,7 +343,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. End Spec. - Variable B : Set. + Variable B : Type. Fixpoint mapi_aux (pf:N->N)(f : N -> A -> B)(m:t A) { struct m }: t B := match m with @@ -359,7 +359,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. End A. - Lemma mapi_aux_1 : forall (elt elt':Set)(m: t elt)(pf:N->N)(x:key)(e:elt) + Lemma mapi_aux_1 : forall (elt elt':Type)(m: t elt)(pf:N->N)(x:key)(e:elt) (f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f (pf y) e) (mapi_aux pf f m). Proof. @@ -387,14 +387,14 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. rewrite Hy in Hy'; simpl in Hy'; auto. Qed. - Lemma mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt) (f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. intros elt elt' m; exact (mapi_aux_1 (fun n => n)). Qed. - Lemma mapi_aux_2 : forall (elt elt':Set)(m: t elt)(pf:N->N)(x:key) + Lemma mapi_aux_2 : forall (elt elt':Type)(m: t elt)(pf:N->N)(x:key) (f:key->elt->elt'), In x (mapi_aux pf f m) -> In x m. Proof. unfold In, MapsTo. @@ -407,20 +407,20 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. destruct x; [|destruct p]; eauto. Qed. - Lemma mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key) (f:key->elt->elt'), In x (mapi f m) -> In x m. Proof. intros elt elt' m; exact (mapi_aux_2 m (fun n => n)). Qed. - Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m). Proof. unfold map; intros. destruct (@mapi_1 _ _ m x e (fun _ => f)) as (e',(_,H0)); auto. Qed. - Lemma map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), + Lemma map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m. Proof. unfold map; intros. @@ -433,12 +433,12 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. Anyway, map2 isn't in Ocaml... *) - Definition anti_elements (A:Set)(l:list (key*A)) := L.fold (@add _) l (empty _). + Definition anti_elements (A:Type)(l:list (key*A)) := L.fold (@add _) l (empty _). - Definition map2 (A B C:Set)(f:option A->option B -> option C)(m:t A)(m':t B) : t C := + Definition map2 (A B C:Type)(f:option A->option B -> option C)(m:t A)(m':t B) : t C := anti_elements (L.map2 f (elements m) (elements m')). - Lemma add_spec : forall (A:Set)(m:t A) x y e, + Lemma add_spec : forall (A:Type)(m:t A) x y e, find x (add y e m) = if ME.eq_dec x y then Some e else find x m. Proof. intros. @@ -457,7 +457,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. apply (@add_3 _ m y x a e); unfold E.eq in *; auto. Qed. - Lemma anti_elements_mapsto_aux : forall (A:Set)(l:list (key*A)) m k e, + Lemma anti_elements_mapsto_aux : forall (A:Type)(l:list (key*A)) m k e, NoDupA (eq_key (A:=A)) l -> (forall x, L.PX.In x l -> In x m -> False) -> (MapsTo k e (L.fold (@add _) l m) <-> L.PX.MapsTo k e l \/ MapsTo k e m). @@ -501,7 +501,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. right; apply add_2; unfold E.eq in *; auto. Qed. - Lemma anti_elements_mapsto : forall (A:Set) l k e, NoDupA (eq_key (A:=A)) l -> + Lemma anti_elements_mapsto : forall (A:Type) l k e, NoDupA (eq_key (A:=A)) l -> (MapsTo k e (anti_elements l) <-> L.PX.MapsTo k e l). Proof. intros. @@ -513,7 +513,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. inversion H1. Qed. - Lemma find_anti_elements : forall (A:Set)(l: list (key*A)) x, sort (@lt_key _) l -> + Lemma find_anti_elements : forall (A:Type)(l: list (key*A)) x, sort (@lt_key _) l -> find x (anti_elements l) = L.find x l. Proof. intros. @@ -530,7 +530,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. apply find_2; auto. Qed. - Lemma find_elements : forall (A:Set)(m: t A) x, + Lemma find_elements : forall (A:Type)(m: t A) x, L.find x (elements m) = find x m. Proof. intros. @@ -546,7 +546,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. apply L.find_2; auto. Qed. - Lemma elements_in : forall (A:Set)(s:t A) x, L.PX.In x (elements s) <-> In x s. + Lemma elements_in : forall (A:Type)(s:t A) x, L.PX.In x (elements s) <-> In x s. Proof. intros. unfold L.PX.In, In. @@ -560,7 +560,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. rewrite find_elements; auto. Qed. - Lemma map2_1 : forall (A B C:Set)(m: t A)(m': t B)(x:key) + Lemma map2_1 : forall (A B C:Type)(m: t A)(m': t B)(x:key) (f:option A->option B ->option C), In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). Proof. @@ -577,7 +577,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. apply elements_3; auto. Qed. - Lemma map2_2 : forall (A B C: Set)(m: t A)(m': t B)(x:key) + Lemma map2_2 : forall (A B C:Type)(m: t A)(m': t B)(x:key) (f:option A->option B ->option C), In x (map2 f m m') -> In x m \/ In x m'. Proof. @@ -597,11 +597,11 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. (** same trick for [equal] *) - Definition equal (A:Set)(cmp:A -> A -> bool)(m m' : t A) : bool := + Definition equal (A:Type)(cmp:A -> A -> bool)(m m' : t A) : bool := L.equal cmp (elements m) (elements m'). Lemma equal_1 : - forall (A:Set)(m: t A)(m': t A)(cmp: A -> A -> bool), + forall (A:Type)(m: t A)(m': t A)(cmp: A -> A -> bool), Equivb cmp m m' -> equal cmp m m' = true. Proof. unfold equal, Equivb, Equiv, Cmp. @@ -619,7 +619,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType. Qed. Lemma equal_2 : - forall (A:Set)(m: t A)(m': t A)(cmp: A -> A -> bool), + forall (A:Type)(m: t A)(m': t A)(cmp: A -> A -> bool), equal cmp m m' = true -> Equivb cmp m m'. Proof. unfold equal, Equivb, Equiv, Cmp. diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index 9a7d4ab82b..917534e195 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -48,7 +48,7 @@ Unset Strict Implicit. *) -Definition Cmp (elt:Set)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true. +Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true. (** ** Weak signature for maps @@ -63,12 +63,12 @@ Module Type WSfun (E : EqualityType). Definition key := E.t. - Parameter t : Set -> Set. + Parameter t : Type -> Type. (** the abstract type of maps *) Section Types. - Variable elt:Set. + Variable elt:Type. Parameter empty : t elt. (** The empty map. *) @@ -93,8 +93,7 @@ Module Type WSfun (E : EqualityType). (** [mem x m] returns [true] if [m] contains a binding for [x], and [false] otherwise. *) - Variable elt' : Set. - Variable elt'': Set. + Variable elt' elt'' : Type. Parameter map : (elt -> elt') -> t elt -> t elt'. (** [map f m] returns a map with same domain as [m], where the associated @@ -225,25 +224,25 @@ Module Type WSfun (E : EqualityType). End Types. (** Specification of [map] *) - Parameter map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + Parameter map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m). - Parameter map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), + Parameter map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m. (** Specification of [mapi] *) - Parameter mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + Parameter mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt) (f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). - Parameter mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + Parameter mapi_2 : forall (elt elt':Type)(m: t elt)(x:key) (f:key->elt->elt'), In x (mapi f m) -> In x m. (** Specification of [map2] *) - Parameter map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Parameter map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). - Parameter map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Parameter map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. @@ -273,7 +272,7 @@ End WS. Module Type Sfun (E : OrderedType). Include Type WSfun E. Section elt. - Variable elt:Set. + Variable elt:Type. Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p'). (* Additional specification of [elements] *) Parameter elements_3 : forall m, sort lt_key (elements m). diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index a47d431b34..e2ea687945 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -25,19 +25,10 @@ Module Import MX := OrderedTypeFacts X. Module Import PX := KeyOrderedType X. Definition key := X.t. -Definition t (elt:Set) := list (X.t * elt). +Definition t (elt:Type) := list (X.t * elt). Section Elt. -Variable elt : Set. - -(* Now in KeyOrderedType: -Definition eqk (p p':key*elt) := X.eq (fst p) (fst p'). -Definition eqke (p p':key*elt) := - X.eq (fst p) (fst p') /\ (snd p) = (snd p'). -Definition ltk (p p':key*elt) := X.lt (fst p) (fst p'). -Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). -Definition In k m := exists e:elt, MapsTo k e m. -*) +Variable elt : Type. Notation eqk := (eqk (elt:=elt)). Notation eqke := (eqke (elt:=elt)). @@ -523,7 +514,7 @@ Proof. rewrite H2; simpl; auto. Qed. -Variable elt':Set. +Variable elt':Type. (** * [map] and [mapi] *) @@ -544,7 +535,7 @@ Section Elt2. (* A new section is necessary for previous definitions to work with different [elt], especially [MapsTo]... *) -Variable elt elt' : Set. +Variable elt elt' : Type. (** Specification of [map] *) @@ -680,10 +671,10 @@ Section Elt3. (** * [map2] *) -Variable elt elt' elt'' : Set. +Variable elt elt' elt'' : Type. Variable f : option elt -> option elt' -> option elt''. -Definition option_cons (A:Set)(k:key)(o:option A)(l:list (key*A)) := +Definition option_cons (A:Type)(k:key)(o:option A)(l:list (key*A)) := match o with | Some e => (k,e)::l | None => l @@ -735,7 +726,7 @@ Fixpoint combine (m : t elt) : t elt' -> t oee' := end end. -Definition fold_right_pair (A B C:Set)(f: A->B->C->C)(l:list (A*B))(i:C) := +Definition fold_right_pair (A B C:Type)(f: A->B->C->C)(l:list (A*B))(i:C) := List.fold_right (fun p => f (fst p) (snd p)) i l. Definition map2_alt m m' := @@ -1034,12 +1025,12 @@ Module E := X. Definition key := E.t. -Record slist (elt:Set) : Set := +Record slist (elt:Type) := {this :> Raw.t elt; sorted : sort (@Raw.PX.ltk elt) this}. -Definition t (elt:Set) : Set := slist elt. +Definition t (elt:Type) : Type := slist elt. Section Elt. - Variable elt elt' elt'':Set. + Variable elt elt' elt'':Type. Implicit Types m : t elt. Implicit Types x y : key. @@ -1132,22 +1123,22 @@ Section Elt. End Elt. - Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m). Proof. intros elt elt' m; exact (@Raw.map_1 elt elt' m.(this)). Qed. - Lemma map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), + Lemma map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m. Proof. intros elt elt' m; exact (@Raw.map_2 elt elt' m.(this)). Qed. - Lemma mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt) (f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. intros elt elt' m; exact (@Raw.mapi_1 elt elt' m.(this)). Qed. - Lemma mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key) (f:key->elt->elt'), In x (mapi f m) -> In x m. Proof. intros elt elt' m; exact (@Raw.mapi_2 elt elt' m.(this)). Qed. - Lemma map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). @@ -1155,7 +1146,7 @@ Section Elt. intros elt elt' elt'' m m' x f; exact (@Raw.map2_1 elt elt' elt'' f m.(this) m.(sorted) m'.(this) m'.(sorted) x). Qed. - Lemma map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. Proof. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 1273e5403a..6903b67aee 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -170,14 +170,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Definition key := positive. - Inductive tree (A : Set) : Set := + Inductive tree (A : Type) := | Leaf : tree A | Node : tree A -> option A -> tree A -> tree A. Definition t := tree. Section A. - Variable A:Set. + Variable A:Type. Implicit Arguments Leaf [A]. @@ -818,7 +818,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. (** [map] and [mapi] *) - Variable B : Set. + Variable B : Type. Fixpoint xmapi (f : positive -> A -> B) (m : t A) (i : positive) {struct m} : t B := @@ -836,7 +836,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End A. Lemma xgmapi: - forall (A B: Set) (f: positive -> A -> B) (i j : positive) (m: t A), + forall (A B: Type) (f: positive -> A -> B) (i j : positive) (m: t A), find i (xmapi f m j) = option_map (f (append j i)) (find i m). Proof. induction i; intros; destruct m; simpl; auto. @@ -846,7 +846,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Theorem gmapi: - forall (A B: Set) (f: positive -> A -> B) (i: positive) (m: t A), + forall (A B: Type) (f: positive -> A -> B) (i: positive) (m: t A), find i (mapi f m) = option_map (f i) (find i m). Proof. intros. @@ -857,7 +857,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma mapi_1 : - forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:key->elt->elt'), + forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. @@ -872,7 +872,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. Lemma mapi_2 : - forall (elt elt':Set)(m: t elt)(x:key)(f:key->elt->elt'), + forall (elt elt':Type)(m: t elt)(x:key)(f:key->elt->elt'), In x (mapi f m) -> In x m. Proof. intros. @@ -885,21 +885,21 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. simpl in *; discriminate. Qed. - Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m). Proof. intros; unfold map. destruct (mapi_1 (fun _ => f) H); intuition. Qed. - Lemma map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), + Lemma map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m. Proof. intros; unfold map in *; eapply mapi_2; eauto. Qed. Section map2. - Variable A B C : Set. + Variable A B C : Type. Variable f : option A -> option B -> option C. Implicit Arguments Leaf [A]. @@ -948,10 +948,10 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. End map2. - Definition map2 (elt elt' elt'':Set)(f:option elt->option elt'->option elt'') := + Definition map2 (elt elt' elt'':Type)(f:option elt->option elt'->option elt'') := _map2 (fun o1 o2 => match o1,o2 with None,None => None | _, _ => f o1 o2 end). - Lemma map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). @@ -967,7 +967,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. destruct H; intuition; try discriminate. Qed. - Lemma map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. Proof. @@ -983,17 +983,17 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. - Definition fold (A : Set)(B : Type) (f: positive -> A -> B -> B) (tr: t A) (v: B) := + Definition fold (A : Type)(B : Type) (f: positive -> A -> B -> B) (tr: t A) (v: B) := List.fold_left (fun a p => f (fst p) (snd p) a) (elements tr) v. Lemma fold_1 : - forall (A:Set)(m:t A)(B:Type)(i : B) (f : key -> A -> B -> B), + forall (A:Type)(m:t A)(B:Type)(i : B) (f : key -> A -> B -> B), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i. Proof. intros; unfold fold; auto. Qed. - Fixpoint equal (A:Set)(cmp : A -> A -> bool)(m1 m2 : t A) {struct m1} : bool := + Fixpoint equal (A:Type)(cmp : A -> A -> bool)(m1 m2 : t A) {struct m1} : bool := match m1, m2 with | Leaf, _ => is_empty m2 | _, Leaf => is_empty m1 @@ -1006,14 +1006,14 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. && equal cmp l1 l2 && equal cmp r1 r2 end. - Definition Equal (A:Set)(m m':t A) := + Definition Equal (A:Type)(m m':t A) := forall y, find y m = find y m'. - Definition Equiv (A:Set)(eq_elt:A->A->Prop) m m' := + Definition Equiv (A:Type)(eq_elt:A->A->Prop) m m' := (forall k, In k m <-> In k m') /\ (forall k e e', MapsTo k e m -> MapsTo k e' m' -> eq_elt e e'). - Definition Equivb (A:Set)(cmp: A->A->bool) := Equiv (Cmp cmp). + Definition Equivb (A:Type)(cmp: A->A->bool) := Equiv (Cmp cmp). - Lemma equal_1 : forall (A:Set)(m m':t A)(cmp:A->A->bool), + Lemma equal_1 : forall (A:Type)(m m':t A)(cmp:A->A->bool), Equivb cmp m m' -> equal cmp m m' = true. Proof. induction m. @@ -1067,7 +1067,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply andb_true_intro; split; auto. Qed. - Lemma equal_2 : forall (A:Set)(m m':t A)(cmp:A->A->bool), + Lemma equal_2 : forall (A:Type)(m m':t A)(cmp:A->A->bool), equal cmp m m' = true -> Equivb cmp m m'. Proof. induction m. @@ -1127,7 +1127,7 @@ Module PositiveMapAdditionalFacts. (* Derivable from the Map interface *) Theorem gsspec: - forall (A:Set)(i j: positive) (x: A) (m: t A), + forall (A:Type)(i j: positive) (x: A) (m: t A), find i (add j x m) = if peq_dec i j then Some x else find i m. Proof. intros. @@ -1136,7 +1136,7 @@ Module PositiveMapAdditionalFacts. (* Not derivable from the Map interface *) Theorem gsident: - forall (A:Set)(i: positive) (m: t A) (v: A), + forall (A:Type)(i: positive) (m: t A) (v: A), find i m = Some v -> add i v m = m. Proof. induction i; intros; destruct m; simpl; simpl in H; try congruence. @@ -1145,7 +1145,7 @@ Module PositiveMapAdditionalFacts. Qed. Lemma xmap2_lr : - forall (A B : Set)(f g: option A -> option A -> option B)(m : t A), + forall (A B : Type)(f g: option A -> option A -> option B)(m : t A), (forall (i j : option A), f i j = g j i) -> xmap2_l f m = xmap2_r g m. Proof. @@ -1156,7 +1156,7 @@ Module PositiveMapAdditionalFacts. Qed. Theorem map2_commut: - forall (A B: Set) (f g: option A -> option A -> option B), + forall (A B: Type) (f g: option A -> option A -> option B), (forall (i j: option A), f i j = g j i) -> forall (m1 m2: t A), _map2 f m1 m2 = _map2 g m2 m1. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 0be7351cc6..0c12516c4b 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -23,17 +23,11 @@ Module Raw (X:DecidableType). Module Import PX := KeyDecidableType X. Definition key := X.t. -Definition t (elt:Set) := list (X.t * elt). +Definition t (elt:Type) := list (X.t * elt). Section Elt. -Variable elt : Set. - -(* now in KeyDecidableType: -Definition eqk (p p':key*elt) := X.eq (fst p) (fst p'). -Definition eqke (p p':key*elt) := - X.eq (fst p) (fst p') /\ (snd p) = (snd p'). -*) +Variable elt : Type. Notation eqk := (eqk (elt:=elt)). Notation eqke := (eqke (elt:=elt)). @@ -457,7 +451,7 @@ Proof. firstorder. Qed. -Variable elt':Set. +Variable elt':Type. (** * [map] and [mapi] *) @@ -478,7 +472,7 @@ Section Elt2. (* A new section is necessary for previous definitions to work with different [elt], especially [MapsTo]... *) -Variable elt elt' : Set. +Variable elt elt' : Type. (** Specification of [map] *) @@ -598,7 +592,7 @@ Qed. End Elt2. Section Elt3. -Variable elt elt' elt'' : Set. +Variable elt elt' elt'' : Type. Notation oee' := (option elt * option elt')%type. @@ -608,7 +602,7 @@ Definition combine_l (m:t elt)(m':t elt') : t oee' := Definition combine_r (m:t elt)(m':t elt') : t oee' := mapi (fun k e' => (find k m, Some e')) m'. -Definition fold_right_pair (A B C:Set)(f:A->B->C->C)(l:list (A*B))(i:C) := +Definition fold_right_pair (A B C:Type)(f:A->B->C->C)(l:list (A*B))(i:C) := List.fold_right (fun p => f (fst p) (snd p)) i l. Definition combine (m:t elt)(m':t elt') : t oee' := @@ -732,7 +726,7 @@ Qed. Variable f : option elt -> option elt' -> option elt''. -Definition option_cons (A:Set)(k:key)(o:option A)(l:list (key*A)) := +Definition option_cons (A:Type)(k:key)(o:option A)(l:list (key*A)) := match o with | Some e => (k,e)::l | None => l @@ -874,12 +868,12 @@ Module Make (X: DecidableType) <: WS with Module E:=X. Module E := X. Definition key := E.t. - Record slist (elt:Set) : Set := + Record slist (elt:Type) := {this :> Raw.t elt; NoDup : NoDupA (@Raw.PX.eqk elt) this}. - Definition t (elt:Set) := slist elt. + Definition t (elt:Type) := slist elt. Section Elt. - Variable elt elt' elt'':Set. + Variable elt elt' elt'':Type. Implicit Types m : t elt. Implicit Types x y : key. @@ -968,22 +962,22 @@ Section Elt. End Elt. - Lemma map_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt)(f:elt->elt'), + Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'), MapsTo x e m -> MapsTo x (f e) (map f m). Proof. intros elt elt' m; exact (@Raw.map_1 elt elt' m.(this)). Qed. - Lemma map_2 : forall (elt elt':Set)(m: t elt)(x:key)(f:elt->elt'), + Lemma map_2 : forall (elt elt':Type)(m: t elt)(x:key)(f:elt->elt'), In x (map f m) -> In x m. Proof. intros elt elt' m; exact (@Raw.map_2 elt elt' m.(this)). Qed. - Lemma mapi_1 : forall (elt elt':Set)(m: t elt)(x:key)(e:elt) + Lemma mapi_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt) (f:key->elt->elt'), MapsTo x e m -> exists y, E.eq y x /\ MapsTo x (f y e) (mapi f m). Proof. intros elt elt' m; exact (@Raw.mapi_1 elt elt' m.(this)). Qed. - Lemma mapi_2 : forall (elt elt':Set)(m: t elt)(x:key) + Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key) (f:key->elt->elt'), In x (mapi f m) -> In x m. Proof. intros elt elt' m; exact (@Raw.mapi_2 elt elt' m.(this)). Qed. - Lemma map2_1 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Lemma map2_1 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x m \/ In x m' -> find x (map2 f m m') = f (find x m) (find x m'). @@ -991,7 +985,7 @@ Section Elt. intros elt elt' elt'' m m' x f; exact (@Raw.map2_1 elt elt' elt'' f m.(this) m.(NoDup) m'.(this) m'.(NoDup) x). Qed. - Lemma map2_2 : forall (elt elt' elt'':Set)(m: t elt)(m': t elt') + Lemma map2_2 : forall (elt elt' elt'':Type)(m: t elt)(m': t elt') (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. Proof. diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index 5c701c0055..3a08b0f4f1 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -34,7 +34,7 @@ Definition elt := X.t. Notation "s #1" := (fst s) (at level 9, format "s '#1'"). Notation "s #2" := (snd s) (at level 9, format "s '#2'"). -Lemma distr_pair : forall (A B:Set)(s:A*B)(a:A)(b:B), s = (a,b) -> +Lemma distr_pair : forall (A B:Type)(s:A*B)(a:A)(b:B), s = (a,b) -> s#1 = a /\ s#2 = b. Proof. destruct s; simpl; injection 1; auto. @@ -45,7 +45,7 @@ Qed. The fourth field of [Node] is the height of the tree *) -Inductive tree : Set := +Inductive tree := | Leaf : tree | Node : tree -> X.t -> tree -> int -> tree. @@ -2092,7 +2092,7 @@ Qed. (** ** Enumeration of the elements of a tree *) -Inductive enumeration : Set := +Inductive enumeration := | End : enumeration | More : elt -> tree -> enumeration -> enumeration. @@ -2360,7 +2360,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X. Module E := X. Module Raw := Raw I X. - Record bbst : Set := Bbst {this :> Raw.t; is_bst : Raw.bst this; is_avl: Raw.avl this}. + Record bbst := Bbst {this :> Raw.t; is_bst : Raw.bst this; is_avl: Raw.avl this}. Definition t := bbst. Definition elt := E.t. diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index e0e83c57c8..55cfd7e7c3 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -494,7 +494,7 @@ destruct (mem x s); destruct (mem x s'); intuition. Qed. Section Fold. -Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA). +Variables (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA). Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f). Variables (i:A). Variables (s s':t)(x:elt). @@ -892,7 +892,7 @@ rewrite filter_iff; auto; set_iff; tauto. Qed. Lemma fold_compat : - forall (A:Set)(eqA:A->A->Prop)(st:(Setoid_Theory _ eqA)) + forall (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA) (f g:elt->A->A), (compat_op E.eq eqA f) -> (transpose eqA f) -> (compat_op E.eq eqA g) -> (transpose eqA g) -> diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index eb2a730868..bc0cf95e18 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -52,7 +52,7 @@ Module Type WSfun (E : EqualityType). Definition elt := E.t. - Parameter t : Set. (** the abstract type of sets *) + Parameter t : Type. (** the abstract type of sets *) (** Logical predicates *) Parameter In : elt -> t -> Prop. @@ -386,7 +386,7 @@ Module Type Sdep. Declare Module E : OrderedType. Definition elt := E.t. - Parameter t : Set. + Parameter t : Type. Parameter In : elt -> t -> Prop. Definition Equal s s' := forall a : elt, In a s <-> In a s'. diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v index 01060eccee..928083b601 100644 --- a/theories/FSets/FSetList.v +++ b/theories/FSets/FSetList.v @@ -1054,7 +1054,7 @@ Module Make (X: OrderedType) <: S with Module E := X. Module Raw := Raw X. Module E := X. - Record slist : Set := {this :> Raw.t; sorted : sort E.lt this}. + Record slist := {this :> Raw.t; sorted : sort E.lt this}. Definition t := slist. Definition elt := E.t. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 93adf67902..f3da02a832 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -317,7 +317,7 @@ Module WProperties (Import E : DecidableType)(M : WSfun E). *) Lemma fold_0 : - forall s (A : Set) (i : A) (f : elt -> A -> A), + forall s (A : Type) (i : A) (f : elt -> A -> A), exists l : list elt, NoDup l /\ (forall x : elt, In x s <-> InA E.eq x l) /\ @@ -338,7 +338,7 @@ Module WProperties (Import E : DecidableType)(M : WSfun E). [fold_2]. *) Lemma fold_1 : - forall s (A : Set) (eqA : A -> A -> Prop) + forall s (A : Type) (eqA : A -> A -> Prop) (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A), Empty s -> eqA (fold f s i) i. Proof. @@ -351,7 +351,7 @@ Module WProperties (Import E : DecidableType)(M : WSfun E). Qed. Lemma fold_2 : - forall s s' x (A : Set) (eqA : A -> A -> Prop) + forall s s' x (A : Type) (eqA : A -> A -> Prop) (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A), compat_op E.eq eqA f -> transpose eqA f -> @@ -371,7 +371,7 @@ Module WProperties (Import E : DecidableType)(M : WSfun E). the initial element, it is Leibniz-equal to it. *) Lemma fold_1b : - forall s (A : Set)(i : A) (f : elt -> A -> A), + forall s (A : Type)(i : A) (f : elt -> A -> A), Empty s -> (fold f s i) = i. Proof. intros. @@ -479,7 +479,7 @@ Module WProperties (Import E : DecidableType)(M : WSfun E). (** Other properties of [fold]. *) Section Fold. - Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA). + Variables (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA). Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f). Section Fold_1. @@ -972,7 +972,7 @@ Module OrdProperties (M:S). (** More properties of [fold] : behavior with respect to Above/Below *) Lemma fold_3 : - forall s s' x (A : Set) (eqA : A -> A -> Prop) + forall s s' x (A : Type) (eqA : A -> A -> Prop) (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A), compat_op E.eq eqA f -> Above x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)). @@ -989,7 +989,7 @@ Module OrdProperties (M:S). Qed. Lemma fold_4 : - forall s s' x (A : Set) (eqA : A -> A -> Prop) + forall s s' x (A : Type) (eqA : A -> A -> Prop) (st : Setoid_Theory A eqA) (i : A) (f : elt -> A -> A), compat_op E.eq eqA f -> Below x s -> Add x s s' -> eqA (fold f s' i) (fold f s (f x i)). @@ -1010,7 +1010,7 @@ Module OrdProperties (M:S). no need for [(transpose eqA f)]. *) Section FoldOpt. - Variables (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA). + Variables (A:Type)(eqA:A->A->Prop)(st:Setoid_Theory _ eqA). Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f). Lemma fold_equal : diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 3039c058c4..866c3f6208 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -807,7 +807,7 @@ Module Make (X: DecidableType) <: WS with Module E := X. Module Raw := Raw X. Module E := X. - Record slist : Set := {this :> Raw.t; unique : NoDupA E.eq this}. + Record slist := {this :> Raw.t; unique : NoDupA E.eq this}. Definition t := slist. Definition elt := E.t. diff --git a/theories/FSets/OrderedType.v b/theories/FSets/OrderedType.v index 22a0383a90..0dfc05689a 100644 --- a/theories/FSets/OrderedType.v +++ b/theories/FSets/OrderedType.v @@ -14,14 +14,14 @@ Unset Strict Implicit. (** * Ordered types *) -Inductive Compare (X : Set) (lt eq : X -> X -> Prop) (x y : X) : Set := +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. Module Type OrderedType. - Parameter Inline t : Set. + Parameter Inline t : Type. Parameter Inline eq : t -> t -> Prop. Parameter Inline lt : t -> t -> Prop. @@ -361,7 +361,7 @@ Module KeyOrderedType(O:OrderedType). Import MO. Section Elt. - Variable elt : Set. + Variable elt : Type. Notation key:=t. Definition eqk (p p':key*elt) := eq (fst p) (fst p'). diff --git a/theories/FSets/OrderedTypeAlt.v b/theories/FSets/OrderedTypeAlt.v index 314a95068c..9f8412a60f 100644 --- a/theories/FSets/OrderedTypeAlt.v +++ b/theories/FSets/OrderedTypeAlt.v @@ -23,7 +23,7 @@ whereas [compare], defined in [OrderedType.v] is [EQ _ | LT _ | GT _ ] Module Type OrderedTypeAlt. - Parameter t : Set. + Parameter t : Type. Parameter compare : t -> t -> comparison. diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index 4a376e55d6..dbc72e0e7a 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -25,7 +25,7 @@ Require Import Compare_dec. the equality is the usual one of Coq. *) Module Type UsualOrderedType. - Parameter Inline t : Set. + Parameter Inline t : Type. Definition eq := @eq t. Parameter Inline lt : t -> t -> Prop. Definition eq_refl := @refl_equal t. |