]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/Coq/Logic/ProofIrrelevance.mma
made executable again
[helm.git] / matita / matita / contribs / procedural / Coq / Logic / ProofIrrelevance.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 (*#***********************************************************************)
20
21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
22
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
24
25 (*   \VV/  **************************************************************)
26
27 (*    //   *      This file is distributed under the terms of the       *)
28
29 (*         *       GNU Lesser General Public License Version 2.1        *)
30
31 (*#***********************************************************************)
32
33 (*#* This is a proof in the pure Calculus of Construction that
34     classical logic in Prop + dependent elimination of disjunction entails
35     proof-irrelevance.
36
37     Since, dependent elimination is derivable in the Calculus of
38     Inductive Constructions (CCI), we get proof-irrelevance from classical
39     logic in the CCI.
40
41     Reference:
42
43     - [Coquand] T. Coquand, "Metamathematical Investigations of a
44       Calculus of Constructions", Proceedings of Logic in Computer Science
45       (LICS'90), 1990.
46
47     Proof skeleton: classical logic + dependent elimination of
48     disjunction + discrimination of proofs implies the existence of a
49     retract from [Prop] into [bool], hence inconsistency by encoding any
50     paradox of system U- (e.g. Hurkens' paradox).
51 *)
52
53 include "Logic/Hurkens.ma".
54
55 (* UNEXPORTED
56 Section Proof_irrelevance_CC
57 *)
58
59 (* UNEXPORTED
60 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or.var
61 *)
62
63 (* UNEXPORTED
64 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_introl.var
65 *)
66
67 (* UNEXPORTED
68 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_intror.var
69 *)
70
71 (* UNEXPORTED
72 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_elim.var
73 *)
74
75 (* UNEXPORTED
76 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_elim_redl.var
77 *)
78
79 (* UNEXPORTED
80 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_elim_redr.var
81 *)
82
83 (* UNEXPORTED
84 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/or_dep_elim.var
85 *)
86
87 (* UNEXPORTED
88 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/em.var
89 *)
90
91 (* UNEXPORTED
92 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/B.var
93 *)
94
95 (* UNEXPORTED
96 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/b1.var
97 *)
98
99 (* UNEXPORTED
100 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CC/b2.var
101 *)
102
103 (*#* [p2b] and [b2p] form a retract if [~b1=b2] *)
104
105 inline procedural "cic:/Coq/Logic/ProofIrrelevance/p2b.con" as definition.
106
107 inline procedural "cic:/Coq/Logic/ProofIrrelevance/b2p.con" as definition.
108
109 inline procedural "cic:/Coq/Logic/ProofIrrelevance/p2p1.con" as lemma.
110
111 inline procedural "cic:/Coq/Logic/ProofIrrelevance/p2p2.con" as lemma.
112
113 (*#* Using excluded-middle a second time, we get proof-irrelevance *)
114
115 inline procedural "cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cc.con" as theorem.
116
117 (* UNEXPORTED
118 End Proof_irrelevance_CC
119 *)
120
121 (*#* The Calculus of Inductive Constructions (CCI) enjoys dependent
122     elimination, hence classical logic in CCI entails proof-irrelevance.
123 *)
124
125 (* UNEXPORTED
126 Section Proof_irrelevance_CCI
127 *)
128
129 (* UNEXPORTED
130 cic:/Coq/Logic/ProofIrrelevance/Proof_irrelevance_CCI/em.var
131 *)
132
133 inline procedural "cic:/Coq/Logic/ProofIrrelevance/or_elim_redl.con" as definition.
134
135 inline procedural "cic:/Coq/Logic/ProofIrrelevance/or_elim_redr.con" as definition.
136
137 inline procedural "cic:/Coq/Logic/ProofIrrelevance/or_indd.con" as theorem.
138
139 inline procedural "cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cci.con" as theorem.
140
141 (* UNEXPORTED
142 End Proof_irrelevance_CCI
143 *)
144
145 (*#* Remark: in CCI, [bool] can be taken in [Set] as well in the
146     paradox and since [~true=false] for [true] and [false] in
147     [bool], we get the inconsistency of [em : forall A:Prop, {A}+{~A}] in CCI
148 *)
149