1 files changed, 138 insertions, 0 deletions
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
new file mode 100644
index 00000000..55eed096
--- /dev/null
+++ b/theories/Logic/Diaconescu.v
@@ -0,0 +1,138 @@
+(************************************************************************)
+(*  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: Diaconescu.v,v 1.5.2.1 2004/07/16 19:31:06 herbelin Exp $ 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.
+
+   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
+
+   [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in
+   Proceedings of AMS, vol 51, pp 176-178, 1975.
+
+   [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?,
+   preprint, 1999.
+
+*)
+
+Section PredExt_GuardRelChoice_imp_EM.
+
+(* The axiom of extensionality for predicates *)
+
+Definition PredicateExtensionality :=
+  forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.
+
+(* From predicate extensionality we get propositional extensionality
+   hence proof-irrelevance *)
+
+Require Import ClassicalFacts.
+
+Variable pred_extensionality : PredicateExtensionality.
+  
+Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B.
+Proof.
+  intros A B H.
+  change ((fun _ => A) true = (fun _ => B) true) in |- *.
+  rewrite
+   pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B).
+    reflexivity.
+    intros _; exact H.
+Qed.
+
+Lemma proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2.
+Proof.
+  apply (ext_prop_dep_proof_irrel_cic prop_ext).
+Qed.
+
+(* From proof-irrelevance and relational choice, we get guarded
+   relational choice *)
+
+Require Import ChoiceFacts.
+
+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')).
+Proof.
+  exact
+   (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
+Qed.
+
+(* The form of choice we need: there is a functional relation which chooses
+   an element in any non empty subset of bool *)
+
+Require Import Bool.
+
+Lemma AC :
+  exists R : (bool -> Prop) -> bool -> Prop,
+   (forall P:bool -> Prop,
+      (exists b : bool, P b) ->
+       exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
+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).
+Qed.
+
+(* The proof of the excluded middle *)
+(* Remark: P could have been in Set or Type *)
+
+Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
+Proof.
+intro P.
+
+(* first we exhibit the choice functional relation R *)
+destruct AC as [R H].
+
+set (class_of_true := fun b => b = true \/ P).
+set (class_of_false := fun b => b = false \/ P).
+
+(* the actual "decision": is (R class_of_true) = true or false? *)
+destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
+exists true; left; reflexivity.
+destruct H0.
+
+(* the actual "decision": is (R class_of_false) = true or false? *)
+destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
+exists false; left; reflexivity.
+destruct H1.
+
+(* case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
+right.
+intro HP.
+assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).
+intro b; split.
+unfold class_of_false in |- *; right; assumption.
+unfold class_of_true in |- *; right; assumption.
+assert (Heq : class_of_true = class_of_false).
+apply pred_extensionality with (1 := Hequiv).
+apply diff_true_false.
+rewrite <- H0.
+rewrite <- H1.
+rewrite <- H0''. reflexivity.
+rewrite Heq.
+assumption.
+
+(* cases where P is true *)
+left; assumption.
+left; assumption.
+
+Qed.
+
+End PredExt_GuardRelChoice_imp_EM.