matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma

   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 "ground_2/xoa/ex_2_3.ma".
  16 include "static_2/syntax/ac.ma".
  17 include "basic_2/notation/relations/exclaim_5.ma".
  18 include "basic_2/rt_computation/cpms.ma".
  19
  20 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  21
  22 (* activate genv *)
  23 (* Basic_2A1: uses: snv *)
  24 inductive cnv (h) (a): relation3 genv lenv term ≝
  25 | cnv_sort: ∀G,L,s. cnv h a G L (⋆s)
  26 | cnv_zero: ∀I,G,K,V. cnv h a G K V → cnv h a G (K.ⓑ[I]V) (#0)
  27 | cnv_lref: ∀I,G,K,i. cnv h a G K (#i) → cnv h a G (K.ⓘ[I]) (#↑i)
  28 | cnv_bind: ∀p,I,G,L,V,T. cnv h a G L V → cnv h a G (L.ⓑ[I]V) T → cnv h a G L (ⓑ[p,I]V.T)
  29 | cnv_appl: ∀n,p,G,L,V,W0,T,U0. ad a n → cnv h a G L V → cnv h a G L T →
  30             ❪G,L❫ ⊢ V ➡*[1,h] W0 → ❪G,L❫ ⊢ T ➡*[n,h] ⓛ[p]W0.U0 → cnv h a G L (ⓐV.T)
  31 | cnv_cast: ∀G,L,U,T,U0. cnv h a G L U → cnv h a G L T →
  32             ❪G,L❫ ⊢ U ➡*[h] U0 → ❪G,L❫ ⊢ T ➡*[1,h] U0 → cnv h a G L (ⓝU.T)
  33 .
  34
  35 interpretation "context-sensitive native validity (term)"
  36   'Exclaim h a G L T = (cnv h a G L T).
  37
  38 (* Basic inversion lemmas ***************************************************)
  39
  40 fact cnv_inv_zero_aux (h) (a):
  41      ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → X = #0 →
  42      ∃∃I,K,V. ❪G,K❫ ⊢ V ![h,a] & L = K.ⓑ[I]V.
  43 #h #a #G #L #X * -G -L -X
  44 [ #G #L #s #H destruct
  45 | #I #G #K #V #HV #_ /2 width=5 by ex2_3_intro/
  46 | #I #G #K #i #_ #H destruct
  47 | #p #I #G #L #V #T #_ #_ #H destruct
  48 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #H destruct
  49 | #G #L #U #T #U0 #_ #_ #_ #_ #H destruct
  50 ]
  51 qed-.
  52
  53 lemma cnv_inv_zero (h) (a):
  54       ∀G,L. ❪G,L❫ ⊢ #0 ![h,a] →
  55       ∃∃I,K,V. ❪G,K❫ ⊢ V ![h,a] & L = K.ⓑ[I]V.
  56 /2 width=3 by cnv_inv_zero_aux/ qed-.
  57
  58 fact cnv_inv_lref_aux (h) (a):
  59      ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀i. X = #(↑i) →
  60      ∃∃I,K. ❪G,K❫ ⊢ #i ![h,a] & L = K.ⓘ[I].
  61 #h #a #G #L #X * -G -L -X
  62 [ #G #L #s #j #H destruct
  63 | #I #G #K #V #_ #j #H destruct
  64 | #I #G #L #i #Hi #j #H destruct /2 width=4 by ex2_2_intro/
  65 | #p #I #G #L #V #T #_ #_ #j #H destruct
  66 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #j #H destruct
  67 | #G #L #U #T #U0 #_ #_ #_ #_ #j #H destruct
  68 ]
  69 qed-.
  70
  71 lemma cnv_inv_lref (h) (a):
  72       ∀G,L,i. ❪G,L❫ ⊢ #↑i ![h,a] →
  73       ∃∃I,K. ❪G,K❫ ⊢ #i ![h,a] & L = K.ⓘ[I].
  74 /2 width=3 by cnv_inv_lref_aux/ qed-.
  75
  76 fact cnv_inv_gref_aux (h) (a): ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀l. X = §l → ⊥.
  77 #h #a #G #L #X * -G -L -X
  78 [ #G #L #s #l #H destruct
  79 | #I #G #K #V #_ #l #H destruct
  80 | #I #G #K #i #_ #l #H destruct
  81 | #p #I #G #L #V #T #_ #_ #l #H destruct
  82 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #l #H destruct
  83 | #G #L #U #T #U0 #_ #_ #_ #_ #l #H destruct
  84 ]
  85 qed-.
  86
  87 (* Basic_2A1: uses: snv_inv_gref *)
  88 lemma cnv_inv_gref (h) (a): ∀G,L,l. ❪G,L❫ ⊢ §l ![h,a] → ⊥.
  89 /2 width=8 by cnv_inv_gref_aux/ qed-.
  90
  91 fact cnv_inv_bind_aux (h) (a):
  92      ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] →
  93      ∀p,I,V,T. X = ⓑ[p,I]V.T →
  94      ∧∧ ❪G,L❫ ⊢ V ![h,a] & ❪G,L.ⓑ[I]V❫ ⊢ T ![h,a].
  95 #h #a #G #L #X * -G -L -X
  96 [ #G #L #s #q #Z #X1 #X2 #H destruct
  97 | #I #G #K #V #_ #q #Z #X1 #X2 #H destruct
  98 | #I #G #K #i #_ #q #Z #X1 #X2 #H destruct
  99 | #p #I #G #L #V #T #HV #HT #q #Z #X1 #X2 #H destruct /2 width=1 by conj/
 100 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #q #Z #X1 #X2 #H destruct
 101 | #G #L #U #T #U0 #_ #_ #_ #_ #q #Z #X1 #X2 #H destruct
 102 ]
 103 qed-.
 104
 105 (* Basic_2A1: uses: snv_inv_bind *)
 106 lemma cnv_inv_bind (h) (a):
 107       ∀p,I,G,L,V,T. ❪G,L❫ ⊢ ⓑ[p,I]V.T ![h,a] →
 108       ∧∧ ❪G,L❫ ⊢ V ![h,a] & ❪G,L.ⓑ[I]V❫ ⊢ T ![h,a].
 109 /2 width=4 by cnv_inv_bind_aux/ qed-.
 110
 111 fact cnv_inv_appl_aux (h) (a):
 112      ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀V,T. X = ⓐV.T →
 113      ∃∃n,p,W0,U0. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
 114                   ❪G,L❫ ⊢ V ➡*[1,h] W0 & ❪G,L❫ ⊢ T ➡*[n,h] ⓛ[p]W0.U0.
 115 #h #a #G #L #X * -L -X
 116 [ #G #L #s #X1 #X2 #H destruct
 117 | #I #G #K #V #_ #X1 #X2 #H destruct
 118 | #I #G #K #i #_ #X1 #X2 #H destruct
 119 | #p #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
 120 | #n #p #G #L #V #W0 #T #U0 #Ha #HV #HT #HVW0 #HTU0 #X1 #X2 #H destruct /3 width=7 by ex5_4_intro/
 121 | #G #L #U #T #U0 #_ #_ #_ #_ #X1 #X2 #H destruct
 122 ]
 123 qed-.
 124
 125 (* Basic_2A1: uses: snv_inv_appl *)
 126 lemma cnv_inv_appl (h) (a):
 127       ∀G,L,V,T. ❪G,L❫ ⊢ ⓐV.T ![h,a] →
 128       ∃∃n,p,W0,U0. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
 129                    ❪G,L❫ ⊢ V ➡*[1,h] W0 & ❪G,L❫ ⊢ T ➡*[n,h] ⓛ[p]W0.U0.
 130 /2 width=3 by cnv_inv_appl_aux/ qed-.
 131
 132 fact cnv_inv_cast_aux (h) (a):
 133      ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀U,T. X = ⓝU.T →
 134      ∃∃U0. ❪G,L❫ ⊢ U ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
 135            ❪G,L❫ ⊢ U ➡*[h] U0 & ❪G,L❫ ⊢ T ➡*[1,h] U0.
 136 #h #a #G #L #X * -G -L -X
 137 [ #G #L #s #X1 #X2 #H destruct
 138 | #I #G #K #V #_ #X1 #X2 #H destruct
 139 | #I #G #K #i #_ #X1 #X2 #H destruct
 140 | #p #I #G #L #V #T #_ #_ #X1 #X2 #H destruct
 141 | #n #p #G #L #V #W0 #T #U0 #_ #_ #_ #_ #_ #X1 #X2 #H destruct
 142 | #G #L #U #T #U0 #HV #HT #HU0 #HTU0 #X1 #X2 #H destruct /2 width=3 by ex4_intro/
 143 ]
 144 qed-.
 145
 146 (* Basic_2A1: uses: snv_inv_cast *)
 147 lemma cnv_inv_cast (h) (a):
 148       ∀G,L,U,T. ❪G,L❫ ⊢ ⓝU.T ![h,a] →
 149       ∃∃U0. ❪G,L❫ ⊢ U ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
 150             ❪G,L❫ ⊢ U ➡*[h] U0 & ❪G,L❫ ⊢ T ➡*[1,h] U0.
 151 /2 width=3 by cnv_inv_cast_aux/ qed-.
 152
 153 (* Basic forward lemmas *****************************************************)
 154
 155 lemma cnv_fwd_flat (h) (a) (I) (G) (L):
 156       ∀V,T. ❪G,L❫ ⊢ ⓕ[I]V.T ![h,a] →
 157       ∧∧ ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a].
 158 #h #a * #G #L #V #T #H
 159 [ elim (cnv_inv_appl … H) #n #p #W #U #_ #HV #HT #_ #_
 160 | elim (cnv_inv_cast … H) #U #HV #HT #_ #_
 161 ] -H /2 width=1 by conj/
 162 qed-.
 163
 164 lemma cnv_fwd_pair_sn (h) (a) (I) (G) (L):
 165       ∀V,T. ❪G,L❫ ⊢ ②[I]V.T ![h,a] → ❪G,L❫ ⊢ V ![h,a].
 166 #h #a * [ #p ] #I #G #L #V #T #H
 167 [ elim (cnv_inv_bind … H) -H #HV #_
 168 | elim (cnv_fwd_flat … H) -H #HV #_
 169 ] //
 170 qed-.
 171
 172 (* Basic_2A1: removed theorems 3:
 173               shnv_cast shnv_inv_cast snv_shnv_cast
 174 *)