]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/Coq/Logic/Berardi.mma
made executable again
[helm.git] / matita / matita / contribs / procedural / Coq / Logic / Berardi.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "Coq.ma".
18
19 include "Init/Prelude.ma".
20
21 (*#***********************************************************************)
22
23 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
24
25 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
26
27 (*   \VV/  **************************************************************)
28
29 (*    //   *      This file is distributed under the terms of the       *)
30
31 (*         *       GNU Lesser General Public License Version 2.1        *)
32
33 (*#***********************************************************************)
34
35 (*i $Id: Berardi.v,v 1.5.2.2 2004/08/03 17:42:43 herbelin Exp $ i*)
36
37 (*#* This file formalizes Berardi's paradox which says that in
38    the calculus of constructions, excluded middle (EM) and axiom of
39    choice (AC) imply proof irrelevance (PI).
40    Here, the axiom of choice is not necessary because of the use
41    of inductive types.
42 <<
43 @article{Barbanera-Berardi:JFP96,
44    author    = {F. Barbanera and S. Berardi},
45    title     = {Proof-irrelevance out of Excluded-middle and Choice
46                 in the Calculus of Constructions},
47    journal   = {Journal of Functional Programming},
48    year      = {1996},
49    volume    = {6},
50    number    = {3},
51    pages     = {519-525}
52 }
53 >> *)
54
55 (* UNEXPORTED
56 Set Implicit Arguments.
57 *)
58
59 (* UNEXPORTED
60 Section Berardis_paradox
61 *)
62
63 (*#* Excluded middle *)
64
65 (* UNEXPORTED
66 cic:/Coq/Logic/Berardi/Berardis_paradox/EM.var
67 *)
68
69 (*#* Conditional on any proposition. *)
70
71 inline procedural "cic:/Coq/Logic/Berardi/IFProp.con" as definition.
72
73 (*#* Axiom of choice applied to disjunction.
74     Provable in Coq because of dependent elimination. *)
75
76 inline procedural "cic:/Coq/Logic/Berardi/AC_IF.con" as lemma.
77
78 (*#* We assume a type with two elements. They play the role of booleans.
79     The main theorem under the current assumptions is that [T=F] *)
80
81 (* UNEXPORTED
82 cic:/Coq/Logic/Berardi/Berardis_paradox/Bool.var
83 *)
84
85 (* UNEXPORTED
86 cic:/Coq/Logic/Berardi/Berardis_paradox/T.var
87 *)
88
89 (* UNEXPORTED
90 cic:/Coq/Logic/Berardi/Berardis_paradox/F.var
91 *)
92
93 (*#* The powerset operator *)
94
95 inline procedural "cic:/Coq/Logic/Berardi/pow.con" as definition.
96
97 (*#* A piece of theory about retracts *)
98
99 (* UNEXPORTED
100 Section Retracts
101 *)
102
103 (* UNEXPORTED
104 cic:/Coq/Logic/Berardi/Berardis_paradox/Retracts/A.var
105 *)
106
107 (* UNEXPORTED
108 cic:/Coq/Logic/Berardi/Berardis_paradox/Retracts/B.var
109 *)
110
111 inline procedural "cic:/Coq/Logic/Berardi/retract.ind".
112
113 inline procedural "cic:/Coq/Logic/Berardi/retract_cond.ind".
114
115 (*#* The dependent elimination above implies the axiom of choice: *)
116
117 inline procedural "cic:/Coq/Logic/Berardi/AC.con" as lemma.
118
119 (* UNEXPORTED
120 End Retracts
121 *)
122
123 (*#* This lemma is basically a commutation of implication and existential
124     quantification:  (EX x | A -> P(x))  <=> (A -> EX x | P(x))
125     which is provable in classical logic ( => is already provable in
126     intuitionnistic logic). *)
127
128 inline procedural "cic:/Coq/Logic/Berardi/L1.con" as lemma.
129
130 (*#* The paradoxical set *)
131
132 inline procedural "cic:/Coq/Logic/Berardi/U.con" as definition.
133
134 (*#* Bijection between [U] and [(pow U)] *)
135
136 inline procedural "cic:/Coq/Logic/Berardi/f.con" as definition.
137
138 inline procedural "cic:/Coq/Logic/Berardi/g.con" as definition.
139
140 (*#* We deduce that the powerset of [U] is a retract of [U].
141     This lemma is stated in Berardi's article, but is not used
142     afterwards. *)
143
144 inline procedural "cic:/Coq/Logic/Berardi/retract_pow_U_U.con" as lemma.
145
146 (*#* Encoding of Russel's paradox *)
147
148 (*#* The boolean negation. *)
149
150 inline procedural "cic:/Coq/Logic/Berardi/Not_b.con" as definition.
151
152 (*#* the set of elements not belonging to itself *)
153
154 inline procedural "cic:/Coq/Logic/Berardi/R.con" as definition.
155
156 inline procedural "cic:/Coq/Logic/Berardi/not_has_fixpoint.con" as lemma.
157
158 inline procedural "cic:/Coq/Logic/Berardi/classical_proof_irrelevence.con" as theorem.
159
160 (* UNEXPORTED
161 End Berardis_paradox
162 *)
163