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: ClassicalFacts.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
35 (*#* Some facts and definitions about classical logic *)
37 (*#* [prop_degeneracy] (also referred as propositional completeness) *)
39 (* asserts (up to consistency) that there are only two distinct formulas *)
41 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_degeneracy.con" as definition.
43 (*#* [prop_extensionality] asserts equivalent formulas are equal *)
45 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_extensionality.con" as definition.
47 (*#* [excluded_middle] asserts we can reason by case on the truth *)
49 (* or falsity of any formula *)
51 inline procedural "cic:/Coq/Logic/ClassicalFacts/excluded_middle.con" as definition.
53 (*#* [proof_irrelevance] asserts equality of all proofs of a given formula *)
55 inline procedural "cic:/Coq/Logic/ClassicalFacts/proof_irrelevance.con" as definition.
57 (*#* We show [prop_degeneracy <-> (prop_extensionality /\ excluded_middle)] *)
59 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_degen_ext.con" as lemma.
61 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_degen_em.con" as lemma.
63 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_ext_em_degen.con" as lemma.
65 (*#* We successively show that:
68 implies equality of [A] and [A->A] for inhabited [A], which
69 implies the existence of a (trivial) retract from [A->A] to [A]
70 (just take the identity), which
71 implies the existence of a fixpoint operator in [A]
72 (e.g. take the Y combinator of lambda-calculus)
75 inline procedural "cic:/Coq/Logic/ClassicalFacts/inhabited.con" as definition.
77 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_ext_A_eq_A_imp_A.con" as lemma.
79 inline procedural "cic:/Coq/Logic/ClassicalFacts/retract.ind".
81 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_ext_retract_A_A_imp_A.con" as lemma.
83 inline procedural "cic:/Coq/Logic/ClassicalFacts/has_fixpoint.ind".
85 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_fixpoint.con" as lemma.
87 (*#* Assume we have booleans with the property that there is at most 2
88 booleans (which is equivalent to dependent case analysis). Consider
89 the fixpoint of the negation function: it is either true or false by
90 dependent case analysis, but also the opposite by fixpoint. Hence
93 We then map bool proof-irrelevance to all propositions.
97 Section Proof_irrelevance_gen
101 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool.var
105 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/true.var
109 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/false.var
113 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim.var
117 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim_redl.var
121 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim_redr.var
124 (* UNAVAILABLE OBJECT: cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_dep_induction.con *)
126 inline procedural "cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_dep_induction.con" "Proof_irrelevance_gen__" as definition.
128 inline procedural "cic:/Coq/Logic/ClassicalFacts/aux.con" as lemma.
130 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_gen.con" as lemma.
133 End Proof_irrelevance_gen
136 (*#* In the pure Calculus of Constructions, we can define the boolean
137 proposition bool = (C:Prop)C->C->C but we cannot prove that it has at
142 Section Proof_irrelevance_CC
145 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP.con" as definition.
147 inline procedural "cic:/Coq/Logic/ClassicalFacts/TrueP.con" as definition.
149 inline procedural "cic:/Coq/Logic/ClassicalFacts/FalseP.con" as definition.
151 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_elim.con" as definition.
153 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_elim_redl.con" as definition.
155 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_elim_redr.con" as definition.
157 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_dep_induction.con" as definition.
159 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_cc.con" as lemma.
162 End Proof_irrelevance_CC
165 (*#* In the Calculus of Inductive Constructions, inductively defined booleans
166 enjoy dependent case analysis, hence directly proof-irrelevance from
167 propositional extensionality.
171 Section Proof_irrelevance_CIC
174 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP.ind".
176 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP_elim_redl.con" as definition.
178 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP_elim_redr.con" as definition.
180 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP_indd.con" as theorem.
182 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_cic.con" as lemma.
185 End Proof_irrelevance_CIC
188 (*#* Can we state proof irrelevance from propositional degeneracy
189 (i.e. propositional extensionality + excluded middle) without
190 dependent case analysis ?
192 Conjecture: it seems possible to build a model of CC interpreting
193 all non-empty types by the set of all lambda-terms. Such a model would
194 satisfy propositional degeneracy without satisfying proof-irrelevance
195 (nor dependent case analysis). This would imply that the previous
196 results cannot be refined.