matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/genv_primitive.etc

   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 include "apps_2/MLTT1_1/syntax.ma".
  16
  17 (* PRIMITIVE GLOBAL CONSTANTS  **********************************************)
  18
  19 (* symbolic names for referring the primitive global constants *)
  20
  21 definition empty ≝ 0. (* empty type *)
  22
  23 definition erec ≝ 1. (* empty eliminator *)
  24
  25 definition one ≝ 2. (* unit type *)
  26
  27 definition tt ≝ 3. (* unit constructor *)
  28
  29 definition orec ≝ 4. (* unit eliminator *)
  30
  31 definition nat ≝ 5. (* natural numbers type *)
  32
  33 definition zero ≝ 6. (* natural numbers constructor: zero *)
  34
  35 definition succ ≝ 7. (* natural numbers constructor: successor *)
  36
  37 definition nrec ≝ 8. (* natural numbers eliminator *)
  38
  39 definition ii ≝ 9. (* intensional identity type *)
  40
  41 definition refl ≝ 10. (* intensional identity constructor *)
  42
  43 definition irec ≝ 11. (* intensional identity eliminator *)
  44
  45 definition sum ≝ 12. (* disjoint sum type *)
  46
  47 definition sn ≝ 13. (* disjoint sum constructor: left *)
  48
  49 definition dx ≝ 14. (* disjoint sum constructor: right *)
  50
  51 definition srec ≝ 15. (* disjoint sum eliminator *)
  52
  53 definition prod ≝ 16. (* dependent product type *)
  54
  55 definition pair ≝ 17. (* dependent product constructor *)
  56
  57 definition prec ≝ 18. (* dependent product eliminator *)
  58
  59 definition fun ≝ 19. (* dependent function type *)
  60
  61 definition abst ≝ 20. (* dependent function constructor *)
  62
  63 definition ap ≝ 21. (* dependent function eliminator *)
  64
  65 definition univ ≝ 22. (* first universe type *)
  66
  67 definition ue ≝ 23. (* first universe constructor: empty *)
  68
  69 definition uo ≝ 24. (* first universe constructor: one *)
  70
  71 definition un ≝ 25. (* first universe constructor: nat *)
  72
  73 definition ui ≝ 26. (* first universe constructor: ii *)
  74
  75 definition us ≝ 27. (* first universe constructor: sum *)
  76
  77 definition up ≝ 28. (* first universe constructor: union *)
  78
  79 definition uf ≝ 29. (* first universe constructor: fun *)
  80
  81 definition urec ≝ 30. (* first universe eliminator *)
  82
  83 definition primitives ≝ 31. (* number of primitive constants *)
  84
  85 (* primitive global environment *)
  86
  87 definition Gp: lenv ≝
  88    ⋆
  89    Λ □ (* empty *)
  90    Λ □ ⤏ □ (* erec *)
  91    Λ □ (* one *)
  92    Λ □ (* tt *)
  93    Λ □ ⤏ □ ⤏ □ (* orec *)
  94    Λ □ (* nat *)
  95    Λ □ (* zero *)
  96    Λ □ ⤏ □ (* succ *)
  97    Λ □ ⤏ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* nrec *)
  98    Λ □ ⤏ □ ⤏ □ ⤏ □ (* ii *)
  99    Λ □ ⤏ □ (* refl *)
 100    Λ □ ⤏ (□ ⤏ □) ⤏ □ (* irec *)
 101    Λ □ ⤏ □ ⤏ □ (* sum *)
 102    Λ □ ⤏ □ (* sn *)
 103    Λ □ ⤏ □ (* dx *)
 104    Λ □ ⤏ (□ ⤏  □) ⤏ (□ ⤏ □) ⤏ □ (* srec *)
 105    Λ □ ⤏ (□ ⤏ □) ⤏ □ (* prod *)
 106    Λ □ ⤏ □ ⤏ □ (* pair *)
 107    Λ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* prec *)
 108    Λ □ ⤏ (□ ⤏ □) ⤏ □ (* fun *)
 109    Λ (□ ⤏ □) ⤏ □ (* abst *)
 110    Λ □ ⤏ □ ⤏ □ (* ap *)
 111    Λ □ (* univ *)
 112    Λ □ (* ue *)
 113    Λ □ (* uo *)
 114    Λ □ (* un *)
 115    Λ □ ⤏ □ ⤏ □ ⤏ □ (* ui *)
 116    Λ □ ⤏ □ ⤏ □ (* us *)
 117    Λ □ ⤏ (□ ⤏ □) ⤏ □ (* up *)
 118    Λ □ ⤏ (□ ⤏ □) ⤏ □ (* uf *)
 119    Λ □ ⤏ □ (* urec *)
 120 .
 121
 122 (* notation for applying the primitive constants *)
 123
 124 interpretation
 125   "empty type (MLTT)"
 126   'Empty = (TAtom (GRef empty)).
 127
 128 interpretation
 129   "empty eliminator (MLTT)"
 130   'ERec T = (TPair Appl T (TAtom (GRef erec))).
 131
 132 interpretation
 133   "unit type (MLTT)"
 134   'One = (TAtom (GRef one)).
 135
 136 interpretation
 137   "unit constructor (MLTT)"
 138   'TT = (TAtom (GRef tt)).
 139
 140 interpretation
 141   "unit eliminator (MLTT)"
 142   'SRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec)))).
 143
 144 interpretation
 145   "natural numbers type (MLTT)"
 146   'Nat = (TAtom (GRef nat)).
 147
 148 interpretation
 149   "natural numbers constructor: zero (MLTT)"
 150   'Zero = (TAtom (GRef zero)).
 151
 152 interpretation
 153   "natural numbers constructor: successor (MLTT)"
 154   'Succ T = (TPair Appl T (TAtom (GRef succ))).
 155
 156 interpretation
 157   "natural numbers eliminator (MLTT)"
 158   'NRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef nrec))))).
 159
 160 interpretation
 161   "intensional identity type (MLTT)"
 162   'II T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ii))))).
 163
 164 interpretation
 165   "intensional identity constructor (MLTT)"
 166   'Refl T = (TPair Appl T (TAtom (GRef refl))).
 167
 168 interpretation
 169   "intensional identity eliminator (MLTT)"
 170   'IRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef irec)))).
 171
 172 interpretation
 173   "sum type (MLTT)"
 174   'Sum T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef sum)))).
 175
 176 interpretation
 177   "sum constructorL left (MLTT)"
 178   'Sn T = (TPair Appl T (TAtom (GRef sn))).
 179
 180 interpretation
 181   "sum constructor: right (MLTT)"
 182   'Dx T = (TPair Appl T (TAtom (GRef dx))).
 183
 184 interpretation
 185   "sum eliminator (MLTT)"
 186   'SRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec))))).
 187
 188 interpretation
 189   "product type (MLTT)"
 190   'Prod T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prod)))).
 191
 192 interpretation
 193   "product constructor (MLTT)"
 194   'Pair T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef pair)))).
 195
 196 interpretation
 197   "product eliminator (MLTT)"
 198   'PRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prec)))).
 199
 200 interpretation
 201   "function type (MLTT)"
 202   'Fun T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef fun)))).
 203
 204 interpretation
 205   "function constructor (MLTT)"
 206   'Abst T = (TPair Appl T (TAtom (GRef abst))).
 207
 208 interpretation
 209   "function eliminator (MLTT)"
 210   'AP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ap)))).
 211
 212 interpretation
 213   "first universe type (MLTT)"
 214   'Univ = (TAtom (GRef univ)).
 215
 216 interpretation
 217   "first universe constructor: empty (MLTT)"
 218   'UE = (TAtom (GRef ue)).
 219
 220 interpretation
 221   "first universe constructor: one (MLTT)"
 222   'UO = (TAtom (GRef us)).
 223
 224 interpretation
 225   "first universe constructor: nat (MLTT)"
 226   'UN = (TAtom (GRef un)).
 227
 228 interpretation
 229   "first universe constructor: ii (MLTT)"
 230   'UI T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ui))))).
 231
 232 interpretation
 233   "first universe constructor: sum (MLTT)"
 234   'US T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef us)))).
 235
 236 interpretation
 237   "first universe constructor: product (MLTT)"
 238   'UP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef up)))).
 239
 240 interpretation
 241   "first universe constructor: function (MLTT)"
 242   'UF T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef uf)))).
 243
 244 interpretation
 245   "first universe eliminator (MLTT)"
 246   'URec T = (TPair Appl T (TAtom (GRef urec))).