helm/software/matita/contribs/procedural/Coq/Logic/Eqdep.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: Eqdep.v,v 1.10.2.1 2004/07/16 19:31:06 herbelin Exp $ i*)
  36
  37 (*#* This file defines dependent equality and shows its equivalence with
  38     equality on dependent pairs (inhabiting sigma-types). It axiomatizes
  39     the invariance by substitution of reflexive equality proofs and
  40     shows the equivalence between the 4 following statements
  41
  42     - Invariance by Substitution of Reflexive Equality Proofs.
  43     - Injectivity of Dependent Equality
  44     - Uniqueness of Identity Proofs
  45     - Uniqueness of Reflexive Identity Proofs
  46     - Streicher's Axiom K
  47
  48   These statements are independent of the calculus of constructions [2].
  49
  50   References:
  51
  52   [1] T. Streicher, Semantical Investigations into Intensional Type Theory,
  53       Habilitationsschrift, LMU M\252\nchen, 1993.
  54   [2] M. Hofmann, T. Streicher, The groupoid interpretation of type theory,
  55       Proceedings of the meeting Twenty-five years of constructive
  56       type theory, Venice, Oxford University Press, 1998
  57 *)
  58
  59 (* UNEXPORTED
  60 Section Dependent_Equality
  61 *)
  62
  63 (* UNEXPORTED
  64 cic:/Coq/Logic/Eqdep/Dependent_Equality/U.var
  65 *)
  66
  67 (* UNEXPORTED
  68 cic:/Coq/Logic/Eqdep/Dependent_Equality/P.var
  69 *)
  70
  71 (*#* Dependent equality *)
  72
  73 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep.ind".
  74
  75 (* UNEXPORTED
  76 Hint Constructors eq_dep: core v62.
  77 *)
  78
  79 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_sym.con" as lemma.
  80
  81 (* UNEXPORTED
  82 Hint Immediate eq_dep_sym: core v62.
  83 *)
  84
  85 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_trans.con" as lemma.
  86
  87 inline procedural "cic:/Coq/Logic/Eqdep/eq_indd.con" as theorem.
  88
  89 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep1.ind".
  90
  91 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep1_dep.con" as lemma.
  92
  93 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_dep1.con" as lemma.
  94
  95 (*#* Invariance by Substitution of Reflexive Equality Proofs *)
  96
  97 inline procedural "cic:/Coq/Logic/Eqdep/eq_rect_eq.con".
  98
  99 (*#* Injectivity of Dependent Equality is a consequence of *)
 100
 101 (*#* Invariance by Substitution of Reflexive Equality Proof *)
 102
 103 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep1_eq.con" as lemma.
 104
 105 inline procedural "cic:/Coq/Logic/Eqdep/eq_dep_eq.con" as lemma.
 106
 107 (* UNEXPORTED
 108 End Dependent_Equality
 109 *)
 110
 111 (*#* Uniqueness of Identity Proofs (UIP) is a consequence of *)
 112
 113 (*#* Injectivity of Dependent Equality *)
 114
 115 inline procedural "cic:/Coq/Logic/Eqdep/UIP.con" as lemma.
 116
 117 (*#* Uniqueness of Reflexive Identity Proofs is a direct instance of UIP *)
 118
 119 inline procedural "cic:/Coq/Logic/Eqdep/UIP_refl.con" as lemma.
 120
 121 (*#* Streicher axiom K is a direct consequence of Uniqueness of
 122     Reflexive Identity Proofs *)
 123
 124 inline procedural "cic:/Coq/Logic/Eqdep/Streicher_K.con" as lemma.
 125
 126 (*#* We finally recover eq_rec_eq (alternatively eq_rect_eq) from K *)
 127
 128 inline procedural "cic:/Coq/Logic/Eqdep/eq_rec_eq.con" as lemma.
 129
 130 (*#* Dependent equality is equivalent to equality on dependent pairs *)
 131
 132 inline procedural "cic:/Coq/Logic/Eqdep/equiv_eqex_eqdep.con" as lemma.
 133
 134 (*#* UIP implies the injectivity of equality on dependent pairs *)
 135
 136 inline procedural "cic:/Coq/Logic/Eqdep/inj_pair2.con" as lemma.
 137
 138 (*#* UIP implies the injectivity of equality on dependent pairs *)
 139
 140 inline procedural "cic:/Coq/Logic/Eqdep/inj_pairT2.con" as lemma.
 141
 142 (*#* The main results to be exported *)
 143
 144 (* UNEXPORTED
 145 Hint Resolve eq_dep_intro eq_dep_eq: core v62.
 146 *)
 147
 148 (* UNEXPORTED
 149 Hint Immediate eq_dep_sym: core v62.
 150 *)
 151
 152 (* UNEXPORTED
 153 Hint Resolve inj_pair2 inj_pairT2: core.
 154 *)
 155