]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/Coq/Logic/ClassicalFacts.mma
made executable again
[helm.git] / matita / matita / contribs / procedural / Coq / Logic / ClassicalFacts.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: ClassicalFacts.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
36
37 (*#* Some facts and definitions about classical logic *)
38
39 (*#* [prop_degeneracy] (also referred as propositional completeness) *)
40
41 (*  asserts (up to consistency) that there are only two distinct formulas *)
42
43 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_degeneracy.con" as definition.
44
45 (*#* [prop_extensionality] asserts equivalent formulas are equal *)
46
47 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_extensionality.con" as definition.
48
49 (*#* [excluded_middle] asserts we can reason by case on the truth *)
50
51 (*  or falsity of any formula *)
52
53 inline procedural "cic:/Coq/Logic/ClassicalFacts/excluded_middle.con" as definition.
54
55 (*#* [proof_irrelevance] asserts equality of all proofs of a given formula *)
56
57 inline procedural "cic:/Coq/Logic/ClassicalFacts/proof_irrelevance.con" as definition.
58
59 (*#* We show [prop_degeneracy <-> (prop_extensionality /\ excluded_middle)] *)
60
61 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_degen_ext.con" as lemma.
62
63 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_degen_em.con" as lemma.
64
65 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_ext_em_degen.con" as lemma.
66
67 (*#* We successively show that:
68
69    [prop_extensionality]
70      implies equality of [A] and [A->A] for inhabited [A], which 
71      implies the existence of a (trivial) retract from [A->A] to [A]
72         (just take the identity), which
73      implies the existence of a fixpoint operator in [A]
74         (e.g. take the Y combinator of lambda-calculus)
75 *)
76
77 inline procedural "cic:/Coq/Logic/ClassicalFacts/inhabited.con" as definition.
78
79 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_ext_A_eq_A_imp_A.con" as lemma.
80
81 inline procedural "cic:/Coq/Logic/ClassicalFacts/retract.ind".
82
83 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_ext_retract_A_A_imp_A.con" as lemma.
84
85 inline procedural "cic:/Coq/Logic/ClassicalFacts/has_fixpoint.ind".
86
87 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_fixpoint.con" as lemma.
88
89 (*#* Assume we have booleans with the property that there is at most 2
90     booleans (which is equivalent to dependent case analysis). Consider
91     the fixpoint of the negation function: it is either true or false by
92     dependent case analysis, but also the opposite by fixpoint. Hence
93     proof-irrelevance.
94
95     We then map bool proof-irrelevance to all propositions.
96 *)
97
98 (* UNEXPORTED
99 Section Proof_irrelevance_gen
100 *)
101
102 (* UNEXPORTED
103 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool.var
104 *)
105
106 (* UNEXPORTED
107 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/true.var
108 *)
109
110 (* UNEXPORTED
111 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/false.var
112 *)
113
114 (* UNEXPORTED
115 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim.var
116 *)
117
118 (* UNEXPORTED
119 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim_redl.var
120 *)
121
122 (* UNEXPORTED
123 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim_redr.var
124 *)
125
126 (* UNAVAILABLE OBJECT: cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_dep_induction.con *)
127
128 inline procedural "cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_dep_induction.con" "Proof_irrelevance_gen__" as definition.
129
130 inline procedural "cic:/Coq/Logic/ClassicalFacts/aux.con" as lemma.
131
132 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_gen.con" as lemma.
133
134 (* UNEXPORTED
135 End Proof_irrelevance_gen
136 *)
137
138 (*#* In the pure Calculus of Constructions, we can define the boolean
139     proposition bool = (C:Prop)C->C->C but we cannot prove that it has at
140     most 2 elements.
141 *)
142
143 (* UNEXPORTED
144 Section Proof_irrelevance_CC
145 *)
146
147 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP.con" as definition.
148
149 inline procedural "cic:/Coq/Logic/ClassicalFacts/TrueP.con" as definition.
150
151 inline procedural "cic:/Coq/Logic/ClassicalFacts/FalseP.con" as definition.
152
153 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_elim.con" as definition.
154
155 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_elim_redl.con" as definition.
156
157 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_elim_redr.con" as definition.
158
159 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_dep_induction.con" as definition.
160
161 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_cc.con" as lemma.
162
163 (* UNEXPORTED
164 End Proof_irrelevance_CC
165 *)
166
167 (*#* In the Calculus of Inductive Constructions, inductively defined booleans
168     enjoy dependent case analysis, hence directly proof-irrelevance from
169     propositional extensionality.
170 *)
171
172 (* UNEXPORTED
173 Section Proof_irrelevance_CIC
174 *)
175
176 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP.ind".
177
178 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP_elim_redl.con" as definition.
179
180 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP_elim_redr.con" as definition.
181
182 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP_indd.con" as theorem.
183
184 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_cic.con" as lemma.
185
186 (* UNEXPORTED
187 End Proof_irrelevance_CIC
188 *)
189
190 (*#* Can we state proof irrelevance from propositional degeneracy
191   (i.e. propositional extensionality + excluded middle) without
192   dependent case analysis ?
193
194   Conjecture: it seems possible to build a model of CC interpreting
195   all non-empty types by the set of all lambda-terms. Such a model would
196   satisfy propositional degeneracy without satisfying proof-irrelevance
197   (nor dependent case analysis). This would imply that the previous
198   results cannot be refined.
199 *)
200