helm/software/matita/contribs/procedural/Coq/Logic/ClassicalFacts.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: ClassicalFacts.v,v 1.6.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
  36
  37 (*#* Some facts and definitions about classical logic *)
  38
  39 (*#* [prop_degeneracy] (also referred as propositional completeness) *)
  40
  41 (*  asserts (up to consistency) that there are only two distinct formulas *)
  42
  43 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_degeneracy.con" as definition.
  44
  45 (*#* [prop_extensionality] asserts equivalent formulas are equal *)
  46
  47 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_extensionality.con" as definition.
  48
  49 (*#* [excluded_middle] asserts we can reason by case on the truth *)
  50
  51 (*  or falsity of any formula *)
  52
  53 inline procedural "cic:/Coq/Logic/ClassicalFacts/excluded_middle.con" as definition.
  54
  55 (*#* [proof_irrelevance] asserts equality of all proofs of a given formula *)
  56
  57 inline procedural "cic:/Coq/Logic/ClassicalFacts/proof_irrelevance.con" as definition.
  58
  59 (*#* We show [prop_degeneracy <-> (prop_extensionality /\ excluded_middle)] *)
  60
  61 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_degen_ext.con" as lemma.
  62
  63 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_degen_em.con" as lemma.
  64
  65 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_ext_em_degen.con" as lemma.
  66
  67 (*#* We successively show that:
  68
  69    [prop_extensionality]
  70      implies equality of [A] and [A->A] for inhabited [A], which
  71      implies the existence of a (trivial) retract from [A->A] to [A]
  72         (just take the identity), which
  73      implies the existence of a fixpoint operator in [A]
  74         (e.g. take the Y combinator of lambda-calculus)
  75 *)
  76
  77 inline procedural "cic:/Coq/Logic/ClassicalFacts/inhabited.con" as definition.
  78
  79 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_ext_A_eq_A_imp_A.con" as lemma.
  80
  81 inline procedural "cic:/Coq/Logic/ClassicalFacts/retract.ind".
  82
  83 inline procedural "cic:/Coq/Logic/ClassicalFacts/prop_ext_retract_A_A_imp_A.con" as lemma.
  84
  85 inline procedural "cic:/Coq/Logic/ClassicalFacts/has_fixpoint.ind".
  86
  87 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_fixpoint.con" as lemma.
  88
  89 (*#* Assume we have booleans with the property that there is at most 2
  90     booleans (which is equivalent to dependent case analysis). Consider
  91     the fixpoint of the negation function: it is either true or false by
  92     dependent case analysis, but also the opposite by fixpoint. Hence
  93     proof-irrelevance.
  94
  95     We then map bool proof-irrelevance to all propositions.
  96 *)
  97
  98 (* UNEXPORTED
  99 Section Proof_irrelevance_gen
 100 *)
 101
 102 (* UNEXPORTED
 103 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool.var
 104 *)
 105
 106 (* UNEXPORTED
 107 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/true.var
 108 *)
 109
 110 (* UNEXPORTED
 111 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/false.var
 112 *)
 113
 114 (* UNEXPORTED
 115 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim.var
 116 *)
 117
 118 (* UNEXPORTED
 119 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim_redl.var
 120 *)
 121
 122 (* UNEXPORTED
 123 cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_elim_redr.var
 124 *)
 125
 126 (* UNAVAILABLE OBJECT: cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_dep_induction.con *)
 127
 128 inline procedural "cic:/Coq/Logic/ClassicalFacts/Proof_irrelevance_gen/bool_dep_induction.con" "Proof_irrelevance_gen__" as definition.
 129
 130 inline procedural "cic:/Coq/Logic/ClassicalFacts/aux.con" as lemma.
 131
 132 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_gen.con" as lemma.
 133
 134 (* UNEXPORTED
 135 End Proof_irrelevance_gen
 136 *)
 137
 138 (*#* In the pure Calculus of Constructions, we can define the boolean
 139     proposition bool = (C:Prop)C->C->C but we cannot prove that it has at
 140     most 2 elements.
 141 *)
 142
 143 (* UNEXPORTED
 144 Section Proof_irrelevance_CC
 145 *)
 146
 147 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP.con" as definition.
 148
 149 inline procedural "cic:/Coq/Logic/ClassicalFacts/TrueP.con" as definition.
 150
 151 inline procedural "cic:/Coq/Logic/ClassicalFacts/FalseP.con" as definition.
 152
 153 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_elim.con" as definition.
 154
 155 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_elim_redl.con" as definition.
 156
 157 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_elim_redr.con" as definition.
 158
 159 inline procedural "cic:/Coq/Logic/ClassicalFacts/BoolP_dep_induction.con" as definition.
 160
 161 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_cc.con" as lemma.
 162
 163 (* UNEXPORTED
 164 End Proof_irrelevance_CC
 165 *)
 166
 167 (*#* In the Calculus of Inductive Constructions, inductively defined booleans
 168     enjoy dependent case analysis, hence directly proof-irrelevance from
 169     propositional extensionality.
 170 *)
 171
 172 (* UNEXPORTED
 173 Section Proof_irrelevance_CIC
 174 *)
 175
 176 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP.ind".
 177
 178 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP_elim_redl.con" as definition.
 179
 180 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP_elim_redr.con" as definition.
 181
 182 inline procedural "cic:/Coq/Logic/ClassicalFacts/boolP_indd.con" as theorem.
 183
 184 inline procedural "cic:/Coq/Logic/ClassicalFacts/ext_prop_dep_proof_irrel_cic.con" as lemma.
 185
 186 (* UNEXPORTED
 187 End Proof_irrelevance_CIC
 188 *)
 189
 190 (*#* Can we state proof irrelevance from propositional degeneracy
 191   (i.e. propositional extensionality + excluded middle) without
 192   dependent case analysis ?
 193
 194   Conjecture: it seems possible to build a model of CC interpreting
 195   all non-empty types by the set of all lambda-terms. Such a model would
 196   satisfy propositional degeneracy without satisfying proof-irrelevance
 197   (nor dependent case analysis). This would imply that the previous
 198   results cannot be refined.
 199 *)
 200