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 (n) (h) (G):
  22                       ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[n, h] T2 →
  23                       ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2.
  24 #n #h #G #L2 #T1 #T2 #HT12 #L1 #H
  25 @(lprs_ind_sn … H) -L1 /2 width=3 by lpr_cpms_trans/
  26 qed-.
  27
  28 lemma lprs_cpm_trans (n) (h) (G):
  29                      ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[n, h] T2 →
  30                      ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2.
  31 /3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-.
  32
  33 (* Basic_2A1: includes cprs_bind2 *)
  34 lemma cpms_bind_dx (n) (h) (G) (L):
  35                    ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 →
  36                    ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[n, h] T2 →
  37                    ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n, h] ⓑ{p,I}V2.T2.
  38 /4 width=5 by lprs_cpms_trans, lprs_pair, cpms_bind/ qed.
  39
  40 (* Inversion lemmas with t-bound context-sensitive rt-computarion for terms *)
  41
  42 (* Basic_1: was: pr3_gen_abst *)
  43 (* Basic_2A1: includes: cprs_inv_abst1 *)
  44 (* Basic_2A1: uses: scpds_inv_abst1 *)
  45 lemma cpms_inv_abst_sn (n) (h) (G) (L):
  46                        ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡*[n, h] X2 →
  47                        ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[n, h] T2 &
  48                                 X2 = ⓛ{p}V2.T2.
  49 #n #h #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 (* Basic_2A1: includes: cprs_inv_abst *)
  57 lemma cpms_inv_abst_bi (n) (h) (G) (L):
  58                        ∀p,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[n, h] ⓛ{p}W2.T2 →
  59                        ∧∧ ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2.
  60 #n #h #G #L #p #W1 #W2 #T1 #T2 #H
  61 elim (cpms_inv_abst_sn … H) -H #W #T #HW1 #HT1 #H destruct
  62 /2 width=1 by conj/
  63 qed-.
  64
  65 (* Basic_1: was pr3_gen_abbr *)
  66 (* Basic_2A1: includes: cprs_inv_abbr1 *)
  67 lemma cpms_inv_abbr_sn (n) (h) (G) (L):
  68                        ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡*[n, h] X2 →
  69                        ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n, h] T2 & X2 = ⓓ{p}V2.T2
  70                         | ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n ,h] T2 & ⬆*[1] X2 ≘ T2 & p = Ⓣ.
  71 #n #h #G #L #p #V1 #T1 #X2 #H
  72 @(cpms_ind_dx … H) -X2 -n /3 width=5 by ex3_2_intro, or_introl/
  73 #n1 #n2 #X #X2 #_ * *
  74 [ #V #T #HV1 #HT1 #H #HX2 destruct
  75   elim (cpm_inv_abbr1 … HX2) -HX2 *
  76   [ #V2 #T2 #HV2 #HT2 #H destruct
  77     /6 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro, or_introl/
  78   | #T2 #HT2 #HXT2 #Hp
  79     /6 width=7 by lprs_cpm_trans, lprs_pair, cpms_trans, ex3_intro, or_intror/
  80   ]
  81 | #T #HT1 #HXT #Hp #HX2
  82   elim (cpm_lifts_sn … HX2 (Ⓣ) … (L.ⓓV1) … HXT) -X
  83   /4 width=3 by cpms_step_dx, drops_refl, drops_drop, ex3_intro, or_intror/
  84 ]
  85 qed-.
  86
  87 (* Basic_2A1: uses: scpds_inv_abbr_abst *)
  88 lemma cpms_inv_abbr_abst (n) (h) (G) (L):
  89                          ∀p1,p2,V1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓓ{p1}V1.T1 ➡*[n, h] ⓛ{p2}W2.T2 →
  90                          ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n, h] T & ⬆*[1] ⓛ{p2}W2.T2 ≘ T & p1 = Ⓣ.
  91 #n #h #G #L #p1 #p2 #V1 #W2 #T1 #T2 #H
  92 elim (cpms_inv_abbr_sn … H) -H *
  93 [ #V #T #_ #_ #H destruct
  94 | /2 width=3 by ex3_intro/
  95 ]
  96 qed-.