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