matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_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 "basic_2/rt_transition/cpg_drops.ma".
  16 include "basic_2/rt_transition/cpm.ma".
  17
  18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
  19
  20 (* Properties with generic slicing for local environments *******************)
  21
  22 (* Basic_1: includes: pr0_lift pr2_lift *)
  23 (* Basic_2A1: includes: cpr_lift *)
  24 lemma cpm_lifts_sn (h) (n) (G): d_liftable2_sn … lifts (λL. cpm h G L n).
  25 #h #n #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
  26 elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
  27 /3 width=5 by ex2_intro/
  28 qed-.
  29
  30 lemma cpm_lifts_bi (h) (n) (G): d_liftable2_bi … lifts (λL. cpm h G L n).
  31 #h #n #G #K #T1 #T2 * /3 width=11 by cpg_lifts_bi, ex2_intro/
  32 qed-.
  33
  34 (* Inversion lemmas with generic slicing for local environments *************)
  35
  36 (* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
  37 (* Basic_2A1: includes: cpr_inv_lift1 *)
  38 lemma cpm_inv_lifts_sn (h) (n) (G): d_deliftable2_sn … lifts (λL. cpm h G L n).
  39 #h #n #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
  40 elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
  41 /3 width=5 by ex2_intro/
  42 qed-.
  43
  44 lemma cpm_inv_lifts_bi (h) (n) (G): d_deliftable2_bi … lifts (λL. cpm h G L n).
  45 #h #n #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/
  46 qed-.
  47
  48 (* Advanced properties ******************************************************)
  49
  50 (* Basic_1: includes: pr2_delta1 *)
  51 (* Basic_2A1: includes: cpr_delta *)
  52 lemma cpm_delta_drops (h) (n) (G) (L):
  53       ∀K,V,V2,W2,i.
  54       ⇩[i] L ≘ K.ⓓV → ❪G,K❫ ⊢ V ➡[h,n] V2 →
  55       ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ➡[h,n] W2.
  56 #h #n #G #L #K #V #V2 #W2 #i #HLK *
  57 /3 width=8 by cpg_delta_drops, ex2_intro/
  58 qed.
  59
  60 lemma cpm_ell_drops (h) (n) (G) (L):
  61       ∀K,V,V2,W2,i.
  62       ⇩[i] L ≘ K.ⓛV → ❪G,K❫ ⊢ V ➡[h,n] V2 →
  63       ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ➡[h,↑n] W2.
  64 #h #n #G #L #K #V #V2 #W2 #i #HLK *
  65 /3 width=8 by cpg_ell_drops, isrt_succ, ex2_intro/
  66 qed.
  67
  68 (* Advanced inversion lemmas ************************************************)
  69
  70 lemma cpm_inv_atom1_drops (h) (n) (G) (L):
  71       ∀I,T2. ❪G,L❫ ⊢ ⓪[I] ➡[h,n] T2 →
  72       ∨∨ ∧∧ T2 = ⓪[I] & n = 0
  73        | ∃∃s. T2 = ⋆(⫯[h]s) & I = Sort s & n = 1
  74        | ∃∃K,V,V2,i. ⇩[i] L ≘ K.ⓓV & ❪G,K❫ ⊢ V ➡[h,n] V2 & ⇧[↑i] V2 ≘ T2 & I = LRef i
  75        | ∃∃m,K,V,V2,i. ⇩[i] L ≘ K.ⓛV & ❪G,K❫ ⊢ V ➡[h,m] V2 & ⇧[↑i] V2 ≘ T2 & I = LRef i & n = ↑m.
  76 #h #n #G #L #I #T2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
  77 [ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
  78   /3 width=1 by or4_intro0, conj/
  79 | #s1 #s2 #H1 #H2 #H3 #H4 destruct lapply (isrt_inv_01 … Hc) -Hc
  80   /4 width=3 by or4_intro1, ex3_intro, sym_eq/ (**) (* sym_eq *)
  81 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
  82   /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/
  83 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
  84   elim (isrt_inv_plus_SO_dx … Hc) -Hc
  85   /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
  86 ]
  87 qed-.
  88
  89 lemma cpm_inv_lref1_drops (h) (n) (G) (L):
  90       ∀T2,i. ❪G,L❫ ⊢ #i ➡[h,n] T2 →
  91       ∨∨ ∧∧ T2 = #i & n = 0
  92        | ∃∃K,V,V2. ⇩[i] L ≘ K.ⓓV & ❪G,K❫ ⊢ V ➡[h,n] V2 & ⇧[↑i] V2 ≘ T2
  93        | ∃∃m,K,V,V2. ⇩[i] L ≘ K. ⓛV & ❪G,K❫ ⊢ V ➡[h,m] V2 & ⇧[↑i] V2 ≘ T2 & n = ↑m.
  94 #h #n #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H *
  95 [ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
  96   /3 width=1 by or3_intro0, conj/
  97 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
  98   /4 width=6 by ex3_3_intro, ex2_intro, or3_intro1/
  99 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
 100   elim (isrt_inv_plus_SO_dx … Hc) -Hc
 101   /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/
 102 ]
 103 qed-.
 104
 105 (* Advanced forward lemmas **************************************************)
 106
 107 fact cpm_fwd_plus_aux (h) (n) (G) (L):
 108      ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 →
 109      ∀n1,n2. n1+n2 = n →
 110      ∃∃T. ❪G,L❫ ⊢ T1 ➡[h,n1] T & ❪G,L❫ ⊢ T ➡[h,n2] T2.
 111 #h #n #G #L #T1 #T2 #H @(cpm_ind … H) -G -L -T1 -T2 -n
 112 [ #I #G #L #n1 #n2 #H
 113   elim (plus_inv_O3 … H) -H #H1 #H2 destruct
 114   /2 width=3 by ex2_intro/
 115 | #G #L #s #x1 #n2 #H
 116   elim (plus_inv_S3_sn … H) -H *
 117   [ #H1 #H2 destruct /2 width=3 by ex2_intro/
 118   | #n1 #H1 #H elim (plus_inv_O3 … H) -H #H2 #H3 destruct
 119     /2 width=3 by ex2_intro/
 120   ]
 121 | #n #G #K #V1 #V2 #W2 #_ #IH #HVW2 #n1 #n2 #H destruct
 122   elim IH [|*: // ] -IH #V #HV1 #HV2
 123   elim (lifts_total V 𝐔❨↑O❩) #W #HVW
 124   /5 width=11 by cpm_lifts_bi, cpm_delta, drops_refl, drops_drop, ex2_intro/
 125 | #n #G #K #V1 #V2 #W2 #HV12 #IH #HVW2 #x1 #n2 #H
 126   elim (plus_inv_S3_sn … H) -H *
 127   [ #H1 #H2 destruct -IH /3 width=3 by cpm_ell, ex2_intro/
 128   | #n1 #H1 #H2 destruct -HV12
 129     elim (IH n1) [|*: // ] -IH #V #HV1 #HV2
 130     elim (lifts_total V 𝐔❨↑O❩) #W #HVW
 131     /5 width=11 by cpm_lifts_bi, cpm_ell, drops_refl, drops_drop, ex2_intro/
 132   ]
 133 | #n #I #G #K #T2 #U2 #i #_ #IH #HTU2 #n1 #n2 #H destruct
 134   elim IH [|*: // ] -IH #T #HT1 #HT2
 135   elim (lifts_total T 𝐔❨↑O❩) #U #HTU
 136   /5 width=11 by cpm_lifts_bi, cpm_lref, drops_refl, drops_drop, ex2_intro/
 137 | #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
 138   elim IHT [|*: // ] -IHT #T #HT1 #HT2
 139   /3 width=5 by cpm_bind, ex2_intro/
 140 | #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
 141   elim IHT [|*: // ] -IHT #T #HT1 #HT2
 142   /3 width=5 by cpm_appl, ex2_intro/
 143 | #n #G #L #U1 #U2 #T1 #T2 #_ #_ #IHU #IHT #n1 #n2 #H destruct
 144   elim IHU [|*: // ] -IHU #U #HU1 #HU2
 145   elim IHT [|*: // ] -IHT #T #HT1 #HT2
 146   /3 width=5 by cpm_cast, ex2_intro/
 147 | #n #G #K #V #U1 #T1 #T2 #HTU1 #_ #IH #n1 #n2 #H destruct
 148   elim IH [|*: // ] -IH #T #HT1 #HT2
 149   /3 width=3 by cpm_zeta, ex2_intro/
 150 | #n #G #L #U #T1 #T2 #_ #IH #n1 #n2 #H destruct
 151   elim IH [|*: // ] -IH #T #HT1 #HT2
 152   /3 width=3 by cpm_eps, ex2_intro/
 153 | #n #G #L #U1 #U2 #T #HU12 #IH #x1 #n2 #H
 154   elim (plus_inv_S3_sn … H) -H *
 155   [ #H1 #H2 destruct -IH /3 width=4 by cpm_ee, cpm_cast, ex2_intro/
 156   | #n1 #H1 #H2 destruct -HU12
 157     elim (IH n1) [|*: // ] -IH #U #HU1 #HU2
 158     /3 width=3 by cpm_ee, ex2_intro/
 159   ]
 160 | #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ #IH #n1 #n2 #H destruct
 161   elim IH [|*: // ] -IH #T #HT1 #HT2
 162   /4 width=7 by cpm_beta, cpm_appl, cpm_bind, ex2_intro/
 163 | #n #p #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ #IH #HVU2 #n1 #n2 #H destruct
 164   elim IH [|*: // ] -IH #T #HT1 #HT2
 165   /4 width=7 by cpm_theta, cpm_appl, cpm_bind, ex2_intro/
 166 ]
 167 qed-.
 168
 169 lemma cpm_fwd_plus (h) (G) (L):
 170       ∀n1,n2,T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n1+n2] T2 →
 171       ∃∃T. ❪G,L❫ ⊢ T1 ➡[h,n1] T & ❪G,L❫ ⊢ T ➡[h,n2] T2.
 172 /2 width=3 by cpm_fwd_plus_aux/ qed-.