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 (* The Calculus of Inductive Constructions *)
31 (* Rocquencourt Orsay *)
39 (*#***************************************************************************)
41 (*#* This is a proof in the pure Calculus of Construction that
42 classical logic in Prop + dependent elimination of disjunction entails
45 Since, dependent elimination is derivable in the Calculus of
46 Inductive Constructions (CCI), we get proof-irrelevance from classical
51 - [Coquand] T. Coquand, "Metamathematical Investigations of a
52 Calculus of Constructions", Proceedings of Logic in Computer Science
55 Proof skeleton: classical logic + dependent elimination of
56 disjunction + discrimination of proofs implies the existence of a
57 retract from [Prop] into [bool], hence inconsistency by encoding any
58 paradox of system U- (e.g. Hurkens' paradox).
61 include "Logic/Hurkens.ma".
64 Section Proof_irrelevance_CC
68 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or.var
72 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_introl.var
76 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_intror.var
80 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_elim.var
84 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_elim_redl.var
88 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_elim_redr.var
92 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_dep_elim.var
96 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/em.var
100 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/B.var
104 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/b1.var
108 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/b2.var
111 (*#* [p2b] and [b2p] form a retract if [~b1=b2] *)
113 inline procedural "cic:/Coq/Logic/ProofIrrelevance/p2b.con" as definition.
115 inline procedural "cic:/Coq/Logic/ProofIrrelevance/b2p.con" as definition.
117 inline procedural "cic:/Coq/Logic/ProofIrrelevance/p2p1.con" as lemma.
119 inline procedural "cic:/Coq/Logic/ProofIrrelevance/p2p2.con" as lemma.
121 (*#* Using excluded-middle a second time, we get proof-irrelevance *)
123 inline procedural "cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cc.con" as theorem.
126 End Proof_irrelevance_CC
129 (*#* The Calculus of Inductive Constructions (CCI) enjoys dependent
130 elimination, hence classical logic in CCI entails proof-irrelevance.
134 Section Proof_irrelevance_CCI
138 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CCI/em.var
141 inline procedural "cic:/Coq/Logic/ProofIrrelevance/or_elim_redl.con" as definition.
143 inline procedural "cic:/Coq/Logic/ProofIrrelevance/or_elim_redr.con" as definition.
145 inline procedural "cic:/Coq/Logic/ProofIrrelevance/or_indd.con" as theorem.
147 inline procedural "cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cci.con" as theorem.
150 End Proof_irrelevance_CCI
153 (*#* Remark: in CCI, [bool] can be taken in [Set] as well in the
154 paradox and since [~true=false] for [true] and [false] in
155 [bool], we get the inconsistency of [em : forall A:Prop, {A}+{~A}] in CCI