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,K,V,V2,W2,i.
  53                        ⇩[i] L ≘ K.ⓓV → ❪G,K❫ ⊢ V ➡[h,n] V2 →
  54                        ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ➡[h,n] W2.
  55 #h #n #G #L #K #V #V2 #W2 #i #HLK *
  56 /3 width=8 by cpg_delta_drops, ex2_intro/
  57 qed.
  58
  59 lemma cpm_ell_drops: ∀h,n,G,L,K,V,V2,W2,i.
  60                      ⇩[i] L ≘ K.ⓛV → ❪G,K❫ ⊢ V ➡[h,n] V2 →
  61                      ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ➡[h,↑n] W2.
  62 #h #n #G #L #K #V #V2 #W2 #i #HLK *
  63 /3 width=8 by cpg_ell_drops, isrt_succ, ex2_intro/
  64 qed.
  65
  66 (* Advanced inversion lemmas ************************************************)
  67
  68 lemma cpm_inv_atom1_drops: ∀h,n,I,G,L,T2. ❪G,L❫ ⊢ ⓪[I] ➡[h,n] T2 →
  69                            ∨∨ T2 = ⓪[I] ∧ n = 0
  70                             | ∃∃s. T2 = ⋆(⫯[h]s) & I = Sort s & n = 1
  71                             | ∃∃K,V,V2,i. ⇩[i] L ≘ K.ⓓV & ❪G,K❫ ⊢ V ➡[h,n] V2 &
  72                                           ⇧[↑i] V2 ≘ T2 & I = LRef i
  73                             | ∃∃m,K,V,V2,i. ⇩[i] L ≘ K.ⓛV & ❪G,K❫ ⊢ V ➡[h,m] V2 &
  74                                             ⇧[↑i] V2 ≘ T2 & I = LRef i & n = ↑m.
  75 #h #n #I #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
  76 [ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
  77   /3 width=1 by or4_intro0, conj/
  78 | #s #H1 #H2 #H3 destruct lapply (isrt_inv_01 … Hc) -Hc
  79   /4 width=3 by or4_intro1, ex3_intro, sym_eq/ (**) (* sym_eq *)
  80 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
  81   /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/
  82 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
  83   elim (isrt_inv_plus_SO_dx … Hc) -Hc
  84   /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
  85 ]
  86 qed-.
  87
  88 lemma cpm_inv_lref1_drops: ∀h,n,G,L,T2,i. ❪G,L❫ ⊢ #i ➡[h,n] T2 →
  89                            ∨∨ T2 = #i ∧ n = 0
  90                             | ∃∃K,V,V2. ⇩[i] L ≘ K.ⓓV & ❪G,K❫ ⊢ V ➡[h,n] V2 &
  91                                         ⇧[↑i] V2 ≘ T2
  92                             | ∃∃m,K,V,V2. ⇩[i] L ≘ K. ⓛV & ❪G,K❫ ⊢ V ➡[h,m] V2 &
  93                                           ⇧[↑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,T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 →
 108                                ∀n1,n2. n1+n2 = n →
 109                                ∃∃T. ❪G,L❫ ⊢ T1 ➡[h,n1] T & ❪G,L❫ ⊢ T ➡[h,n2] T2.
 110 #h #n #G #L #T1 #T2 #H @(cpm_ind … H) -G -L -T1 -T2 -n
 111 [ #I #G #L #n1 #n2 #H
 112   elim (plus_inv_O3 … H) -H #H1 #H2 destruct
 113   /2 width=3 by ex2_intro/
 114 | #G #L #s #x1 #n2 #H
 115   elim (plus_inv_S3_sn … H) -H *
 116   [ #H1 #H2 destruct /2 width=3 by ex2_intro/
 117   | #n1 #H1 #H elim (plus_inv_O3 … H) -H #H2 #H3 destruct
 118     /2 width=3 by ex2_intro/
 119   ]
 120 | #n #G #K #V1 #V2 #W2 #_ #IH #HVW2 #n1 #n2 #H destruct
 121   elim IH [|*: // ] -IH #V #HV1 #HV2
 122   elim (lifts_total V 𝐔❨↑O❩) #W #HVW
 123   /5 width=11 by cpm_lifts_bi, cpm_delta, drops_refl, drops_drop, ex2_intro/
 124 | #n #G #K #V1 #V2 #W2 #HV12 #IH #HVW2 #x1 #n2 #H
 125   elim (plus_inv_S3_sn … H) -H *
 126   [ #H1 #H2 destruct -IH /3 width=3 by cpm_ell, ex2_intro/
 127   | #n1 #H1 #H2 destruct -HV12
 128     elim (IH n1) [|*: // ] -IH #V #HV1 #HV2
 129     elim (lifts_total V 𝐔❨↑O❩) #W #HVW
 130     /5 width=11 by cpm_lifts_bi, cpm_ell, drops_refl, drops_drop, ex2_intro/
 131   ]
 132 | #n #I #G #K #T2 #U2 #i #_ #IH #HTU2 #n1 #n2 #H destruct
 133   elim IH [|*: // ] -IH #T #HT1 #HT2
 134   elim (lifts_total T 𝐔❨↑O❩) #U #HTU
 135   /5 width=11 by cpm_lifts_bi, cpm_lref, drops_refl, drops_drop, ex2_intro/
 136 | #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
 137   elim IHT [|*: // ] -IHT #T #HT1 #HT2
 138   /3 width=5 by cpm_bind, ex2_intro/
 139 | #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
 140   elim IHT [|*: // ] -IHT #T #HT1 #HT2
 141   /3 width=5 by cpm_appl, ex2_intro/
 142 | #n #G #L #U1 #U2 #T1 #T2 #_ #_ #IHU #IHT #n1 #n2 #H destruct
 143   elim IHU [|*: // ] -IHU #U #HU1 #HU2
 144   elim IHT [|*: // ] -IHT #T #HT1 #HT2
 145   /3 width=5 by cpm_cast, ex2_intro/
 146 | #n #G #K #V #U1 #T1 #T2 #HTU1 #_ #IH #n1 #n2 #H destruct
 147   elim IH [|*: // ] -IH #T #HT1 #HT2
 148   /3 width=3 by cpm_zeta, ex2_intro/
 149 | #n #G #L #U #T1 #T2 #_ #IH #n1 #n2 #H destruct
 150   elim IH [|*: // ] -IH #T #HT1 #HT2
 151   /3 width=3 by cpm_eps, ex2_intro/
 152 | #n #G #L #U1 #U2 #T #HU12 #IH #x1 #n2 #H
 153   elim (plus_inv_S3_sn … H) -H *
 154   [ #H1 #H2 destruct -IH /3 width=4 by cpm_ee, cpm_cast, ex2_intro/
 155   | #n1 #H1 #H2 destruct -HU12
 156     elim (IH n1) [|*: // ] -IH #U #HU1 #HU2
 157     /3 width=3 by cpm_ee, ex2_intro/
 158   ]
 159 | #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ #IH #n1 #n2 #H destruct
 160   elim IH [|*: // ] -IH #T #HT1 #HT2
 161   /4 width=7 by cpm_beta, cpm_appl, cpm_bind, ex2_intro/
 162 | #n #p #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ #IH #HVU2 #n1 #n2 #H destruct
 163   elim IH [|*: // ] -IH #T #HT1 #HT2
 164   /4 width=7 by cpm_theta, cpm_appl, cpm_bind, ex2_intro/
 165 ]
 166 qed-.
 167
 168 lemma cpm_fwd_plus (h) (G) (L): ∀n1,n2,T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n1+n2] T2 →
 169                                 ∃∃T. ❪G,L❫ ⊢ T1 ➡[h,n1] T & ❪G,L❫ ⊢ T ➡[h,n2] T2.
 170 /2 width=3 by cpm_fwd_plus_aux/ qed-.