matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.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_computation/lprs_lpr.ma".
  16
  17 (* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
  18
  19 (* Properties with t-bound context-sensitive rt-computarion for terms *******)
  20
  21 lemma lprs_cpms_trans (h) (n) (G) (T1:term) (T2:term):
  22       ∀L2. ❪G,L2❫ ⊢ T1 ➡*[h,n] T2 →
  23       ∀L1. ❪G,L1❫ ⊢ ➡*[h,0] L2 → ❪G,L1❫ ⊢ T1 ➡*[h,n] T2.
  24 #h #n #G #T1 #T2 #L2 #HT12 #L1 #H
  25 @(lprs_ind_sn … H) -L1
  26 /2 width=3 by lpr_cpms_trans/
  27 qed-.
  28
  29 lemma lprs_cpm_trans (h) (n) (G) (T1:term) (T2:term):
  30       ∀L2. ❪G,L2❫ ⊢ T1 ➡[h,n] T2 →
  31       ∀L1. ❪G,L1❫ ⊢ ➡*[h,0] L2 → ❪G,L1❫ ⊢ T1 ➡*[h,n] T2.
  32 /3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-.
  33
  34 (* Basic_2A1: includes cprs_bind2 *)
  35 lemma cpms_bind_alt (h) (n) (G) (L):
  36       ∀V1,V2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 →
  37       ∀I,T1,T2. ❪G,L.ⓑ[I]V2❫ ⊢ T1 ➡*[h,n] T2 →
  38       ∀p. ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ➡*[h,n] ⓑ[p,I]V2.T2.
  39 /4 width=5 by lprs_cpms_trans, lprs_pair, cpms_bind/ qed.
  40
  41 (* Inversion lemmas with t-bound context-sensitive rt-computarion for terms *)
  42
  43 (* Basic_1: was: pr3_gen_abst *)
  44 (* Basic_2A1: includes: cprs_inv_abst1 *)
  45 (* Basic_2A1: uses: scpds_inv_abst1 *)
  46 lemma cpms_inv_abst_sn (h) (n) (G) (L):
  47       ∀p,V1,T1,X2. ❪G,L❫ ⊢ ⓛ[p]V1.T1 ➡*[h,n] X2 →
  48       ∃∃V2,T2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 & ❪G,L.ⓛV1❫ ⊢ T1 ➡*[h,n] T2 & X2 = ⓛ[p]V2.T2.
  49 #h #n #G #L #p #V1 #T1 #X2 #H
  50 @(cpms_ind_dx … H) -X2 /2 width=5 by ex3_2_intro/
  51 #n1 #n2 #X #X2 #_ * #V #T #HV1 #HT1 #H1 #H2 destruct
  52 elim (cpm_inv_abst1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H2 destruct
  53 /5 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro/
  54 qed-.
  55
  56 lemma cpms_inv_abst_sn_cprs (h) (n) (p) (G) (L) (W):
  57       ∀T,X. ❪G,L❫ ⊢ ⓛ[p]W.T ➡*[h,n] X →
  58       ∃∃U. ❪G,L.ⓛW❫⊢ T ➡*[h,n] U & ❪G,L❫ ⊢ ⓛ[p]W.U ➡*[h,0] X.
  59 #h #n #p #G #L #W #T #X #H
  60 elim (cpms_inv_abst_sn … H) -H #W0 #U #HW0 #HTU #H destruct
  61 @(ex2_intro … HTU) /2 width=1 by cpms_bind/
  62 qed-.
  63
  64 (* Basic_2A1: includes: cprs_inv_abst *)
  65 lemma cpms_inv_abst_bi (h) (n) (p1) (p2) (G) (L):
  66       ∀W1,W2,T1,T2. ❪G,L❫ ⊢ ⓛ[p1]W1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
  67       ∧∧ p1 = p2 & ❪G,L❫ ⊢ W1 ➡*[h,0] W2 & ❪G,L.ⓛW1❫ ⊢ T1 ➡*[h,n] T2.
  68 #h #n #p1 #p2 #G #L #W1 #W2 #T1 #T2 #H
  69 elim (cpms_inv_abst_sn … H) -H #W #T #HW1 #HT1 #H destruct
  70 /2 width=1 by and3_intro/
  71 qed-.
  72
  73 (* Basic_1: was pr3_gen_abbr *)
  74 (* Basic_2A1: includes: cprs_inv_abbr1 *)
  75 lemma cpms_inv_abbr_sn_dx (h) (n) (G) (L):
  76       ∀p,V1,T1,X2. ❪G,L❫ ⊢ ⓓ[p]V1.T1 ➡*[h,n] X2 →
  77       ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ➡*[h,0] V2 & ❪G,L.ⓓV1❫ ⊢ T1 ➡*[h,n] T2 & X2 = ⓓ[p]V2.T2
  78        | ∃∃T2. ❪G,L.ⓓV1❫ ⊢ T1 ➡*[h,n] T2 & ⇧[1] X2 ≘ T2 & p = Ⓣ.
  79 #h #n #G #L #p #V1 #T1 #X2 #H
  80 @(cpms_ind_dx … H) -X2 -n /3 width=5 by ex3_2_intro, or_introl/
  81 #n1 #n2 #X #X2 #_ * *
  82 [ #V #T #HV1 #HT1 #H #HX2 destruct
  83   elim (cpm_inv_abbr1 … HX2) -HX2 *
  84   [ #V2 #T2 #HV2 #HT2 #H destruct
  85     /6 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro, or_introl/
  86   | #T2 #HT2 #HTX2 #Hp -V
  87     elim (cpm_lifts_sn … HTX2 (Ⓣ) … (L.ⓓV1) … HT2) -T2 [| /3 width=3 by drops_refl, drops_drop/ ] #X #HX2 #HTX
  88     /4 width=3 by cpms_step_dx, ex3_intro, or_intror/
  89   ]
  90 | #T #HT1 #HXT #Hp #HX2
  91   elim (cpm_lifts_sn … HX2 (Ⓣ) … (L.ⓓV1) … HXT) -X
  92   /4 width=3 by cpms_step_dx, drops_refl, drops_drop, ex3_intro, or_intror/
  93 ]
  94 qed-.
  95
  96 (* Basic_2A1: uses: scpds_inv_abbr_abst *)
  97 lemma cpms_inv_abbr_abst (h) (n) (G) (L):
  98       ∀p1,p2,V1,W2,T1,T2. ❪G,L❫ ⊢ ⓓ[p1]V1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
  99       ∃∃T. ❪G,L.ⓓV1❫ ⊢ T1 ➡*[h,n] T & ⇧[1] ⓛ[p2]W2.T2 ≘ T & p1 = Ⓣ.
 100 #h #n #G #L #p1 #p2 #V1 #W2 #T1 #T2 #H
 101 elim (cpms_inv_abbr_sn_dx … H) -H *
 102 [ #V #T #_ #_ #H destruct
 103 | /2 width=3 by ex3_intro/
 104 ]
 105 qed-.