Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

11 files changed, 1289 insertions, 211 deletions

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index bc892ca9..e0be9ed3 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,155 +7,453 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ChoiceFacts.v 8132 2006-03-05 10:59:47Z herbelin $ i*)
+(*i $Id: ChoiceFacts.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
 
-(** 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) *)
+(** ** Some facts and definitions concerning choice and description in
+       intuitionistic logic.
 
-(** 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 *)
+We investigate the relations between the following choice and
+description principles
+
+- AC_rel  = relational form of the (non extensional) axiom of choice
+            (a "set-theoretic" axiom of choice)
+- AC_fun  = functional form of the (non extensional) axiom of choice
+            (a "type-theoretic" axiom of choice)
+- AC!     = functional relation reification
+            (known as axiom of unique choice in topos theory,
+             sometimes called principle of definite description in 
+             the context of constructive type theory)
+
+- GAC_rel = guarded relational form of the (non extensional) axiom of choice
+- GAC_fun = guarded functional form of the (non extensional) axiom of choice
+- GAC!    = guarded functional relation reification
+
+- OAC_rel = "omniscient" relational form of the (non extensional) axiom of choice
+- OAC_fun = "omniscient" functional form of the (non extensional) axiom of choice
+            (called AC* in Bell [Bell])
+- OAC!
+
+- ID_iota    = intuitionistic definite description
+- ID_epsilon = intuitionistic indefinite description
+
+- D_iota     = (weakly classical) definite description principle
+- D_epsilon  = (weakly classical) indefinite description principle
+
+- PI      = proof irrelevance
+- IGP     = independence of general premises
+            (an unconstrained generalisation of the constructive principle of
+             independence of premises)
+- Drinker = drinker's paradox (small form)
+            (called Ex in Bell [Bell])  
+
+We let also
+
+IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal predicate logic
+IPL_2   = 2nd-order impredicative minimal predicate logic
+IPL^2   = 2nd-order functional minimal predicate logic (with ex. quant.)
+
+Table of contents
+
+A. Definitions
+
+B. IPL_2^2 |- AC_rel + AC! = AC_fun
+
+C. 1. AC_rel + PI -> GAC_rel  and  PL_2 |- AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel
+
+C. 2. IPL^2 |- AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker
+
+D. Derivability of choice for decidable relations with well-ordered codomain
+
+E. Equivalence of choices on dependent or non dependent functional types
+
+F. Non contradiction of constructive descriptions wrt functional choices
+
+G. Definite description transports classical logic to the computational world
 
-Section ChoiceEquivalences.
+References:
+
+[Bell] John L. Bell, Choice principles in intuitionistic set theory,
+unpublished.
+
+[Bell93] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic
+Type Theories, Mathematical Logic Quarterly, volume 39, 1993.
+
+[Carlstrøm05] Jesper Carlstrøm, Interpreting descriptions in
+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).
+
+(**********************************************************************)
+(** *** A. Definitions *)
+
+(** Choice, reification and description schemes *)
+
+Section ChoiceSchemes.
 
 Variables A B :Type.
 
