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: Berardi.v,v 1.5.2.2 2004/08/03 17:42:43 herbelin Exp $ i*)
35 (*#* This file formalizes Berardi's paradox which says that in
36 the calculus of constructions, excluded middle (EM) and axiom of
37 choice (AC) imply proof irrelevance (PI).
38 Here, the axiom of choice is not necessary because of the use
41 @article{Barbanera-Berardi:JFP96,
42 author = {F. Barbanera and S. Berardi},
43 title = {Proof-irrelevance out of Excluded-middle and Choice
44 in the Calculus of Constructions},
45 journal = {Journal of Functional Programming},
54 Set Implicit Arguments.
58 Section Berardis_paradox
61 (*#* Excluded middle *)
64 cic:/Coq/Logic/Berardi/Berardis_paradox/EM.var
67 (*#* Conditional on any proposition. *)
69 inline procedural "cic:/Coq/Logic/Berardi/IFProp.con" as definition.
71 (*#* Axiom of choice applied to disjunction.
72 Provable in Coq because of dependent elimination. *)
74 inline procedural "cic:/Coq/Logic/Berardi/AC_IF.con" as lemma.
76 (*#* We assume a type with two elements. They play the role of booleans.
77 The main theorem under the current assumptions is that [T=F] *)
80 cic:/Coq/Logic/Berardi/Berardis_paradox/Bool.var
84 cic:/Coq/Logic/Berardi/Berardis_paradox/T.var
88 cic:/Coq/Logic/Berardi/Berardis_paradox/F.var
91 (*#* The powerset operator *)
93 inline procedural "cic:/Coq/Logic/Berardi/pow.con" as definition.
95 (*#* A piece of theory about retracts *)
102 cic:/Coq/Logic/Berardi/Berardis_paradox/Retracts/A.var
106 cic:/Coq/Logic/Berardi/Berardis_paradox/Retracts/B.var
109 inline procedural "cic:/Coq/Logic/Berardi/retract.ind".
111 inline procedural "cic:/Coq/Logic/Berardi/retract_cond.ind".
113 (*#* The dependent elimination above implies the axiom of choice: *)
115 inline procedural "cic:/Coq/Logic/Berardi/AC.con" as lemma.
121 (*#* This lemma is basically a commutation of implication and existential
122 quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x))
123 which is provable in classical logic ( => is already provable in
124 intuitionnistic logic). *)
126 inline procedural "cic:/Coq/Logic/Berardi/L1.con" as lemma.
128 (*#* The paradoxical set *)
130 inline procedural "cic:/Coq/Logic/Berardi/U.con" as definition.
132 (*#* Bijection between [U] and [(pow U)] *)
134 inline procedural "cic:/Coq/Logic/Berardi/f.con" as definition.
136 inline procedural "cic:/Coq/Logic/Berardi/g.con" as definition.
138 (*#* We deduce that the powerset of [U] is a retract of [U].
139 This lemma is stated in Berardi's article, but is not used
142 inline procedural "cic:/Coq/Logic/Berardi/retract_pow_U_U.con" as lemma.
144 (*#* Encoding of Russel's paradox *)
146 (*#* The boolean negation. *)
148 inline procedural "cic:/Coq/Logic/Berardi/Not_b.con" as definition.
150 (*#* the set of elements not belonging to itself *)
152 inline procedural "cic:/Coq/Logic/Berardi/R.con" as definition.
154 inline procedural "cic:/Coq/Logic/Berardi/not_has_fixpoint.con" as lemma.
156 inline procedural "cic:/Coq/Logic/Berardi/classical_proof_irrelevence.con" as theorem.