1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Diaconescu.v,v 1.5.2.3 2004/08/01 09:36:44 herbelin Exp $ i*)
35 (*#* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory
36 entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner]
37 adapted the proof to show that the axiom of choice in equivalence
38 classes entails Excluded-Middle in Type Theory.
40 This is an adaptatation of the proof by Hugo Herbelin to show that
41 the relational form of the Axiom of Choice + Extensionality for
42 predicates entails Excluded-Middle
44 [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in
45 Proceedings of AMS, vol 51, pp 176-178, 1975.
47 [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?,
53 Section PredExt_GuardRelChoice_imp_EM
56 (*#* The axiom of extensionality for predicates *)
58 inline procedural "cic:/Coq/Logic/Diaconescu/PredicateExtensionality.con" as definition.
60 (*#* From predicate extensionality we get propositional extensionality
61 hence proof-irrelevance *)
63 include "Logic/ClassicalFacts.ma".
66 cic:/Coq/Logic/Diaconescu/PredExt_GuardRelChoice_imp_EM/pred_extensionality.var
69 inline procedural "cic:/Coq/Logic/Diaconescu/prop_ext.con" as lemma.
71 inline procedural "cic:/Coq/Logic/Diaconescu/proof_irrel.con" as lemma.
73 (*#* From proof-irrelevance and relational choice, we get guarded
76 include "Logic/ChoiceFacts.ma".
79 cic:/Coq/Logic/Diaconescu/PredExt_GuardRelChoice_imp_EM/rel_choice.var
82 inline procedural "cic:/Coq/Logic/Diaconescu/guarded_rel_choice.con" as lemma.
84 (*#* The form of choice we need: there is a functional relation which chooses
85 an element in any non empty subset of bool *)
87 include "Bool/Bool.ma".
89 inline procedural "cic:/Coq/Logic/Diaconescu/AC.con" as lemma.
91 (*#* The proof of the excluded middle *)
93 (*#* Remark: P could have been in Set or Type *)
95 inline procedural "cic:/Coq/Logic/Diaconescu/pred_ext_and_rel_choice_imp_EM.con" as theorem.
98 End PredExt_GuardRelChoice_imp_EM