-Definition RelationalChoice :=
-  forall (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')).
+Variables P:A->Prop.
+
+Variables R:A->B->Prop.
+
+(** **** Constructive choice and description *)
+
+(** AC_rel *)
+
+Definition RelationalChoice_on :=
+  forall R:A->B->Prop,
+  (forall x : A, exists y : B, R x y) ->
+  (exists R' : A->B->Prop, subrelation R' R /\ forall x, exists! y, R' x y).
+
+(** AC_fun *)
+
+Definition FunctionalChoice_on :=
+  forall R:A->B->Prop,
+  (forall x : A, exists y : B, R x y) ->
+  (exists f : A->B, forall x : A, R x (f x)).
+
+(** AC! or Functional Relation Reification (known as Axiom of Unique Choice
+    in topos theory; also called principle of definite description *)
+
+Definition FunctionalRelReification_on :=
+  forall R:A->B->Prop,
+  (forall x : A, exists! y : B, R x y) ->
+  (exists f : A->B, forall x : A, R x (f x)).
+
+(** ID_epsilon (constructive version of indefinite description;
+    combined with proof-irrelevance, it may be connected to
+    Carlstrøm's type theory with a constructive indefinite description
+    operator) *)
+
+Definition ConstructiveIndefiniteDescription_on :=
+  forall P:A->Prop,
+  (exists x, P x) -> { x:A | P x }.
+
+(** ID_iota (constructive version of definite description; combined
+    with proof-irrelevance, it may be connected to Carlstrøm's and
+    Stenlund's type theory with a constructive definite description
+    operator) *)
+
+Definition ConstructiveDefiniteDescription_on :=
+  forall P:A->Prop,
+  (exists! x, P x) -> { x:A | P x }.
+
+(** **** Weakly classical choice and description *)
 
-Definition FunctionalChoice :=
-  forall (R:A -> B -> Prop),
-    (forall x:A, exists y : B, R x y) ->
-     exists f : A -> B, (forall x:A, R x (f x)).
+(** GAC_rel *)
 
-Definition ParamDefiniteDescription :=
-  forall (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)).
+Definition GuardedRelationalChoice_on := 
+  forall P : A->Prop, forall R : A->B->Prop,
+  (forall x : A, P x -> exists y : B, R x y) ->
+  (exists R' : A->B->Prop, 
+     subrelation R' R /\ forall x, P x -> exists! y, R' x y).
+
+(** GAC_fun *)
+
+Definition GuardedFunctionalChoice_on := 
+  forall P : A->Prop, forall R : A->B->Prop, 
+  inhabited B ->
+  (forall x : A, P x -> exists y : B, R x y) ->
+  (exists f : A->B, forall x, P x -> R x (f x)).
+
+(** GFR_fun *)
+
+Definition GuardedFunctionalRelReification_on :=
+  forall P : A->Prop, forall R : A->B->Prop, 
+  inhabited B ->
+  (forall x : A, P x -> exists! y : B, R x y) ->
+  (exists f : A->B, forall x : A, P x -> R x (f x)).
+
+(** OAC_rel *)
+
+Definition OmniscientRelationalChoice_on := 
+  forall R : A->B->Prop,
+  exists R' : A->B->Prop, 
+    subrelation R' R /\ forall x : A, (exists y : B, R x y) -> exists! y, R' x y.
+
+(** OAC_fun *)
+
+Definition OmniscientFunctionalChoice_on := 
+  forall R : A->B->Prop, 
+  inhabited B ->
+  exists f : A->B, forall x : A, (exists y : B, R x y) -> R x (f x).
+
+(** D_epsilon *)
+
+Definition ClassicalIndefiniteDescription := 
+  forall P:A->Prop,
+  A -> { x:A | (exists x, P x) -> P x }.
+
+(** D_iota *)
+
+Definition ClassicalDefiniteDescription := 
+  forall P:A->Prop,
+  A -> { x:A | (exists! x, P x) -> P x }.
+
+End ChoiceSchemes.
+
+(** Generalized schemes *)
+
+Notation RelationalChoice :=
+  (forall A B, RelationalChoice_on A B).
+Notation FunctionalChoice :=
+  (forall A B, FunctionalChoice_on A B).
+Notation FunctionalChoiceOnInhabitedSet :=
+  (forall A B, inhabited B -> FunctionalChoice_on A B).
+Notation FunctionalRelReification :=
+  (forall A B, FunctionalRelReification_on A B).
+
+Notation GuardedRelationalChoice := 
+  (forall A B, GuardedRelationalChoice_on A B).
+Notation GuardedFunctionalChoice :=
+  (forall A B, GuardedFunctionalChoice_on A B).
+Notation GuardedFunctionalRelReification :=
+  (forall A B, GuardedFunctionalRelReification_on A B).
+
+Notation OmniscientRelationalChoice :=
+  (forall A B, OmniscientRelationalChoice_on A B).
+Notation OmniscientFunctionalChoice :=
+  (forall A B, OmniscientFunctionalChoice_on A B).
+
+Notation ConstructiveDefiniteDescription := 
+  (forall A, ConstructiveDefiniteDescription_on A).
+Notation ConstructiveIndefiniteDescription := 
+  (forall A, ConstructiveIndefiniteDescription_on A).
+
+(** Subclassical schemes *)
+
+Definition ProofIrrelevance :=
+  forall (A:Prop) (a1 a2:A), a1 = a2.
+
+Definition IndependenceOfGeneralPremises :=
+  forall (A:Type) (P:A -> Prop) (Q:Prop), 
+    inhabited A ->
+    (Q -> exists x, P x) -> exists x, Q -> P x.
+
+Definition SmallDrinker'sParadox :=
+  forall (A:Type) (P:A -> Prop), inhabited A ->
+  exists x, (exists x, P x) -> P x.
+
+(**********************************************************************)
+(** *** B. AC_rel + PDP = 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) *)
+
+(** 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 *)
 
 Lemma description_rel_choice_imp_funct_choice :
- ParamDefiniteDescription -> RelationalChoice -> FunctionalChoice.
-intros Descr RelCh.
-red in |- *; intros R H.
-destruct (RelCh R H) as [R' H0].
-destruct (Descr R') as [f H1].
-intro x.
-elim (H0 x); intros y [H2 [H3 H4]]; exists y; split; [ exact H3 | exact H4 ].
+  forall A B : Type,
+  FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B.
+Proof.
+intros A B Descr RelCh R H.
+destruct (RelCh R H) as (R',(HR'R,H0)).
+destruct (Descr R') as (f,Hf).
+firstorder.
 exists f; intro x.
-elim (H0 x); intros y [H2 [H3 H4]].
-rewrite <- (H4 (f x) (H1 x)).
-exact H2.
+destruct (H0 x) as (y,(HR'xy,Huniq)).
+rewrite <- (Huniq (f x) (Hf x)).
+apply HR'R; assumption.
 Qed.
 
-Lemma funct_choice_imp_rel_choice : FunctionalChoice -> RelationalChoice.
-intros FunCh.
-red in |- *; intros R H.
-destruct (FunCh R H) as [f H0].
-exists (fun x y => y = f x).
-intro x; exists (f x); split;
- [ apply H0
- | split; [ reflexivity | intros y H1; symmetry  in |- *; exact H1 ] ].
+Lemma funct_choice_imp_rel_choice : 
+  forall A B, FunctionalChoice_on A B -> RelationalChoice_on A B.
+Proof.
+intros A B FunCh R H.
+destruct (FunCh R H) as (f,H0).
+exists (fun x y => f x = y).
+split.
+  intros x y Heq; rewrite <- Heq; trivial.
+  intro x; exists (f x); split.
+    reflexivity.
+    trivial.
 Qed.
 
-Lemma funct_choice_imp_description :
- FunctionalChoice -> ParamDefiniteDescription.
-intros FunCh.
-red in |- *; intros R H.
+Lemma funct_choice_imp_description : 
+  forall A B, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
+Proof.
+intros A B FunCh R H.
 destruct (FunCh R) as [f H0].
 (* 1 *)
 intro x.
-elim (H x); intros y [H0 H1].
-exists y; exact H0.
+destruct (H x) as (y,(HRxy,_)).
+exists y; exact HRxy.
 (* 2 *)
 exists f; exact H0.
 Qed.
 
 Theorem FunChoice_Equiv_RelChoice_and_ParamDefinDescr :
- FunctionalChoice <-> RelationalChoice /\ ParamDefiniteDescription.
-split.
+  forall A B, FunctionalChoice_on A B <-> 
+    RelationalChoice_on A B /\ FunctionalRelReification_on A B.
+Proof.
+intros A B; split.
 intro H; split;
  [ exact (funct_choice_imp_rel_choice H)
  | exact (funct_choice_imp_description H) ].
 intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H).
 Qed.
 
-End ChoiceEquivalences.
+(**********************************************************************)
+(** *** C. Connection between the guarded, non guarded and descriptive choices and *)
 
 (** 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 premises or proof-irrelevance *)
 
-Definition GuardedRelationalChoice (A B:Type) :=
-  forall (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,
-         P x ->
-         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.
+(**********************************************************************)
+(** **** C. 1. AC_rel + PI -> GAC_rel and AC_rel + IGP -> GAC_rel and GAC_rel = OAC_rel *)
 
 Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice :
-  (forall A B, RelationalChoice A B)
-    -> ProofIrrelevance -> (forall A B, GuardedRelationalChoice A B).
+  RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
 Proof.
 intros rel_choice proof_irrel.
 red in |- *; intros A B P R H.
-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].
+destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)).
+intros (x,HPx).
+destruct (H x HPx) as (y,HRxy).
 exists y; exact HRxy.
 set (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.
-  exact HRxy.
-  split.
-    red in |- *; exists HPx; exact HR'xy.
-    intros y' HR''xy'.
+exists R''; split.
+  intros x y (HPx,HR'xy).
+    change x with (projT1 (existT P x HPx)); apply HR'R; exact HR'xy.
+  intros x HPx.
+  destruct (H0 (existT P x HPx)) as (y,(HR'xy,Huniq)).
+    exists y; split. exists HPx; exact HR'xy.
+    intros y' (H'Px,HR'xy').
       apply Huniq.
-      unfold R'' in HR''xy'.
-      destruct HR''xy' as [H'Px HR'xy'].
-      rewrite proof_irrel with (a1 := HPx) (a2 := H'Px).
-      exact HR'xy'.
+      rewrite proof_irrel with (a1 := HPx) (a2 := H'Px); exact HR'xy'.
 Qed.
 
-Definition IndependenceOfGeneralPremises :=
-  forall (A:Type) (P:A -> Prop) (Q:Prop),
-    (Q -> exists x, P x) -> exists x, Q -> P x.
-
 Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice :
- forall A B, RelationalChoice A B -> 
-   IndependenceOfGeneralPremises -> GuardedRelationalChoice A B.
-Proof.
-intros A B RelCh IndPrem.
-red in |- *; intros P R H.
-destruct (RelCh (fun x y => P x -> R x y)) as [R' H0].
-  intro x. apply IndPrem.
-    apply H.
-  exists R'.
-  intros x HPx.
-    destruct (H0 x) as [y [H1 H2]].
-    exists y. split. 
-      apply (H1 HPx).
-      exact H2.
+ forall A B, inhabited B -> RelationalChoice_on A B -> 
+  IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B.
+Proof.
+intros A B Inh AC_rel IndPrem P R H.
+destruct (AC_rel (fun x y => P x -> R x y)) as (R',(HR'R,H0)).
+  intro x. apply IndPrem. exact Inh. intro Hx. 
+    apply H; assumption.
+  exists (fun x y => P x /\ R' x y).
+  firstorder.
+Qed.
+
+Lemma guarded_rel_choice_imp_rel_choice :
+ forall A B, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
+Proof.
+intros A B GAC_rel R H.
+destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)).
+  firstorder.
+exists R'; firstorder.
 Qed.
 
+(** OAC_rel = GAC_rel *)
+
+Lemma guarded_iff_omniscient_rel_choice :
+  GuardedRelationalChoice <-> OmniscientRelationalChoice.
+Proof.
+split.
+  intros GAC_rel A B R.
+    apply (GAC_rel A B (fun x => exists y, R x y) R); auto.
+  intros OAC_rel A B P R H.
+    destruct (OAC_rel A B R) as (f,Hf); exists f; firstorder.
+Qed.
+
+(**********************************************************************)
+(** **** C. 2. AC_fun + IGP = GAC_fun = OAC_fun = AC_fun + Drinker *)
+
+(** AC_fun + IGP = GAC_fun *)
+ 
+Lemma guarded_fun_choice_imp_indep_of_general_premises :
+ GuardedFunctionalChoice -> IndependenceOfGeneralPremises.
+Proof.
+intros GAC_fun A P Q Inh H.
+destruct (GAC_fun unit A (fun _ => Q) (fun _ => P) Inh) as (f,Hf).
+tauto.
+exists (f tt); auto.
+Qed.
+
+Lemma guarded_fun_choice_imp_fun_choice :
+ GuardedFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
+Proof.
+intros GAC_fun A B Inh R H.
+destruct (GAC_fun A B (fun _ => True) R Inh) as (f,Hf).
+firstorder.
+exists f; auto.
+Qed.
+
+Lemma fun_choice_and_indep_general_prem_imp_guarded_fun_choice :
+  FunctionalChoiceOnInhabitedSet -> IndependenceOfGeneralPremises
+  -> GuardedFunctionalChoice.
+Proof.
+intros AC_fun IndPrem A B P R Inh H.
+apply (AC_fun A B Inh (fun x y => P x -> R x y)).
+intro x; apply IndPrem; eauto.
+Qed.
+
+(** AC_fun + Drinker = OAC_fun *)
+
+(** This was already observed by Bell [Bell] *)
+
+Lemma omniscient_fun_choice_imp_small_drinker :
+  OmniscientFunctionalChoice -> SmallDrinker'sParadox.
+Proof.
+intros OAC_fun A P Inh.
+destruct (OAC_fun unit A (fun _ => P)) as (f,Hf).
+auto.
+exists (f tt); firstorder.
+Qed.
+
+Lemma omniscient_fun_choice_imp_fun_choice :
+  OmniscientFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
+Proof.
+intros OAC_fun A B Inh R H.
+destruct (OAC_fun A B R Inh) as (f,Hf).
+exists f; firstorder.
+Qed.
+
+Lemma fun_choice_and_small_drinker_imp_omniscient_fun_choice :
+  FunctionalChoiceOnInhabitedSet -> SmallDrinker'sParadox 
+  -> OmniscientFunctionalChoice.
+Proof.
+intros AC_fun Drinker A B R Inh.
+destruct (AC_fun A B Inh (fun x y => (exists y, R x y) -> R x y)) as (f,Hf).
+  intro x; apply (Drinker B (R x) Inh).
+  exists f; assumption.
+Qed.
+
+(** OAC_fun = GAC_fun *)
+
+(** This is derivable from the intuitionistic equivalence between IGP and Drinker
+but we give a direct proof *)
+
+Lemma guarded_iff_omniscient_fun_choice :
+  GuardedFunctionalChoice <-> OmniscientFunctionalChoice.
+Proof.
+split.
+  intros GAC_fun A B R Inh.
+    apply (GAC_fun A B (fun x => exists y, R x y) R); auto.
+  intros OAC_fun A B P R Inh H.
+    destruct (OAC_fun A B R Inh) as (f,Hf).
+ exists f; firstorder.
+Qed.
+
+(**********************************************************************)
+(** *** D. Derivability of choice for decidable relations with well-ordered codomain *)
 
 (** Countable codomains, such as [nat], can be equipped with a
     well-order, which implies the existence of a least element on
     inhabited decidable subsets. As a consequence, the relational form of
     the axiom of choice is derivable on [nat] for decidable relations.
 
-    We show instead that definite description and the functional form
-    of the axiom of choice are equivalent on decidable relation with [nat]
-    as codomain 
+    We show instead that functional relation reification and the
+    functional form of the axiom of choice are equivalent on decidable
+    relation with [nat] as codomain 
 *)
 
 Require Import Wf_nat.
@@ -163,12 +462,11 @@ Require Import Decidable.
 Require Import Arith.
 
 Definition has_unique_least_element (A:Type) (R:A->A->Prop) (P:A->Prop) :=
-  (exists x, (P x /\ forall x', P x' -> R x x')
-      /\ forall x', P x' /\ (forall x'', P x'' -> R x' x'') -> x=x').
+  exists! x, P x /\ forall x', P x' -> R x x'.
 
 Lemma dec_inh_nat_subset_has_unique_least_element :
   forall P:nat->Prop, (forall n, P n \/ ~ P n) ->
-    (exists n, P n) -> has_unique_least_element nat le P.
+    (exists n, P n) -> has_unique_least_element le P.
 Proof.
 intros P Pdec (n0,HPn0).
 assert
@@ -194,30 +492,228 @@ assert
   assumption.
   destruct H0.
   rewrite Heqn; assumption.
-destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
-  repeat split; 
+  destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0];
+  repeat split;
   assumption || intros n' (HPn',Hminn'); apply le_antisym; auto.
 Qed.
 
-Definition FunctionalChoice_on (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)).
+Definition FunctionalChoice_on_rel (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)).
 
 Lemma classical_denumerable_description_imp_fun_choice : 
   forall A:Type, 
-  ParamDefiniteDescription A nat -> 
-  forall R, (forall x y, decidable (R x y)) -> FunctionalChoice_on A nat R.
+  FunctionalRelReification_on A nat -> 
+  forall R:A->nat->Prop, 
+    (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R.
 Proof.
 intros A Descr.
 red in |- *; intros R Rdec H.
 set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y').
-destruct (Descr R') as [f Hf].
+destruct (Descr R') as (f,Hf).
   intro x.
   apply (dec_inh_nat_subset_has_unique_least_element (R x)). 
     apply Rdec.
     apply (H x).
 exists f.
 intros x.
-destruct (Hf x) as [Hfx _].
+destruct (Hf x) as (Hfx,_).
+assumption.
+Qed.
+
+(**********************************************************************)
+(** *** E. Choice on dependent and non dependent function types are equivalent *)
+
+(** **** E. 1. Choice on dependent and non dependent function types are equivalent *)
+
+Definition DependentFunctionalChoice_on (A:Type) (B:A -> Type) :=
+  forall R:forall x:A, B x -> Prop,
+  (forall x:A, exists y : B x, R x y) ->
+  (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+
+Notation DependentFunctionalChoice := 
+  (forall A (B:A->Type), DependentFunctionalChoice_on B).
+
+(** The easy part *)
+
+Theorem dep_non_dep_functional_choice : 
+  DependentFunctionalChoice -> FunctionalChoice.
+Proof.
+intros AC_depfun A B R H.
+  destruct (AC_depfun A (fun _ => B) R H) as (f,Hf).
+  exists f; trivial.
+Qed.
+
+(** Deriving choice on product types requires some computation on
+    singleton propositional types, so we need computational
+    conjunction projections and dependent elimination of conjunction
+    and equality *)
+
+Scheme and_indd := Induction for and Sort Prop.
+Scheme eq_indd := Induction for eq Sort Prop.
+
+Definition proj1_inf (A B:Prop) (p : A/\B) :=
+  let (a,b) := p in a.
+
+Theorem non_dep_dep_functional_choice : 
+  FunctionalChoice -> DependentFunctionalChoice.
+Proof.
+intros AC_fun A B R H.
+pose (B' := { x:A & B x }). 
+pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). 
+destruct (AC_fun A B' R') as (f,Hf).
+intros x. destruct (H x) as (y,Hy).
+exists (existT (fun x => B x) x y). split; trivial.
+exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))).
+intro x; destruct (Hf x) as (Heq,HR) using and_indd.
+destruct (f x); simpl in *.
+destruct Heq using eq_indd; trivial.
+Qed.
+
+(** **** E. 2. Reification of dependent and non dependent functional relation  are equivalent *)
+
+Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) :=
+  forall (R:forall x:A, B x -> Prop),
+  (forall x:A, exists! y : B x, R x y) ->
+  (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+
+Notation DependentFunctionalRelReification :=
+  (forall A (B:A->Type), DependentFunctionalRelReification_on B).
+
+(** The easy part *)
+
+Theorem dep_non_dep_functional_rel_reification : 
+  DependentFunctionalRelReification -> FunctionalRelReification.
+Proof.
+intros DepFunReify A B R H.
+  destruct (DepFunReify A (fun _ => B) R H) as (f,Hf).
+  exists f; trivial.
+Qed.
+
+(** Deriving choice on product types requires some computation on
+    singleton propositional types, so we need computational
+    conjunction projections and dependent elimination of conjunction
+    and equality *)
+
+Theorem non_dep_dep_functional_rel_reification : 
+  FunctionalRelReification -> DependentFunctionalRelReification.
+Proof.
+intros AC_fun A B R H.
+pose (B' := { x:A & B x }). 
+pose (R' := fun (x:A) (y:B') => projT1 y = x /\ R (projT1 y) (projT2 y)). 
+destruct (AC_fun A B' R') as (f,Hf).
+intros x. destruct (H x) as (y,(Hy,Huni)).
+  exists (existT (fun x => B x) x y). repeat split; trivial.
+  intros (x',y') (Heqx',Hy').
+  simpl in *.
+  destruct Heqx'.
+  rewrite (Huni y'); trivial.
+exists (fun x => eq_rect _ _ (projT2 (f x)) _ (proj1_inf (Hf x))).
+intro x; destruct (Hf x) as (Heq,HR) using and_indd.
+destruct (f x); simpl in *.
+destruct Heq using eq_indd; trivial.
+Qed.
+
+(**********************************************************************)
+(** *** F. Non contradiction of constructive descriptions wrt functional axioms of choice *)
+
+(** **** F. 1. Non contradiction of indefinite description *)
+
+Lemma relative_non_contradiction_of_indefinite_desc :
+      (ConstructiveIndefiniteDescription -> False)
+   -> (FunctionalChoice -> False).
+Proof.
+intros H AC_fun.
+assert (AC_depfun := non_dep_dep_functional_choice AC_fun).
+pose (A0 := { A:Type & { P:A->Prop & exists x, P x }}).
+pose (B0 := fun x:A0 => projT1 x).
+pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y).
+pose (H0 := fun x:A0 => projT2 (projT2 x)).
+destruct (AC_depfun A0 B0 R0 H0) as (f, Hf).
+apply H.
+intros A P H'.
+exists (f (existT (fun _ => sigT _) A
+            (existT (fun P => exists x, P x) P H'))).
+pose (Hf' := 
+          Hf (existT (fun _ => sigT _) A
+            (existT (fun P => exists x, P x) P H'))).
 assumption.
 Qed.
+
+Lemma constructive_indefinite_descr_fun_choice :
+   ConstructiveIndefiniteDescription -> FunctionalChoice.
+Proof.
+intros IndefDescr A B R H.
+exists (fun x => proj1_sig (IndefDescr B (R x) (H x))).
+intro x.
+apply (proj2_sig (IndefDescr B (R x) (H x))).
+Qed.
+
+(** **** F. 2. Non contradiction of definite description *)
+
+Lemma relative_non_contradiction_of_definite_descr :
+      (ConstructiveDefiniteDescription -> False)
+   -> (FunctionalRelReification -> False).
+Proof.
+intros H FunReify.
+assert (DepFunReify := non_dep_dep_functional_rel_reification FunReify).
+pose (A0 := { A:Type & { P:A->Prop & exists! x, P x }}).
+pose (B0 := fun x:A0 => projT1 x).
+pose (R0 := fun x:A0 => fun y:B0 x => projT1 (projT2 x) y).
+pose (H0 := fun x:A0 => projT2 (projT2 x)).
+destruct (DepFunReify A0 B0 R0 H0) as (f, Hf).
+apply H.
+intros A P H'.
+exists (f (existT (fun _ => sigT _) A
+            (existT (fun P => exists! x, P x) P H'))).
+pose (Hf' := 
+          Hf (existT (fun _ => sigT _) A
+            (existT (fun P => exists! x, P x) P H'))).
+assumption.
+Qed.
+
+Lemma constructive_definite_descr_fun_reification :
+   ConstructiveDefiniteDescription -> FunctionalRelReification.
+Proof.
+intros DefDescr A B R H.
+exists (fun x => proj1_sig (DefDescr B (R x) (H x))).
+intro x.
+apply (proj2_sig (DefDescr B (R x) (H x))).
+Qed.
+
+(**********************************************************************)
+(** *** G. Excluded-middle + definite description => computational excluded-middle *)
+
+(** The idea for the following proof comes from [ChicliPottierSimpson02] *)
+
+(** Classical logic and axiom of unique choice (i.e. functional
+    relation reification), as shown in [ChicliPottierSimpson02],
+    implies the double-negation of excluded-middle in [Set] (which is
+    incompatible with the impredicativity of [Set]).
+
+    We adapt the proof to show that constructive definite description
+    transports excluded-middle from [Prop] to [Set].
+
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    Simpson, Mathematical Quotients and Quotient Types in Coq,
+    Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
+    Springer Verlag.  *)
+
+Require Import Setoid.
+
+Theorem constructive_definite_descr_excluded_middle :
+  ConstructiveDefiniteDescription ->
+  (forall P:Prop, P \/ ~ P) -> (forall P:Prop, {P} + {~ P}).
+Proof.
+intros Descr EM P.
+pose (select := fun b:bool => if b then P else ~P).
+assert { b:bool | select b } as ([|],HP).
+  apply Descr.
+  rewrite <- unique_existence; split.
+  destruct (EM P).
+      exists true; trivial.
+      exists false; trivial.
+    intros [|] [|] H1 H2; simpl in *; reflexivity || contradiction.
+left; trivial.
+right; trivial.
+Qed.  
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 5a633f84..bb8186ae 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -6,28 +6,40 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalChoice.v 6401 2004-12-05 16:44:57Z herbelin $ i*)
+(*i $Id: ClassicalChoice.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
 
-(** This file provides classical logic and functional choice *)
+(** This file provides classical logic, and functional choice *)
 
-(** This file extends ClassicalDescription.v with the axiom of choice.
-    As ClassicalDescription.v, it implies the double-negation of
-    excluded-middle in Set and implies a strongly classical
-    world. Especially it conflicts with impredicativity of Set, knowing
-    that true<>false in Set.
-*)
+(** This file extends ClassicalUniqueChoice.v with the axiom of 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
+    impredicativity of [Set], knowing that [true<>false] in [Set].  *)
 
-Require Export ClassicalDescription.
+Require Export ClassicalUniqueChoice.
 Require Export RelationalChoice.
 Require Import ChoiceFacts.
 
+Set Implicit Arguments.
+
+Definition subset (U:Type) (P Q:U->Prop) : Prop := forall x, P x -> Q x.
+
+Theorem singleton_choice :
+  forall (A : Type) (P : A->Prop),
+  (exists x : A, P x) -> exists P' : A->Prop, subset P' P /\ exists! x, P' x.
+Proof.
+intros A P H.
+destruct (relational_choice unit A (fun _ => P) (fun _ => H)) as (R',(Hsub,HR')).
+exists (R' tt); firstorder.
+Qed.
+
 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 (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.
 intros A B.
 apply description_rel_choice_imp_funct_choice.
-exact (description A B).
+exact (unique_choice A B).
 exact (relational_choice A B).
 Qed.
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index ce3e279c..7053266a 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -6,73 +6,95 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalDescription.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: ClassicalDescription.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
 
 (** This file provides classical logic and definite description *)
 
-(** Classical logic and definite description, as shown in [1],
-    implies the double-negation of excluded-middle in Set, hence it
-    implies a strongly classical world. Especially it conflicts with
-    impredicativity of Set, knowing that true<>false in Set.
+(** 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] *)
 
-    [1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical
-    Quotients and Quotient Types in Coq, Proceedings of TYPES 2002,
-    Lecture Notes in Computer Science 2646, Springer Verlag.
-*)
+Set Implicit Arguments.
 
 Require Export Classical.
+Require Import ChoiceFacts.
 
-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)).
+Notation Local "'inhabited' A" := A (at level 200, 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}.
+Proof.
+apply 
+  (constructive_definite_descr_excluded_middle 
+   constructive_definite_description classic).
+Qed.
+
+Theorem classical_definite_description : 
+  forall (A : Type) (P : A->Prop), inhabited A ->
+  { x : A | (exists! x : A, P x) -> P x }.
+Proof.
+intros A P i.
+destruct (excluded_middle_informative (exists! x, P x)) as [Hex|HnonP].
+  apply constructive_definite_description with (P:= fun x => (exists! x : A, P x) -> P x).
+  destruct Hex as (x,(Hx,Huni)).
+  exists x; split.
+    intros _; exact Hx.
+    firstorder.
+exists i; tauto.
+Qed.
+
+(** Church's iota operator *)
 
-(** Principle of definite descriptions (aka axiom of unique choice) *)
+Definition iota (A : Type) (i:inhabited A) (P : A->Prop) : A
+  := proj1_sig (classical_definite_description P i).
+
+Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : 
+  (exists! x:A, P x) -> P (iota i P)
+  := proj2_sig (classical_definite_description P i).
+
+(** Weaker lemmas (compatibility lemmas) *)
+
+Unset Implicit Arguments.
+
+Lemma 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) ->
+      (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+Proof.
+intros A B R H.
+assert (Hexuni:forall x, exists! y, R x y).
+  intro x. apply H.
+exists (fun x => proj1_sig (constructive_definite_description (R x) (Hexuni x))).
+intro x.
+apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))).
+Qed.
 
 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) ->
+   (exists f : A->B, forall x:A, R x (f x)).
 Proof.
 intros A B.
 apply (dependent_description A (fun _ => B)).
 Qed.
 
-(** The followig proof comes from [1] *)
+(** Axiom of unique "choice" (functional reification of functional relations) *)
+
+Set Implicit Arguments.
 
-Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Require Import Setoid.
+
+Theorem unique_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.
-intro HnotEM.
-set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
-assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).
-apply description.
-intro A.
-destruct (classic A) as [Ha| Hnota].
-  exists true; split.
-    left; split; [ assumption | reflexivity ].
-    intros y [[_ Hy]| [Hna _]].
-      assumption.
-      contradiction.
-  exists false; split.
-    right; split; [ assumption | reflexivity ].
-    intros y [[Ha _]| [_ Hy]].
-      contradiction.
-      assumption.
-destruct H as [f Hf].
-apply HnotEM.
-intro P.
-assert (HfP := Hf P).
-(* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
-destruct (f P).
-  left.
-  destruct HfP as [[Ha _]| [_ Hfalse]].
-    assumption.
-    discriminate.
-  right.
-  destruct HfP as [[_ Hfalse]| [Hna _]].
-    discriminate.
-    assumption.
+intros A B R H.
+apply (description A B).
+intro x. apply H.
 Qed.
- 
diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
new file mode 100644
index 00000000..b7293bec
--- /dev/null
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -0,0 +1,90 @@
+(************************************************************************)
+(*  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: ClassicalEpsilon.v 8933 2006-06-09 14:08:38Z herbelin $ i*)
+
+(** *** This file provides classical logic and indefinite description
+    (Hilbert's epsilon operator) *)
+
+(** Classical epsilon's operator (i.e. indefinite description) implies
+    excluded-middle in [Set] and leads to a classical world populated
+    with non computable functions. It conflicts with the
+    impredicativity of [Set] *)
+
+Require Export Classical.
+Require Import ChoiceFacts.
+
+Set Implicit Arguments.
+
+Notation Local "'inhabited' A" := A (at level 200, only parsing).
+
+Axiom constructive_indefinite_description :
+  forall (A : Type) (P : A->Prop), 
+  (ex P) -> { x : A | P x }.
+
+Lemma constructive_definite_description :
+  forall (A : Type) (P : A->Prop), 
+  (exists! x : A, P x) -> { x : A | P x }.
+Proof.
+intros; apply constructive_indefinite_description; firstorder.
+Qed.
+
+Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
+Proof.
+apply 
+  (constructive_definite_descr_excluded_middle 
+   constructive_definite_description classic).
+Qed.
+
+Theorem classical_indefinite_description : 
+  forall (A : Type) (P : A->Prop), inhabited A ->
+  { x : A | ex P -> P x }.
+Proof.
+intros A P i.
+destruct (excluded_middle_informative (exists x, P x)) as [Hex|HnonP].
+  apply constructive_indefinite_description with (P:= fun x => ex P -> P x).
+  destruct Hex as (x,Hx).
+    exists x; intros _; exact Hx.
+    firstorder.
+Qed.
+
+(** Hilbert's epsilon operator *)
+
+Definition epsilon (A : Type) (i:inhabited A) (P : A->Prop) : A
+  := proj1_sig (classical_indefinite_description P i).
+
+Definition epsilon_spec (A : Type) (i:inhabited A) (P : A->Prop) : 
+  (ex P) -> P (epsilon i P)
+  := proj2_sig (classical_indefinite_description P i).
+
+Opaque epsilon.
+
+(** Open question: is classical_indefinite_description constructively
+    provable from [relational_choice] and
+    [constructive_definite_description] (at least, using the fact that
+    [functional_choice] is provable from [relational_choice] and
+    [unique_choice], we know that the double negation of
+    [classical_indefinite_description] is provable (see
+    [relative_non_contradiction_of_indefinite_desc]). *)
+
+(** Remark: we use [ex P] rather than [exists x, P x] (which is [ex
+    (fun x => P x)] to ease unification *)
+
+(** *** Weaker lemmas (compatibility lemmas) *)
+
+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)).
+Proof.
+intros A B R H.
+exists (fun x => proj1_sig (constructive_indefinite_description (H x))).
+intro x.
+apply (proj2_sig (constructive_indefinite_description  (H x))).
+Qed.
+
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 91056250..70da74d3 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalFacts.v 8136 2006-03-05 21:57:47Z herbelin $ i*)
+(*i $Id: ClassicalFacts.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
 
 (** ** Some facts and definitions about classical logic
 
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
new file mode 100644
index 00000000..79bef2af
--- /dev/null
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*  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: ClassicalUniqueChoice.v 8893 2006-06-04 18:04:53Z herbelin $ i*)
+
+(** This file provides classical logic and unique choice *)
+
+(** Classical logic and unique choice, as shown in
+    [ChicliPottierSimpson02], implies the double-negation of
+    excluded-middle in [Set], hence it implies a strongly classical
+    world. Especially it conflicts with the impredicativity of [Set].
+
+    [ChicliPottierSimpson02] Laurent Chicli, Loïc Pottier, Carlos
+    Simpson, Mathematical Quotients and Quotient Types in Coq,
+    Proceedings of TYPES 2002, Lecture Notes in Computer Science 2646,
+    Springer Verlag.  *)
+
+Require Export Classical.
+
+Axiom
+  dependent_unique_choice :
+    forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
+      (forall x : A, exists! y : B x, R x y) ->
+      (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+
+(** Unique choice reifies functional relations into functions *)
+
+Theorem unique_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.
+intros A B.
+apply (dependent_unique_choice A (fun _ => B)).
+Qed.
+
+(** The followig proof comes from [ChicliPottierSimpson02] *)
+
+Require Import Setoid.
+
+Theorem classic_set : ((forall P:Prop, {P} + {~ P}) -> False) -> False.
+Proof.
+intro HnotEM.
+set (R := fun A b => A /\ true = b \/ ~ A /\ false = b).
+assert (H :  exists f : Prop -> bool, (forall A:Prop, R A (f A))).
+apply unique_choice.
+intro A.
+destruct (classic A) as [Ha| Hnota].
+  exists true; split.
+    left; split; [ assumption | reflexivity ].
+    intros y [[_ Hy]| [Hna _]].
+      assumption.
+      contradiction.
+  exists false; split.
+    right; split; [ assumption | reflexivity ].
+    intros y [[Ha _]| [_ Hy]].
+      contradiction.
+      assumption.
+destruct H as [f Hf].
+apply HnotEM.
+intro P.
+assert (HfP := Hf P).
+(* Elimination from Hf to Set is not allowed but from f to Set yes ! *)
+destruct (f P).
+  left.
+  destruct HfP as [[Ha _]| [_ Hfalse]].
+    assumption.
+    discriminate.
+  right.
+  destruct HfP as [[_ Hfalse]| [Hna _]].
+    discriminate.
+    assumption.
+Qed.
+ 
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index f8b0e65b..ce3e84a7 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Classical_Prop.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Classical_Prop.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
 
 (** Classical Propositional Logic *)
 
@@ -22,6 +22,15 @@ unfold not in |- *; intros; elim (classic p); auto.
 intro NP; elim (H NP).
 Qed.
 
+(** Peirce's law states [forall P Q:Prop, ((P -> Q) -> P) -> P]. 
+    Thanks to [forall P, False -> P], it is equivalent to the
+    following form *)
+
+Lemma Peirce : forall P:Prop, ((P -> False) -> P) -> P.
+Proof.
+intros P H; destruct (classic P); auto.
+Qed.
+
 Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P.
 Proof.
 intros; apply NNPP; red in |- *.
diff --git a/theories/Logic/DecidableType.v b/theories/Logic/DecidableType.v
new file mode 100644
index 00000000..a38b111f
--- /dev/null
+++ b/theories/Logic/DecidableType.v
@@ -0,0 +1,156 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* $Id: DecidableType.v 8933 2006-06-09 14:08:38Z herbelin $ *)
+
+Require Export SetoidList.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Types with decidable Equalities (but no ordering) *)
+
+Module Type DecidableType. 
+
+  Parameter t : Set.
+
+  Parameter eq : t -> t -> Prop.
+
+  Axiom eq_refl : forall x : t, eq x x.
+  Axiom eq_sym : forall x y : t, eq x y -> eq y x.
+  Axiom eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
+
+  Parameter eq_dec : forall x y : t, { eq x y } + { ~ eq x y }.
+
+  Hint Immediate eq_sym.
+  Hint Resolve eq_refl eq_trans.
+
+End DecidableType. 
+
+(** * Additional notions about keys and datas used in FMap *)
+
+Module KeyDecidableType(D:DecidableType).
+ Import D.
+
+ Section Elt.
+ Variable elt : Set.
+ Notation key:=t.
+
+  Definition eqk (p p':key*elt) := eq (fst p) (fst p').
+  Definition eqke (p p':key*elt) := 
+          eq (fst p) (fst p') /\ (snd p) = (snd p').
+
+  Hint Unfold eqk eqke.
+  Hint Extern 2 (eqke ?a ?b) => split.
+
+   (* eqke is stricter than eqk *)
+ 
+   Lemma eqke_eqk : forall x x', eqke x x' -> eqk x x'.
+   Proof.
+     unfold eqk, eqke; intuition.
+   Qed.
+
+  (* eqk, eqke are equalities *)
+ 
+  Lemma eqk_refl : forall e, eqk e e.
+  Proof. auto. Qed.
+
+  Lemma eqke_refl : forall e, eqke e e.
+  Proof. auto. Qed.
+
+  Lemma eqk_sym : forall e e', eqk e e' -> eqk e' e.
+  Proof. auto. Qed.
+
+  Lemma eqke_sym : forall e e', eqke e e' -> eqke e' e.
+  Proof. unfold eqke; intuition. Qed.
+
+  Lemma eqk_trans : forall e e' e'', eqk e e' -> eqk e' e'' -> eqk e e''.
+  Proof. eauto. Qed.
+
+  Lemma eqke_trans : forall e e' e'', eqke e e' -> eqke e' e'' -> eqke e e''.
+  Proof.
+    unfold eqke; intuition; [ eauto | congruence ].
+  Qed.
+
+  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
+  Hint Immediate eqk_sym eqke_sym.
+
+  Lemma InA_eqke_eqk : 
+     forall x m, InA eqke x m -> InA eqk x m.
+  Proof.
+    unfold eqke; induction 1; intuition.
+  Qed.
+  Hint Resolve InA_eqke_eqk.
+
+  Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
+  Proof.
+   intros; apply InA_eqA with p; auto; apply eqk_trans; auto.
+  Qed.
+
+  Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
+  Definition In k m := exists e:elt, MapsTo k e m.
+
+  Hint Unfold MapsTo In.
+
+  (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
+
+  Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
+  Proof.
+  firstorder.
+  exists x; auto.
+  induction H.
+  destruct y.
+  exists e; auto.
+  destruct IHInA as [e H0].
+  exists e; auto.
+  Qed.
+
+  Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
+  Proof.
+  intros; unfold MapsTo in *; apply InA_eqA with (x,e); eauto.
+  Qed.
+
+  Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
+  Proof.
+  destruct 2 as (e,E); exists e; eapply MapsTo_eq; eauto.
+  Qed. 
+
+  Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
+  Proof.
+    inversion 1.
+    inversion_clear H0; eauto.
+    destruct H1; simpl in *; intuition.
+  Qed.      
+
+  Lemma In_inv_2 : forall k k' e e' l, 
+      InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
+  Proof.  
+   inversion_clear 1; compute in H0; intuition.
+  Qed.
+
+  Lemma In_inv_3 : forall x x' l, 
+      InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
+  Proof.
+   inversion_clear 1; compute in H0; intuition.
+  Qed.
+
+ End Elt.
+
+ Hint Unfold eqk eqke.
+ Hint Extern 2 (eqke ?a ?b) => split.
+ Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
+ Hint Immediate eqk_sym eqke_sym.
+ Hint Resolve InA_eqke_eqk.
+ Hint Unfold MapsTo In.
+ Hint Resolve In_inv_2 In_inv_3.
+
+End KeyDecidableType.
+
+
+
+
+
diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v
new file mode 100644
index 00000000..a4f99de2
--- /dev/null
+++ b/theories/Logic/DecidableTypeEx.v
@@ -0,0 +1,50 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(* $Id: DecidableTypeEx.v 8933 2006-06-09 14:08:38Z herbelin $ *)
+
+Require Import DecidableType OrderedType OrderedTypeEx.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Examples of Decidable Type structures. *)
+
+(** A particular case of [DecidableType] where 
+    the equality is the usual one of Coq. *)
+
+Module Type UsualDecidableType.
+ Parameter t : Set.
+ Definition eq := @eq t.
+ Definition eq_refl := @refl_equal t.
+ Definition eq_sym := @sym_eq t.
+ Definition eq_trans := @trans_eq t.
+ Parameter eq_dec : forall x y, { eq x y }+{~eq x y }.
+End UsualDecidableType.
+
+(** a [UsualDecidableType] is in particular an [DecidableType]. *)
+
+Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U.
+
+(** An OrderedType can be seen as a DecidableType *)
+
+Module OT_as_DT (O:OrderedType) <: DecidableType. 
+ Module OF := OrderedTypeFacts O.
+ Definition t := O.t.
+ Definition eq := O.eq. 
+ Definition eq_refl := O.eq_refl. 
+ Definition eq_sym := O.eq_sym. 
+ Definition eq_trans := O.eq_trans. 
+ Definition eq_dec := OF.eq_dec. 
+End OT_as_DT.
+
+(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *)
+
+Module Nat_as_DT <: UsualDecidableType := OT_as_DT (Nat_as_OT).
+Module Positive_as_DT <: UsualDecidableType := OT_as_DT (Positive_as_OT).
+Module N_as_DT <: UsualDecidableType := OT_as_DT (N_as_OT).
+Module Z_as_DT <: UsualDecidableType := OT_as_DT (Z_as_OT).
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 3e94deda..19d5d7ec 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,26 +7,46 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Diaconescu.v 6401 2004-12-05 16:44:57Z herbelin $ i*)
+(*i $Id: Diaconescu.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
 
-(** R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
-   entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
-   adapted the proof to show that the axiom of choice in equivalence
-   classes entails Excluded-Middle in Type Theory.
+(** Diaconescu showed that the Axiom of Choice entails Excluded-Middle
+   in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show
+   that the axiom of choice in equivalence classes entails
+   Excluded-Middle in Type Theory [LacasWerner99].
 
-   This is an adaptatation of the proof by Hugo Herbelin to show that
-   the relational form of the Axiom of Choice + Extensionality for
-   predicates entails Excluded-Middle
+   Three variants of Diaconescu's result in type theory are shown below.
 
-   [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in
-   Proceedings of AMS, vol 51, pp 176-178, 1975.
+   A. A proof that the relational form of the Axiom of Choice +
+      Extensionality for Predicates entails Excluded-Middle (by Hugo
+      Herbelin)
 
-   [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?,
-   preprint, 1999.
+   B. A proof that the relational form of the Axiom of Choice + Proof
+      Irrelevance entails Excluded-Middle for Equality Statements (by
+      Benjamin Werner)
 
+   C. A proof that extensional Hilbert epsilon's description operator
+      entails excluded-middle (taken from Bell [Bell93])
+
+   See also [Carlström] for a discussion of the connection between the
+   Extensional Axiom of Choice and Excluded-Middle
+
+   [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation,
+   in Proceedings of AMS, vol 51, pp 176-178, 1975.
+
+   [LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply
+   the excluded middle?, preprint, 1999.
+
+   [Bell93] John L. Bell, Hilbert's epsilon operator and classical
+   logic, Journal of Philosophical Logic, 22: 1-18, 1993
+
+   [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext,
+   Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
 *)
 
-Section PredExt_GuardRelChoice_imp_EM.
+(**********************************************************************)
+(** *** A. Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle       *)
+
+Section PredExt_RelChoice_imp_EM.
 
 (** The axiom of extensionality for predicates *)
 
@@ -59,15 +80,9 @@ Qed.
 
 Require Import ChoiceFacts.
 
-Variable rel_choice : forall A B:Type, RelationalChoice A B.
+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,
-        P x ->
-         exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')).
+Lemma guarded_rel_choice : GuardedRelationalChoice.
 Proof.
  apply
   (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
@@ -78,16 +93,19 @@ Qed.
 
 Require Import Bool.
 
-Lemma AC :
+Lemma AC_bool_subset_to_bool :
   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)
-   (R := fun (Q:bool -> Prop) (y:bool) => Q y).
-  exact (fun _ H => H).
+  destruct (guarded_rel_choice _ _ 
+   (fun Q:bool -> Prop =>  exists y : _, Q y)
+   (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)).
+    exact (fun _ H => H).
+  exists R; intros P HP. 
+  destruct (HR P HP) as (y,(Hy,Huni)).
+  exists y; firstorder.
 Qed.
 
 (** The proof of the excluded middle *)
@@ -98,7 +116,7 @@ Proof.
 intro P.
 
 (** first we exhibit the choice functional relation R *)
-destruct AC as [R H].
+destruct AC_bool_subset_to_bool as [R H].
 
 set (class_of_true := fun b => b = true \/ P).
 set (class_of_false := fun b => b = false \/ P).
@@ -135,4 +153,152 @@ left; assumption.
 
 Qed.
 
-End PredExt_GuardRelChoice_imp_EM.
+End PredExt_RelChoice_imp_EM.
+
+(**********************************************************************)
+(** *** B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
+
+(** This is an adaptation of Diaconescu's paradox exploiting that
+    proof-irrelevance is some form of extensionality *)
+
+Section ProofIrrel_RelChoice_imp_EqEM.
+
+Variable rel_choice : RelationalChoice.
+
+Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y.
+
+(** Let [a1] and [a2] be two elements in some type [A] *)
+
+Variable A :Type.
+Variables a1 a2 : A.
+
+(** We build the subset [A'] of [A] made of [a1] and [a2] *)
+
+Definition A' := sigT (fun x => x=a1 \/ x=a2).
+
+Definition a1':A'.
+exists a1 ; auto.
+Defined.
+
+Definition a2':A'.
+exists a2 ; auto.
+Defined.
+
+(** By proof-irrelevance, projection is a retraction *)
+
+Lemma projT1_injective : a1=a2 -> a1'=a2'.
+Proof.
+  intro Heq ; unfold a1', a2', A'.
+  rewrite Heq.
+  replace (or_introl (a2=a2) (refl_equal a2)) 
+     with (or_intror (a2=a2) (refl_equal a2)).
+  reflexivity.
+  apply proof_irrelevance.
+Qed.
+
+(** But from the actual proofs of being in [A'], we can assert in the
+    proof-irrelevant world the existence of relevant boolean witnesses *)
+
+Lemma decide : forall x:A', exists y:bool ,
+  (projT1 x = a1 /\ y = true ) \/ (projT1 x = a2 /\ y = false).
+Proof.
+  intros [a [Ha1|Ha2]]; [exists true | exists false]; auto.
+Qed.
+
+(** Thanks to the axiom of choice, the boolean witnesses move from the
+    propositional world to the relevant world *)
+
+Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2.
+Proof.
+  destruct 
+    (rel_choice A' bool 
+       (fun x y =>  projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false))
+    as (R,(HRsub,HR)). 
+    apply decide.
+  destruct (HR a1') as (b1,(Ha1'b1,_Huni1)).
+  destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].
+  destruct (HR a2') as (b2,(Ha2'b2,Huni2)).
+  destruct (HRsub a2' b2 Ha2'b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].
+    left; symmetry; assumption.
+    right; intro H.
+    subst b1; subst b2.
+    rewrite (projT1_injective H) in Ha1'b1.
+    assert (false = true) by auto using Huni2.
+    discriminate.
+  left; assumption.
+Qed.
+
+(** An alternative more concise proof can be done by directly using
+    the guarded relational choice *)
+
+Declare Implicit Tactic auto.
+
+Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2.
+Proof.
+  assert (decide: forall x:A, x=a1 \/ x=a2 -> 
+                exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false).
+    intros a [Ha1|Ha2]; [exists true | exists false]; auto.
+  assert (guarded_rel_choice := 
+          rel_choice_and_proof_irrel_imp_guarded_rel_choice 
+	  rel_choice 
+	  proof_irrelevance).
+  destruct 
+    (guarded_rel_choice A bool 
+      (fun x => x=a1 \/ x=a2)
+      (fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false))
+      as (R,(HRsub,HR)). 
+      apply decide.
+  destruct (HR a1) as (b1,(Ha1b1,_Huni1)). left; reflexivity.
+  destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].
+  destruct (HR a2) as (b2,(Ha2b2,Huni2)). right; reflexivity.
+  destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].
+    left; symmetry; assumption.
+    right; intro H.
+    subst b1; subst b2; subst a1.
+    assert (false = true) by auto using Huni2, Ha1b1.
+    discriminate.
+  left; assumption.
+Qed.
+
+End ProofIrrel_RelChoice_imp_EqEM.
+
+(**********************************************************************)
+(** *** B. Extensional Hilbert's epsilon description operator -> Excluded-Middle *)
+
+(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
+
+Notation Local "'inhabited' A" := A (at level 10, only parsing).
+
+Section ExtensionalEpsilon_imp_EM.
+
+Variable epsilon : forall A : Type, inhabited A -> (A -> Prop) -> A.
+
+Hypothesis epsilon_spec : 
+  forall (A:Type) (i:inhabited A) (P:A->Prop), 
+  (exists x, P x) -> P (epsilon A i P).
+
+Hypothesis epsilon_extensionality :
+  forall (A:Type) (i:inhabited A) (P Q:A->Prop),
+  (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q.
+
+Notation Local eps := (epsilon bool true) (only parsing).
+
+Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P.
+Proof.
+intro P.
+pose (B := fun y => y=false \/ P).
+pose (C := fun y => y=true  \/ P).
+assert (B (eps B)) as [Hfalse|HP] 
+  by (apply epsilon_spec; exists false; left; reflexivity).
+assert (C (eps C)) as [Htrue|HP] 
+  by (apply epsilon_spec; exists true; left; reflexivity).
+  right; intro HP.
+  assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption).
+  rewrite epsilon_extensionality with (1:=H) in Hfalse.
+  rewrite Htrue in Hfalse.
+  discriminate.
+auto.
+auto.
+Qed.
+
+End ExtensionalEpsilon_imp_EM.
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index 11979057..ec168f09 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -6,15 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RelationalChoice.v 6001 2004-08-01 09:27:26Z herbelin $ i*)
+(*i $Id: RelationalChoice.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
 
 (** This file axiomatizes the relational form of the axiom of choice *)
 
-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')).
+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, 
+       subrelation R' R /\ forall x : A, exists! y : B, R' x y.