matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.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 "basic_2/notation/relations/pconveta_5.ma".
  16 include "basic_2/rt_computation/cpms.ma".
  17
  18 (* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************)
  19
  20 (* avtivate genv *)
  21 inductive cpce (h): relation4 genv lenv term term ≝
  22 | cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s)
  23 | cpce_atom: ∀G,i. cpce h G (⋆) (#i) (#i)
  24 | cpce_unit: ∀I,G,K. cpce h G (K.ⓤ{I}) (#0) (#0)
  25 | cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0)
  26 | cpce_ldec: ∀G,K,W. (∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
  27              cpce h G (K.ⓛW) (#0) (#0)
  28 | cpce_eta : ∀n,p,G,K,W,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U →
  29              cpce h G K W W1 → ⇧*[1] W1 ≘ W2 →
  30              cpce h G K V V1 → ⇧*[1] V1 ≘ V2 →
  31              cpce h G (K.ⓛW) (#0) (ⓝW2.+ⓛV2.ⓐ#0.#1)
  32 | cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T →
  33              ⇧*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U
  34 | cpce_gref: ∀G,L,l. cpce h G L (§l) (§l)
  35 | cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
  36              cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 →
  37              cpce h G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
  38 | cpce_flat: ∀I,G,L,V1,V2,T1,T2.
  39              cpce h G L V1 V2 → cpce h G L T1 T2 →
  40              cpce h G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
  41 .
  42
  43 interpretation
  44   "context-sensitive parallel eta-conversion (term)"
  45   'PConvEta h G L T1 T2 = (cpce h G L T1 T2).
  46
  47 (* Basic inversion lemmas ***************************************************)
  48
  49 lemma cpce_inv_sort_sn (h) (G) (L) (s):
  50       ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2.
  51 #h #G #Y #s0 #X2
  52 @(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2
  53 [ #G #L #s #_ //
  54 | #G #i #_ //
  55 | #I #G #K #_ //
  56 | #G #K #V #_ //
  57 | #G #K #W #_ #_ //
  58 | #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct
  59 | #I #G #K #T #U #i #_ #_ #H destruct
  60 | #G #L #l #_ //
  61 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
  62 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
  63 ]
  64 qed-.
  65
  66 lemma cpce_inv_atom_sn (h) (G) (i):
  67       ∀X2. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2.
  68 #h #G #i0 #X2
  69 @(insert_eq_0 … LAtom) #Y
  70 @(insert_eq_0 … (#i0)) #X1
  71 * -G -Y -X1 -X2
  72 [ #G #L #s #_ #_ //
  73 | #G #i #_ #_ //
  74 | #I #G #K #_ #_ //
  75 | #G #K #V #_ #_ //
  76 | #G #K #W #_ #_ #_ //
  77 | #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct
  78 | #I #G #K #T #U #i #_ #_ #_ #H destruct
  79 | #G #L #l #_ #_ //
  80 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  81 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  82 ]
  83 qed-.
  84
  85 lemma cpce_inv_unit_sn (h) (I) (G) (K):
  86       ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
  87 #h #I0 #G #K0 #X2
  88 @(insert_eq_0 … (K0.ⓤ{I0})) #Y
  89 @(insert_eq_0 … (#0)) #X1
  90 * -G -Y -X1 -X2
  91 [ #G #L #s #_ #_ //
  92 | #G #i #_ #_ //
  93 | #I #G #K #_ #_ //
  94 | #G #K #V #_ #_ //
  95 | #G #K #W #_ #_ #_ //
  96 | #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct
  97 | #I #G #K #T #U #i #_ #_ #H #_ destruct
  98 | #G #L #l #_ #_ //
  99 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 100 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 101 ]
 102 qed-.
 103
 104 lemma cpce_inv_ldef_sn (h) (G) (K) (V):
 105       ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
 106 #h #G #K0 #V0 #X2
 107 @(insert_eq_0 … (K0.ⓓV0)) #Y
 108 @(insert_eq_0 … (#0)) #X1
 109 * -G -Y -X1 -X2
 110 [ #G #L #s #_ #_ //
 111 | #G #i #_ #_ //
 112 | #I #G #K #_ #_ //
 113 | #G #K #V #_ #_ //
 114 | #G #K #W #_ #_ #_ //
 115 | #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct
 116 | #I #G #K #T #U #i #_ #_ #H #_ destruct
 117 | #G #L #l #_ #_ //
 118 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 119 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 120 ]
 121 qed-.
 122
 123 lemma cpce_inv_ldec_sn (h) (G) (K) (W):
 124       ∀X2. ⦃G,K.ⓛW⦄ ⊢ #0 ⬌η[h] X2 →
 125       ∨∨ ∧∧ ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2
 126        | ∃∃n,p,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U
 127                               & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[1] W1 ≘ W2
 128                               & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[1] V1 ≘ V2
 129                               & ⓝW2.+ⓛV2.ⓐ#0.#1 = X2.
 130 #h #G #K0 #W0 #X2
 131 @(insert_eq_0 … (K0.ⓛW0)) #Y
 132 @(insert_eq_0 … (#0)) #X1
 133 * -G -Y -X1 -X2
 134 [ #G #L #s #H #_ destruct
 135 | #G #i #_ #H destruct
 136 | #I #G #K #_ #H destruct
 137 | #G #K #V #_ #H destruct
 138 | #G #K #W #HW #_ #H destruct /4 width=5 by or_introl, conj/
 139 | #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #HWU #HW1 #HW12 #HV1 #HV12 #_ #H destruct
 140   /3 width=14 by or_intror, ex6_8_intro/
 141 | #I #G #K #T #U #i #_ #_ #H #_ destruct
 142 | #G #L #l #H #_ destruct
 143 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 144 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 145 ]
 146 qed-.
 147
 148 lemma cpce_inv_lref_sn (h) (I) (G) (K) (i):
 149       ∀X2. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
 150       ∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⇧*[1] T2 ≘ X2.
 151 #h #I0 #G #K0 #i0 #X2
 152 @(insert_eq_0 … (K0.ⓘ{I0})) #Y
 153 @(insert_eq_0 … (#↑i0)) #X1
 154 * -G -Y -X1 -X2
 155 [ #G #L #s #H #_ destruct
 156 | #G #i #_ #H destruct
 157 | #I #G #K #H #_ destruct
 158 | #G #K #V #H #_ destruct
 159 | #G #K #W #_ #H #_ destruct
 160 | #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H #_ destruct
 161 | #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/
 162 | #G #L #l #H #_ destruct
 163 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 164 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 165 ]
 166 qed-.
 167
 168 lemma cpce_inv_gref_sn (h) (G) (L) (l):
 169       ∀X2. ⦃G,L⦄ ⊢ §l ⬌η[h] X2 → §l = X2.
 170 #h #G #Y #l0 #X2
 171 @(insert_eq_0 … (§l0)) #X1 * -G -Y -X1 -X2
 172 [ #G #L #s #_ //
 173 | #G #i #_ //
 174 | #I #G #K #_ //
 175 | #G #K #V #_ //
 176 | #G #K #W #_ #_ //
 177 | #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct
 178 | #I #G #K #T #U #i #_ #_ #H destruct
 179 | #G #L #l #_ //
 180 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
 181 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 182 ]
 183 qed-.
 184
 185 lemma cpce_inv_bind_sn (h) (p) (I) (G) (K) (V1) (T1):
 186       ∀X2. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 →
 187       ∃∃V2,T2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,K.ⓑ{I}V1⦄ ⊢ T1 ⬌η[h] T2 & ⓑ{p,I}V2.T2 = X2.
 188 #h #p0 #I0 #G #Y #V0 #T0 #X2
 189 @(insert_eq_0 … (ⓑ{p0,I0}V0.T0)) #X1 * -G -Y -X1 -X2
 190 [ #G #L #s #H destruct
 191 | #G #i #H destruct
 192 | #I #G #K #H destruct
 193 | #G #K #V #H destruct
 194 | #G #K #W #_ #H destruct
 195 | #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct
 196 | #I #G #K #T #U #i #_ #_ #H destruct
 197 | #G #L #l #H destruct
 198 | #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
 199 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 200 ]
 201 qed-.
 202
 203 lemma cpce_inv_flat_sn (h) (I) (G) (L) (V1) (T1):
 204       ∀X2. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 →
 205       ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,L⦄ ⊢ T1 ⬌η[h] T2 & ⓕ{I}V2.T2 = X2.
 206 #h #I0 #G #Y #V0 #T0 #X2
 207 @(insert_eq_0 … (ⓕ{I0}V0.T0)) #X1 * -G -Y -X1 -X2
 208 [ #G #L #s #H destruct
 209 | #G #i #H destruct
 210 | #I #G #K #H destruct
 211 | #G #K #V #H destruct
 212 | #G #K #W #_ #H destruct
 213 | #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct
 214 | #I #G #K #T #U #i #_ #_ #H destruct
 215 | #G #L #l #H destruct
 216 | #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 217 | #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
 218 ]
 219 qed-.