matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_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/cpt_fqu.ma".
  17
  18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
  19
  20 (* Properties with generic slicing for local environments *******************)
  21
  22 lemma cpt_lifts_sn (h) (n) (G):
  23       d_liftable2_sn … lifts (λL. cpt h G L n).
  24 #h #n #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
  25 elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
  26 /3 width=5 by ex2_intro/
  27 qed-.
  28
  29 lemma cpt_lifts_bi (h) (n) (G):
  30       d_liftable2_bi … lifts (λL. cpt 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 lemma cpt_inv_lifts_sn (h) (n) (G):
  37       d_deliftable2_sn … lifts (λL. cpt h G L n).
  38 #h #n #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
  39 elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
  40 /3 width=5 by ex2_intro/
  41 qed-.
  42
  43 lemma cpt_inv_lifts_bi (h) (n) (G):
  44       d_deliftable2_bi … lifts (λL. cpt 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 lemma cpt_delta_drops (h) (n) (G):
  51       ∀L,K,V,i. ⇩*[i] L ≘ K.ⓓV → ∀V2. ❪G,K❫ ⊢ V ⬆[h,n] V2 →
  52       ∀W2. ⇧*[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ⬆[h,n] W2.
  53 #h #n #G #L #K #V #i #HLK #V2 *
  54 /3 width=8 by cpg_delta_drops, ex2_intro/
  55 qed.
  56
  57 lemma cpt_ell_drops (h) (n) (G):
  58       ∀L,K,V,i. ⇩*[i] L ≘ K.ⓛV → ∀V2. ❪G,K❫ ⊢ V ⬆[h,n] V2 →
  59       ∀W2. ⇧*[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ⬆[h,↑n] W2.
  60 #h #n #G #L #K #V #i #HLK #V2 *
  61 /3 width=8 by cpg_ell_drops, ist_succ, ex2_intro/
  62 qed.
  63
  64 (* Advanced inversion lemmas ************************************************)
  65
  66 lemma cpt_inv_atom_sn_drops (h) (n) (I) (G) (L):
  67       ∀X2. ❪G,L❫ ⊢ ⓪[I] ⬆[h,n] X2 →
  68       ∨∨ ∧∧ X2 = ⓪[I] & n = 0
  69        | ∃∃s. X2 = ⋆(⫯[h]s) & I = Sort s & n = 1
  70        | ∃∃K,V,V2,i. ⇩*[i] L ≘ K.ⓓV & ❪G,K❫ ⊢ V ⬆[h,n] V2 & ⇧*[↑i] V2 ≘ X2 & I = LRef i
  71        | ∃∃m,K,V,V2,i. ⇩*[i] L ≘ K.ⓛV & ❪G,K❫ ⊢ V ⬆[h,m] V2 & ⇧*[↑i] V2 ≘ X2 & I = LRef i & n = ↑m.
  72 #h #n #I #G #L #X2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
  73 [ #H1 #H2 destruct
  74   /3 width=1 by or4_intro0, conj/
  75 | #s #H1 #H2 #H3 destruct
  76   /3 width=3 by or4_intro1, ex3_intro/
  77 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
  78   /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/
  79 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
  80   elim (ist_inv_plus_SO_dx … H2) -H2
  81   /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
  82 ]
  83 qed-.
  84
  85 lemma cpt_inv_lref_sn_drops (h) (n) (G) (L) (i):
  86       ∀X2. ❪G,L❫ ⊢ #i ⬆[h,n] X2 →
  87       ∨∨ ∧∧ X2 = #i & n = 0
  88        | ∃∃K,V,V2. ⇩*[i] L ≘ K.ⓓV & ❪G,K❫ ⊢ V ⬆[h,n] V2 & ⇧*[↑i] V2 ≘ X2
  89        | ∃∃m,K,V,V2. ⇩*[i] L ≘ K. ⓛV & ❪G,K❫ ⊢ V ⬆[h,m] V2 & ⇧*[↑i] V2 ≘ X2 & n = ↑m.
  90 #h #n #G #L #i #X2 * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H *
  91 [ #H1 #H2 destruct
  92   /3 width=1 by or3_intro0, conj/
  93 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
  94   /4 width=6 by ex3_3_intro, ex2_intro, or3_intro1/
  95 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
  96   elim (ist_inv_plus_SO_dx … H) -H
  97   /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/
  98 ]
  99 qed-.
 100
 101 (* Advanced forward lemmas **************************************************)
 102
 103 fact cpt_fwd_plus_aux (h) (n) (G) (L):
 104      ∀T1,T2. ❪G,L❫ ⊢ T1 ⬆[h,n] T2 → ∀n1,n2. n1+n2 = n →
 105      ∃∃T. ❪G,L❫ ⊢ T1 ⬆[h,n1] T & ❪G,L❫ ⊢ T ⬆[h,n2] T2.
 106 #h #n #G #L #T1 #T2 #H @(cpt_ind … H) -G -L -T1 -T2 -n
 107 [ #I #G #L #n1 #n2 #H
 108   elim (plus_inv_O3 … H) -H #H1 #H2 destruct
 109   /2 width=3 by ex2_intro/
 110 | #G #L #s #x1 #n2 #H
 111   elim (plus_inv_S3_sn … H) -H *
 112   [ #H1 #H2 destruct /2 width=3 by ex2_intro/
 113   | #n1 #H1 #H elim (plus_inv_O3 … H) -H #H2 #H3 destruct
 114     /2 width=3 by ex2_intro/
 115   ]
 116 | #n #G #K #V1 #V2 #W2 #_ #IH #HVW2 #n1 #n2 #H destruct
 117   elim IH [|*: // ] -IH #V #HV1 #HV2
 118   elim (lifts_total V 𝐔❨↑O❩) #W #HVW
 119   /5 width=11 by cpt_lifts_bi, cpt_delta, drops_refl, drops_drop, ex2_intro/
 120 | #n #G #K #V1 #V2 #W2 #HV12 #IH #HVW2 #x1 #n2 #H
 121   elim (plus_inv_S3_sn … H) -H *
 122   [ #H1 #H2 destruct -IH /3 width=3 by cpt_ell, ex2_intro/
 123   | #n1 #H1 #H2 destruct -HV12
 124     elim (IH n1) [|*: // ] -IH #V #HV1 #HV2
 125     elim (lifts_total V 𝐔❨↑O❩) #W #HVW
 126     /5 width=11 by cpt_lifts_bi, cpt_ell, drops_refl, drops_drop, ex2_intro/
 127   ]
 128 | #n #I #G #K #T2 #U2 #i #_ #IH #HTU2 #n1 #n2 #H destruct
 129   elim IH [|*: // ] -IH #T #HT1 #HT2
 130   elim (lifts_total T 𝐔❨↑O❩) #U #HTU
 131   /5 width=11 by cpt_lifts_bi, cpt_lref, drops_refl, drops_drop, ex2_intro/
 132 | #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
 133   elim IHT [|*: // ] -IHT #T #HT1 #HT2
 134   /3 width=5 by cpt_bind, ex2_intro/
 135 | #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
 136   elim IHT [|*: // ] -IHT #T #HT1 #HT2
 137   /3 width=5 by cpt_appl, ex2_intro/
 138 | #n #G #L #U1 #U2 #T1 #T2 #_ #_ #IHU #IHT #n1 #n2 #H destruct
 139   elim IHU [|*: // ] -IHU #U #HU1 #HU2
 140   elim IHT [|*: // ] -IHT #T #HT1 #HT2
 141   /3 width=5 by cpt_cast, ex2_intro/
 142 | #n #G #L #U1 #U2 #T #HU12 #IH #x1 #n2 #H
 143   elim (plus_inv_S3_sn … H) -H *
 144   [ #H1 #H2 destruct -IH /3 width=4 by cpt_ee, cpt_cast, ex2_intro/
 145   | #n1 #H1 #H2 destruct -HU12
 146     elim (IH n1) [|*: // ] -IH #U #HU1 #HU2
 147     /3 width=3 by cpt_ee, ex2_intro/
 148   ]
 149 ]
 150 qed-.
 151
 152 lemma cpt_fwd_plus (h) (n1) (n2) (G) (L):
 153       ∀T1,T2. ❪G,L❫ ⊢ T1 ⬆[h,n1+n2] T2 →
 154       ∃∃T. ❪G,L❫ ⊢ T1 ⬆[h,n1] T & ❪G,L❫ ⊢ T ⬆[h,n2] T2.
 155 /2 width=3 by cpt_fwd_plus_aux/ qed-.