matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_drops.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 "static_2/relocation/drops_ltc.ma".
  16 include "basic_2/rt_transition/cpm_drops.ma".
  17 include "basic_2/rt_computation/cpms.ma".
  18
  19 (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
  20
  21 (* Properties with generic slicing for local environments *******************)
  22
  23 lemma cpms_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpms h G L n).
  24 /3 width=6 by d2_liftable_sn_ltc, cpm_lifts_sn/ qed-.
  25
  26 (* Basic_2A1: uses: scpds_lift *)
  27 (* Basic_2A1: includes: cprs_lift *)
  28 (* Basic_1: includes: pr3_lift *)
  29 lemma cpms_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpms h G L n).
  30 #n #h #G @d_liftable2_sn_bi
  31 /2 width=6 by cpms_lifts_sn, lifts_mono/
  32 qed-.
  33
  34 (* Inversion lemmas with generic slicing for local environments *************)
  35
  36 (* Basic_2A1: uses: scpds_inv_lift1 *)
  37 (* Basic_2A1: includes: cprs_inv_lift1 *)
  38 (* Basic_1: includes: pr3_gen_lift *)
  39 lemma cpms_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpms h G L n).
  40 /3 width=6 by d2_deliftable_sn_ltc, cpm_inv_lifts_sn/ qed-.
  41
  42 lemma cpms_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpms h G L n).
  43 #n #h #G @d_deliftable2_sn_bi
  44 /2 width=6 by cpms_inv_lifts_sn, lifts_inj/
  45 qed-.
  46
  47 (* Advanced properties ******************************************************)
  48
  49 lemma cpms_delta (n) (h) (G): ∀K,V1,V2. ❪G,K❫ ⊢ V1 ➡*[n,h] V2 →
  50                               ∀W2. ⇧*[1] V2 ≘ W2 → ❪G,K.ⓓV1❫ ⊢ #0 ➡*[n,h] W2.
  51 #n #h #G #K #V1 #V2 #H @(cpms_ind_dx … H) -V2
  52 [ /3 width=3 by cpm_cpms, cpm_delta/
  53 | #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
  54   elim (lifts_total V (𝐔❨1❩)) #W #HVW
  55   /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/
  56 ]
  57 qed.
  58
  59 lemma cpms_ell (n) (h) (G): ∀K,V1,V2. ❪G,K❫ ⊢ V1 ➡*[n,h] V2 →
  60                             ∀W2. ⇧*[1] V2 ≘ W2 → ❪G,K.ⓛV1❫ ⊢ #0 ➡*[↑n,h] W2.
  61 #n #h #G #K #V1 #V2 #H @(cpms_ind_dx … H) -V2
  62 [ /3 width=3 by cpm_cpms, cpm_ell/
  63 | #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
  64   elim (lifts_total V (𝐔❨1❩)) #W #HVW >plus_S1
  65   /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/
  66 ]
  67 qed.
  68
  69 lemma cpms_lref (n) (h) (I) (G): ∀K,T,i. ❪G,K❫ ⊢ #i ➡*[n,h] T →
  70                                  ∀U. ⇧*[1] T ≘ U → ❪G,K.ⓘ[I]❫ ⊢ #↑i ➡*[n,h] U.
  71 #n #h #I #G #K #T #i #H @(cpms_ind_dx … H) -T
  72 [ /3 width=3 by cpm_cpms, cpm_lref/
  73 | #n1 #n2 #T #T2 #_ #IH #HT2 #U2 #HTU2
  74   elim (lifts_total T (𝐔❨1❩)) #U #TU
  75   /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/
  76 ]
  77 qed.
  78
  79 lemma cpms_cast_sn (n) (h) (G) (L):
  80                    ∀U1,U2. ❪G,L❫ ⊢ U1 ➡*[n,h] U2 →
  81                    ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[n,h] T2 →
  82                    ❪G,L❫ ⊢ ⓝU1.T1 ➡*[n,h] ⓝU2.T2.
  83 #n #h #G #L #U1 #U2 #H @(cpms_ind_sn … H) -U1 -n
  84 [ /3 width=3 by cpm_cpms, cpm_cast/
  85 | #n1 #n2 #U1 #U #HU1 #_ #IH #T1 #T2 #H
  86   elim (cpm_fwd_plus … H) -H #T #HT1 #HT2
  87   /3 width=3 by cpms_step_sn, cpm_cast/
  88 ]
  89 qed.
  90
  91 (* Note: apparently this was missing in basic_1 *)
  92 (* Basic_2A1: uses: cprs_delta *)
  93 lemma cpms_delta_drops (n) (h) (G):
  94                        ∀L,K,V,i. ⇩*[i] L ≘ K.ⓓV →
  95                        ∀V2. ❪G,K❫ ⊢ V ➡*[n,h] V2 →
  96                        ∀W2. ⇧*[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ➡*[n,h] W2.
  97 #n #h #G #L #K #V #i #HLK #V2 #H @(cpms_ind_dx … H) -V2
  98 [ /3 width=6 by cpm_cpms, cpm_delta_drops/
  99 | #n1 #n2 #V1 #V2 #_ #IH #HV12 #W2 #HVW2
 100   lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
 101   elim (lifts_total V1 (𝐔❨↑i❩)) #W1 #HVW1
 102   /3 width=11 by cpm_lifts_bi, cpms_step_dx/
 103 ]
 104 qed.
 105
 106 lemma cpms_ell_drops (n) (h) (G):
 107                      ∀L,K,W,i. ⇩*[i] L ≘ K.ⓛW →
 108                      ∀W2. ❪G,K❫ ⊢ W ➡*[n,h] W2 →
 109                      ∀V2. ⇧*[↑i] W2 ≘ V2 → ❪G,L❫ ⊢ #i ➡*[↑n,h] V2.
 110 #n #h #G #L #K #W #i #HLK #W2 #H @(cpms_ind_dx … H) -W2
 111 [ /3 width=6 by cpm_cpms, cpm_ell_drops/
 112 | #n1 #n2 #W1 #W2 #_ #IH #HW12 #V2 #HWV2
 113   lapply (drops_isuni_fwd_drop2 … HLK) -HLK // #HLK
 114   elim (lifts_total W1 (𝐔❨↑i❩)) #V1 #HWV1 >plus_S1
 115   /3 width=11 by cpm_lifts_bi, cpms_step_dx/
 116 ]
 117 qed.
 118
 119 (* Advanced inversion lemmas ************************************************)
 120
 121 lemma cpms_inv_lref1_drops (n) (h) (G):
 122                            ∀L,T2,i. ❪G,L❫ ⊢ #i ➡*[n,h] T2 →
 123                            ∨∨ ∧∧ T2 = #i & n = 0
 124                             | ∃∃K,V,V2. ⇩*[i] L ≘ K.ⓓV & ❪G,K❫ ⊢ V ➡*[n,h] V2 &
 125                                         ⇧*[↑i] V2 ≘ T2
 126                             | ∃∃m,K,V,V2. ⇩*[i] L ≘ K.ⓛV & ❪G,K❫ ⊢ V ➡*[m,h] V2 &
 127                                           ⇧*[↑i] V2 ≘ T2 & n = ↑m.
 128 #n #h #G #L #T2 #i #H @(cpms_ind_dx … H) -T2
 129 [ /3 width=1 by or3_intro0, conj/
 130 | #n1 #n2 #T #T2 #_ #IH #HT2 cases IH -IH *
 131   [ #H1 #H2 destruct
 132     elim (cpm_inv_lref1_drops … HT2) -HT2 *
 133     [ /3 width=1 by or3_intro0, conj/
 134     | /4 width=6 by cpm_cpms, or3_intro1, ex3_3_intro/
 135     | /4 width=8 by cpm_cpms, or3_intro2, ex4_4_intro/
 136     ]
 137   | #K #V0 #V #HLK #HV0 #HVT
 138     lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
 139     elim (cpm_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
 140     /4 width=6 by cpms_step_dx, ex3_3_intro, or3_intro1/
 141   | #m #K #V0 #V #HLK #HV0 #HVT #H destruct
 142     lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
 143     elim (cpm_inv_lifts_sn … HT2 … H0LK … HVT) -H0LK -T
 144     /4 width=8 by cpms_step_dx, ex4_4_intro, or3_intro2/
 145   ]
 146 ]
 147 qed-.
 148
 149 lemma cpms_inv_delta_sn (n) (h) (G) (K) (V):
 150       ∀T2. ❪G,K.ⓓV❫ ⊢ #0 ➡*[n,h] T2 →
 151       ∨∨ ∧∧ T2 = #0 & n = 0
 152        | ∃∃V2. ❪G,K❫ ⊢ V ➡*[n,h] V2 & ⇧*[1] V2 ≘ T2.
 153 #n #h #G #K #V #T2 #H
 154 elim (cpms_inv_lref1_drops … H) -H *
 155 [ /3 width=1 by or_introl, conj/
 156 | #Y #X #V2 #H #HV2 #HVT2
 157   lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
 158   /3 width=3 by ex2_intro, or_intror/
 159 | #m #Y #X #V2 #H #HV2 #HVT2
 160   lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
 161 ]
 162 qed-.
 163
 164 lemma cpms_inv_ell_sn (n) (h) (G) (K) (V):
 165       ∀T2. ❪G,K.ⓛV❫ ⊢ #0 ➡*[n,h] T2 →
 166       ∨∨ ∧∧ T2 = #0 & n = 0
 167        | ∃∃m,V2. ❪G,K❫ ⊢ V ➡*[m,h] V2 & ⇧*[1] V2 ≘ T2 & n = ↑m.
 168 #n #h #G #K #V #T2 #H
 169 elim (cpms_inv_lref1_drops … H) -H *
 170 [ /3 width=1 by or_introl, conj/
 171 | #Y #X #V2 #H #HV2 #HVT2
 172   lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
 173 | #m #Y #X #V2 #H #HV2 #HVT2 #H0 destruct
 174   lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
 175   /3 width=5 by ex3_2_intro, or_intror/
 176 ]
 177 qed-.
 178
 179 lemma cpms_inv_lref_sn (n) (h) (G) (I) (K):
 180       ∀U2,i. ❪G,K.ⓘ[I]❫ ⊢ #↑i ➡*[n,h] U2 →
 181       ∨∨ ∧∧ U2 = #↑i & n = 0
 182        | ∃∃T2. ❪G,K❫ ⊢ #i ➡*[n,h] T2 & ⇧*[1] T2 ≘ U2.
 183 #n #h #G #I #K #U2 #i #H
 184 elim (cpms_inv_lref1_drops … H) -H *
 185 [ /3 width=1 by or_introl, conj/
 186 | #L #V #V2 #H #HV2 #HVU2
 187   lapply (drops_inv_drop1 … H) -H #HLK
 188   elim (lifts_split_trans … HVU2 (𝐔❨↑i❩) (𝐔❨1❩)) -HVU2
 189   [| // ] #T2 #HVT2 #HTU2
 190   /4 width=6 by cpms_delta_drops, ex2_intro, or_intror/
 191 | #m #L #V #V2 #H #HV2 #HVU2 #H0 destruct
 192   lapply (drops_inv_drop1 … H) -H #HLK
 193   elim (lifts_split_trans … HVU2 (𝐔❨↑i❩) (𝐔❨1❩)) -HVU2
 194   [| // ] #T2 #HVT2 #HTU2
 195   /4 width=6 by cpms_ell_drops, ex2_intro, or_intror/
 196 ]
 197 qed-.
 198
 199 fact cpms_inv_succ_sn (n) (h) (G) (L):
 200                       ∀T1,T2. ❪G,L❫ ⊢ T1 ➡*[↑n,h] T2 →
 201                       ∃∃T. ❪G,L❫ ⊢ T1 ➡*[1,h] T & ❪G,L❫ ⊢ T ➡*[n,h] T2.
 202 #n #h #G #L #T1 #T2
 203 @(insert_eq_0 … (↑n)) #m #H
 204 @(cpms_ind_sn … H) -T1 -m
 205 [ #H destruct
 206 | #x1 #n2 #T1 #T #HT1 #HT2 #IH #H
 207   elim (plus_inv_S3_sn x1 n2) [1,2: * |*: // ] -H
 208   [ #H1 #H2 destruct -HT2
 209     elim IH -IH // #T0 #HT0 #HT02
 210     /3 width=3 by cpms_step_sn, ex2_intro/
 211   | #n1 #H1 #H2 destruct -IH
 212     elim (cpm_fwd_plus … 1 n1 T1 T) [|*: // ] -HT1 #T0 #HT10 #HT0
 213     /3 width=5 by cpms_step_sn, cpm_cpms, ex2_intro/
 214   ]
 215 ]
 216 qed-.