Révision de theories/Logic concernant les axiomes de descriptions.

Mise à jour du tableau des axiomes dans la FAQ.



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

14 files changed, 358 insertions, 84 deletions

diff --git a/CHANGES b/CHANGES
index f13e1b8311..018cfce023 100644
--- a/CHANGES
+++ b/CHANGES
@@ -37,8 +37,9 @@ Libraries
 - Loading FSets/FMap used to open unwanted scopes of integer datatypes 
   (see bug #1347). These scopes may need to be opened manually now.
 - Few changes in Reals (lemmas on prod_f_SO now on prod_f_R0).
-- Slight restructuration and extension of the Logic library regarding choice
-  and classical logic.
+- Slight restructuration of the Logic library regarding choice and classical
+  logic. Addition of files providing intuitionistic axiomatizations of
+  descriptions: Epsilon.v, Description.v and IndefiniteDescription.v
 
 Language
 
diff --git a/Makefile.common b/Makefile.common
index 7d2aef090b..ba790f62b6 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -478,7 +478,8 @@ LOGICVO:=\
  theories/Logic/EqdepFacts.vo         theories/Logic/ProofIrrelevanceFacts.vo \
  theories/Logic/ClassicalEpsilon.vo   theories/Logic/ClassicalUniqueChoice.vo \
  theories/Logic/DecidableType.vo      theories/Logic/DecidableTypeEx.vo \
- theories/Logic/ConstructiveEpsilon.vo
+ theories/Logic/Epsilon.vo            theories/Logic/ConstructiveEpsilon.vo \
+ theories/Logic/Description.vo        theories/Logic/IndefiniteDescription.vo
 
 ARITHVO:=\
  theories/Arith/Arith.vo        theories/Arith/Gt.vo          \
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 7355838a5d..46351e23df 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -478,8 +478,9 @@ equations have to be treated by hand or using specialised tactics.
 \Question{What axioms can be safely added to {\Coq}?}
 
 There are a few typical useful axioms that are independent from the
-Calculus of Inductive Constructions and that can be safely added to
-{\Coq}. These axioms are stated in the directory {\tt Logic} of the
+Calculus of Inductive Constructions and that are considered consistent with
+the theory of {\Coq}.
+Most of these axioms are stated in the directory {\tt Logic} of the
 standard library of {\Coq}. The most interesting ones are
 
 \begin{itemize}
@@ -487,6 +488,8 @@ standard library of {\Coq}. The most interesting ones are
 \item Proof-irrelevance: $\forall A:Prop \forall p_1 p_2:A, p_1=p_2$
 \item Unicity of equality proofs (or equivalently Streicher's axiom $K$):
 $\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$
+\item Hilbert's $\epsilon$ operator: if $A \neq \emptyset$, then there is $\epsilon_P$ such that $\exists x P(x) \rightarrow P(\epsilon_P)$
+\item Church's $\iota$ operator: if $A \neq \emptyset$, then there is $\iota_P$ such that $\exists! x P(x) \rightarrow P(\iota_P)$
 \item The axiom of unique choice: $\forall x \exists! y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$
 \item The functional axiom of choice: $\forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$
 \item Extensionality of predicates: $\forall P Q:A\rightarrow Prop, (\forall x, P(x) \leftrightarrow Q(x)) \rightarrow P=Q$
diff --git a/doc/faq/axioms.fig b/doc/faq/axioms.fig
index f07759302f..78e448865f 100644
--- a/doc/faq/axioms.fig
+++ b/doc/faq/axioms.fig
@@ -7,78 +7,131 @@ Letter
 Single
 -2
 1200 2
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600
+5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 14032.500 7222.500 4725 3825 4425 4800 4200 6000
 	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 8925.000 3600 9075 3450 8925 3600 8775
 	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6150.000 3600 6300 3450 6150 3600 6000
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 0 1 3600.000 8625.000 3600 8775 3450 8625 3600 8475
 	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8325.000 3600 8475 3450 8325 3600 8175
 	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6450.000 3600 6600 3450 6450 3600 6300
 	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8625.000 3600 8775 3450 8625 3600 8475
 	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 6750.000 3600 6900 3450 6750 3600 6600
 	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 8925.000 3600 9075 3450 8925 3600 8775
 	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 7050.000 3600 7200 3450 7050 3600 6900
 	1 1 1.00 60.00 120.00
+5 1 0 1 0 7 50 -1 -1 0.000 0 0 1 1 3600.000 9225.000 3600 9375 3450 9225 3600 9075
 	1 1 1.00 60.00 120.00
-5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 14032.500 5272.500 4725 1875 4425 2850 4200 4050
 	1 1 1.00 60.00 120.00
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+5 1 0 1 0 7 50 -1 -1 0.000 0 1 1 0 6309.515 5767.724 4200 3825 3450 5550 3825 7200
 	1 1 1.00 60.00 120.00
-	 4200 5175 4200 5775
+6 2025 300 7725 525
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
+	 7725 525 2025 525
+4 0 0 50 -1 0 12 0.0000 4 180 5700 2025 450 The dependency graph of axioms in the Calculus of Inductive Constructions\001
+-6
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
-	 7050 5175 4575 5775
+	 4200 6225 4200 7200
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
-	 4200 4275 4200 4875
+	 7725 3900 7200 6000
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
-	 4950 4275 7125 4875
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	 7200 6225 7200 7050
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
 	1 1 1.00 60.00 120.00
-	 7725 1950 7200 4050
+	1 1 1.00 60.00 120.00
+	 5550 5625 5550 6000
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 4350 3075 7350 1950
+	 4575 6000 6450 6000
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
+	1 1 1.00 60.00 120.00
+	1 1 1.00 60.00 120.00
+	 3375 3225 3375 3600
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
-	 7200 4275 7200 4875
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 3075 1875 3975 1875
+	 3373 1950 3376 2250
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
 	1 1 1.00 60.00 120.00
 	1 1 1.00 60.00 120.00
-	 5550 3675 5550 4050
+	 3375 2625 3375 3000
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 4575 4050 6450 4050
-2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
+	 2175 3600 3750 3600
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 3075 2475 2475 2475
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 3374 1125 3377 1425
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
+	 1049 1950 1052 2250
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
-	 3525 1875 3525 2250
+	 1048 1125 1051 1425
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
 	1 1 1.00 60.00 120.00
-	 2325 1875 2250 3975
+	 3075 975 1575 975
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 3075 1725 2025 1725
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 4
+	 8025 5925 8250 5925 9000 4950 9150 4950
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 8625 5400 8250 3900
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 7050 7350 4575 7950
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 4200 7500 4200 7950
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 4714 6255 7039 7080
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 0 2
+	1 1 1.00 60.00 120.00
+	 1500 3900 2175 6000
+2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 1 1 2
+	1 1 1.00 60.00 120.00
+	1 1 1.00 60.00 120.00
+	 1139 2771 1364 3521
 2 1 0 1 0 7 50 -1 -1 0.000 0 0 -1 0 0 2
-	 7800 1275 2100 1275
-4 0 0 50 -1 0 12 0.0000 4 135 1305 6600 5100 Proof-irrelevance\001
-4 0 0 50 -1 0 12 0.0000 4 135 1260 3675 4200 Excluded-middle\001
-4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 1800 Predicate extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 180 1050 3375 3525 (Diaconescu)\001
-4 0 0 50 -1 0 12 0.0000 4 180 1905 4650 3600 Propositional degeneracy\001
-4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 1800 Relational choice axiom\001
-4 0 0 50 -1 0 12 0.0000 4 180 1575 1725 1800 Description principle\001
-4 0 0 50 -1 0 12 0.0000 4 135 1830 2550 2400 Functional choice axiom\001
-4 0 0 50 -1 0 12 0.0000 4 195 2340 3600 5100 Decidability of equality on $A$\001
-4 0 0 50 -1 0 12 0.0000 4 180 2175 4425 4575 (needs Prop-impredicativity)\001
-4 0 0 50 -1 0 12 0.0000 4 180 705 5025 4725 (Berardi)\001
-4 0 0 50 -1 0 12 0.0000 4 180 1620 1500 3075 (if Set impredicative)\001
-4 0 0 50 -1 0 12 0.0000 4 135 1560 1500 4200 Not excluded-middle\001
-4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 6000 Axiom K on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 7200 Invariance by substitution of reflexivity proofs for equality on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 4200 Propositional extensionality\001
-4 0 0 50 -1 0 12 0.0000 4 180 5700 2100 1200 The dependency graph of axioms in the Calculus of Inductive Constructions\001
-4 0 0 50 -1 0 12 0.0000 4 180 3210 3600 6900 Injectivity of equality on sigma-types on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 6300 Uniqueness of reflexivity proofs for equality on A\001
-4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 6600 Uniqueness of equality proofs on A\001
+	 4425 4875 7350 3825
+3 0 0 1 0 7 50 -1 -1 0.000 0 0 0 4
+	 6450 7050 4050 6675 3750 6825 3750 7050
+	 0.000 1.000 1.000 0.000
+4 0 0 50 -1 0 12 0.0000 4 180 1830 6900 3750 Predicate extensionality\001
+4 0 0 50 -1 0 12 0.0000 4 135 1800 3825 3750 Relational choice axiom\001
+4 0 0 50 -1 0 12 0.0000 4 180 2100 6150 6150 Propositional extensionality\001
+4 0 0 50 -1 0 12 0.0000 4 180 1005 450 1050 Operator iota\001
+4 0 0 50 -1 2 12 0.0000 4 135 1020 450 1650 Constructive\001
+4 0 0 50 -1 2 12 0.0000 4 180 1530 450 1875 definite description\001
+4 0 0 50 -1 2 12 0.0000 4 180 2010 9000 5175 Functional extensionality\001
+4 0 0 50 -1 0 12 0.0000 4 180 4740 150 10050 Statements in boldface are the most "interesting" ones for Coq\001
+4 0 0 50 -1 0 12 0.0000 4 180 4800 3600 9375 Invariance by substitution of reflexivity proofs for equality on A\001
+4 0 0 50 -1 0 12 0.0000 4 180 3735 3600 8475 Uniqueness of reflexivity proofs for equality on A\001
+4 0 0 50 -1 0 12 0.0000 4 180 2670 3600 8775 Uniqueness of equality proofs on A\001
+4 0 0 50 -1 0 12 0.0000 4 135 1080 3600 8175 Axiom K on A\001
+4 0 0 50 -1 2 12 0.0000 4 135 1455 6450 7275 Proof-irrelevance\001
+4 0 0 50 -1 2 12 0.0000 4 180 3360 3600 9075 Injectivity of equality on Sigma-types on A\001
+4 0 0 50 -1 0 12 0.0000 4 180 2175 4950 6525 (needs Prop-impredicativity)\001
+4 0 0 50 -1 0 12 0.0000 4 180 705 6000 6750 (Berardi)\001
+4 0 0 50 -1 2 12 0.0000 4 135 1290 3675 6225 Excluded-middle\001
+4 0 0 50 -1 0 12 0.0000 4 180 1905 4950 5550 Propositional degeneracy\001
+4 0 0 50 -1 0 12 0.0000 4 180 1050 3750 5250 (Diaconescu)\001
+4 0 0 50 -1 0 12 0.0000 4 180 2475 3375 7425 Decidability of equality on any A\001
+4 0 0 50 -1 0 12 0.0000 4 180 1620 1275 5025 (if Set impredicative)\001
+4 0 0 50 -1 0 12 0.0000 4 135 1560 1575 6225 Not excluded-middle\001
+4 0 0 50 -1 0 12 0.0000 4 180 1770 450 2625 in propositional context\001
+4 0 0 50 -1 2 12 0.0000 4 135 1020 3150 1650 Constructive\001
+4 0 0 50 -1 2 12 0.0000 4 180 1665 3150 1875 indefinite description\001
+4 0 0 50 -1 0 12 0.0000 4 180 2610 3150 2400 Constructive indefinite description\001
+4 0 0 50 -1 0 12 0.0000 4 180 1770 3150 2625 in propositional context\001
+4 0 0 50 -1 2 12 0.0000 4 135 1935 3150 3150 Functional choice axiom\001
+4 0 0 50 -1 0 12 0.0000 4 135 2100 450 2400 Constructive definite descr.\001
+4 0 0 50 -1 2 12 0.0000 4 180 1845 450 3750 Axiom of unique choice\001
+4 0 0 50 -1 2 12 0.0000 4 180 1365 3150 1050 Operator epsilon\001
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 8deb362cd9..f38a651d04 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -314,8 +314,22 @@ Proof.
   auto.
 Qed.
 
-(** Being inhabited *)
+(** * Being inhabited *)
+
+(** The predicate [inhabited] can be used in different contexts. If [A] is
+    thought as a type, [inhabited A] states that [A] is inhabited. If [A] is
+    thought as a computationally relevant proposition, then 
+    [inhabited A] weakens [A] so as to hide its computational meaning.
+    The so-weakened proof remains computationally relevant but only in
+    a propositional context.
+*)
 
 Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.
 
 Hint Resolve inhabits: core.
+
+Lemma exists_inhabited : forall (A:Type) (P:A->Prop), 
+  (exists x, P x) -> inhabited A.
+Proof.
+  destruct 1; auto.
+Qed.
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index f418f2d14d..20fc0ec804 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -1,4 +1,3 @@
-(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -60,17 +59,19 @@ Table of contents
 
 2. IPL_2^2 |- AC_rel + AC! = AC_fun
 
-3. typed IPL_2 + Sigma-types + PI |- AC_rel = GAC_rel  and  IPL_2 |- AC_rel + IGP -> GAC_rel and IPL_2 |- GAC_rel = OAC_rel
+3.1. typed IPL_2 + Sigma-types + PI |- AC_rel = GAC_rel  and  IPL_2 |- AC_rel + IGP -> GAC_rel and IPL_2 |- GAC_rel = OAC_rel
 
-4. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker
+3.2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker
 
-5. Derivability of choice for decidable relations with well-ordered codomain
+3.3. D_iota -> ID_iota  and  D_epsilon <-> ID_epsilon + Drinker
 
-6. Equivalence of choices on dependent or non dependent functional types
+4. Derivability of choice for decidable relations with well-ordered codomain
 
-7. Non contradiction of constructive descriptions wrt functional choices
+5. Equivalence of choices on dependent or non dependent functional types
 
-8. Definite description transports classical logic to the computational world
+6. Non contradiction of constructive descriptions wrt functional choices
+
+7. Definite description transports classical logic to the computational world
 
 References:
 
@@ -86,8 +87,6 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005.
 
 Set Implicit Arguments.
 
-Notation Local "'inhabited' A" := A (at level 10, only parsing).
-
 (**********************************************************************)
 (** * Definitions *)
 
@@ -185,15 +184,15 @@ Definition OmniscientFunctionalChoice_on :=
 
 (** D_epsilon *)
 
-Definition ClassicalIndefiniteDescription := 
+Definition EpsilonStatement_on := 
   forall P:A->Prop,
-    A -> { x:A | (exists x, P x) -> P x }.
+    inhabited A -> { x:A | (exists x, P x) -> P x }.
 
 (** D_iota *)
 
-Definition ClassicalDefiniteDescription := 
+Definition IotaStatement_on := 
   forall P:A->Prop,
-    A -> { x:A | (exists! x, P x) -> P x }.
+    inhabited A -> { x:A | (exists! x, P x) -> P x }.
 
 End ChoiceSchemes.
 
@@ -225,6 +224,11 @@ Notation ConstructiveDefiniteDescription :=
 Notation ConstructiveIndefiniteDescription := 
   (forall A, ConstructiveIndefiniteDescription_on A).
 
+Notation IotaStatement := 
+  (forall A, IotaStatement_on A).
+Notation EpsilonStatement := 
+  (forall A, EpsilonStatement_on A).
+
 (** Subclassical schemes *)
 
 Definition ProofIrrelevance :=
@@ -240,16 +244,17 @@ Definition SmallDrinker'sParadox :=
     exists x, (exists x, P x) -> P x.
 
 (**********************************************************************)
-(** * AC_rel + PDP = AC_fun
+(** * AC_rel + AC! = AC_fun
 
    We show that the functional formulation of the axiom of Choice
    (usual formulation in type theory) is equivalent to its relational
-   formulation (only formulation of set theory) + the axiom of
-   (parametric) definite description (aka axiom of unique choice) *)
+   formulation (only formulation of set theory) + functional relation
+   reification (aka axiom of unique choice, or, principle of (parametric)
+   definite descriptions) *)
 
 (** This shows that the axiom of choice can be assumed (under its
    relational formulation) without known inconsistency with classical logic,
-   though definite description conflicts with classical logic *)
+   though functional relation reification conflicts with classical logic *)
 
 Lemma description_rel_choice_imp_funct_choice :
   forall A B : Type,
@@ -303,11 +308,13 @@ Proof.
 Qed.
 
 (**********************************************************************)
-(** * Connection between the guarded, non guarded and descriptive choices and *)
+(** * Connection between the guarded, non guarded and omniscient choices *)
 
-(** We show that the guarded relational formulation of the axiom of Choice
-   comes from the non guarded formulation in presence either of the
-   independance of general premises or proof-irrelevance *)
+(** We show that the guarded formulations of the axiom of choice
+   are equivalent to their "omniscient" variant and comes from the non guarded
+   formulation in presence either of the independance of general premises 
+   or subset types (themselves derivable from subtypes thanks to proof-
+   irrelevance) *)
 
 (**********************************************************************)
 (** ** AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *)
@@ -388,6 +395,7 @@ Proof.
   exists (f tt); auto.
 Qed.
 
+
 Lemma guarded_fun_choice_imp_fun_choice :
   GuardedFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
 Proof.
@@ -474,6 +482,57 @@ Proof.
 Qed.
 
 (**********************************************************************)
+(** ** D_iota -> ID_iota  and  D_epsilon <-> ID_epsilon + Drinker *)
+
+(** D_iota -> ID_iota *)
+
+Lemma iota_imp_constructive_definite_description :
+  IotaStatement -> ConstructiveDefiniteDescription.
+Proof.
+  intros D_iota A P H.
+  destruct D_iota with (P:=P) as (x,H1).
+  destruct H; red in H; auto.
+  exists x; apply H1; assumption.
+Qed.
+
+(** ID_epsilon + Drinker <-> D_epsilon *)
+
+Lemma epsilon_imp_constructive_indefinite_description:
+  EpsilonStatement -> ConstructiveIndefiniteDescription.
+Proof.
+  intros D_epsilon A P H.
+  destruct D_epsilon with (P:=P) as (x,H1).
+  destruct H; auto.
+  exists x; apply H1; assumption.
+Qed.
+
+Lemma constructive_indefinite_description_and_small_drinker_imp_epsilon :
+  SmallDrinker'sParadox -> ConstructiveIndefiniteDescription ->
+  EpsilonStatement.
+Proof.
+  intros Drinkers D_epsilon A P Inh; 
+  apply D_epsilon; apply Drinkers; assumption.
+Qed.
+
+Lemma epsilon_imp_small_drinker :
+  EpsilonStatement -> SmallDrinker'sParadox.
+Proof.
+  intros D_epsilon A P Inh; edestruct D_epsilon; eauto.
+Qed.
+
+Theorem constructive_indefinite_description_and_small_drinker_iff_epsilon :
+  (SmallDrinker'sParadox * ConstructiveIndefiniteDescription ->
+  EpsilonStatement) *
+  (EpsilonStatement ->
+   SmallDrinker'sParadox * ConstructiveIndefiniteDescription).
+Proof.
+  auto decomp using
+    epsilon_imp_constructive_indefinite_description,
+    constructive_indefinite_description_and_small_drinker_imp_epsilon,
+    epsilon_imp_small_drinker.
+Qed.
+
+(**********************************************************************)
 (** * Derivability of choice for decidable relations with well-ordered codomain *)
 
 (** Countable codomains, such as [nat], can be equipped with a
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 51f1b3eff0..b0301994b6 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -8,9 +8,15 @@
 
 (*i $Id$ i*)
 
-(** This file provides classical logic, and functional choice *)
-
-(** This file extends ClassicalUniqueChoice.v with the axiom of choice.
+(** This file provides classical logic and functional choice; this
+    especially provides both indefinite descriptions and choice functions
+    but this is weaker than providing epsilon operator and classical logic
+    as the indefinite descriptions provided by the axiom of choice can
+    be used only in a propositional context (especially, they cannot
+    be used to build choice functions outside the scope of a theorem
+    proof) *)
+
+(** This file extends ClassicalUniqueChoice.v with full choice.
     As ClassicalUniqueChoice.v, it implies the double-negation of
     excluded-middle in [Set] and leads to a classical world populated
     with non computable functions. Especially it conflicts with the
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 51accc4ff8..aa65eb44c8 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -8,12 +8,13 @@
 
 (*i $Id$ i*)
 
-(** This file provides classical logic and definite description *)
+(** This file provides classical logic and definite description, which is
+    equivalent to providing classical logic and Church's iota operator *)
 
-(** Classical definite description operator (i.e. iota) implies
-    excluded-middle in [Set] and leads to a classical world populated
-    with non computable functions. It conflicts with the
-    impredicativity of [Set] *)
+(** Classical logic and definite descriptions implies excluded-middle
+    in [Set] and leads to a classical world populated with non
+    computable functions. It conflicts with the impredicativity of
+    [Set] *)
 
 Set Implicit Arguments.
 
diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
index 102edba5da..c45aeb6f91 100644
--- a/theories/Logic/ClassicalEpsilon.v
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -8,10 +8,10 @@
 
 (*i $Id$ i*)
 
-(** This file provides classical logic and indefinite description
-    (Hilbert's epsilon operator) *)
+(** This file provides classical logic and indefinite description under
+    the form of Hilbert's epsilon operator *)
 
-(** Classical epsilon's operator (i.e. indefinite description) implies
+(** Hilbert's epsilon operator and classical logic implies
     excluded-middle in [Set] and leads to a classical world populated
     with non computable functions. It conflicts with the
     impredicativity of [Set] *)
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index 1fb69d3d3d..2e739dd511 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -8,7 +8,11 @@
 
 (*i $Id$ i*)
 
-(** This file provides classical logic and unique choice *)
+(** This file provides classical logic and unique choice; this is
+    weaker than providing iota operator and classical logic as the
+    definite descriptions provided by the axiom of unique choice can
+    be used only in a propositional context (especially, they cannot
+    be used to build functions outside the scope of a theorem proof) *)
 
 (** Classical logic and unique choice, as shown in
     [ChicliPottierSimpson02], implies the double-negation of
diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v
new file mode 100644
index 0000000000..41cde8aa56
--- /dev/null
+++ b/theories/Logic/Description.v
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(** This file provides a constructive form of definite description; it
+    allows to build functions from the proof of their existence in any
+    context; this is weaker than Church's iota operator *)
+
+Require Import ChoiceFacts.
+
+Set Implicit Arguments.
+
+Axiom constructive_definite_description :
+  forall (A : Type) (P : A->Prop), 
+    (exists! x, P x) -> { x : A | P x }.
diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v
new file mode 100644
index 0000000000..ead91c9eca
--- /dev/null
+++ b/theories/Logic/Epsilon.v
@@ -0,0 +1,72 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(** This file provides indefinite description under the form of
+    Hilbert's epsilon operator; it does not assume classical logic. *)
+
+Require Import ChoiceFacts.
+
+Set Implicit Arguments.
+
+(** Hilbert's epsilon: operator and specification in one statement *)
+
+Axiom epsilon_statement : 
+  forall (A : Type) (P : A->Prop), inhabited A ->
+    { x : A | (exists x, P x) -> P x }.
+
+Lemma constructive_indefinite_description :
+  forall (A : Type) (P : A->Prop), 
+    (exists x, P x) -> { x : A | P x }.
+Proof.
+  apply epsilon_imp_constructive_indefinite_description.
+  exact epsilon_statement.
+Qed.
+
+Lemma small_drinkers'_paradox :
+  forall (A:Type) (P:A -> Prop), inhabited A ->
+    exists x, (exists x, P x) -> P x.
+Proof.
+  apply epsilon_imp_small_drinker.
+  exact epsilon_statement.
+Qed.
+
+Theorem iota_statement :
+  forall (A : Type) (P : A->Prop), inhabited A ->
+  { x : A | (exists! x : A, P x) -> P x }.
+Proof.
+  intros; destruct epsilon_statement with (P:=P); firstorder.
+Qed.
+
+Lemma constructive_definite_description :
+  forall (A : Type) (P : A->Prop), 
+    (exists! x, P x) -> { x : A | P x }.
+Proof.
+  apply iota_imp_constructive_definite_description.
+  exact iota_statement.
+Qed.
+
+(** Hilbert's epsilon operator and its specification *)
+
+Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A
+  := proj1_sig (epsilon_statement P i).
+
+Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : 
+  (exists x, P x) -> P (epsilon i P)
+  := proj2_sig (epsilon_statement P i).
+
+(** Church's iota operator and its specification *)
+
+Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A
+  := proj1_sig (iota_statement P i).
+
+Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : 
+  (exists! x:A, P x) -> P (iota i P)
+  := proj2_sig (iota_statement P i).
+
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 7627d2a6b2..7e02d06f33 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -270,7 +270,7 @@ Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2.
  
 
 (************************************************************************)
-(** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *)
+(** * Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *)
 
 Module Type EqdepElimination.
 
diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v
new file mode 100644
index 0000000000..ce9405f85a
--- /dev/null
+++ b/theories/Logic/IndefiniteDescription.v
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(** This file provides a constructive form of indefinite description that
+    allows to build choice functions; this is weaker than Hilbert's
+    epsilon operator (which implies weakly classical properties) but
+    stronger than the axiom of choice (which cannot be used outside
+    the context of a theorem proof). *)
+
+Require Import ChoiceFacts.
+
+Set Implicit Arguments.
+
+Axiom constructive_indefinite_description :
+  forall (A : Type) (P : A->Prop), 
+    (exists x, P x) -> { x : A | P x }.
+
+Lemma constructive_definite_description :
+  forall (A : Type) (P : A->Prop), 
+    (exists! x, P x) -> { x : A | P x }.
+Proof.
+  intros; apply constructive_indefinite_description; firstorder.
+Qed.
+
+Lemma functional_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)).
+Proof.
+  apply constructive_indefinite_descr_fun_choice.
+  exact constructive_indefinite_description.
+Qed.