Cleaning a little bit the files talking about descriptions: avoiding

same name for different statements as noticed by Adam Chlipala on
coq-club, avoiding stating the same axiom twice in distinct files.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14628 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 61 insertions, 38 deletions

diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 54e7bab88f..d35ed13899 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -16,14 +16,12 @@
 
 Set Implicit Arguments.
 
-Require Export Classical.
+Require Export Classical.   (* Axiomatize classical reasoning *)
+Require Export Description. (* Axiomatize constructive form of Church's iota *)
 Require Import ChoiceFacts.
 
 Notation Local inhabited A := A (only parsing).
 
-Axiom constructive_definite_description :
-  forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }.
-
 (** The idea for the following proof comes from [ChicliPottierSimpson02] *)
 
 Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 4839b6da23..8dd51482c5 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -8,17 +8,18 @@
 
 (*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*)
 
-(** This module proves the constructive description schema, which
-infers the sigma-existence (i.e., [Set]-existence) of a witness to a
-predicate from the regular existence (i.e., [Prop]-existence). One
-requires that the underlying set is countable and that the predicate
-is decidable. *)
+(** This provides with a proof of the constructive form of definite
+and indefinite descriptions for Sigma^0_1-formulas (hereafter called
+"small" formulas), which infers the sigma-existence (i.e.,
+[Type]-existence) of a witness to a decidable predicate over a
+countable domain from the regular existence (i.e.,
+[Prop]-existence). *)
 
 (** Coq does not allow case analysis on sort [Prop] when the goal is in
-[Set]. Therefore, one cannot eliminate [exists n, P n] in order to
+not in [Prop]. Therefore, one cannot eliminate [exists n, P n] in order to
 show [{n : nat | P n}]. However, one can perform a recursion on an
 inductive predicate in sort [Prop] so that the returning type of the
-recursion is in [Set]. This trick is described in Coq'Art book, Sect.
+recursion is in [Type]. This trick is described in Coq'Art book, Sect.
 14.2.3 and 15.4. In particular, this trick is used in the proof of
 [Fix_F] in the module Coq.Init.Wf. There, recursion is done on an
 inductive predicate [Acc] and the resulting type is in [Type].
@@ -39,7 +40,7 @@ For the first one we provide explicit and short proof terms. *)
 
 (* Direct version *)
 
-Section ConstructiveIndefiniteDescription_Direct.
+Section ConstructiveIndefiniteGroundDescription_Direct.
 
 Variable P : nat -> Prop.
 
@@ -77,11 +78,11 @@ Fixpoint linear_search m (b : before_witness m) : {n : nat | P n} :=
     | right no => linear_search (S m) (inv_before_witness m b no)
   end.
 
-Definition constructive_indefinite_description_nat :
+Definition constructive_indefinite_ground_description_nat :
   (exists n, P n) -> {n:nat | P n} :=
   fun e => linear_search O (let (n, p) := e in O_witness n (stop n p)).
 
-End ConstructiveIndefiniteDescription_Direct.
+End ConstructiveIndefiniteGroundDescription_Direct.
 
 (************************************************************************)
 
@@ -89,7 +90,7 @@ End ConstructiveIndefiniteDescription_Direct.
 
 Require Import Arith.
 
-Section ConstructiveIndefiniteDescription_Acc.
+Section ConstructiveIndefiniteGroundDescription_Acc.
 
 Variable P : nat -> Prop.
 
@@ -149,40 +150,40 @@ destruct (IH y Ryx) as [n Hn].
 exists n; assumption.
 Defined.
 
-Theorem constructive_indefinite_description_nat_Acc :
+Theorem constructive_indefinite_ground_description_nat_Acc :
   (exists n : nat, P n) -> {n : nat | P n}.
 Proof.
 intros H; apply acc_implies_P_eventually.
 apply P_eventually_implies_acc_ex; assumption.
 Defined.
 
-End ConstructiveIndefiniteDescription_Acc.
+End ConstructiveIndefiniteGroundDescription_Acc.
 
 (************************************************************************)
 
-Section ConstructiveEpsilon_nat.
+Section ConstructiveGroundEpsilon_nat.
 
 Variable P : nat -> Prop.
 
 Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}.
 
-Definition constructive_epsilon_nat (E : exists n : nat, P n) : nat
-  := proj1_sig (constructive_indefinite_description_nat P P_decidable E).
+Definition constructive_ground_epsilon_nat (E : exists n : nat, P n) : nat
+  := proj1_sig (constructive_indefinite_ground_description_nat P P_decidable E).
 
-Definition constructive_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_epsilon_nat E)
-  := proj2_sig (constructive_indefinite_description_nat P P_decidable E).
+Definition constructive_ground_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_ground_epsilon_nat E)
+  := proj2_sig (constructive_indefinite_ground_description_nat P P_decidable E).
 
-End ConstructiveEpsilon_nat.
+End ConstructiveGroundEpsilon_nat.
 
 (************************************************************************)
 
