diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-04 17:33:35 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-04 17:33:35 +0000 |
| commit | 58c70113a815a42593c566f64f2de840fc7e48a1 (patch) | |
| tree | c667f773ad8084832e54cebe46e6fabe07a9adeb | |
| parent | 1f559440d19d9e27a3c935a26b6c8447c2220654 (diff) | |
migration from Set to Type of FSet/FMap + some dependencies...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
39 files changed, 327 insertions, 316 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 652ac955e..686118e4b 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -196,7 +196,7 @@ Qed. Lemma if_negb : - forall (A:Set) (b:bool) (x y:A), + forall (A:Type) (b:bool) (x y:A), (if negb b then x else y) = (if b then y else x). Proof. destruct b; trivial. @@ -686,14 +686,14 @@ Qed. (* Rewrite rules about andb, orb and if (used in romega) *) -Lemma andb_if : forall (A:Set)(a a':A)(b b' : bool), +Lemma andb_if : forall (A:Type)(a a':A)(b b' : bool), (if b && b' then a else a') = (if b then if b' then a else a' else a'). Proof. destruct b; destruct b'; auto. Qed. -Lemma negb_if : forall (A:Set)(a a':A)(b:bool), +Lemma negb_if : forall (A:Type)(a a':A)(b:bool), (if negb b then a else a') = (if b then a' else a). Proof. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index af3cdb801..a31a0fd84 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 6bdff3d7b..87111b1a7 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 0c180fcbd..26b892885 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 9a7d4ab82..917534e19 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 a47d431b3..e2ea68794 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 1273e5403..6903b67ae 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 0be7351cc..0c12516c4 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 5c701c005..3a08b0f4f 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 e0e83c57c..55cfd7e7c 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 eb2a73086..bc0cf95e1 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 01060ecce..928083b60 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 93adf6790..f3da02a83 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 3039c058c..866c3f620 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 22a0383a9..0dfc05689 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 314a95068..9f8412a60 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 4a376e55d..dbc72e0e7 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. diff --git a/theories/IntMap/Fset.v b/theories/IntMap/Fset.v index 351a7c7d7..bcdc4a7bf 100644 --- a/theories/IntMap/Fset.v +++ b/theories/IntMap/Fset.v @@ -18,7 +18,7 @@ Require Import Map. Section Dom. - Variables A B : Set. + Variables A B : Type. Fixpoint MapDomRestrTo (m:Map A) : Map B -> Map A := match m with @@ -229,7 +229,7 @@ End Dom. Section InDom. - Variables A B : Set. + Variables A B : Type. Lemma in_dom_restrto : forall (m:Map A) (m':Map B) (a:ad), @@ -259,7 +259,7 @@ Definition FSet := Map unit. Section FSetDefs. - Variable A : Set. + Variable A : Type. Definition in_FSet : ad -> FSet -> bool := in_dom unit. diff --git a/theories/IntMap/Lsort.v b/theories/IntMap/Lsort.v index f8cd372a4..7f818aab7 100644 --- a/theories/IntMap/Lsort.v +++ b/theories/IntMap/Lsort.v @@ -19,7 +19,7 @@ Require Import Mapiter. Section LSort. - Variable A : Set. + Variable A : Type. Fixpoint alist_sorted (l:alist A) : bool := match l with @@ -90,7 +90,7 @@ Section LSort. Qed. Lemma app_length : - forall (C:Set) (l l':list C), length (l ++ l') = length l + length l'. + forall (C:Type) (l l':list C), length (l ++ l') = length l + length l'. Proof. simple induction l. trivial. intros. simpl in |- *. rewrite (H l'). reflexivity. @@ -172,7 +172,7 @@ Section LSort. simple induction l. intros. elim (le_Sn_O _ H). intro r. elim r. intros a y l0 H. simple induction n. simpl in |- *. intro. split with y. rewrite (Neqb_correct a). reflexivity. - intros. elim (H _ (le_S_n _ _ H1)). intros y0 H2. + intros. elim (H _ (le_S_n _ _ H0)). intros y0 H2. elim (sumbool_of_bool (Neqb a (alist_nth_ad n0 l0))). intro H3. split with y. rewrite (Neqb_complete _ _ H3). simpl in |- *. rewrite (Neqb_correct (alist_nth_ad n0 l0)). reflexivity. diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v index 6b914264f..96c89691d 100644 --- a/theories/IntMap/Map.v +++ b/theories/IntMap/Map.v @@ -25,9 +25,9 @@ Definition ad := N. Section MapDefs. (** We now define maps from ad to A. *) - Variable A : Set. + Variable A : Type. - Inductive Map : Set := + Inductive Map := | M0 : Map | M1 : ad -> A -> Map | M2 : Map -> Map -> Map. diff --git a/theories/IntMap/Mapaxioms.v b/theories/IntMap/Mapaxioms.v index 0343e9e94..6fced3285 100644 --- a/theories/IntMap/Mapaxioms.v +++ b/theories/IntMap/Mapaxioms.v @@ -17,7 +17,7 @@ Require Import Fset. Section MapAxioms. - Variables A B C : Set. + Variables A B C : Type. Lemma eqm_sym : forall f f':ad -> option A, eqm A f f' -> eqm A f' f. Proof. @@ -574,7 +574,7 @@ Section MapAxioms. End MapAxioms. Lemma MapDomRestrTo_ext : - forall (A B:Set) (m1:Map A) (m2:Map B) (m'1:Map A) + forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A) (m'2:Map B), eqmap A m1 m'1 -> eqmap B m2 m'2 -> @@ -585,7 +585,7 @@ Proof. Qed. Lemma MapDomRestrTo_ext_l : - forall (A B:Set) (m1:Map A) (m2:Map B) (m'1:Map A), + forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A), eqmap A m1 m'1 -> eqmap A (MapDomRestrTo A B m1 m2) (MapDomRestrTo A B m'1 m2). Proof. @@ -593,7 +593,7 @@ Proof. Qed. Lemma MapDomRestrTo_ext_r : - forall (A B:Set) (m1:Map A) (m2 m'2:Map B), + forall (A B:Type) (m1:Map A) (m2 m'2:Map B), eqmap B m2 m'2 -> eqmap A (MapDomRestrTo A B m1 m2) (MapDomRestrTo A B m1 m'2). Proof. @@ -601,7 +601,7 @@ Proof. Qed. Lemma MapDomRestrBy_ext : - forall (A B:Set) (m1:Map A) (m2:Map B) (m'1:Map A) + forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A) (m'2:Map B), eqmap A m1 m'1 -> eqmap B m2 m'2 -> @@ -612,7 +612,7 @@ Proof. Qed. Lemma MapDomRestrBy_ext_l : - forall (A B:Set) (m1:Map A) (m2:Map B) (m'1:Map A), + forall (A B:Type) (m1:Map A) (m2:Map B) (m'1:Map A), eqmap A m1 m'1 -> eqmap A (MapDomRestrBy A B m1 m2) (MapDomRestrBy A B m'1 m2). Proof. @@ -620,7 +620,7 @@ Proof. Qed. Lemma MapDomRestrBy_ext_r : - forall (A B:Set) (m1:Map A) (m2 m'2:Map B), + forall (A B:Type) (m1:Map A) (m2 m'2:Map B), eqmap B m2 m'2 -> eqmap A (MapDomRestrBy A B m1 m2) (MapDomRestrBy A B m1 m'2). Proof. @@ -628,7 +628,7 @@ Proof. Qed. Lemma MapDomRestrBy_m_m : - forall (A:Set) (m:Map A), + forall (A:Type) (m:Map A), eqmap A (MapDomRestrBy A unit m (MapDom A m)) (M0 A). Proof. intros. apply eqmap_trans with (m' := MapDomRestrBy A A m m). apply eqmap_sym. diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v index d6a9aad47..8eff8c31d 100644 --- a/theories/IntMap/Mapc.v +++ b/theories/IntMap/Mapc.v @@ -23,7 +23,7 @@ Require Import Mapcanon. Section MapC. - Variables A B C : Set. + Variables A B C : Type. Lemma MapPut_as_Merge_c : forall m:Map A, diff --git a/theories/IntMap/Mapcanon.v b/theories/IntMap/Mapcanon.v index 0b922864f..794ecb12c 100644 --- a/theories/IntMap/Mapcanon.v +++ b/theories/IntMap/Mapcanon.v @@ -24,7 +24,7 @@ Require Import Mapcard. Section MapCanon. - Variable A : Set. + Variable A : Type. Inductive mapcanon : Map A -> Prop := | M0_canon : mapcanon (M0 A) @@ -277,7 +277,7 @@ Section MapCanon. exact (mapcanon_M2_2 _ _ H4). Qed. - Variable B : Set. + Variable B : Type. Lemma MapDomRestrTo_canon : forall m:Map A, @@ -337,7 +337,7 @@ End MapCanon. Section FSetCanon. - Variable A : Set. + Variable A : Type. Lemma MapDom_canon : forall m:Map A, mapcanon A m -> mapcanon unit (MapDom A m). @@ -354,7 +354,7 @@ End FSetCanon. Section MapFoldCanon. - Variables A B : Set. + Variables A B : Type. Lemma MapFold_canon_1 : forall m0:Map B, diff --git a/theories/IntMap/Mapcard.v b/theories/IntMap/Mapcard.v index 399fc0c53..26ead03cc 100644 --- a/theories/IntMap/Mapcard.v +++ b/theories/IntMap/Mapcard.v @@ -24,7 +24,7 @@ Require Import Peano_dec. Section MapCard. - Variables A B : Set. + Variables A B : Type. Lemma MapCard_M0 : MapCard A (M0 A) = 0. Proof. @@ -55,10 +55,10 @@ Section MapCard. reflexivity. intro H0. rewrite H0 in H. discriminate H. intros. elim (sumbool_of_bool (Nbit0 a)). intro H2. - rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H1. elim (H0 (Ndiv2 a) y H1). intros n H3. + rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1) in H. elim (X0 (Ndiv2 a) y H). intros n H3. simpl in |- *. rewrite H3. split with (MapCard A m0 + n). rewrite <- (plus_Snm_nSm (MapCard A m0) n). reflexivity. - intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H1. elim (H (Ndiv2 a) y H1). + intro H2. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1) in H. elim (X (Ndiv2 a) y H). intros n H3. simpl in |- *. rewrite H3. split with (n + MapCard A m1). reflexivity. Qed. @@ -68,11 +68,11 @@ Section MapCard. Proof. simple induction m. intro. discriminate H. intros a y H. split with a. split with y. apply M1_semantics_1. - intros. simpl in H1. elim (plus_is_one (MapCard A m0) (MapCard A m1) H1). - intro H2. elim H2. intros. elim (H0 H4). intros a H5. split with (Ndouble_plus_one a). + intros. simpl in H. elim (plus_is_one (MapCard A m0) (MapCard A m1) H). + intro H2. elim H2. intros H3 H4. elim (X0 H4). intros a H5. split with (Ndouble_plus_one a). rewrite (MapGet_M2_bit_0_1 A _ (Ndouble_plus_one_bit0 a) m0 m1). rewrite Ndouble_plus_one_div2. exact H5. - intro H2. elim H2. intros. elim (H H3). intros a H5. split with (Ndouble a). + intro H2. elim H2. intros H3 H4. elim (X H3). intros a H5. split with (Ndouble a). rewrite (MapGet_M2_bit_0_0 A _ (Ndouble_bit0 a) m0 m1). rewrite Ndouble_div2. exact H5. Qed. @@ -116,7 +116,7 @@ Section MapCard. Qed. Lemma length_as_fold : - forall (C:Set) (l:list C), + forall (C:Type) (l:list C), length l = fold_right (fun (_:C) (n:nat) => S n) 0 l. Proof. simple induction l. reflexivity. @@ -182,25 +182,25 @@ Section MapCard. rewrite H0. rewrite H1. reflexivity. intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. simpl in H0. left. rewrite H0. rewrite H1. reflexivity. - intros. simpl in H2. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. - elim (sumbool_of_bool (Nbit0 a)). intro H4. rewrite H4 in H1. + intros. simpl in H0. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H. + elim (sumbool_of_bool (Nbit0 a)). intro H4. rewrite H4 in H. elim - (H0 (MapPut A m1 (Ndiv2 a) y) (Ndiv2 a) y ( + (X0 (MapPut A m1 (Ndiv2 a) y) (Ndiv2 a) y ( MapCard A m1) (MapCard A (MapPut A m1 (Ndiv2 a) y)) ( refl_equal _) (refl_equal _) (refl_equal _)). - intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. rewrite <- H2 in H3. left. + intro H5. rewrite H in H1. simpl in H1. rewrite H5 in H1. rewrite <- H0 in H1. left. assumption. - intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. - rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)) in H3. - simpl in H3. rewrite <- H2 in H3. right. assumption. - intro H4. rewrite H4 in H1. + intro H5. rewrite H in H1. simpl in H1. rewrite H5 in H1. + rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A m1)) in H1. + simpl in H1. rewrite <- H0 in H1. right. assumption. + intro H4. rewrite H4 in H. elim - (H (MapPut A m0 (Ndiv2 a) y) (Ndiv2 a) y ( + (X (MapPut A m0 (Ndiv2 a) y) (Ndiv2 a) y ( MapCard A m0) (MapCard A (MapPut A m0 (Ndiv2 a) y)) ( refl_equal _) (refl_equal _) (refl_equal _)). - intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. rewrite <- H2 in H3. + intro H5. rewrite H in H1. simpl in H1. rewrite H5 in H1. rewrite <- H0 in H1. left. assumption. - intro H5. rewrite H1 in H3. simpl in H3. rewrite H5 in H3. simpl in H3. rewrite <- H2 in H3. + intro H5. rewrite H in H1. simpl in H1. rewrite H5 in H1. simpl in H1. rewrite <- H0 in H1. right. assumption. Qed. @@ -239,15 +239,15 @@ Section MapCard. intros p H1. rewrite H1 in H. rewrite (MapCard_Put1_equals_2 p a a0 y y0) in H. discriminate H. intro H0. rewrite H0 in H. rewrite (Nxor_eq _ _ H0). split with y. apply M1_semantics_1. - intros. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H1. elim (sumbool_of_bool (Nbit0 a)). - intro H2. rewrite H2 in H1. simpl in H1. elim (H0 (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)). + intros. rewrite (MapPut_semantics_3_1 A m0 m1 a y) in H. elim (sumbool_of_bool (Nbit0 a)). + intro H2. rewrite H2 in H. simpl in H. elim (X0 (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H)). intros y0 H3. split with y0. rewrite <- H3. exact (MapGet_M2_bit_0_1 A a H2 m0 m1). - intro H2. rewrite H2 in H1. simpl in H1. + intro H2. rewrite H2 in H. simpl in H. rewrite (plus_comm (MapCard A (MapPut A m0 (Ndiv2 a) y)) (MapCard A m1)) - in H1. - rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1. - elim (H (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1)). intros y0 H3. split with y0. + in H. + rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H. + elim (X (Ndiv2 a) y ((fun n m p:nat => plus_reg_l m p n) _ _ _ H)). intros y0 H3. split with y0. rewrite <- H3. exact (MapGet_M2_bit_0_0 A a H2 m0 m1). Qed. @@ -372,27 +372,27 @@ Section MapCard. simpl in |- *. intros. elim (sumbool_of_bool (Neqb a a1)). intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. right. rewrite H1. assumption. intro H2. rewrite H2 in H. rewrite H in H1. simpl in H1. left. rewrite H1. assumption. - intros. simpl in H1. simpl in H2. elim (sumbool_of_bool (Nbit0 a)). intro H4. - rewrite H4 in H1. rewrite H1 in H3. - rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H3. + intros. simpl in H1. simpl in H. elim (sumbool_of_bool (Nbit0 a)). intro H4. + rewrite H4 in H. rewrite H in H1. + rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H1. elim - (H0 (MapRemove A m1 (Ndiv2 a)) (Ndiv2 a) ( + (X0 (MapRemove A m1 (Ndiv2 a)) (Ndiv2 a) ( MapCard A m1) (MapCard A (MapRemove A m1 (Ndiv2 a))) (refl_equal _) (refl_equal _) (refl_equal _)). - intro H5. rewrite H5 in H2. left. rewrite H3. exact H2. - intro H5. rewrite H5 in H2. + simpl in H0; intro H5. rewrite H5 in H0. left. rewrite H1. exact H0. + simpl in H0; intro H5. rewrite H5 in H0. rewrite <- (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (Ndiv2 a)))) - in H2. - right. rewrite H3. exact H2. - intro H4. rewrite H4 in H1. rewrite H1 in H3. - rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H3. + in H0. + right. rewrite H1. exact H0. + intro H4. rewrite H4 in H. rewrite H in H1. + rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H1. elim - (H (MapRemove A m0 (Ndiv2 a)) (Ndiv2 a) ( + (X (MapRemove A m0 (Ndiv2 a)) (Ndiv2 a) ( MapCard A m0) (MapCard A (MapRemove A m0 (Ndiv2 a))) (refl_equal _) (refl_equal _) (refl_equal _)). - intro H5. rewrite H5 in H2. left. rewrite H3. exact H2. - intro H5. rewrite H5 in H2. right. rewrite H3. exact H2. + simpl in H0; intro H5. rewrite H5 in H0. left. rewrite H1. exact H0. + simpl in H0; intro H5. rewrite H5 in H0. right. rewrite H1. exact H0. Qed. Lemma MapCard_Remove_ub : @@ -448,25 +448,25 @@ Section MapCard. intros a y a0 H. simpl in H. elim (sumbool_of_bool (Neqb a a0)). intro H0. rewrite (Neqb_complete _ _ H0). split with y. exact (M1_semantics_1 A a0 y). intro H0. rewrite H0 in H. discriminate H. - intros. simpl in H1. elim (sumbool_of_bool (Nbit0 a)). intro H2. rewrite H2 in H1. - rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H1. - rewrite (MapGet_M2_bit_0_1 A a H2 m0 m1). apply H0. + intros. simpl in H. elim (sumbool_of_bool (Nbit0 a)). intro H0. rewrite H0 in H. + rewrite (MapCard_makeM2 m0 (MapRemove A m1 (Ndiv2 a))) in H. + rewrite (MapGet_M2_bit_0_1 A a H0 m0 m1). apply X0. change (S (MapCard A m0) + MapCard A (MapRemove A m1 (Ndiv2 a)) = - MapCard A m0 + MapCard A m1) in H1. + MapCard A m0 + MapCard A m1) in H. rewrite (plus_Snm_nSm (MapCard A m0) (MapCard A (MapRemove A m1 (Ndiv2 a)))) - in H1. - exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1). - intro H2. rewrite H2 in H1. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply H. - rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H1. + in H. + exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H). + intro H2. rewrite H2 in H. rewrite (MapGet_M2_bit_0_0 A a H2 m0 m1). apply X. + rewrite (MapCard_makeM2 (MapRemove A m0 (Ndiv2 a)) m1) in H. change (S (MapCard A (MapRemove A m0 (Ndiv2 a))) + MapCard A m1 = - MapCard A m0 + MapCard A m1) in H1. + MapCard A m0 + MapCard A m1) in H. rewrite (plus_comm (S (MapCard A (MapRemove A m0 (Ndiv2 a)))) (MapCard A m1)) - in H1. - rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H1. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H1). + in H. + rewrite (plus_comm (MapCard A m0) (MapCard A m1)) in H. exact ((fun n m p:nat => plus_reg_l m p n) _ _ _ H). Qed. Lemma MapCard_Remove_1_conv : @@ -652,7 +652,7 @@ End MapCard. Section MapCard2. - Variables A B : Set. + Variables A B : Type. Lemma MapSubset_card_eq_1 : forall (n:nat) (m:Map A) (m':Map B), @@ -708,7 +708,7 @@ End MapCard2. Section MapCard3. - Variables A B : Set. + Variables A B : Type. Lemma MapMerge_Card_lb_l : forall m m':Map A, MapCard A (MapMerge A m m') >= MapCard A m. diff --git a/theories/IntMap/Mapfold.v b/theories/IntMap/Mapfold.v index 99db86c6f..6bc0cd914 100644 --- a/theories/IntMap/Mapfold.v +++ b/theories/IntMap/Mapfold.v @@ -22,9 +22,9 @@ Require Import List. Section MapFoldResults. - Variable A : Set. + Variable A : Type. - Variable M : Set. + Variable M : Type. Variable neutral : M. Variable op : M -> M -> M. @@ -268,17 +268,17 @@ End MapFoldResults. Section MapFoldDistr. - Variable A : Set. + Variable A : Type. - Variable M : Set. + Variable M : Type. Variable neutral : M. Variable op : M -> M -> M. - Variable M' : Set. + Variable M' : Type. Variable neutral' : M'. Variable op' : M' -> M' -> M'. - Variable N : Set. + Variable N : Type. Variable times : M -> N -> M'. @@ -309,17 +309,17 @@ End MapFoldDistr. Section MapFoldDistrL. - Variable A : Set. + Variable A : Type. - Variable M : Set. + Variable M : Type. Variable neutral : M. Variable op : M -> M -> M. - Variable M' : Set. + Variable M' : Type. Variable neutral' : M'. Variable op' : M' -> M' -> M'. - Variable N : Set. + Variable N : Type. Variable times : N -> M -> M'. @@ -341,7 +341,7 @@ End MapFoldDistrL. Section MapFoldExists. - Variable A : Set. + Variable A : Type. Lemma MapFold_orb_1 : forall (f:ad -> A -> bool) (m:Map A) (pf:ad -> ad), @@ -373,7 +373,7 @@ End MapFoldExists. Section DMergeDef. - Variable A : Set. + Variable A : Type. Definition DMerge := MapFold (Map A) (Map A) (M0 A) (MapMerge A) (fun (_:ad) (m:Map A) => m). diff --git a/theories/IntMap/Mapiter.v b/theories/IntMap/Mapiter.v index e551e47d9..79e59a90e 100644 --- a/theories/IntMap/Mapiter.v +++ b/theories/IntMap/Mapiter.v @@ -19,7 +19,7 @@ Require Import List. Section MapIter. - Variable A : Set. + Variable A : Type. Section MapSweepDef. @@ -180,16 +180,16 @@ Section MapIter. intro H1. rewrite (M1_semantics_2 _ a a1 a0 H1) in H. discriminate H. intros. elim (sumbool_of_bool (Nbit0 a)). intro H3. - rewrite (MapGet_M2_bit_0_1 _ _ H3 m0 m1) in H1. - rewrite <- (Ndiv2_double_plus_one a H3) in H2. - elim (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) (Ndiv2 a) y H1 H2). intros a'' H4. elim H4. + rewrite (MapGet_M2_bit_0_1 _ _ H3 m0 m1) in H. + rewrite <- (Ndiv2_double_plus_one a H3) in H0. + elim (X0 (fun a0:ad => pf (Ndouble_plus_one a0)) (Ndiv2 a) y H H0). intros a'' H4. elim H4. intros y'' H5. simpl in |- *. elim (option_sum _ (MapSweep1 (fun a:ad => pf (Ndouble a)) m0)). intro H6. elim H6. intro r. elim r. intros a''' y''' H7. rewrite H7. split with a'''. split with y'''. reflexivity. intro H6. rewrite H6. split with a''. split with y''. assumption. - intro H3. rewrite (MapGet_M2_bit_0_0 _ _ H3 m0 m1) in H1. - rewrite <- (Ndiv2_double a H3) in H2. - elim (H (fun a0:ad => pf (Ndouble a0)) (Ndiv2 a) y H1 H2). intros a'' H4. elim H4. + intro H3. rewrite (MapGet_M2_bit_0_0 _ _ H3 m0 m1) in H. + rewrite <- (Ndiv2_double a H3) in H0. + elim (X (fun a0:ad => pf (Ndouble a0)) (Ndiv2 a) y H H0). intros a'' H4. elim H4. intros y'' H5. split with a''. split with y''. simpl in |- *. rewrite H5. reflexivity. Qed. @@ -203,7 +203,7 @@ Section MapIter. End MapSweepDef. - Variable B : Set. + Variable B : Type. Fixpoint MapCollect1 (f:ad -> A -> Map B) (pf:ad -> ad) (m:Map A) {struct m} : Map B := @@ -220,7 +220,7 @@ Section MapIter. Section MapFoldDef. - Variable M : Set. + Variable M : Type. Variable neutral : M. Variable op : M -> M -> M. @@ -248,7 +248,7 @@ Section MapIter. trivial. Qed. - Variable State : Set. + Variable State : Type. Variable f : State -> ad -> A -> State * M. Fixpoint MapFold1_state (state:State) (pf:ad -> ad) @@ -271,7 +271,7 @@ Section MapIter. Definition MapFold_state (state:State) := MapFold1_state state (fun a:ad => a). - Lemma pair_sp : forall (B C:Set) (x:B * C), x = (fst x, snd x). + Lemma pair_sp : forall (B C:Type) (x:B * C), x = (fst x, snd x). Proof. simple induction x. trivial. Qed. @@ -364,23 +364,23 @@ Section MapIter. (fun a0:ad => pf (Ndouble a0)) m0) (MapFold1 alist anil aapp (fun (a0:ad) (y:A) => acons (a0, y) anil) (fun a0:ad => pf (Ndouble_plus_one a0)) m1)) a = - Some y) in H1. + Some y) in H. rewrite (alist_semantics_app (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil) (fun a0:ad => pf (Ndouble a0)) m0) (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil) (fun a0:ad => pf (Ndouble_plus_one a0)) m1) a) - in H1. + in H. elim (option_sum A (alist_semantics (MapFold1 alist anil aapp (fun (a0:ad) (y0:A) => acons (a0, y0) anil) (fun a0:ad => pf (Ndouble a0)) m0) a)). - intro H2. elim H2. intros y0 H3. elim (H (fun a0:ad => pf (Ndouble a0)) a y0 H3). intros a0 H4. + intro H2. elim H2. intros y0 H3. elim (X (fun a0:ad => pf (Ndouble a0)) a y0 H3). intros a0 H4. split with (Ndouble a0). assumption. - intro H2. rewrite H2 in H1. elim (H0 (fun a0:ad => pf (Ndouble_plus_one a0)) a y H1). + intro H2. rewrite H2 in H. elim (X0 (fun a0:ad => pf (Ndouble_plus_one a0)) a y H). intros a0 H3. split with (Ndouble_plus_one a0). assumption. Qed. @@ -516,7 +516,7 @@ Section MapIter. Qed. Lemma fold_right_aapp : - forall (M:Set) (neutral:M) (op:M -> M -> M), + forall (M:Type) (neutral:M) (op:M -> M -> M), (forall a b c:M, op (op a b) c = op a (op b c)) -> (forall a:M, op neutral a = a) -> forall (f:ad -> A -> M) (l l':alist), @@ -535,7 +535,7 @@ Section MapIter. Qed. Lemma MapFold_as_fold_1 : - forall (M:Set) (neutral:M) (op:M -> M -> M), + forall (M:Type) (neutral:M) (op:M -> M -> M), (forall a b c:M, op (op a b) c = op a (op b c)) -> (forall a:M, op neutral a = a) -> (forall a:M, op a neutral = a) -> @@ -554,7 +554,7 @@ Section MapIter. Qed. Lemma MapFold_as_fold : - forall (M:Set) (neutral:M) (op:M -> M -> M), + forall (M:Type) (neutral:M) (op:M -> M -> M), (forall a b c:M, op (op a b) c = op a (op b c)) -> (forall a:M, op neutral a = a) -> (forall a:M, op a neutral = a) -> diff --git a/theories/IntMap/Maplists.v b/theories/IntMap/Maplists.v index f4b5bbe92..56396cdad 100644 --- a/theories/IntMap/Maplists.v +++ b/theories/IntMap/Maplists.v @@ -340,7 +340,7 @@ Section MapLists. Section ListOfDomDef. - Variable A : Set. + Variable A : Type. Definition ad_list_of_dom := MapFold A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil). @@ -418,7 +418,7 @@ Section MapLists. End ListOfDomDef. Lemma ad_list_of_dom_Dom_1 : - forall (A:Set) (m:Map A) (pf:ad -> ad), + forall (A:Type) (m:Map A) (pf:ad -> ad), MapFold1 A (list ad) nil (app (A:=ad)) (fun (a:ad) (_:A) => a :: nil) pf m = MapFold1 unit (list ad) nil (app (A:=ad)) @@ -429,7 +429,7 @@ Section MapLists. Qed. Lemma ad_list_of_dom_Dom : - forall (A:Set) (m:Map A), + forall (A:Type) (m:Map A), ad_list_of_dom A m = ad_list_of_dom unit (MapDom A m). Proof. intros. exact (ad_list_of_dom_Dom_1 A m (fun a0:ad => a0)). diff --git a/theories/IntMap/Mapsubset.v b/theories/IntMap/Mapsubset.v index 1db99b368..74b716312 100644 --- a/theories/IntMap/Mapsubset.v +++ b/theories/IntMap/Mapsubset.v @@ -20,7 +20,7 @@ Require Import Mapiter. Section MapSubsetDef. - Variables A B : Set. + Variables A B : Type. Definition MapSubset (m:Map A) (m':Map B) := forall a:ad, in_dom A a m = true -> in_dom B a m' = true. @@ -105,7 +105,7 @@ End MapSubsetDef. Section MapSubsetOrder. - Variables A B C : Set. + Variables A B C : Type. Lemma MapSubset_refl : forall m:Map A, MapSubset A A m m. Proof. @@ -165,7 +165,7 @@ End FSubsetOrder. Section MapSubsetExtra. - Variables A B : Set. + Variables A B : Type. Lemma MapSubset_Dom_1 : forall (m:Map A) (m':Map B), @@ -303,7 +303,7 @@ Section MapSubsetExtra. exact (MapSubset_imp_2 _ _ _ _ H1). Qed. - Variables C D : Set. + Variables C D : Type. Lemma MapSubset_DomRestrTo_mono : forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D), @@ -338,7 +338,7 @@ End MapSubsetExtra. Section MapDisjointDef. - Variables A B : Set. + Variables A B : Type. Definition MapDisjoint (m:Map A) (m':Map B) := forall a:ad, in_dom A a m = true -> in_dom B a m' = true -> False. @@ -414,7 +414,7 @@ End MapDisjointDef. Section MapDisjointExtra. - Variables A B : Set. + Variables A B : Type. Lemma MapDisjoint_ext : forall (m0 m1:Map A) (m2 m3:Map B), @@ -549,7 +549,7 @@ Section MapDisjointExtra. apply MapDomRestrBy_m_empty. Qed. - Variable C : Set. + Variable C : Type. Lemma MapDomRestr_disjoint : forall (m:Map A) (m':Map B) (m'':Map C), @@ -576,7 +576,7 @@ Section MapDisjointExtra. intros. elim (andb_prop _ _ H0). intros. rewrite H1 in H. rewrite H2 in H. discriminate H. Qed. - Variable D : Set. + Variable D : Type. Lemma MapSubset_Disjoint : forall (m:Map A) (m':Map B) (m'':Map C) (m''':Map D), diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 20dc61ef1..77caa9c22 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -20,7 +20,7 @@ Set Implicit Arguments. Section first_definitions. - Variable A : Set. + Variable A : Type. Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}. Definition set := list A. @@ -100,7 +100,7 @@ Section first_definitions. Qed. Lemma set_mem_ind : - forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set), + forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set), (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z). Proof. @@ -110,7 +110,7 @@ Section first_definitions. Qed. Lemma set_mem_ind2 : - forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set), + forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set), (set_In a x -> P y) -> (~ set_In a x -> P z) -> P (if set_mem a x then y else z). @@ -373,7 +373,7 @@ End first_definitions. Section other_definitions. - Variables A B : Set. + Variables A B : Type. Definition set_prod : set A -> set B -> set (A * B) := list_prod (A:=A) (B:=B). diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 6c4e76d82..e4f1a92ba 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -21,7 +21,7 @@ Unset Strict Implicit. found in [Sorting]. *) Section Type_with_equality. -Variable A : Set. +Variable A : Type. Variable eqA : A -> A -> Prop. (** Being in a list modulo an equality relation over type [A]. *) @@ -173,7 +173,7 @@ Hint Constructors lelistA sort. Lemma InfA_ltA : forall l x y, ltA x y -> InfA y l -> InfA x l. Proof. - intro s; case s; constructor; inversion_clear H0. + destruct l; constructor; inversion_clear H0; eapply ltA_trans; eauto. Qed. @@ -434,7 +434,7 @@ End Filter. Section Fold. -Variable B:Set. +Variable B:Type. Variable eqB:B->B->Prop. (** Compatibility of a two-argument function with respect to two equalities. *) @@ -613,7 +613,7 @@ Hint Unfold compat_bool compat_nat compat_P. Hint Constructors InA NoDupA sort lelistA eqlistA. Section Find. -Variable A B : Set. +Variable A B : Type. Variable eqA : A -> A -> Prop. Hypothesis eqA_sym : forall x y, eqA x y -> eqA y x. Hypothesis eqA_trans : forall x y z, eqA x y -> eqA y z -> eqA x z. diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v index e372ae75c..fed25ad74 100644 --- a/theories/Logic/DecidableType.v +++ b/theories/Logic/DecidableType.v @@ -16,7 +16,7 @@ Unset Strict Implicit. Module Type EqualityType. - Parameter Inline t : Set. + Parameter Inline t : Type. Parameter Inline eq : t -> t -> Prop. @@ -33,7 +33,7 @@ End EqualityType. Module Type DecidableType. - Parameter Inline t : Set. + Parameter Inline t : Type. Parameter Inline eq : t -> t -> Prop. @@ -54,7 +54,7 @@ Module KeyDecidableType(D:DecidableType). Import D. 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/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v index f6961781c..30a7bb633 100644 --- a/theories/Logic/DecidableTypeEx.v +++ b/theories/Logic/DecidableTypeEx.v @@ -18,7 +18,7 @@ Unset Strict Implicit. the equality is the usual one of Coq. *) Module Type UsualDecidableType. - Parameter Inline t : Set. + Parameter Inline t : Type. Definition eq := @eq t. Definition eq_refl := @refl_equal t. Definition eq_sym := @sym_eq t. @@ -33,7 +33,7 @@ Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. (** an shortcut for easily building a UsualDecidableType *) Module Type MiniDecidableType. - Parameter Inline t : Set. + Parameter Inline t : Type. Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }. End MiniDecidableType. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 80491c0aa..42130bbb5 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -16,11 +16,11 @@ Set Implicit Arguments. Section multiset_defs. - Variable A : Set. + Variable A : Type. Variable eqA : A -> A -> Prop. Hypothesis Aeq_dec : forall x y:A, {eqA x y} + {~ eqA x y}. - Inductive multiset : Set := + Inductive multiset : Type := Bag : (A -> nat) -> multiset. Definition EmptyBag := Bag (fun a:A => 0). diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 7c6b551c6..6c9a064c1 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -15,7 +15,7 @@ Section Axiomatisation. - Variable U : Set. + Variable U : Type. Variable op : U -> U -> U. Variable cong : U -> U -> Prop. diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 2f5dfafef..573d5adb8 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -25,7 +25,7 @@ Section defs. (** ** Definition of trees over an ordered set *) - Variable A : Set. + Variable A : Type. Variable leA : relation A. Variable eqA : relation A. @@ -43,7 +43,7 @@ Section defs. Let emptyBag := EmptyBag A. Let singletonBag := SingletonBag _ eqA_dec. - Inductive Tree : Set := + Inductive Tree := | Tree_Leaf : Tree | Tree_Node : A -> Tree -> Tree -> Tree. @@ -87,6 +87,23 @@ Section defs. Qed. (* This lemma ought to be generated automatically by the Inversion tools *) + Lemma is_heap_rect : + forall P:Tree -> Type, + P Tree_Leaf -> + (forall (a:A) (T1 T2:Tree), + leA_Tree a T1 -> + leA_Tree a T2 -> + is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) -> + forall T:Tree, is_heap T -> P T. + Proof. + simple induction T; auto with datatypes. + intros a G PG D PD PN. + elim (invert_heap a G D); auto with datatypes. + intros H1 H2; elim H2; intros H3 H4; elim H4; intros. + apply X0; auto with datatypes. + Qed. + + (* This lemma ought to be generated automatically by the Inversion tools *) Lemma is_heap_rec : forall P:Tree -> Set, P Tree_Leaf -> @@ -100,7 +117,7 @@ Section defs. intros a G PG D PD PN. elim (invert_heap a G D); auto with datatypes. intros H1 H2; elim H2; intros H3 H4; elim H4; intros. - apply H0; auto with datatypes. + apply X; auto with datatypes. Qed. Lemma low_trans : @@ -136,7 +153,7 @@ Section defs. (** ** Specification of heap insertion *) - Inductive insert_spec (a:A) (T:Tree) : Set := + Inductive insert_spec (a:A) (T:Tree) : Type := insert_exist : forall T1:Tree, is_heap T1 -> @@ -152,11 +169,11 @@ Section defs. auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes. simpl in |- *; unfold meq, munion in |- *; auto using node_is_heap with datatypes. elim (leA_dec a a0); intros. - elim (H3 a0); intros. + elim (X a0); intros. apply insert_exist with (Tree_Node a T2 T0); auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes. simpl in |- *; apply treesort_twist1; trivial with datatypes. - elim (H3 a); intros T3 HeapT3 ConT3 LeA. + elim (X a); intros T3 HeapT3 ConT3 LeA. apply insert_exist with (Tree_Node a0 T2 T3); auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes. apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes. @@ -169,7 +186,7 @@ Section defs. (** ** Building a heap from a list *) - Inductive build_heap (l:list A) : Set := + Inductive build_heap (l:list A) : Type := heap_exist : forall T:Tree, is_heap T -> @@ -193,7 +210,7 @@ Section defs. (** ** Building the sorted list *) - Inductive flat_spec (T:Tree) : Set := + Inductive flat_spec (T:Tree) : Type := flat_exist : forall l:list A, sort leA l -> @@ -204,7 +221,7 @@ Section defs. Proof. intros T h; elim h; intros. apply flat_exist with (nil (A:=A)); auto with datatypes. - elim H2; intros l1 s1 i1 m1; elim H4; intros l2 s2 i2 m2. + elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2. elim (merge _ leA_dec eqA_dec s1 s2); intros. apply flat_exist with (a :: l); simpl in |- *; auto with datatypes. apply meq_trans with diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 166b59a9f..8ff4e460e 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -25,7 +25,7 @@ Set Implicit Arguments. Section Perm. - Variable A : Set. + Variable A : Type. Hypothesis eq_dec : forall x y:A, {x=y} + {~ x=y}. Notation permutation := (permutation _ eq_dec). @@ -214,7 +214,7 @@ Section Perm. apply permut_remove_hd with a; auto. Qed. - Variable B : Set. + Variable B : Type. Variable eqB_dec : forall x y:B, { x=y }+{ ~x=y }. (** Permutation is compatible with map. *) diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 84eac9905..e012bde19 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -23,7 +23,7 @@ Set Implicit Arguments. Section Perm. -Variable A : Set. +Variable A : Type. Variable eqA : relation A. Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. @@ -198,7 +198,7 @@ Proof. Qed. -Variable B : Set. +Variable B : Type. Variable eqB : B->B->Prop. Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }. Variable eqB_trans : forall x y z, eqB x y -> eqB y z -> eqB x z. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 4c23f0f93..026a305b1 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -38,7 +38,7 @@ Section defs. (** * From lists to multisets *) - Variable A : Set. + Variable A : Type. Variable eqA : relation A. Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v index c1a43f64f..9828d1a24 100644 --- a/theories/Sorting/Sorting.v +++ b/theories/Sorting/Sorting.v @@ -17,7 +17,7 @@ Set Implicit Arguments. Section defs. - Variable A : Set. + Variable A : Type. Variable leA : relation A. Variable eqA : relation A. @@ -59,6 +59,16 @@ Section defs. intros; inversion H; auto with datatypes. Qed. + Lemma sort_rect : + forall P:list A -> Type, + P nil -> + (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) -> + forall y:list A, sort y -> P y. + Proof. + simple induction y; auto with datatypes. + intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes. + Qed. + Lemma sort_rec : forall P:list A -> Set, P nil -> @@ -71,7 +81,7 @@ Section defs. (** * Merging two sorted lists *) - Inductive merge_lem (l1 l2:list A) : Set := + Inductive merge_lem (l1 l2:list A) : Type := merge_exist : forall l:list A, sort l -> @@ -85,7 +95,7 @@ Section defs. Proof. simple induction 1; intros. apply merge_exist with l2; auto with datatypes. - elim H3; intros. + elim H2; intros. apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes. elim (leA_dec a a0); intros. @@ -104,7 +114,7 @@ Section defs. apply lelistA_inv with l; trivial with datatypes. (* 2 (leA a0 a) *) - elim H5; simpl in |- *; intros. + elim X0; simpl in |- *; intros. apply merge_exist with (a0 :: l3); simpl in |- *; auto using cons_sort, cons_leA with datatypes. apply meq_trans with |