diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
| commit | 3675bac6c38e0a26516e434be08bc100865b339b (patch) | |
| tree | 87f8eb1905c7b508dea60b1e216f79120e9e772d /theories | |
| parent | c881bc37b91a201f7555ee021ccb74adb360d131 (diff) | |
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
59 files changed, 340 insertions, 387 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 665f96c68..e79b5d7c3 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -122,7 +122,7 @@ induction 1; auto with arith. Qed. Lemma exists_in_int : - forall k l, exists_between k l -> exists2 m : nat | in_int k l m & Q m. + forall k l, exists_between k l -> exists2 m : nat, in_int k l m & Q m. Proof. induction 1. case IHexists_between; intros p inp Qp; exists p; auto with arith. @@ -174,7 +174,7 @@ induction 1; intros; auto with arith. apply le_trans with (S k); auto with arith. Qed. -Definition eventually (n:nat) := exists2 k : nat | k <= n & Q k. +Definition eventually (n:nat) := exists2 k : nat, k <= n & Q k. Lemma event_O : eventually 0 -> Q 0. Proof. diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index b5afebd94..b3a85ba06 100755 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -41,7 +41,7 @@ Proof le_lt_or_eq. (* By special request of G. Kahn - Used in Group Theory *) Lemma discrete_nat : - forall n m, n < m -> S n = m \/ ( exists r : nat | m = S (S (n + r))). + forall n m, n < m -> S n = m \/ (exists r : nat, m = S (S (n + r))). Proof. intros m n H. lapply (lt_le_S m n); auto with arith. diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index 02c48f028..b246de635 100644 --- a/theories/Arith/Euclid.v +++ b/theories/Arith/Euclid.v @@ -36,7 +36,7 @@ Qed. Lemma quotient : forall n, n > 0 -> - forall m:nat, {q : nat | exists r : nat | m = q * n + r /\ n > r}. + forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}. intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. elim (le_gt_dec b n). intro lebn. @@ -53,7 +53,7 @@ Qed. Lemma modulo : forall n, n > 0 -> - forall m:nat, {r : nat | exists q : nat | m = q * n + r /\ n > r}. + forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}. intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. elim (le_gt_dec b n). intro lebn. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index a7a50795e..6e95af673 100755 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -179,10 +179,10 @@ Variable R : A -> A -> Prop. (* Relational form of inversion *) Variable F : A -> nat -> Prop. Definition inv_lt_rel x y := - exists2 n : _ | F x n & (forall m, F y m -> n < m). + exists2 n : _, F x n & (forall m, F y m -> n < m). Hypothesis F_compat : forall x y:A, R x y -> inv_lt_rel x y. -Remark acc_lt_rel : forall x:A, ( exists n : _ | F x n) -> Acc R x. +Remark acc_lt_rel : forall x:A, (exists n : _, F x n) -> Acc R x. intros x [n fxn]; generalize x fxn; clear x fxn. pattern n in |- *; apply lt_wf_ind; intros. constructor; intros. diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index ef48e6272..1baa54241 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -70,4 +70,4 @@ Section Bool_eq_dec. right; apply beq_false_not_eq; assumption. Defined. -End Bool_eq_dec.
\ No newline at end of file +End Bool_eq_dec. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index d5a1179c8..2da0d6c02 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -118,4 +118,4 @@ Definition CompOpp (r:comparison) := | Eq => Eq | Lt => Gt | Gt => Lt - end.
\ No newline at end of file + end. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 7cfe160a0..e225bbddb 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -118,15 +118,15 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x. (*Rule order is important to give printing priority to fully typed ALL and EX*) -Notation "'exists' x | p" := (ex (fun x => p)) - (at level 200, x ident, p at level 99) : type_scope. -Notation "'exists' x : t | p" := (ex (fun x:t => p)) - (at level 200, x ident, p at level 99) : type_scope. - -Notation "'exists2' x | p & q" := (ex2 (fun x => p) (fun x => q)) - (at level 200, x ident, p, q at level 99) : type_scope. -Notation "'exists2' x : t | p & q" := (ex2 (fun x:t => p) (fun x:t => q)) - (at level 200, x ident, t at level 200, p, q at level 99) : type_scope. +Notation "'exists' x , p" := (ex (fun x => p)) + (at level 200, x ident) : type_scope. +Notation "'exists' x : t , p" := (ex (fun x:t => p)) + (at level 200, x ident) : type_scope. + +Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) + (at level 200, x ident, p at level 200) : type_scope. +Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q)) + (at level 200, x ident, t at level 200, p at level 200) : type_scope. (** Universal quantification *) diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v deleted file mode 100644 index f95f56d37..000000000 --- a/theories/Init/LogicSyntax.v +++ /dev/null @@ -1,47 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -Require Export Notations. -Require Export Logic. - -(** Symbolic notations for things in [Logic.v] *) - -(* Order is important to give printing priority to fully typed ALL and - exists *) - -V7only [ Notation All := (all ?). ]. -Notation "'ALL' x | p" := (all ? [x]p) (at level 10, p at level 8) - V8only "'ALL' x , p" (at level 200, p at level 200). -Notation "'ALL' x : t | p" := (all ? [x:t]p) (at level 10, p at level 8) - V8only "'ALL' x : t , p" (at level 200). - -V7only [ Notation Ex := (ex ?). ]. -Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8) - V8only "'exists' x , p" (at level 200, x at level 99). -Notation "'EX' x : t | p" := (ex ? [x:t]p) (at level 10, p at level 8) - V8only "'exists' x : t , p" (at level 200, x at level 99). - -V7only [ Notation Ex2 := (ex2 ?). ]. -Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) - (at level 10, p, q at level 8) - V8only "'exists2' x , p & q" (at level 200, x at level 99). -Notation "'EX' x : t | p & q" := (ex2 ? [x:t]p [x:t]q) - (at level 10, p, q at level 8) - V8only "'exists2' x : t , p & q" (at level 200, x at level 99). - -V7only[ -(** Parsing only of things in [Logic.v] *) - -Notation "< A > 'All' ( P )" := (all A P) (A annot, at level 1, only parsing). -Notation "< A > x = y" := (eq A x y) - (A annot, at level 1, x at level 0, only parsing). -Notation "< A > x <> y" := ~(eq A x y) - (A annot, at level 1, x at level 0, only parsing). -]. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 05bfae722..2a1c84165 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -88,4 +88,4 @@ Delimit Scope type_scope with type. Delimit Scope core_scope with core. Open Scope core_scope. -Open Scope type_scope.
\ No newline at end of file +Open Scope type_scope. diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index da23394c0..20f39e0ef 100755 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -66,7 +66,7 @@ Qed. (********************************) Lemma Hd : - forall l:list A, {a : A | exists m : list A | a :: m = l} + {Isnil l}. + forall l:list A, {a : A | exists m : list A, a :: m = l} + {Isnil l}. intro l; case l. auto. intros a m; intros; left; exists a; exists m; reflexivity. @@ -80,7 +80,7 @@ Qed. Lemma Tl : forall l:list A, - {m : list A | ( exists a : A | a :: m = l) \/ Isnil l /\ Isnil m}. + {m : list A | (exists a : A, a :: m = l) \/ Isnil l /\ Isnil m}. intro l; case l. exists (nil (A:=A)); auto. intros a m; intros; exists m; left; exists a; reflexivity. @@ -341,7 +341,7 @@ Fixpoint try_find (l:list A) : Exc B := end. Lemma Try_find : - forall l:list A, {c : B | exists2 a : A | In a l & T a c} + {AllS P l}. + forall l:list A, {c : B | exists2 a : A, In a l & T a c} + {AllS P l}. induction l as [| a m [[b H1]| H]]. auto. left; exists b; destruct H1 as [a' H2 H3]; exists a'; auto. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 192603273..ca9bea509 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -19,20 +19,20 @@ Definition RelationalChoice := forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B | R x y) -> - exists R' : A -> B -> Prop - | (forall x:A, - exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). + (forall x:A, exists y : B, R x y) -> + exists R' : A -> B -> Prop, + (forall x:A, + exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). Definition FunctionalChoice := forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B | R x y) -> - exists f : A -> B | (forall x:A, R x (f x)). + (forall x:A, exists y : B, R x y) -> + exists f : A -> B, (forall x:A, R x (f x)). Definition ParamDefiniteDescription := forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B | R x y /\ (forall y':B, R x y' -> y = y')) -> - exists f : A -> B | (forall x:A, R x (f x)). + (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) -> + exists f : A -> B, (forall x:A, R x (f x)). Lemma description_rel_choice_imp_funct_choice : ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice. @@ -86,11 +86,11 @@ Qed. Definition GuardedRelationalChoice := forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop), - (forall x:A, P x -> exists y : B | R x y) -> - exists R' : A -> B -> Prop - | (forall x:A, + (forall x:A, P x -> exists y : B, R x y) -> + exists R' : A -> B -> Prop, + (forall x:A, P x -> - exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). + exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). Definition ProofIrrelevance := forall (A:Prop) (a1 a2:A), a1 = a2. @@ -103,7 +103,7 @@ destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as [R' H0]. intros [x HPx]. destruct (H x HPx) as [y HRxy]. exists y; exact HRxy. -pose (R'' := fun (x:A) (y:B) => exists H : P x | R' (existT P x H) y). +pose (R'' := fun (x:A) (y:B) => exists H : P x, R' (existT P x H) y). exists R''; intros x HPx. destruct (H0 (existT P x HPx)) as [y [HRxy [HR'xy Huniq]]]. exists y. split. @@ -120,7 +120,7 @@ Qed. Definition IndependenceOfPremises := forall (A:Type) (P:A -> Prop) (Q:Prop), - (Q -> exists x : _ | P x) -> exists x : _ | Q -> P x. + (Q -> exists x : _, P x) -> exists x : _, Q -> P x. Lemma rel_choice_indep_of_premises_imp_guarded_rel_choice : RelationalChoice -> IndependenceOfPremises -> GuardedRelationalChoice. @@ -136,4 +136,4 @@ destruct (RelCh A B (fun x y => P x -> R x y)) as [R' H0]. exists y. split. apply (H1 HPx). exact H2. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 80bbce461..7b6fcdf53 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -23,8 +23,8 @@ Require Import ChoiceFacts. Theorem choice : forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B | R x y) -> - exists f : A -> B | (forall x:A, R x (f x)). + (forall x:A, exists y : B, R x y) -> + exists f : A -> B, (forall x:A, R x (f x)). Proof. apply description_rel_choice_imp_funct_choice. exact description. diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 26e696a7c..a20036f0a 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -26,15 +26,15 @@ Axiom dependent_description : forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), (forall x:A, - exists y : B x | R x y /\ (forall y':B x, R x y' -> y = y')) -> - exists f : forall x:A, B x | (forall x:A, R x (f x)). + exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) -> + exists f : forall x:A, B x, (forall x:A, R x (f x)). (** Principle of definite description (aka axiom of unique choice) *) Theorem description : forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B | R x y /\ (forall y':B, R x y' -> y = y')) -> - exists f : A -> B | (forall x:A, R x (f x)). + (forall x:A, exists y : B, R x y /\ (forall y':B, R x y' -> y = y')) -> + exists f : A -> B, (forall x:A, R x (f x)). Proof. intros A B. apply (dependent_description A (fun _ => B)). @@ -46,7 +46,7 @@ Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False. Proof. intro HnotEM. pose (R := fun A b => A /\ true = b \/ ~ A /\ false = b). -assert (H : exists f : Prop -> bool | (forall A:Prop, R A (f A))). +assert (H : exists f : Prop -> bool, (forall A:Prop, R A (f A))). apply description. intro A. destruct (classic A) as [Ha| Hnota]. diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index e308eff14..a06be5ae2 100755 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -18,7 +18,7 @@ Variable U : Set. (** de Morgan laws for quantifiers *) Lemma not_all_ex_not : - forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U | ~ P n. + forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. Proof. unfold not in |- *; intros P notall. apply NNPP; unfold not in |- *. @@ -30,7 +30,7 @@ apply abs; exists n; trivial. Qed. Lemma not_all_not_ex : - forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U | P n. + forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. Proof. intros P H. elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n. @@ -38,7 +38,7 @@ apply NNPP; trivial. Qed. Lemma not_ex_all_not : - forall P:U -> Prop, ~ ( exists n : U | P n) -> forall n:U, ~ P n. + forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. Proof. unfold not in |- *; intros P notex n abs. apply notex. @@ -46,7 +46,7 @@ exists n; trivial. Qed. Lemma not_ex_not_all : - forall P:U -> Prop, ~ ( exists n : U | ~ P n) -> forall n:U, P n. + forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n. Proof. intros P H n. apply NNPP. @@ -54,14 +54,14 @@ red in |- *; intro K; apply H; exists n; trivial. Qed. Lemma ex_not_not_all : - forall P:U -> Prop, ( exists n : U | ~ P n) -> ~ (forall n:U, P n). + forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). Proof. unfold not in |- *; intros P exnot allP. elim exnot; auto. Qed. Lemma all_not_not_ex : - forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U | P n). + forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). Proof. unfold not in |- *; intros P allnot exP; elim exP; intros n p. apply allnot with n; auto. diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index 6bfd08e43..f3f29747c 100755 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -18,7 +18,7 @@ Variable U : Type. (** de Morgan laws for quantifiers *) Lemma not_all_ex_not : - forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U | ~ P n. + forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n. Proof. unfold not in |- *; intros P notall. apply NNPP; unfold not in |- *. @@ -30,7 +30,7 @@ apply abs; exists n; trivial. Qed. Lemma not_all_not_ex : - forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U | P n. + forall P:U -> Prop, ~ (forall n:U, ~ P n) -> exists n : U, P n. Proof. intros P H. elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n. @@ -38,7 +38,7 @@ apply NNPP; trivial. Qed. Lemma not_ex_all_not : - forall P:U -> Prop, ~ ( exists n : U | P n) -> forall n:U, ~ P n. + forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n. Proof. unfold not in |- *; intros P notex n abs. apply notex. @@ -46,7 +46,7 @@ exists n; trivial. Qed. Lemma not_ex_not_all : - forall P:U -> Prop, ~ ( exists n : U | ~ P n) -> forall n:U, P n. + forall P:U -> Prop, ~ (exists n : U, ~ P n) -> forall n:U, P n. Proof. intros P H n. apply NNPP. @@ -54,14 +54,14 @@ red in |- *; intro K; apply H; exists n; trivial. Qed. Lemma ex_not_not_all : - forall P:U -> Prop, ( exists n : U | ~ P n) -> ~ (forall n:U, P n). + forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n). Proof. unfold not in |- *; intros P exnot allP. elim exnot; auto. Qed. Lemma all_not_not_ex : - forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U | P n). + forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n). Proof. unfold not in |- *; intros P allnot exP; elim exP; intros n p. apply allnot with n; auto. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index b03ec80e8..e1fb12f39 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -63,11 +63,11 @@ Variable rel_choice : RelationalChoice. Lemma guarded_rel_choice : forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop), - (forall x:A, P x -> exists y : B | R x y) -> - exists R' : A -> B -> Prop - | (forall x:A, + (forall x:A, P x -> exists y : B, R x y) -> + exists R' : A -> B -> Prop, + (forall x:A, P x -> - exists y : B | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). + exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). Proof. exact (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel). @@ -79,13 +79,13 @@ Qed. Require Import Bool. Lemma AC : - exists R : (bool -> Prop) -> bool -> Prop - | (forall P:bool -> Prop, - ( exists b : bool | P b) -> - exists b : bool | P b /\ R P b /\ (forall b':bool, R P b' -> b = b')). + exists R : (bool -> Prop) -> bool -> Prop, + (forall P:bool -> Prop, + (exists b : bool, P b) -> + exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')). Proof. apply guarded_rel_choice with - (P := fun Q:bool -> Prop => exists y : _ | Q y) + (P := fun Q:bool -> Prop => exists y : _, Q y) (R := fun (Q:bool -> Prop) (y:bool) => Q y). exact (fun _ H => H). Qed. @@ -135,4 +135,4 @@ left; assumption. Qed. -End PredExt_GuardRelChoice_imp_EM.
\ No newline at end of file +End PredExt_GuardRelChoice_imp_EM. diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index c55095e47..12c3f746a 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -13,8 +13,8 @@ Axiom relational_choice : forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists y : B | R x y) -> - exists R' : A -> B -> Prop - | (forall x:A, - exists y : B - | R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
\ No newline at end of file + (forall x:A, exists y : B, R x y) -> + exists R' : A -> B -> Prop, + (forall x:A, + exists y : B, + R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 6ef509d06..ab8fa3545 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -876,8 +876,8 @@ Qed. Lemma Pminus_mask_Gt : forall p q:positive, (p ?= q) Eq = Gt -> - exists h : positive - | Pminus_mask p q = IsPos h /\ + exists h : positive, + Pminus_mask p q = IsPos h /\ q + h = p /\ (h = xH \/ Pminus_mask_carry p q = IsPos (Ppred h)). Proof. intro x; induction x as [p| p| ]; intro y; destruct y as [q| q| ]; diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index c0e2bb020..11410c789 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -124,7 +124,7 @@ Qed. (** [nat_of_P] maps to the strictly positive subset of [nat] *) -Lemma ZL4 : forall p:positive, exists h : nat | nat_of_P p = S h. +Lemma ZL4 : forall p:positive, exists h : nat, nat_of_P p = S h. Proof. intro y; induction y as [p H| p H| ]; [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *; diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 72c99fc10..8be8c47fa 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -55,7 +55,7 @@ intros n m; pattern n, m in |- *; apply nat_double_ind; Qed. Lemma even_odd_cor : - forall n:nat, exists p : nat | n = (2 * p)%nat \/ n = S (2 * p). + forall n:nat, exists p : nat, n = (2 * p)%nat \/ n = S (2 * p). intro. assert (H := even_or_odd n). exists (div2 n). @@ -87,7 +87,7 @@ Qed. Lemma euclidian_division : forall x y:R, y <> 0 -> - exists k : Z | ( exists r : R | x = IZR k * y + r /\ 0 <= r < Rabs y). + exists k : Z, (exists r : R, x = IZR k * y + r /\ 0 <= r < Rabs y). intros. pose (k0 := diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index 5eab01e5b..d7531e49f 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -20,9 +20,9 @@ Theorem MVT : a < b -> (forall c:R, a <= c <= b -> continuity_pt f c) -> (forall c:R, a <= c <= b -> continuity_pt g c) -> - exists c : R - | ( exists P : a < c < b - | (g b - g a) * derive_pt f c (pr1 c P) = + exists c : R, + (exists P : a < c < b, + (g b - g a) * derive_pt f c (pr1 c P) = (f b - f a) * derive_pt g c (pr2 c P)). intros; assert (H2 := Rlt_le _ _ H). pose (h := fun y:R => (g b - g a) * f y - (f b - f a) * g y). @@ -140,7 +140,7 @@ Qed. Lemma MVT_cor1 : forall (f:R -> R) (a b:R) (pr:derivable f), a < b -> - exists c : R | f b - f a = derive_pt f c (pr c) * (b - a) /\ a < c < b. + exists c : R, f b - f a = derive_pt f c (pr c) * (b - a) /\ a < c < b. intros f a b pr H; cut (forall c:R, a < c < b -> derivable_pt f c); [ intro | intros; apply pr ]. cut (forall c:R, a < c < b -> derivable_pt id c); @@ -164,7 +164,7 @@ Theorem MVT_cor2 : forall (f f':R -> R) (a b:R), a < b -> (forall c:R, a <= c <= b -> derivable_pt_lim f c (f' c)) -> - exists c : R | f b - f a = f' c * (b - a) /\ a < c < b. + exists c : R, f b - f a = f' c * (b - a) /\ a < c < b. intros f f' a b H H0; cut (forall c:R, a <= c <= b -> derivable_pt f c). intro; cut (forall c:R, a < c < b -> derivable_pt f c). intro; cut (forall c:R, a <= c <= b -> continuity_pt f c). @@ -194,9 +194,9 @@ Lemma MVT_cor3 : forall (f f':R -> R) (a b:R), a < b -> (forall x:R, a <= x -> x <= b -> derivable_pt_lim f x (f' x)) -> - exists c : R | a <= c /\ c <= b /\ f b = f a + f' c * (b - a). + exists c : R, a <= c /\ c <= b /\ f b = f a + f' c * (b - a). intros f f' a b H H0; - assert (H1 : exists c : R | f b - f a = f' c * (b - a) /\ a < c < b); + assert (H1 : exists c : R, f b - f a = f' c * (b - a) /\ a < c < b); [ apply MVT_cor2; [ apply H | intros; elim H1; intros; apply (H0 _ H2 H3) ] | elim H1; intros; exists x; elim H2; intros; elim H4; intros; split; [ left; assumption | split; [ left; assumption | rewrite <- H3; ring ] ] ]. @@ -207,7 +207,7 @@ Lemma Rolle : (forall x:R, a <= x <= b -> continuity_pt f x) -> a < b -> f a = f b -> - exists c : R | ( exists P : a < c < b | derive_pt f c (pr c P) = 0). + exists c : R, (exists P : a < c < b, derive_pt f c (pr c P) = 0). intros; assert (H2 : forall x:R, a < x < b -> derivable_pt id x). intros; apply derivable_pt_id. assert (H3 := MVT f id a b pr H2 H0 H); @@ -669,7 +669,7 @@ Lemma antiderivative_Ucte : forall (f g1 g2:R -> R) (a b:R), antiderivative f g1 a b -> antiderivative f g2 a b -> - exists c : R | (forall x:R, a <= x <= b -> g1 x = g2 x + c). + exists c : R, (forall x:R, a <= x <= b -> g1 x = g2 x + c). unfold antiderivative in |- *; intros; elim H; clear H; intros; elim H0; clear H0; intros H0 _; exists (g1 a - g2 a); intros; assert (H3 : forall x:R, a <= x <= b -> derivable_pt g1 x). @@ -696,4 +696,4 @@ apply derivable_pt_lim_minus; [ elim (H _ H9) | elim (H0 _ H9) ]; intros; assert (H8 := null_derivative_loc (g1 - g2)%F a b H5 H6 H7); unfold constant_D_eq in H8; assert (H9 := H8 _ H2); unfold minus_fct in H9; rewrite <- H9; ring. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 4111377b7..b6375829b 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -22,8 +22,8 @@ Definition CVU (fn:nat -> R -> R) (f:R -> R) (x:R) (r:posreal) : Prop := forall eps:R, 0 < eps -> - exists N : nat - | (forall (n:nat) (y:R), + exists N : nat, + (forall (n:nat) (y:R), (N <= n)%nat -> Boule x r y -> Rabs (f y - fn n y) < eps). (* Normal convergence *) @@ -104,7 +104,7 @@ cut (0 < eps / 3); [ assumption | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H _ H3); intros N0 H4. assert (H5 := H0 N0 y H1). -cut ( exists del : posreal | (forall h:R, Rabs h < del -> Boule x r (y + h))). +cut (exists del : posreal, (forall h:R, Rabs h < del -> Boule x r (y + h))). intro. elim H6; intros del1 H7. unfold continuity_pt in H5; unfold continue_in in H5; unfold limit1_in in H5; @@ -256,4 +256,4 @@ unfold An in |- *; apply H4; unfold Boule in |- *; simpl in |- *; rewrite Rminus_0_r; pattern (Rabs x) at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rlt_0_1. apply Rplus_le_lt_0_compat; [ apply Rabs_pos | apply Rlt_0_1 ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index ad67223ad..346938735 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1306,7 +1306,7 @@ Hint Resolve not_1_INR: real. (**********) -Lemma IZN : forall n:Z, (0 <= n)%Z -> exists m : nat | n = Z_of_nat m. +Lemma IZN : forall n:Z, (0 <= n)%Z -> exists m : nat, n = Z_of_nat m. intros z; idtac; apply Z_of_nat_complete; assumption. Qed. @@ -1483,7 +1483,7 @@ Lemma tech_single_z_r_R1 : forall r (n:Z), r < IZR n -> IZR n <= r + 1 -> - ( exists s : Z | s <> n /\ r < IZR s /\ IZR s <= r + 1) -> False. + (exists s : Z, s <> n /\ r < IZR s /\ IZR s <= r + 1) -> False. intros r z H1 H2 [s [H3 [H4 H5]]]. apply H3; apply single_z_r_R1 with r; trivial. Qed. @@ -1626,6 +1626,6 @@ Qed. (**********) Lemma completeness_weak : forall E:R -> Prop, - bound E -> ( exists x : R | E x) -> exists m : R | is_lub E m. + bound E -> (exists x : R, E x) -> exists m : R, is_lub E m. intros; elim (completeness E H H0); intros; split with x; assumption. Qed. diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 40848009a..6a2d3bdd7 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -120,7 +120,7 @@ Qed. Lemma AbsList_P2 : forall (l:Rlist) (x y:R), - In y (AbsList l x) -> exists z : R | In z l /\ y = Rabs (z - x) / 2. + In y (AbsList l x) -> exists z : R, In z l /\ y = Rabs (z - x) / 2. intros; induction l as [| r l Hrecl]. elim H. elim H; intro. @@ -132,7 +132,7 @@ assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros; Qed. Lemma MaxRlist_P2 : - forall l:Rlist, ( exists y : R | In y l) -> In (MaxRlist l) l. + forall l:Rlist, (exists y : R, In y l) -> In (MaxRlist l) l. intros; induction l as [| r l Hrecl]. simpl in H; elim H; trivial. induction l as [| r0 l Hrecl0]. @@ -164,7 +164,7 @@ Qed. Lemma pos_Rl_P2 : forall (l:Rlist) (x:R), - In x l <-> ( exists i : nat | (i < Rlength l)%nat /\ x = pos_Rl l i). + In x l <-> (exists i : nat, (i < Rlength l)%nat /\ x = pos_Rl l i). intros; induction l as [| r l Hrecl]. split; intro; [ elim H | elim H; intros; elim H0; intros; elim (lt_n_O _ H1) ]. @@ -186,9 +186,9 @@ Qed. Lemma Rlist_P1 : forall (l:Rlist) (P:R -> R -> Prop), - (forall x:R, In x l -> exists y : R | P x y) -> - exists l' : Rlist - | Rlength l = Rlength l' /\ + (forall x:R, In x l -> exists y : R, P x y) -> + exists l' : Rlist, + Rlength l = Rlength l' /\ (forall i:nat, (i < Rlength l)%nat -> P (pos_Rl l i) (pos_Rl l' i)). intros; induction l as [| r l Hrecl]. exists nil; intros; split; @@ -196,7 +196,7 @@ exists nil; intros; split; assert (H0 : In r (cons r l)). simpl in |- *; left; reflexivity. assert (H1 := H _ H0); - assert (H2 : forall x:R, In x l -> exists y : R | P x y). + assert (H2 : forall x:R, In x l -> exists y : R, P x y). intros; apply H; simpl in |- *; right; assumption. assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0); intros; elim H5; clear H5; intros; split. @@ -308,7 +308,7 @@ Qed. Lemma RList_P3 : forall (l:Rlist) (x:R), - In x l <-> ( exists i : nat | x = pos_Rl l i /\ (i < Rlength l)%nat). + In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < Rlength l)%nat). intros; split; intro; [ induction l as [| r l Hrecl] | induction l as [| r l Hrecl] ]. elim H. @@ -605,7 +605,7 @@ Qed. Lemma RList_P19 : forall l:Rlist, - l <> nil -> exists r : R | ( exists r0 : Rlist | l = cons r r0). + l <> nil -> exists r : R, (exists r0 : Rlist, l = cons r r0). intros; induction l as [| r l Hrecl]; [ elim H; reflexivity | exists r; exists l; reflexivity ]. Qed. @@ -613,8 +613,8 @@ Qed. Lemma RList_P20 : forall l:Rlist, (2 <= Rlength l)%nat -> - exists r : R - | ( exists r1 : R | ( exists l' : Rlist | l = cons r (cons r1 l'))). + exists r : R, + (exists r1 : R, (exists l' : Rlist, l = cons r (cons r1 l'))). intros; induction l as [| r l Hrecl]; [ simpl in H; elim (le_Sn_O _ H) | induction l as [| r0 l Hrecl0]; @@ -741,4 +741,4 @@ change (S (m - Rlength l1) = (S m - Rlength l1)%nat) in |- *; apply minus_Sn_m; assumption. replace (cons r r0) with (cons_Rlist (cons r nil) r0); [ symmetry in |- *; apply RList_P27 | reflexivity ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 37d987855..492b2571c 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -140,7 +140,7 @@ repeat rewrite <- INR_IZR_INZ; auto with real. Qed. (**********) -Lemma fp_nat : forall r:R, frac_part r = 0 -> exists c : Z | r = IZR c. +Lemma fp_nat : forall r:R, frac_part r = 0 -> exists c : Z, r = IZR c. unfold frac_part in |- *; intros; split with (Int_part r); apply Rminus_diag_uniq; auto with zarith real. Qed. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index f60c609a0..b7d490225 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -234,8 +234,8 @@ Qed. Definition derivable_pt_lim f (x l:R) : Prop := forall eps:R, 0 < eps -> - exists delta : posreal - | (forall h:R, + exists delta : posreal, + (forall h:R, h <> 0 -> Rabs h < delta -> Rabs ((f (x + h) - f x) / h - l) < eps). Definition derivable_pt_abs f (x l:R) : Prop := derivable_pt_lim f x l. @@ -255,7 +255,7 @@ Arguments Scope derive [Rfun_scope _]. Definition antiderivative f (g:R -> R) (a b:R) : Prop := (forall x:R, - a <= x <= b -> exists pr : derivable_pt g x | f x = derive_pt g x pr) /\ + a <= x <= b -> exists pr : derivable_pt g x, f x = derive_pt g x pr) /\ a <= b. (************************************) (** Class of differential functions *) @@ -446,7 +446,7 @@ Qed. (***********************************) (**********) Lemma derivable_derive : - forall f (x:R) (pr:derivable_pt f x), exists l : R | derive_pt f x pr = l. + forall f (x:R) (pr:derivable_pt f x), exists l : R, derive_pt f x pr = l. intros; exists (projT1 pr). unfold derive_pt in |- *; reflexivity. Qed. @@ -1476,4 +1476,4 @@ unfold Rdiv in |- *; rewrite <- Ropp_mult_distr_l_reverse; apply Rplus_lt_reg_r with l. unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rplus_0_r; assumption. apply Rinv_0_lt_compat; prove_sup0. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index a02c5da6c..980bb2b51 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -395,7 +395,7 @@ Lemma continuous_neq_0 : forall (f:R -> R) (x0:R), continuity_pt f x0 -> f x0 <> 0 -> - exists eps : posreal | (forall h:R, Rabs h < eps -> f (x0 + h) <> 0). + exists eps : posreal, (forall h:R, Rabs h < eps -> f (x0 + h) <> 0). intros; unfold continuity_pt in H; unfold continue_in in H; unfold limit1_in in H; unfold limit_in in H; elim (H (Rabs (f x0 / 2))). intros; elim H1; intros. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index a047c78c0..62de585bc 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -144,7 +144,7 @@ Axiom archimed : forall r:R, IZR (up r) > r /\ IZR (up r) - r <= 1. Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m. (**********) -Definition bound (E:R -> Prop) := exists m : R | is_upper_bound E m. +Definition bound (E:R -> Prop) := exists m : R, is_upper_bound E m. (**********) Definition is_lub (E:R -> Prop) (m:R) := @@ -154,4 +154,4 @@ Definition is_lub (E:R -> Prop) (m:R) := Axiom completeness : forall E:R -> Prop, - bound E -> ( exists x : R | E x) -> sigT (fun m:R => is_lub E m). + bound E -> (exists x : R, E x) -> sigT (fun m:R => is_lub E m). diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 62eff1d1f..188699e6d 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -226,10 +226,10 @@ Lemma Pow_x_infinity : forall x:R, Rabs x > 1 -> forall b:R, - exists N : nat | (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) >= b). + exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) >= b). Proof. intros; elim (archimed (b * / (Rabs x - 1))); intros; clear H1; - cut ( exists N : nat | INR N >= b * / (Rabs x - 1)). + cut (exists N : nat, INR N >= b * / (Rabs x - 1)). intro; elim H1; clear H1; intros; exists x0; intros; apply (Rge_trans (Rabs (x ^ n)) (Rabs (x ^ x0)) b). apply Rle_ge; apply Power_monotonic; assumption. @@ -289,7 +289,7 @@ Lemma pow_lt_1_zero : Rabs x < 1 -> forall y:R, 0 < y -> - exists N : nat | (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) < y). + exists N : nat, (forall n:nat, (n >= N)%nat -> Rabs (x ^ n) < y). Proof. intros; elim (Req_dec x 0); intro. exists 1%nat; rewrite H1; intros n GE; rewrite pow_ne_zero. @@ -789,5 +789,5 @@ Qed. Definition infinit_sum (s:nat -> R) (l:R) : Prop := forall eps:R, eps > 0 -> - exists N : nat - | (forall n:nat, (n >= N)%nat -> R_dist (sum_f_R0 s n) l < eps).
\ No newline at end of file + exists N : nat, + (forall n:nat, (n >= N)%nat -> R_dist (sum_f_R0 s n) l < eps). diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 2766aa2fe..8b087856c 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -427,7 +427,7 @@ Lemma maxN : a < b -> sigT (fun n:nat => a + INR n * del < b /\ b <= a + INR (S n) * del). intros; pose (I := fun n:nat => a + INR n * del < b); - assert (H0 : exists n : nat | I n). + assert (H0 : exists n : nat, I n). exists 0%nat; unfold I in |- *; rewrite Rmult_0_l; rewrite Rplus_0_r; assumption. cut (Nbound I). @@ -498,7 +498,7 @@ intro f; intros; unfold bound in |- *; exists (b - a); unfold is_upper_bound in |- *; intros; unfold E in H1; elim H1; clear H1; intros H1 _; elim H1; intros; assumption. -assert (H2 : exists x : R | E x). +assert (H2 : exists x : R, E x). assert (H2 := Heine f (fun x:R => a <= x <= b) (compact_P3 a b) H0 eps); elim H2; intros; exists (Rmin x (b - a)); unfold E in |- *; split; @@ -512,7 +512,7 @@ assert (H3 := completeness E H1 H2); elim H3; intros; cut (0 < x <= b - a). intro; elim H4; clear H4; intros; apply existT with (mkposreal _ H4); split. apply H5. unfold is_lub in p; elim p; intros; unfold is_upper_bound in H6; - pose (D := Rabs (x0 - y)); elim (classic ( exists y : R | D < y /\ E y)); + pose (D := Rabs (x0 - y)); elim (classic (exists y : R, D < y /\ E y)); intro. elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13; intros; apply H15; assumption. @@ -701,8 +701,8 @@ intros; rewrite H2 in H7; rewrite H3 in H7; simpl in |- *; (forall t:R, a <= t <= b -> t = b \/ - ( exists i : nat - | (i < pred (Rlength (SubEqui del H)))%nat /\ + (exists i : nat, + (i < pred (Rlength (SubEqui del H)))%nat /\ co_interval (pos_Rl (SubEqui del H) i) (pos_Rl (SubEqui del H) (S i)) t)). intro; elim (H8 _ H7); intro. @@ -744,7 +744,7 @@ apply Rge_minus; apply Rle_ge; assumption. intros; clear H0 H1 H4 phi H5 H6 t H7; case (Req_dec t0 b); intro. left; assumption. right; pose (I := fun j:nat => a + INR j * del <= t0); - assert (H1 : exists n : nat | I n). + assert (H1 : exists n : nat, I n). exists 0%nat; unfold I in |- *; rewrite Rmult_0_l; rewrite Rplus_0_r; elim H8; intros; assumption. assert (H4 : Nbound I). @@ -818,15 +818,15 @@ unfold RiemannInt in |- *; case (RiemannInt_exists pr1 RinvN RinvN_cv); unfold RiemannInt in |- *; case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; cut - ( exists psi1 : nat -> StepFun a b - | (forall n:nat, + (exists psi1 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\ Rabs (RiemannInt_SF (psi1 n)) < RinvN n)). cut - ( exists psi2 : nat -> StepFun b a - | (forall n:nat, + (exists psi2 : nat -> StepFun b a, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\ @@ -1324,8 +1324,8 @@ replace eps with (3 * (eps / 5) + eps / 5 + eps / 5). repeat apply Rplus_lt_compat. assert (H7 : - exists psi1 : nat -> StepFun a b - | (forall n:nat, + exists psi1 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\ @@ -1334,8 +1334,8 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro; apply (projT2 (phi_sequence_prop RinvN pr1 n0)). assert (H8 : - exists psi2 : nat -> StepFun a b - | (forall n:nat, + exists psi2 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (g t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\ @@ -1344,8 +1344,8 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro; apply (projT2 (phi_sequence_prop RinvN pr2 n0)). assert (H9 : - exists psi3 : nat -> StepFun a b - | (forall n:nat, + exists psi3 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t + l * g t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\ @@ -1513,8 +1513,8 @@ pose (phi1 := fun N:nat => phi_sequence RinvN pr N); pose (f := fct_cte c); assert (H1 : - exists psi1 : nat -> StepFun a b - | (forall n:nat, + exists psi1 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr n t) <= psi1 n t) /\ @@ -1606,8 +1606,8 @@ apply Rcontinuity_abs. pose (phi3 := phi_sequence RinvN pr2); assert (H0 : - exists psi3 : nat -> StepFun a b - | (forall n:nat, + exists psi3 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (Rabs (f t) - phi3 n t) <= psi3 n t) /\ @@ -1616,16 +1616,16 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro; apply (projT2 (phi_sequence_prop RinvN pr2 n)). assert (H1 : - exists psi2 : nat -> StepFun a b - | (forall n:nat, + exists psi2 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (Rabs (f t) - phi2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). assert (H1 : - exists psi2 : nat -> StepFun a b - | (forall n:nat, + exists psi2 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). @@ -1656,8 +1656,8 @@ pose (phi1 := fun N:nat => phi_sequence RinvN pr1 N); change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) x) in |- *; assert (H1 : - exists psi1 : nat -> StepFun a b - | (forall n:nat, + exists psi1 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi1 n t) <= psi1 n t) /\ @@ -1681,8 +1681,8 @@ cut (forall N:nat, IsStepFun (phi2_aux N) a b). intro; pose (phi2_m := fun N:nat => mkStepFun (X N)). assert (H2 : - exists psi2 : nat -> StepFun a b - | (forall n:nat, + exists psi2 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (g t - phi2 n t) <= psi2 n t) /\ Rabs (RiemannInt_SF (psi2 n)) < RinvN n)). @@ -2328,8 +2328,8 @@ apply Rmult_eq_reg_l with 3; clear x u x0 x1 eps H H0 N1 H1 N2 H2; assert (H1 : - exists psi1 : nat -> StepFun a b - | (forall n:nat, + exists psi1 : nat -> StepFun a b, + (forall n:nat, (forall t:R, Rmin a b <= t /\ t <= Rmax a b -> Rabs (f t - phi_sequence RinvN pr1 n t) <= psi1 n t) /\ @@ -2338,8 +2338,8 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr1 n)); intro; apply (projT2 (phi_sequence_prop RinvN pr1 n)). assert (H2 : - exists psi2 : nat -> StepFun b c - | (forall n:nat, + exists psi2 : nat -> StepFun b c, + (forall n:nat, (forall t:R, Rmin b c <= t /\ t <= Rmax b c -> Rabs (f t - phi_sequence RinvN pr2 n t) <= psi2 n t) /\ @@ -2348,8 +2348,8 @@ split with (fun n:nat => projT1 (phi_sequence_prop RinvN pr2 n)); intro; apply (projT2 (phi_sequence_prop RinvN pr2 n)). assert (H3 : - exists psi3 : nat -> StepFun a c - | (forall n:nat, + exists psi3 : nat -> StepFun a c, + (forall n:nat, (forall t:R, Rmin a c <= t /\ t <= Rmax a c -> Rabs (f t - phi_sequence RinvN pr3 n t) <= psi3 n t) /\ @@ -3260,4 +3260,4 @@ intro f; intros; case (Rle_dec a b); intro; [ auto with real | assert (H0 := RiemannInt_P1 pr); rewrite (RiemannInt_P8 pr H0); rewrite (RiemannInt_P33 _ H0 H); ring ] ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 5f47466ac..19782f2bc 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -21,7 +21,7 @@ Set Implicit Arguments. (**************************************************) Definition Nbound (I:nat -> Prop) : Prop := - exists n : nat | (forall i:nat, I i -> (i <= n)%nat). + exists n : nat, (forall i:nat, I i -> (i <= n)%nat). Lemma IZN_var : forall z:Z, (0 <= z)%Z -> {n : nat | z = Z_of_nat n}. intros; apply Z_of_nat_complete_inf; assumption. @@ -29,15 +29,15 @@ Qed. Lemma Nzorn : forall I:nat -> Prop, - ( exists n : nat | I n) -> + (exists n : nat, I n) -> Nbound I -> sigT (fun n:nat => I n /\ (forall i:nat, I i -> (i <= n)%nat)). -intros I H H0; pose (E := fun x:R => exists i : nat | I i /\ INR i = x); +intros I H H0; pose (E := fun x:R => exists i : nat, I i /\ INR i = x); assert (H1 : bound E). unfold Nbound in H0; elim H0; intros N H1; unfold bound in |- *; exists (INR N); unfold is_upper_bound in |- *; intros; unfold E in H2; elim H2; intros; elim H3; intros; rewrite <- H5; apply le_INR; apply H1; assumption. -assert (H2 : exists x : R | E x). +assert (H2 : exists x : R, E x). elim H; intros; exists (INR x); unfold E in |- *; exists x; split; [ assumption | reflexivity ]. assert (H3 := completeness E H1 H2); elim H3; intros; unfold is_lub in p; @@ -311,8 +311,8 @@ Lemma StepFun_P10 : forall (f:R -> R) (l lf:Rlist) (a b:R), a <= b -> adapted_couple f a b l lf -> - exists l' : Rlist - | ( exists lf' : Rlist | adapted_couple_opt f a b l' lf'). + exists l' : Rlist, + (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). simple induction l. intros; unfold adapted_couple in H0; decompose [and] H0; simpl in H4; discriminate. @@ -886,8 +886,8 @@ Qed. Lemma StepFun_P16 : forall (f:R -> R) (l lf:Rlist) (a b:R), adapted_couple f a b l lf -> - exists l' : Rlist - | ( exists lf' : Rlist | adapted_couple_opt f a b l' lf'). + exists l' : Rlist, + (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). intros; case (Rle_dec a b); intro; [ apply (StepFun_P10 r H) | assert (H1 : b <= a); @@ -1086,14 +1086,14 @@ apply StepFun_P20; rewrite RList_P11; rewrite H2; rewrite H7; simpl in |- *; apply lt_O_Sn. intros; unfold constant_D_eq, open_interval in |- *; intros; cut - ( exists l : R - | constant_D_eq f + (exists l : R, + constant_D_eq f (open_interval (pos_Rl (cons_ORlist lf lg) i) (pos_Rl (cons_ORlist lf lg) (S i))) l). intros; elim H11; clear H11; intros; assert (H12 := H11); assert (Hyp_cons : - exists r : R | ( exists r0 : Rlist | cons_ORlist lf lg = cons r r0)). + exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons; unfold FF in |- *; rewrite RList_P12. @@ -1155,7 +1155,7 @@ pose assert (H12 : Nbound I). unfold Nbound in |- *; exists (Rlength lf); intros; unfold I in H12; elim H12; intros; apply lt_le_weak; assumption. -assert (H13 : exists n : nat | I n). +assert (H13 : exists n : nat, I n). exists 0%nat; unfold I in |- *; split. apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0). right; symmetry in |- *. @@ -1335,14 +1335,14 @@ apply StepFun_P20; rewrite RList_P11; rewrite H7; rewrite H2; simpl in |- *; apply lt_O_Sn. unfold constant_D_eq, open_interval in |- *; intros; cut - ( exists l : R - | constant_D_eq g + (exists l : R, + constant_D_eq g (open_interval (pos_Rl (cons_ORlist lf lg) i) (pos_Rl (cons_ORlist lf lg) (S i))) l). intros; elim H11; clear H11; intros; assert (H12 := H11); assert (Hyp_cons : - exists r : R | ( exists r0 : Rlist | cons_ORlist lf lg = cons r r0)). + exists r : R, (exists r0 : Rlist, cons_ORlist lf lg = cons r r0)). apply RList_P19; red in |- *; intro; rewrite H13 in H8; elim (lt_n_O _ H8). elim Hyp_cons; clear Hyp_cons; intros r [r0 Hyp_cons]; rewrite Hyp_cons; unfold FF in |- *; rewrite RList_P12. @@ -1402,7 +1402,7 @@ pose assert (H12 : Nbound I). unfold Nbound in |- *; exists (Rlength lg); intros; unfold I in H12; elim H12; intros; apply lt_le_weak; assumption. -assert (H13 : exists n : nat | I n). +assert (H13 : exists n : nat, I n). exists 0%nat; unfold I in |- *; split. apply Rle_trans with (pos_Rl (cons_ORlist lf lg) 0). right; symmetry in |- *; rewrite H1; rewrite <- H6; apply RList_P15; @@ -2629,4 +2629,4 @@ apply StepFun_P6; assumption. split; [ assumption | auto with real ]. apply StepFun_P6; apply StepFun_P41 with b; auto with real || apply StepFun_P6; assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 5fb50822b..e6a2f70a7 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -156,8 +156,8 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X') (D:Base X -> Prop) (x0:Base X) (l:Base X') := forall eps:R, eps > 0 -> - exists alp : R - | alp > 0 /\ + exists alp : R, + alp > 0 /\ (forall x:Base X, D x /\ dist X x x0 < alp -> dist X' (f x) l < eps). (*******************************) @@ -323,7 +323,7 @@ Qed. (*********) Definition adhDa (D:R -> Prop) (a:R) : Prop := - forall alp:R, alp > 0 -> exists x : R | D x /\ R_dist x a < alp. + forall alp:R, alp > 0 -> exists x : R, D x /\ R_dist x a < alp. (*********) Lemma single_limit : @@ -554,4 +554,4 @@ change (0 < Rabs l / 2) in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ intro H3; generalize (lt_INR_0 2 (neq_O_lt 2 H3)); unfold INR in |- *; intro; assumption | discriminate ] ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 03544af4b..d8be38f65 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -35,27 +35,27 @@ Fixpoint Rmax_N (N:nat) : R := end. (*********) -Definition EUn r : Prop := exists i : nat | r = Un i. +Definition EUn r : Prop := exists i : nat, r = Un i. (*********) Definition Un_cv (l:R) : Prop := forall eps:R, eps > 0 -> - exists N : nat | (forall n:nat, (n >= N)%nat -> R_dist (Un n) l < eps). + exists N : nat, (forall n:nat, (n >= N)%nat -> R_dist (Un n) l < eps). (*********) Definition Cauchy_crit : Prop := forall eps:R, eps > 0 -> - exists N : nat - | (forall n m:nat, + exists N : nat, + (forall n m:nat, (n >= N)%nat -> (m >= N)%nat -> R_dist (Un n) (Un m) < eps). (*********) Definition Un_growing : Prop := forall n:nat, Un n <= Un (S n). (*********) -Lemma EUn_noempty : exists r : R | EUn r. +Lemma EUn_noempty : exists r : R, EUn r. unfold EUn in |- *; split with (Un 0); split with 0%nat; trivial. Qed. @@ -99,7 +99,7 @@ Qed. (* classical is needed: [not_all_not_ex] *) (*********) -Lemma Un_cv_crit : Un_growing -> bound EUn -> exists l : R | Un_cv l. +Lemma Un_cv_crit : Un_growing -> bound EUn -> exists l : R, Un_cv l. unfold Un_growing, Un_cv in |- *; intros; generalize (completeness_weak EUn H0 EUn_noempty); intro; elim H1; clear H1; intros; split with x; intros; @@ -107,7 +107,7 @@ unfold Un_growing, Un_cv in |- *; intros; elim H0; clear H0; intros; elim H1; clear H1; intros; generalize (H3 x0 H0); intro; cut (forall n:nat, Un n <= x); intro. -cut ( exists N : nat | x - eps < Un N). +cut (exists N : nat, x - eps < Un N). intro; elim H6; clear H6; intros; split with x1. intros; unfold R_dist in |- *; apply (Rabs_def1 (Un n - x) eps). unfold Rgt in H2; @@ -140,7 +140,7 @@ Qed. (*********) Lemma finite_greater : - forall N:nat, exists M : R | (forall n:nat, (n <= N)%nat -> Un n <= M). + forall N:nat, exists M : R, (forall n:nat, (n <= N)%nat -> Un n <= M). intro; induction N as [| N HrecN]. split with (Un 0); intros; rewrite (le_n_O_eq n H); apply (Req_le (Un n) (Un n) (refl_equal (Un n))). @@ -272,4 +272,4 @@ assumption. apply Rabs_pos_lt. apply Rinv_neq_0_compat. assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 17b884d45..75385b424 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -18,7 +18,7 @@ Require Import Classical_Pred_Type. Open Local Scope R_scope. Definition included (D1 D2:R -> Prop) : Prop := forall x:R, D1 x -> D2 x. Definition disc (x:R) (delta:posreal) (y:R) : Prop := Rabs (y - x) < delta. Definition neighbourhood (V:R -> Prop) (x:R) : Prop := - exists delta : posreal | included (disc x delta) V. + exists delta : posreal, included (disc x delta) V. Definition open_set (D:R -> Prop) : Prop := forall x:R, D x -> neighbourhood D x. Definition complementary (D:R -> Prop) (c:R) : Prop := ~ D c. @@ -41,7 +41,7 @@ Qed. Definition point_adherent (D:R -> Prop) (x:R) : Prop := forall V:R -> Prop, - neighbourhood V x -> exists y : R | intersection_domain V D y. + neighbourhood V x -> exists y : R, intersection_domain V D y. Definition adherence (D:R -> Prop) (x:R) : Prop := point_adherent D x. Lemma adherence_P1 : forall D:R -> Prop, included D (adherence D). @@ -87,7 +87,7 @@ Qed. Lemma complementary_P1 : forall D:R -> Prop, - ~ ( exists y : R | intersection_domain D (complementary D) y). + ~ (exists y : R, intersection_domain D (complementary D) y). intro; red in |- *; intro; elim H; intros; unfold intersection_domain, complementary in H0; elim H0; intros; elim H2; assumption. @@ -111,14 +111,14 @@ intro; unfold closed_set, adherence in |- *; pose (P := fun V:R -> Prop => - neighbourhood V x -> exists y : R | intersection_domain V D y); + neighbourhood V x -> exists y : R, intersection_domain V D y); assert (H0 := not_all_ex_not _ P H); elim H0; intros V0 H1; unfold P in H1; assert (H2 := imply_to_and _ _ H1); unfold neighbourhood in |- *; elim H2; intros; unfold neighbourhood in H3; elim H3; intros; exists x0; unfold included in |- *; intros; red in |- *; intro. assert (H8 := H7 V0); - cut ( exists delta : posreal | (forall x:R, disc x1 delta x -> V0 x)). + cut (exists delta : posreal, (forall x:R, disc x1 delta x -> V0 x)). intro; assert (H10 := H8 H9); elim H4; assumption. cut (0 < x0 - Rabs (x - x1)). intro; pose (del := mkposreal _ H9); exists del; intros; @@ -248,8 +248,8 @@ Lemma continuity_P1 : continuity_pt f x <-> (forall W:R -> Prop, neighbourhood W (f x) -> - exists V : R -> Prop - | neighbourhood V x /\ (forall y:R, V y -> W (f y))). + exists V : R -> Prop, + neighbourhood V x /\ (forall y:R, V y -> W (f y))). intros; split. intros; unfold neighbourhood in H0. elim H0; intros del1 H1. @@ -329,10 +329,10 @@ Qed. Theorem Rsepare : forall x y:R, x <> y -> - exists V : R -> Prop - | ( exists W : R -> Prop - | neighbourhood V x /\ - neighbourhood W y /\ ~ ( exists y : R | intersection_domain V W y)). + exists V : R -> Prop, + (exists W : R -> Prop, + neighbourhood V x /\ + neighbourhood W y /\ ~ (exists y : R, intersection_domain V W y)). intros x y Hsep; pose (D := Rabs (x - y)). cut (0 < D / 2). intro; exists (disc x (mkposreal _ H)). @@ -360,17 +360,17 @@ Qed. Record family : Type := mkfamily {ind : R -> Prop; f :> R -> R -> Prop; - cond_fam : forall x:R, ( exists y : R | f x y) -> ind x}. + cond_fam : forall x:R, (exists y : R, f x y) -> ind x}. Definition family_open_set (f:family) : Prop := forall x:R, open_set (f x). Definition domain_finite (D:R -> Prop) : Prop := - exists l : Rlist | (forall x:R, D x <-> In x l). + exists l : Rlist, (forall x:R, D x <-> In x l). Definition family_finite (f:family) : Prop := domain_finite (ind f). Definition covering (D:R -> Prop) (f:family) : Prop := - forall x:R, D x -> exists y : R | f y x. + forall x:R, D x -> exists y : R, f y x. Definition covering_open_set (D:R -> Prop) (f:family) : Prop := covering D f /\ family_open_set f. @@ -380,7 +380,7 @@ Definition covering_finite (D:R -> Prop) (f:family) : Prop := Lemma restriction_family : forall (f:family) (D:R -> Prop) (x:R), - ( exists y : R | (fun z1 z2:R => f z1 z2 /\ D z1) x y) -> + (exists y : R, (fun z1 z2:R => f z1 z2 /\ D z1) x y) -> intersection_domain (ind f) D x. intros; elim H; intros; unfold intersection_domain in |- *; elim H0; intros; split. @@ -395,7 +395,7 @@ Definition subfamily (f:family) (D:R -> Prop) : family := Definition compact (X:R -> Prop) : Prop := forall f:family, covering_open_set X f -> - exists D : R -> Prop | covering_finite X (subfamily f D). + exists D : R -> Prop, covering_finite X (subfamily f D). (**********) Lemma family_P1 : @@ -418,7 +418,7 @@ unfold open_set in |- *; unfold neighbourhood in |- *; intros; elim H3; Qed. Definition bounded (D:R -> Prop) : Prop := - exists m : R | ( exists M : R | (forall x:R, D x -> m <= x <= M)). + exists m : R, (exists M : R, (forall x:R, D x -> m <= x <= M)). Lemma open_set_P6 : forall D1 D2:R -> Prop, open_set D1 -> D1 =_D D2 -> open_set D2. @@ -433,7 +433,7 @@ Qed. Lemma compact_P1 : forall X:R -> Prop, compact X -> bounded X. intros; unfold compact in H; pose (D := fun x:R => True); pose (g := fun x y:R => Rabs y < x); - cut (forall x:R, ( exists y : _ | g x y) -> True); + cut (forall x:R, (exists y : _, g x y) -> True); [ intro | intro; trivial ]. pose (f0 := mkfamily D g H0); assert (H1 := H f0); cut (covering_open_set X f0). @@ -498,7 +498,7 @@ assumption. cut (forall y:R, X y -> 0 < Rabs (y - x) / 2). intro; pose (D := X); pose (g := fun y z:R => Rabs (y - z) < Rabs (y - x) / 2 /\ D y); - cut (forall x:R, ( exists y : _ | g x y) -> D x). + cut (forall x:R, (exists y : _, g x y) -> D x). intro; pose (f0 := mkfamily D g H3); assert (H4 := H f0); cut (covering_open_set X f0). intro; assert (H6 := H4 H5); elim H6; clear H6; intros D' H6. @@ -600,11 +600,11 @@ unfold compact in |- *; intros; (A := fun x:R => a <= x <= b /\ - ( exists D : R -> Prop - | covering_finite (fun c:R => a <= c <= x) (subfamily f0 D))); + (exists D : R -> Prop, + covering_finite (fun c:R => a <= c <= x) (subfamily f0 D))); cut (A a). intro; cut (bound A). -intro; cut ( exists a0 : R | A a0). +intro; cut (exists a0 : R, A a0). intro; assert (H3 := completeness A H1 H2); elim H3; clear H3; intros m H3; unfold is_lub in H3; cut (a <= m <= b). intro; unfold covering_open_set in H; elim H; clear H; intros; @@ -612,7 +612,7 @@ intro; unfold covering_open_set in H; elim H; clear H; intros; clear H6; intros y0 H6; unfold family_open_set in H5; assert (H7 := H5 y0); unfold open_set in H7; assert (H8 := H7 m H6); unfold neighbourhood in H8; elim H8; clear H8; intros eps H8; - cut ( exists x : R | A x /\ m - eps < x <= m). + cut (exists x : R, A x /\ m - eps < x <= m). intro; elim H9; clear H9; intros x H9; elim H9; clear H9; intros; case (Req_dec m b); intro. rewrite H11 in H10; rewrite H11 in H8; unfold A in H9; elim H9; clear H9; @@ -751,7 +751,7 @@ unfold intersection_domain in H17. split. elim H17; intros; assumption. unfold Db in |- *; left; elim H17; intros; assumption. -elim (classic ( exists x : R | A x /\ m - eps < x <= m)); intro. +elim (classic (exists x : R, A x /\ m - eps < x <= m)); intro. assumption. elim H3; intros; cut (is_upper_bound A (m - eps)). intro; assert (H13 := H11 _ H12); cut (m - eps < m). @@ -810,12 +810,12 @@ Qed. Lemma compact_P4 : forall X F:R -> Prop, compact X -> closed_set F -> included F X -> compact F. -unfold compact in |- *; intros; elim (classic ( exists z : R | F z)); +unfold compact in |- *; intros; elim (classic (exists z : R, F z)); intro Hyp_F_NE. pose (D := ind f0); pose (g := f f0); unfold closed_set in H0. pose (g' := fun x y:R => f0 x y \/ complementary F y /\ D x). pose (D' := D). -cut (forall x:R, ( exists y : R | g' x y) -> D' x). +cut (forall x:R, (exists y : R, g' x y) -> D' x). intro; pose (f' := mkfamily D' g' H3); cut (covering_open_set X f'). intro; elim (H _ H4); intros DX H5; exists DX. unfold covering_finite in |- *; unfold covering_finite in H5; elim H5; @@ -847,7 +847,7 @@ unfold covering in |- *; unfold covering in H2; intros. elim (classic (F x)); intro. elim (H2 _ H6); intros y0 H7; exists y0; simpl in |- *; unfold g' in |- *; left; assumption. -cut ( exists z : R | D z). +cut (exists z : R, D z). intro; elim H7; clear H7; intros x0 H7; exists x0; simpl in |- *; unfold g' in |- *; right. split. @@ -908,7 +908,7 @@ intro; elim H; clear H; intros; apply (compact_P5 _ H H0). Qed. Definition image_dir (f:R -> R) (D:R -> Prop) (x:R) : Prop := - exists y : R | x = f y /\ D y. + exists y : R, x = f y /\ D y. (**********) Lemma continuity_compact : @@ -918,7 +918,7 @@ unfold compact in |- *; intros; unfold covering_open_set in H1. elim H1; clear H1; intros. pose (D := ind f1). pose (g := fun x y:R => image_rec f0 (f1 x) y). -cut (forall x:R, ( exists y : R | g x y) -> D x). +cut (forall x:R, (exists y : R, g x y) -> D x). intro; pose (f' := mkfamily D g H3). cut (covering_open_set X f'). intro; elim (H0 f' H4); intros D' H5; exists D'. @@ -958,8 +958,8 @@ Lemma prolongement_C0 : forall (f:R -> R) (a b:R), a <= b -> (forall c:R, a <= c <= b -> continuity_pt f c) -> - exists g : R -> R - | continuity g /\ (forall c:R, a <= c <= b -> g c = f c). + exists g : R -> R, + continuity g /\ (forall c:R, a <= c <= b -> g c = f c). intros; elim H; intro. pose (h := @@ -1153,11 +1153,11 @@ Lemma continuity_ab_maj : forall (f:R -> R) (a b:R), a <= b -> (forall c:R, a <= c <= b -> continuity_pt f c) -> - exists Mx : R | (forall c:R, a <= c <= b -> f c <= f Mx) /\ a <= Mx <= b. + exists Mx : R, (forall c:R, a <= c <= b -> f c <= f Mx) /\ a <= Mx <= b. intros; cut - ( exists g : R -> R - | continuity g /\ (forall c:R, a <= c <= b -> g c = f0 c)). + (exists g : R -> R, + continuity g /\ (forall c:R, a <= c <= b -> g c = f0 c)). intro HypProl. elim HypProl; intros g Hcont_eq. elim Hcont_eq; clear Hcont_eq; intros Hcont Heq. @@ -1166,7 +1166,7 @@ assert (H2 := continuity_compact g (fun c:R => a <= c <= b) Hcont H1). assert (H3 := compact_P2 _ H2). assert (H4 := compact_P1 _ H2). cut (bound (image_dir g (fun c:R => a <= c <= b))). -cut ( exists x : R | image_dir g (fun c:R => a <= c <= b) x). +cut (exists x : R, image_dir g (fun c:R => a <= c <= b) x). intros; assert (H7 := completeness _ H6 H5). elim H7; clear H7; intros M H7; cut (image_dir g (fun c:R => a <= c <= b) M). intro; unfold image_dir in H8; elim H8; clear H8; intros Mxx H8; elim H8; @@ -1179,8 +1179,8 @@ apply H9. elim (classic (image_dir g (fun c:R => a <= c <= b) M)); intro. assumption. cut - ( exists eps : posreal - | (forall y:R, + (exists eps : posreal, + (forall y:R, ~ intersection_domain (disc M eps) (image_dir g (fun c:R => a <= c <= b)) y)). @@ -1207,8 +1207,8 @@ apply Rge_minus; apply Rle_ge; apply H12. apply H11. apply H7; apply H11. cut - ( exists V : R -> Prop - | neighbourhood V M /\ + (exists V : R -> Prop, + neighbourhood V M /\ (forall y:R, ~ intersection_domain V (image_dir g (fun c:R => a <= c <= b)) y)). intro; elim H9; intros V H10; elim H10; clear H10; intros. @@ -1225,8 +1225,8 @@ assert not_all_ex_not _ (fun V:R -> Prop => neighbourhood V M -> - exists y : R - | intersection_domain V (image_dir g (fun c:R => a <= c <= b)) y) H9). + exists y : R, + intersection_domain V (image_dir g (fun c:R => a <= c <= b)) y) H9). elim H10; intros V0 H11; exists V0; assert (H12 := imply_to_and _ _ H11); elim H12; clear H12; intros. split. @@ -1253,7 +1253,7 @@ Lemma continuity_ab_min : forall (f:R -> R) (a b:R), a <= b -> (forall c:R, a <= c <= b -> continuity_pt f c) -> - exists mx : R | (forall c:R, a <= c <= b -> f mx <= f c) /\ a <= mx <= b. + exists mx : R, (forall c:R, a <= c <= b -> f mx <= f c) /\ a <= mx <= b. intros. cut (forall c:R, a <= c <= b -> continuity_pt (- f0) c). intro; assert (H2 := continuity_ab_maj (- f0)%F a b H H1); elim H2; @@ -1274,18 +1274,18 @@ Qed. Definition ValAdh (un:nat -> R) (x:R) : Prop := forall (V:R -> Prop) (N:nat), - neighbourhood V x -> exists p : nat | (N <= p)%nat /\ V (un p). + neighbourhood V x -> exists p : nat, (N <= p)%nat /\ V (un p). Definition intersection_family (f:family) (x:R) : Prop := forall y:R, ind f y -> f y x. Lemma ValAdh_un_exists : - forall (un:nat -> R) (D:=fun x:R => exists n : nat | x = INR n) + forall (un:nat -> R) (D:=fun x:R => exists n : nat, x = INR n) (f:= fun x:R => adherence - (fun y:R => ( exists p : nat | y = un p /\ x <= INR p) /\ D x)) - (x:R), ( exists y : R | f x y) -> D x. + (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)) + (x:R), (exists y : R, f x y) -> D x. intros; elim H; intros; unfold f in H0; unfold adherence in H0; unfold point_adherent in H0; assert (H1 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0). @@ -1296,11 +1296,11 @@ elim (H0 _ H1); intros; unfold intersection_domain in H2; elim H2; intros; Qed. Definition ValAdh_un (un:nat -> R) : R -> Prop := - let D := fun x:R => exists n : nat | x = INR n in + let D := fun x:R => exists n : nat, x = INR n in let f := fun x:R => adherence - (fun y:R => ( exists p : nat | y = un p /\ x <= INR p) /\ D x) in + (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x) in intersection_family (mkfamily D f (ValAdh_un_exists un)). Lemma ValAdh_un_prop : @@ -1322,8 +1322,8 @@ unfold ValAdh in |- *; intros; unfold ValAdh_un in H; (H1 : adherence (fun y0:R => - ( exists p : nat | y0 = un p /\ INR N <= INR p) /\ - ( exists n : nat | INR N = INR n)) x). + (exists p : nat, y0 = un p /\ INR N <= INR p) /\ + (exists n : nat, INR N = INR n)) x). apply H; exists N; reflexivity. unfold adherence in H1; unfold point_adherent in H1; assert (H2 := H1 _ H0); elim H2; intros; unfold intersection_domain in H3; @@ -1348,7 +1348,7 @@ Definition family_closed_set (f:family) : Prop := Definition intersection_vide_in (D:R -> Prop) (f:family) : Prop := forall x:R, (ind f x -> included (f x) D) /\ - ~ ( exists y : R | intersection_family f y). + ~ (exists y : R, intersection_family f y). Definition intersection_vide_finite_in (D:R -> Prop) (f:family) : Prop := intersection_vide_in D f /\ family_finite f. @@ -1357,15 +1357,15 @@ Definition intersection_vide_finite_in (D:R -> Prop) Lemma compact_P6 : forall X:R -> Prop, compact X -> - ( exists z : R | X z) -> + (exists z : R, X z) -> forall g:family, family_closed_set g -> intersection_vide_in X g -> - exists D : R -> Prop | intersection_vide_finite_in X (subfamily g D). + exists D : R -> Prop, intersection_vide_finite_in X (subfamily g D). intros X H Hyp g H0 H1. pose (D' := ind g). pose (f' := fun x y:R => complementary (g x) y /\ D' x). -assert (H2 : forall x:R, ( exists y : R | f' x y) -> D' x). +assert (H2 : forall x:R, (exists y : R, f' x y) -> D' x). intros; elim H2; intros; unfold f' in H3; elim H3; intros; assumption. pose (f0 := mkfamily D' f' H2). unfold compact in H; assert (H3 : covering_open_set X f0). @@ -1397,7 +1397,7 @@ intros; unfold included in |- *; intros; unfold intersection_vide_in in H1; elim (H1 x); intros; elim H6; intros; apply H7. unfold intersection_domain in H5; elim H5; intros; assumption. assumption. -elim (classic ( exists y : R | intersection_domain (ind g) SF y)); intro Hyp'. +elim (classic (exists y : R, intersection_domain (ind g) SF y)); intro Hyp'. red in |- *; intro; elim H5; intros; unfold intersection_family in H6; simpl in H6. cut (X x0). @@ -1418,7 +1418,7 @@ apply H11. apply H9. apply (cond_fam g); exists x0; assumption. unfold covering_finite in H4; elim H4; clear H4; intros H4 _; - cut ( exists z : R | X z). + cut (exists z : R, X z). intro; elim H5; clear H5; intros; unfold covering in H4; elim (H4 x0 H5); intros; simpl in H6; elim Hyp'; exists x1; elim H6; intros; unfold intersection_domain in |- *; split. @@ -1435,18 +1435,18 @@ Qed. Theorem Bolzano_Weierstrass : forall (un:nat -> R) (X:R -> Prop), - compact X -> (forall n:nat, X (un n)) -> exists l : R | ValAdh un l. -intros; cut ( exists l : R | ValAdh_un un l). + compact X -> (forall n:nat, X (un n)) -> exists l : R, ValAdh un l. +intros; cut (exists l : R, ValAdh_un un l). intro; elim H1; intros; exists x; elim (ValAdh_un_prop un x); intros; apply (H4 H2). -assert (H1 : exists z : R | X z). +assert (H1 : exists z : R, X z). exists (un 0%nat); apply H0. -pose (D := fun x:R => exists n : nat | x = INR n). +pose (D := fun x:R => exists n : nat, x = INR n). pose (g := fun x:R => - adherence (fun y:R => ( exists p : nat | y = un p /\ x <= INR p) /\ D x)). -assert (H2 : forall x:R, ( exists y : R | g x y) -> D x). + adherence (fun y:R => (exists p : nat, y = un p /\ x <= INR p) /\ D x)). +assert (H2 : forall x:R, (exists y : R, g x y) -> D x). intros; elim H2; intros; unfold g in H3; unfold adherence in H3; unfold point_adherent in H3. assert (H4 : neighbourhood (disc x0 (mkposreal _ Rlt_0_1)) x0). @@ -1456,7 +1456,7 @@ elim (H3 _ H4); intros; unfold intersection_domain in H5; decompose [and] H5; assumption. pose (f0 := mkfamily D g H2). assert (H3 := compact_P6 X H H1 f0). -elim (classic ( exists l : R | ValAdh_un un l)); intro. +elim (classic (exists l : R, ValAdh_un un l)); intro. assumption. cut (family_closed_set f0). intro; cut (intersection_vide_in X f0). @@ -1480,10 +1480,10 @@ elim (H9 r); intros. simpl in H12; unfold intersection_domain in H12; cut (In r l). intro; elim (H12 H13); intros; assumption. unfold r in |- *; apply MaxRlist_P2; - cut ( exists z : R | intersection_domain (ind f0) SF z). + cut (exists z : R, intersection_domain (ind f0) SF z). intro; elim H13; intros; elim (H9 x); intros; simpl in H15; assert (H17 := H15 H14); exists x; apply H17. -elim (classic ( exists z : R | intersection_domain (ind f0) SF z)); intro. +elim (classic (exists z : R, intersection_domain (ind f0) SF z)); intro. assumption. elim (H8 0); intros _ H14; elim H1; intros; assert @@ -1517,8 +1517,8 @@ Qed. Definition uniform_continuity (f:R -> R) (X:R -> Prop) : Prop := forall eps:posreal, - exists delta : posreal - | (forall x y:R, + exists delta : posreal, + (forall x y:R, X x -> X y -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps). Lemma is_lub_u : @@ -1529,11 +1529,11 @@ Qed. Lemma domain_P1 : forall X:R -> Prop, - ~ ( exists y : R | X y) \/ - ( exists y : R | X y /\ (forall x:R, X x -> x = y)) \/ - ( exists x : R | ( exists y : R | X x /\ X y /\ x <> y)). -intro; elim (classic ( exists y : R | X y)); intro. -right; elim H; intros; elim (classic ( exists y : R | X y /\ y <> x)); intro. + ~ (exists y : R, X y) \/ + (exists y : R, X y /\ (forall x:R, X x -> x = y)) \/ + (exists x : R, (exists y : R, X x /\ X y /\ x <> y)). +intro; elim (classic (exists y : R, X y)); intro. +right; elim H; intros; elim (classic (exists y : R, X y /\ y <> x)); intro. right; elim H1; intros; elim H2; intros; exists x; exists x0; intros. split; [ assumption @@ -1564,7 +1564,7 @@ unfold uniform_continuity in |- *; intros; exists (mkposreal _ Rlt_0_1); (* X possède au moins deux éléments distincts *) assert (X_enc : - exists m : R | ( exists M : R | (forall x:R, X x -> m <= x <= M) /\ m < M)). + exists m : R, (exists M : R, (forall x:R, X x -> m <= x <= M) /\ m < M)). assert (H1 := compact_P1 X H0); unfold bounded in H1; elim H1; intros; elim H2; intros; exists x; exists x0; split. apply H3. @@ -1587,14 +1587,14 @@ pose (g := fun x y:R => X x /\ - ( exists del : posreal - | (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ + (exists del : posreal, + (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ is_lub (fun zeta:R => 0 < zeta <= M - m /\ (forall z:R, Rabs (z - x) < zeta -> Rabs (f0 z - f0 x) < eps / 2)) del /\ disc x (mkposreal (del / 2) (H1 del)) y)). -assert (H2 : forall x:R, ( exists y : R | g x y) -> X x). +assert (H2 : forall x:R, (exists y : R, g x y) -> X x). intros; elim H2; intros; unfold g in H3; elim H3; clear H3; intros H3 _; apply H3. pose (f' := mkfamily X g H2); unfold compact in H0; @@ -1616,7 +1616,7 @@ assert (H4 := H _ H3); unfold continuity_pt in H4; unfold continue_in in H4; unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *; unfold E in |- *; intros; elim H6; clear H6; intros H6 _; elim H6; clear H6; intros _ H6; apply H6. -assert (H7 : exists x : R | E x). +assert (H7 : exists x : R, E x). elim H5; clear H5; intros; exists (Rmin x0 (M - m)); unfold E in |- *; intros; split. split. @@ -1633,11 +1633,11 @@ apply Rlt_le_trans with (Rmin x0 (M - m)); [ apply H8 | apply Rmin_l ]. assert (H8 := completeness _ H6 H7); elim H8; clear H8; intros; cut (0 < x1 <= M - m). intro; elim H8; clear H8; intros; exists (mkposreal _ H8); split. -intros; cut ( exists alp : R | Rabs (z - x) < alp <= x1 /\ E alp). +intros; cut (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp). intros; elim H11; intros; elim H12; clear H12; intros; unfold E in H13; elim H13; intros; apply H15. elim H12; intros; assumption. -elim (classic ( exists alp : R | Rabs (z - x) < alp <= x1 /\ E alp)); intro. +elim (classic (exists alp : R, Rabs (z - x) < alp <= x1 /\ E alp)); intro. assumption. assert (H12 := @@ -1703,8 +1703,8 @@ elim (H0 _ H3); intros DF H4; unfold covering_finite in H4; elim H4; clear H4; cut (forall x:R, In x l -> - exists del : R - | 0 < del /\ + exists del : R, + 0 < del /\ (forall z:R, Rabs (z - x) < del -> Rabs (f0 z - f0 x) < eps / 2) /\ included (g x) (fun z:R => Rabs (z - x) < del / 2)). intros; @@ -1769,7 +1769,7 @@ intros; elim (H5 x); intros; elim (H8 H6); intros; unfold bound in |- *; exists (M - m); unfold is_upper_bound in |- *; unfold E in |- *; intros; elim H11; clear H11; intros H11 _; elim H11; clear H11; intros _ H11; apply H11. -assert (H12 : exists x : R | E x). +assert (H12 : exists x : R, E x). assert (H13 := H _ H9); unfold continuity_pt in H13; unfold continue_in in H13; unfold limit1_in in H13; unfold limit_in in H13; simpl in H13; unfold R_dist in H13; @@ -1791,10 +1791,10 @@ assert (H13 := completeness _ H11 H12); elim H13; clear H13; intros; intro; elim H13; clear H13; intros; exists x0; split. assumption. split. -intros; cut ( exists alp : R | Rabs (z - x) < alp <= x0 /\ E alp). +intros; cut (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp). intros; elim H16; intros; elim H17; clear H17; intros; unfold E in H18; elim H18; intros; apply H20; elim H17; intros; assumption. -elim (classic ( exists alp : R | Rabs (z - x) < alp <= x0 /\ E alp)); intro. +elim (classic (exists alp : R, Rabs (z - x) < alp <= x0 /\ E alp)); intro. assumption. assert (H17 := @@ -1822,4 +1822,4 @@ elim H12; intros; unfold E in H13; elim H13; intros H14 _; elim H14; apply Rlt_le_trans with x1; [ assumption | apply (H16 _ H13) ]. apply H17; intros; unfold E in H18; elim H18; intros; elim H19; intros; assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 60f07f610..6cba456fb 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -1368,7 +1368,7 @@ intros; case (Rtotal_order x y); intro H4; Qed. (**********) -Lemma sin_eq_0_1 : forall x:R, ( exists k : Z | x = IZR k * PI) -> sin x = 0. +Lemma sin_eq_0_1 : forall x:R, (exists k : Z, x = IZR k * PI) -> sin x = 0. intros. elim H; intros. apply (Zcase_sign x0). @@ -1446,7 +1446,7 @@ rewrite Ropp_involutive. reflexivity. Qed. -Lemma sin_eq_0_0 : forall x:R, sin x = 0 -> exists k : Z | x = IZR k * PI. +Lemma sin_eq_0_0 : forall x:R, sin x = 0 -> exists k : Z, x = IZR k * PI. intros. assert (H0 := euclidian_division x PI PI_neq0). elim H0; intros q H1. @@ -1491,7 +1491,7 @@ exists q; reflexivity. Qed. Lemma cos_eq_0_0 : - forall x:R, cos x = 0 -> exists k : Z | x = IZR k * PI + PI / 2. + forall x:R, cos x = 0 -> exists k : Z, x = IZR k * PI + PI / 2. intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H); intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z; rewrite <- Z_R_minus; ring; rewrite Rmult_comm; rewrite <- H3; @@ -1500,7 +1500,7 @@ rewrite (double_var (- PI)); unfold Rdiv in |- *; ring. Qed. Lemma cos_eq_0_1 : - forall x:R, ( exists k : Z | x = IZR k * PI + PI / 2) -> cos x = 0. + forall x:R, (exists k : Z, x = IZR k * PI + PI / 2) -> cos x = 0. intros x H1; rewrite cos_sin; elim H1; intros x0 H2; rewrite H2; replace (PI / 2 + (IZR x0 * PI + PI / 2)) with (IZR x0 * PI + PI). rewrite neg_sin; rewrite <- Ropp_0. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index f18e9188e..ccb79e44a 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -122,7 +122,7 @@ apply Rinv_neq_0_compat; apply INR_fact_neq_0. Qed. Lemma archimed_cor1 : - forall eps:R, 0 < eps -> exists N : nat | / INR N < eps /\ (0 < N)%nat. + forall eps:R, 0 < eps -> exists N : nat, / INR N < eps /\ (0 < N)%nat. intros; cut (/ eps < IZR (up (/ eps))). intro; cut (0 <= up (/ eps))%Z. intro; assert (H2 := IZN _ H1); elim H2; intros; exists (max x 1). diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 1175543b6..4f6951429 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -31,7 +31,7 @@ unfold Un_growing, Un_cv in |- *; intros; unfold is_upper_bound in H2, H3. assert (H5 : forall n:nat, Un n <= x). intro n; apply (H2 (Un n) (Un_in_EUn Un n)). -cut ( exists N : nat | x - eps < Un N). +cut (exists N : nat, x - eps < Un N). intro H6; destruct H6 as [N H6]; exists N. intros n H7; unfold R_dist in |- *; apply (Rabs_def1 (Un n - x) eps). unfold Rgt in H1. @@ -491,13 +491,13 @@ Qed. (**********) Lemma approx_maj : forall (Un:nat -> R) (pr:has_ub Un) (eps:R), - 0 < eps -> exists k : nat | Rabs (majorant Un pr - Un k) < eps. + 0 < eps -> exists k : nat, Rabs (majorant Un pr - Un k) < eps. intros. pose (P := fun k:nat => Rabs (majorant Un pr - Un k) < eps). unfold P in |- *. cut - (( exists k : nat | P k) -> - exists k : nat | Rabs (majorant Un pr - Un k) < eps). + ((exists k : nat, P k) -> + exists k : nat, Rabs (majorant Un pr - Un k) < eps). intros. apply H0. apply not_all_not_ex. @@ -559,13 +559,13 @@ Qed. (**********) Lemma approx_min : forall (Un:nat -> R) (pr:has_lb Un) (eps:R), - 0 < eps -> exists k : nat | Rabs (minorant Un pr - Un k) < eps. + 0 < eps -> exists k : nat, Rabs (minorant Un pr - Un k) < eps. intros. pose (P := fun k:nat => Rabs (minorant Un pr - Un k) < eps). unfold P in |- *. cut - (( exists k : nat | P k) -> - exists k : nat | Rabs (minorant Un pr - Un k) < eps). + ((exists k : nat, P k) -> + exists k : nat, Rabs (minorant Un pr - Un k) < eps). intros. apply H0. apply not_all_not_ex. @@ -710,7 +710,7 @@ Qed. Lemma maj_by_pos : forall Un:nat -> R, sigT (fun l:R => Un_cv Un l) -> - exists l : R | 0 < l /\ (forall n:nat, Rabs (Un n) <= l). + exists l : R, 0 < l /\ (forall n:nat, Rabs (Un n) <= l). intros; elim X; intros. cut (sigT (fun l:R => Un_cv (fun k:nat => Rabs (Un k)) l)). intro. @@ -946,10 +946,10 @@ Lemma tech13 : forall (An:nat -> R) (k:R), 0 <= k < 1 -> Un_cv (fun n:nat => Rabs (An (S n) / An n)) k -> - exists k0 : R - | k < k0 < 1 /\ - ( exists N : nat - | (forall n:nat, (N <= n)%nat -> Rabs (An (S n) / An n) < k0)). + exists k0 : R, + k < k0 < 1 /\ + (exists N : nat, + (forall n:nat, (N <= n)%nat -> Rabs (An (S n) / An n) < k0)). intros; exists (k + (1 - k) / 2). split. split. @@ -1053,7 +1053,7 @@ Qed. (* Un -> +oo *) Definition cv_infty (Un:nat -> R) : Prop := - forall M:R, exists N : nat | (forall n:nat, (N <= n)%nat -> M < Un n). + forall M:R, exists N : nat, (forall n:nat, (N <= n)%nat -> M < Un n). (* Un -> +oo => /Un -> O *) Lemma cv_infty_cv_R0 : @@ -1117,7 +1117,7 @@ pose (Un := fun n:nat => Rabs x ^ (M_nat + n) / INR (fact (M_nat + n))). cut (Un_cv Un 0); unfold Un_cv in |- *; unfold R_dist in |- *; intros. elim (H5 eps H0); intros N H6. exists (M_nat + N)%nat; intros; - cut ( exists p : nat | (p >= N)%nat /\ n = (M_nat + p)%nat). + cut (exists p : nat, (p >= N)%nat /\ n = (M_nat + p)%nat). intro; elim H8; intros p H9. elim H9; intros; rewrite H11; unfold Un in H6; apply H6; assumption. exists (n - M_nat)%nat. @@ -1292,4 +1292,4 @@ left; apply pow_lt; apply Rabs_pos_lt; assumption. left; apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *; intro; assert (H4 := sym_eq H3); elim (fact_neq_0 _ H4). apply H1; assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index ffac3df29..2c035cf83 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -284,8 +284,8 @@ elim (H _ H6); clear H; intros N1 H; pose (C := Rabs (sum_f_R0 (fun k:nat => An k * (Bn k - l)) N1)); assert (H7 : - exists N : nat - | (forall n:nat, (N <= n)%nat -> C / sum_f_R0 An n < eps / 2))... + exists N : nat, + (forall n:nat, (N <= n)%nat -> C / sum_f_R0 An n < eps / 2))... case (Req_dec C 0); intro... exists 0%nat; intros... rewrite H7; unfold Rdiv in |- *; rewrite Rmult_0_l; apply Rmult_lt_0_compat... @@ -414,4 +414,4 @@ apply sum_eq; intros; ring... apply H5; unfold ge in |- *; apply le_S_n; replace (S (pred n)) with n... apply S_pred with 0%nat; apply lt_le_trans with (S x)... apply lt_O_Sn... -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index 06440fd86..f4adc6522 100755 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -62,7 +62,7 @@ Section Relations_of_Relations. Definition commut (R1 R2:relation) : Prop := forall x y:A, - R1 y x -> forall z:A, R2 z y -> exists2 y' : A | R2 y' x & R1 z y'. + R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. End Relations_of_Relations. diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index 349650629..cd15a3d7f 100755 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -81,7 +81,7 @@ Theorem Rstar_Rstar' : forall x y:A, Rstar x y -> Rstar' x y. Definition commut (A:Set) (R1 R2:A -> A -> Prop) := forall x y:A, - R1 y x -> forall z:A, R2 z y -> exists2 y' : A | R2 y' x & R1 z y'. + R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. End Rstar. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 0d77c0617..59f8fb2c8 100755 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -67,7 +67,7 @@ Inductive Totally_ordered (B:Ensemble U) : Prop := Definition Compatible : Relation U := fun x y:U => In U C x -> - In U C y -> exists z : _ | In U C z /\ Upper_Bound (Couple U x y) z. + In U C y -> exists z : _, In U C z /\ Upper_Bound (Couple U x y) z. Inductive Directed (X:Ensemble U) : Prop := Definition_of_Directed : @@ -75,21 +75,21 @@ Inductive Directed (X:Ensemble U) : Prop := Inhabited U X -> (forall x1 x2:U, Included U (Couple U x1 x2) X -> - exists x3 : _ | In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) -> + exists x3 : _, In U X x3 /\ Upper_Bound (Couple U x1 x2) x3) -> Directed X. Inductive Complete : Prop := Definition_of_Complete : - ( exists bot : _ | Bottom bot) -> - (forall X:Ensemble U, Directed X -> exists bsup : _ | Lub X bsup) -> + (exists bot : _, Bottom bot) -> + (forall X:Ensemble U, Directed X -> exists bsup : _, Lub X bsup) -> Complete. Inductive Conditionally_complete : Prop := Definition_of_Conditionally_complete : (forall X:Ensemble U, Included U X C -> - ( exists maj : _ | Upper_Bound X maj) -> - exists bsup : _ | Lub X bsup) -> Conditionally_complete. + (exists maj : _, Upper_Bound X maj) -> + exists bsup : _, Lub X bsup) -> Conditionally_complete. End Bounds. Hint Resolve Totally_ordered_definition Upper_Bound_definition Lower_Bound_definition Lub_definition Glb_definition Bottom_definition diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index 28b2d6fb9..dce4c64e8 100755 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -59,8 +59,8 @@ Lemma cardinal_invert : match p with | O => X = Empty_set U | S n => - exists A : _ - | ( exists x : _ | X = Add U A x /\ ~ In U A x /\ cardinal U A n) + exists A : _, + (exists x : _, X = Add U A x /\ ~ In U A x /\ cardinal U A n) end. Proof. induction 1; simpl in |- *; auto. @@ -78,4 +78,4 @@ Proof. intros X p C; elim C; simpl in |- *; trivial with sets. Qed. -End Ensembles_finis_facts.
\ No newline at end of file +End Ensembles_finis_facts. diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index 2849bce6c..f394b2e5a 100755 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -40,7 +40,7 @@ Section Finite_sets_facts. Variable U : Type. Lemma finite_cardinal : - forall X:Ensemble U, Finite U X -> exists n : nat | cardinal U X n. + forall X:Ensemble U, Finite U X -> exists n : nat, cardinal U X n. Proof. induction 1 as [| A _ [n H]]. exists 0; auto with sets. diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index 85b83d3ab..fd1c90b90 100755 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -93,7 +93,7 @@ Hint Resolve finite_image. Lemma Im_inv : forall (X:Ensemble U) (f:U -> V) (y:V), - In _ (Im X f) y -> exists x : U | In _ X x /\ f x = y. + In _ (Im X f) y -> exists x : U, In _ X x /\ f x = y. Proof. intros X f y H'; elim H'. intros x H'0 y0 H'1; rewrite H'1. @@ -104,14 +104,14 @@ Definition injective (f:U -> V) := forall x y:U, f x = f y -> x = y. Lemma not_injective_elim : forall f:U -> V, - ~ injective f -> exists x : _ | ( exists y : _ | f x = f y /\ x <> y). + ~ injective f -> exists x : _, (exists y : _, f x = f y /\ x <> y). Proof. unfold injective in |- *; intros f H. -cut ( exists x : _ | ~ (forall y:U, f x = f y -> x = y)). +cut (exists x : _, ~ (forall y:U, f x = f y -> x = y)). 2: apply not_all_ex_not with (P := fun x:U => forall y:U, f x = f y -> x = y); trivial with sets. destruct 1 as [x C]; exists x. -cut ( exists y : _ | ~ (f x = f y -> x = y)). +cut (exists y : _, ~ (f x = f y -> x = y)). 2: apply not_all_ex_not with (P := fun y:U => f x = f y -> x = y); trivial with sets. destruct 1 as [y D]; exists y. @@ -120,7 +120,7 @@ Qed. Lemma cardinal_Im_intro : forall (A:Ensemble U) (f:U -> V) (n:nat), - cardinal _ A n -> exists p : nat | cardinal _ (Im A f) p. + cardinal _ A n -> exists p : nat, cardinal _ (Im A f) p. Proof. intros. apply finite_cardinal; apply finite_image. @@ -196,7 +196,7 @@ Lemma Pigeonhole_principle : cardinal _ A n -> forall n':nat, cardinal _ (Im A f) n' -> - n' < n -> exists x : _ | ( exists y : _ | f x = f y /\ x <> y). + n' < n -> exists x : _, (exists y : _, f x = f y /\ x <> y). Proof. intros; apply not_injective_elim. apply Pigeonhole with A n n'; trivial with sets. diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index 20ec73fa6..d401b86c1 100755 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -67,7 +67,7 @@ Lemma approximants_grow : ~ Finite U A -> forall n:nat, cardinal U X n -> - Included U X A -> exists Y : _ | cardinal U Y (S n) /\ Included U Y A. + Included U X A -> exists Y : _, cardinal U Y (S n) /\ Included U Y A. Proof. intros A X H' n H'0; elim H'0; auto with sets. intro H'1. @@ -108,12 +108,12 @@ Lemma approximants_grow' : forall n:nat, cardinal U X n -> Approximant U A X -> - exists Y : _ | cardinal U Y (S n) /\ Approximant U A Y. + exists Y : _, cardinal U Y (S n) /\ Approximant U A Y. Proof. intros A X H' n H'0 H'1; try assumption. elim H'1. intros H'2 H'3. -elimtype ( exists Y : _ | cardinal U Y (S n) /\ Included U Y A). +elimtype (exists Y : _, cardinal U Y (S n) /\ Included U Y A). intros x H'4; elim H'4; intros H'5 H'6; try exact H'5; clear H'4. exists x; auto with sets. split; [ auto with sets | idtac ]. @@ -125,7 +125,7 @@ Qed. Lemma approximant_can_be_any_size : forall A X:Ensemble U, ~ Finite U A -> - forall n:nat, exists Y : _ | cardinal U Y n /\ Approximant U A Y. + forall n:nat, exists Y : _, cardinal U Y n /\ Approximant U A Y. Proof. intros A H' H'0 n; elim n. exists (Empty_set U); auto with sets. @@ -140,8 +140,8 @@ Theorem Image_set_continuous : forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), Finite V X -> Included V X (Im U V A f) -> - exists n : _ - | ( exists Y : _ | (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X). + exists n : _, + (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X). Proof. intros A f X H'; elim H'. intro H'0; exists 0. @@ -183,12 +183,12 @@ Qed. Theorem Image_set_continuous' : forall (A:Ensemble U) (f:U -> V) (X:Ensemble V), Approximant V (Im U V A f) X -> - exists Y : _ | Approximant U A Y /\ Im U V Y f = X. + exists Y : _, Approximant U A Y /\ Im U V Y f = X. Proof. intros A f X H'; try assumption. cut - ( exists n : _ - | ( exists Y : _ | (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)). + (exists n : _, + (exists Y : _, (cardinal U Y n /\ Included U Y A) /\ Im U V Y f = X)). intro H'0; elim H'0; intros n E; elim E; clear H'0. intros x H'0; try assumption. elim H'0; intros H'1 H'2; elim H'1; intros H'3 H'4; try exact H'3; @@ -241,4 +241,4 @@ red in |- *; intro H'2. elim (Pigeonhole_bis A f); auto with sets. Qed. -End Infinite_sets.
\ No newline at end of file +End Infinite_sets. diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 7f8e1695a..c9121032d 100755 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -99,7 +99,7 @@ Hint Resolve le_total_order. Lemma Finite_subset_has_lub : forall X:Ensemble nat, - Finite nat X -> exists m : nat | Upper_Bound nat nat_po X m. + Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m. Proof. intros X H'; elim H'. exists 0. @@ -138,7 +138,7 @@ intros x1 H'1; elim H'1; auto with sets arith. Qed. Lemma Integers_has_no_ub : - ~ ( exists m : nat | Upper_Bound nat nat_po Integers m). + ~ (exists m : nat, Upper_Bound nat nat_po Integers m). Proof. red in |- *; intro H'; elim H'. intros x H'0. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 5ef6bc9b0..15fc690dd 100755 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -48,7 +48,7 @@ Definition Strict_Rel_of : Rel := fun x y:U => Rel_of p x y /\ x <> y. Inductive covers (y x:U) : Prop := Definition_of_covers : Strict_Rel_of x y -> - ~ ( exists z : _ | Strict_Rel_of x z /\ Strict_Rel_of z y) -> + ~ (exists z : _, Strict_Rel_of x z /\ Strict_Rel_of z y) -> covers y x. End Partial_orders. diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 988bbd25a..71ec5b078 100755 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -177,7 +177,7 @@ Qed. Lemma Included_Add : forall (X A:Ensemble U) (x:U), Included U X (Add U A x) -> - Included U X A \/ ( exists A' : _ | X = Add U A' x /\ Included U A' A). + Included U X A \/ (exists A' : _, X = Add U A' x /\ Included U A' A). Proof. intros X A x H'0; try assumption. elim (classic (In U X x)). @@ -267,7 +267,7 @@ Theorem covers_Add : Included U a A -> Included U a' A -> covers (Ensemble U) (Power_set_PO U A) a' a -> - exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x. + exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x. Proof. intros A a a' H' H'0 H'1; try assumption. elim (setcover_inv A a a'); auto with sets. @@ -299,7 +299,7 @@ Theorem covers_is_Add : Included U a A -> Included U a' A -> (covers (Ensemble U) (Power_set_PO U A) a' a <-> - ( exists x : _ | a' = Add U a x /\ In U A x /\ ~ In U a x)). + (exists x : _, a' = Add U a x /\ In U A x /\ ~ In U a x)). Proof. intros A a a' H' H'0; split; intro K. apply covers_Add with (A := A); auto with sets. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index c587744a3..91018f05e 100755 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -254,7 +254,7 @@ Qed. Lemma setcover_intro : forall (U:Type) (A x y:Ensemble U), Strict_Included U x y -> - ~ ( exists z : _ | Strict_Included U x z /\ Strict_Included U z y) -> + ~ (exists z : _, Strict_Included U x z /\ Strict_Included U z y) -> covers (Ensemble U) (Power_set_PO U A) y x. Proof. intros; apply Definition_of_covers; auto with sets. diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index 4fda8d8e9..2a0aaf98b 100755 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -67,7 +67,7 @@ Qed. Theorem Rstar_cases : forall (U:Type) (R:Relation U) (x y:U), - Rstar U R x y -> x = y \/ ( exists u : _ | R x u /\ Rstar U R u y). + Rstar U R x y -> x = y \/ (exists u : _, R x u /\ Rstar U R u y). Proof. intros U R x y H'; elim H'; auto with sets. intros x0 y0 z H'0 H'1 H'2; right; exists y0; auto with sets. @@ -116,7 +116,7 @@ Qed. Theorem RstarRplus_RRstar : forall (U:Type) (R:Relation U) (x y z:U), - Rstar U R x y -> Rplus U R y z -> exists u : _ | R x u /\ Rstar U R u z. + Rstar U R x y -> Rplus U R y z -> exists u : _, R x u /\ Rstar U R u z. Proof. generalize Rstar_contains_Rplus; intro T; red in T. generalize Rstar_transitive; intro T1; red in T1. @@ -134,7 +134,7 @@ Theorem Lemma1 : Strongly_confluent U R -> forall x b:U, Rstar U R x b -> - forall a:U, R x a -> exists z : _ | Rstar U R a z /\ R b z. + forall a:U, R x a -> exists z : _, Rstar U R a z /\ R b z. Proof. intros U R H' x b H'0; elim H'0. intros x0 a H'1; exists a; auto with sets. diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 1fe689002..d84884d41 100755 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -34,7 +34,7 @@ Section Relations_3. Variable R : Relation U. Definition coherent (x y:U) : Prop := - exists z : _ | Rstar U R x z /\ Rstar U R y z. + exists z : _, Rstar U R x z /\ Rstar U R y z. Definition locally_confluent (x:U) : Prop := forall y z:U, R x y -> R x z -> coherent y z. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index 66a7f5b5b..b11c8c635 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -35,7 +35,7 @@ Section Inverse_Image. Variable F : A -> B -> Prop. Let RoF (x y:A) : Prop := - exists2 b : B | F x b & (forall c:B, F y c -> R b c). + exists2 b : B, F x b & (forall c:B, F y c -> R b c). Lemma Acc_inverse_rel : forall b:B, Acc R b -> forall x:A, F x b -> Acc RoF x. induction 1 as [x _ IHAcc]; intros x0 H2. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index e8203c399..3daf09a97 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -54,7 +54,7 @@ Qed. Lemma right_prefix : forall x y z:List, - ltl x (y ++ z) -> ltl x y \/ ( exists y' : List | x = y ++ y' /\ ltl y' z). + ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z). Proof. intros x y; generalize x. elim y; simpl in |- *. @@ -371,4 +371,4 @@ Proof. Qed. -End Wf_Lexicographic_Exponentiation.
\ No newline at end of file +End Wf_Lexicographic_Exponentiation. diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index d7f241dd0..6a6a9882f 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -26,7 +26,7 @@ Remark strip_commut : commut A R1 R2 -> forall x y:A, clos_trans A R1 y x -> - forall z:A, R2 z y -> exists2 y' : A | R2 y' x & clos_trans A R1 z y'. + forall z:A, R2 z y -> exists2 y' : A, R2 y' x & clos_trans A R1 z y'. Proof. induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros. elim H with y x z; auto with sets; intros x0 H2 H3. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 4c2efceb1..1b1cf27d2 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -35,7 +35,7 @@ Open Local Scope Z_scope. Then the diagram will be closed and the theorem proved. *) Lemma Z_of_nat_complete : - forall x:Z, 0 <= x -> exists n : nat | x = Z_of_nat n. + forall x:Z, 0 <= x -> exists n : nat, x = Z_of_nat n. intro x; destruct x; intros; [ exists 0%nat; auto with arith | specialize (ZL4 p); intros Hp; elim Hp; intros; exists (S x); intros; diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index f7015089c..d11242c85 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -93,7 +93,7 @@ Hint Local Resolve Pcompare_refl. (** Comparison first-order specification *) Lemma Zcompare_Gt_spec : - forall n m:Z, (n ?= m) = Gt -> exists h : positive | n + - m = Zpos h. + forall n m:Z, (n ?= m) = Gt -> exists h : positive, n + - m = Zpos h. Proof. intros x y; case x; case y; [ simpl in |- *; intros H; discriminate H diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index ba6d21c4d..30065d705 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -236,7 +236,7 @@ Fixpoint Is_power (p:positive) : Prop := end. Lemma Is_power_correct : - forall p:positive, Is_power p <-> ( exists y : nat | p = shift_nat y 1). + forall p:positive, Is_power p <-> (exists y : nat, p = shift_nat y 1). split; [ elim p; diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index d9bc4d1b2..a0027efb3 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -97,7 +97,7 @@ intros x y H; rewrite H; trivial with arith. Qed. Theorem intro_Z : - forall n:nat, exists y : Z | Z_of_nat n = y /\ 0 <= y * 1 + 0. + forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. Proof. intros x; exists (Z_of_nat x); split; [ trivial with arith diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index f56005080..ede579586 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -17,7 +17,7 @@ Open Local Scope Z_scope. (** Definition and properties of square root on Z *) (** The following tactic replaces all instances of (POS (xI ...)) by - `2*(POS ...)+1` , but only when ... is not made only with xO, XI, or xH. *) + `2*(POS ...)+1`, but only when ... is not made only with xO, XI, or xH. *) Ltac compute_POS := match goal with | |- context [(Zpos (xI ?X1))] => |