-Section ConstructiveEpsilon.
+Section ConstructiveGroundEpsilon.
 
 (** For the current purpose, we say that a set [A] is countable if
 there are functions [f : A -> nat] and [g : nat -> A] such that [g] is
 a left inverse of [f]. *)
 
-Variable A : Set.
+Variable A : Type.
 Variable f : A -> nat.
 Variable g : nat -> A.
 
@@ -199,24 +200,43 @@ Proof.
 intro n; unfold P'; destruct (P_decidable (g n)); auto.
 Defined.
 
-Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}.
+Lemma constructive_indefinite_ground_description : (exists x : A, P x) -> {x : A | P x}.
 Proof.
 intro H. assert (H1 : exists n : nat, P' n).
 destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption.
-apply (constructive_indefinite_description_nat P' P'_decidable)  in H1.
+apply (constructive_indefinite_ground_description_nat P' P'_decidable)  in H1.
 destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption.
 Defined.
 
-Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}.
+Lemma constructive_definite_ground_description : (exists! x : A, P x) -> {x : A | P x}.
 Proof.
-  intros; apply constructive_indefinite_description; firstorder.
+  intros; apply constructive_indefinite_ground_description; firstorder.
 Defined.
 
-Definition constructive_epsilon (E : exists x : A, P x) : A
-  := proj1_sig (constructive_indefinite_description E).
-
-Definition constructive_epsilon_spec (E : (exists x, P x)) : P (constructive_epsilon E)
-  := proj2_sig (constructive_indefinite_description E).
-
-End ConstructiveEpsilon.
-
+Definition constructive_ground_epsilon (E : exists x : A, P x) : A
+  := proj1_sig (constructive_indefinite_ground_description E).
+
+Definition constructive_ground_epsilon_spec (E : (exists x, P x)) : P (constructive_ground_epsilon E)
+  := proj2_sig (constructive_indefinite_ground_description E).
+
+End ConstructiveGroundEpsilon.
+
+(* begin hide *)
+(* Compatibility: the qualificative "ground" was absent from the initial
+names of the results in this file but this had introduced confusion
+with the similarly named statement in Description.v *)
+Notation constructive_indefinite_description_nat :=
+  constructive_indefinite_ground_description_nat (only parsing).
+Notation constructive_epsilon_spec_nat :=
+  constructive_ground_epsilon_spec_nat (only parsing).
+Notation constructive_epsilon_nat :=
+  constructive_ground_epsilon_nat (only parsing).
+Notation constructive_indefinite_description :=
+  constructive_indefinite_ground_description (only parsing).
+Notation constructive_definite_description :=
+  constructive_definite_ground_description (only parsing).
+Notation constructive_epsilon_spec :=
+  constructive_ground_epsilon_spec (only parsing).
+Notation constructive_epsilon :=
+  constructive_ground_epsilon (only parsing).
+(* end hide *)
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v
index 0b951ebcba..2237ea6efa 100644
--- a/theories/Reals/Rlogic.v
+++ b/theories/Reals/Rlogic.v
@@ -41,6 +41,7 @@ Variable P : nat -> Prop.
 Hypothesis HP : forall n, {P n} + {~P n}.
 
 Let ge_fun_sums_ge_lemma : (forall (m n : nat) (f : nat -> R), (lt m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
+Proof.
 intros m n f mn fpos.
 replace (sum_f_R0 f m) with (sum_f_R0 f m + 0) by ring.
 rewrite (tech2 f m n mn).
@@ -52,6 +53,7 @@ apply (Rplus_le_compat _ _ _ _ IHn0 (fpos (S (m + S n0)%nat))).
 Qed.
 
 Let ge_fun_sums_ge : (forall (m n : nat) (f : nat -> R), (le m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n).
+Proof.
 intros m n f mn pos.
  elim (le_lt_or_eq _ _ mn).
  intro; apply ge_fun_sums_ge_lemma; assumption.
@@ -61,6 +63,7 @@ Qed.
 Let f:=fun n => (if HP n then (1/2)^n else 0)%R.
 
 Lemma cauchy_crit_geometric_dec_fun : Cauchy_crit_series f.
+Proof.
 intros e He.
 assert (X:(Pser (fun n:nat => 1) (1/2) (/ (1 - (1/2))))%R).
  apply GP_infinite.
@@ -233,10 +236,11 @@ fourier.
 Qed.
 
 Lemma sig_forall_dec :  {n | ~P n}+{forall n, P n}.
+Proof.
 destruct forall_dec.
  right; assumption.
 left.
-apply constructive_indefinite_description_nat; auto.
+apply constructive_indefinite_ground_description_nat; auto.
  clear - HP.
  firstorder.
 apply Classical_Pred_Type.not_all_ex_not.
@@ -255,6 +259,7 @@ principle also derive [up] and its [specification] *)
 
 Theorem not_not_archimedean :
   forall r : R, ~ (forall n : nat, (INR n <= r)%R).
+Proof.
 intros r H.
 set (E := fun r => exists n : nat, r = INR n).
 assert (exists x : R, E x) by