helm/software/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 (*#***********************************************************************)
  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 (*i $Id: Berardi.v,v 1.5.2.2 2004/08/03 17:42:43 herbelin Exp $ i*)
  34
  35 (*#* This file formalizes Berardi's paradox which says that in
  36    the calculus of constructions, excluded middle (EM) and axiom of
  37    choice (AC) imply proof irrelevance (PI).
  38    Here, the axiom of choice is not necessary because of the use
  39    of inductive types.
  40 <<
  41 @article{Barbanera-Berardi:JFP96,
  42    author    = {F. Barbanera and S. Berardi},
  43    title     = {Proof-irrelevance out of Excluded-middle and Choice
  44                 in the Calculus of Constructions},
  45    journal   = {Journal of Functional Programming},
  46    year      = {1996},
  47    volume    = {6},
  48    number    = {3},
  49    pages     = {519-525}
  50 }
  51 >> *)
  52
  53 (* UNEXPORTED
  54 Set Implicit Arguments.
  55 *)
  56
  57 (* UNEXPORTED
  58 Section Berardis_paradox
  59 *)
  60
  61 (*#* Excluded middle *)
  62
  63 (* UNEXPORTED
  64 cic:/Coq/Logic/Berardi/Berardis_paradox/EM.var
  65 *)
  66
  67 (*#* Conditional on any proposition. *)
  68
  69 inline procedural "cic:/Coq/Logic/Berardi/IFProp.con" as definition.
  70
  71 (*#* Axiom of choice applied to disjunction.
  72     Provable in Coq because of dependent elimination. *)
  73
  74 inline procedural "cic:/Coq/Logic/Berardi/AC_IF.con" as lemma.
  75
  76 (*#* We assume a type with two elements. They play the role of booleans.
  77     The main theorem under the current assumptions is that [T=F] *)
  78
  79 (* UNEXPORTED
  80 cic:/Coq/Logic/Berardi/Berardis_paradox/Bool.var
  81 *)
  82
  83 (* UNEXPORTED
  84 cic:/Coq/Logic/Berardi/Berardis_paradox/T.var
  85 *)
  86
  87 (* UNEXPORTED
  88 cic:/Coq/Logic/Berardi/Berardis_paradox/F.var
  89 *)
  90
  91 (*#* The powerset operator *)
  92
  93 inline procedural "cic:/Coq/Logic/Berardi/pow.con" as definition.
  94
  95 (*#* A piece of theory about retracts *)
  96
  97 (* UNEXPORTED
  98 Section Retracts
  99 *)
 100
 101 (* UNEXPORTED
 102 cic:/Coq/Logic/Berardi/Berardis_paradox/Retracts/A.var
 103 *)
 104
 105 (* UNEXPORTED
 106 cic:/Coq/Logic/Berardi/Berardis_paradox/Retracts/B.var
 107 *)
 108
 109 inline procedural "cic:/Coq/Logic/Berardi/retract.ind".
 110
 111 inline procedural "cic:/Coq/Logic/Berardi/retract_cond.ind".
 112
 113 (*#* The dependent elimination above implies the axiom of choice: *)
 114
 115 inline procedural "cic:/Coq/Logic/Berardi/AC.con" as lemma.
 116
 117 (* UNEXPORTED
 118 End Retracts
 119 *)
 120
 121 (*#* This lemma is basically a commutation of implication and existential
 122     quantification:  (EX x | A -> P(x))  <=> (A -> EX x | P(x))
 123     which is provable in classical logic ( => is already provable in
 124     intuitionnistic logic). *)
 125
 126 inline procedural "cic:/Coq/Logic/Berardi/L1.con" as lemma.
 127
 128 (*#* The paradoxical set *)
 129
 130 inline procedural "cic:/Coq/Logic/Berardi/U.con" as definition.
 131
 132 (*#* Bijection between [U] and [(pow U)] *)
 133
 134 inline procedural "cic:/Coq/Logic/Berardi/f.con" as definition.
 135
 136 inline procedural "cic:/Coq/Logic/Berardi/g.con" as definition.
 137
 138 (*#* We deduce that the powerset of [U] is a retract of [U].
 139     This lemma is stated in Berardi's article, but is not used
 140     afterwards. *)
 141
 142 inline procedural "cic:/Coq/Logic/Berardi/retract_pow_U_U.con" as lemma.
 143
 144 (*#* Encoding of Russel's paradox *)
 145
 146 (*#* The boolean negation. *)
 147
 148 inline procedural "cic:/Coq/Logic/Berardi/Not_b.con" as definition.
 149
 150 (*#* the set of elements not belonging to itself *)
 151
 152 inline procedural "cic:/Coq/Logic/Berardi/R.con" as definition.
 153
 154 inline procedural "cic:/Coq/Logic/Berardi/not_has_fixpoint.con" as lemma.
 155
 156 inline procedural "cic:/Coq/Logic/Berardi/classical_proof_irrelevence.con" as theorem.
 157
 158 (* UNEXPORTED
 159 End Berardis_paradox
 160 *)
 161