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