matita/matita/contribs/lambdadelta/basic_2A/computation/scpds_scpds.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_2A/unfold/lstas_da.ma".
  16 include "basic_2A/computation/lprs_cprs.ma".
  17 include "basic_2A/computation/cpxs_cpxs.ma".
  18 include "basic_2A/computation/scpds.ma".
  19
  20 (* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************)
  21
  22 (* Advanced properties ******************************************************)
  23
  24 lemma scpds_strap2: ∀h,g,G,L,T1,T,T2,d1,d. ⦃G, L⦄ ⊢ T1 ▪[h, g] d1+1 →
  25                     ⦃G, L⦄ ⊢ T1 •*[h, 1] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, d] T2 →
  26                     ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d+1] T2.
  27 #h #g #G #L #T1 #T #T2 #d1 #d #Hd1 #HT1 *
  28 #T0 #d0 #Hd0 #HTd0 #HT0 #HT02
  29 lapply (lstas_da_conf … HT1 … Hd1) <minus_plus_m_m #HTd1
  30 lapply (da_mono … HTd0 … HTd1) -HTd0 -HTd1 #H destruct
  31 lapply (lstas_trans … HT1 … HT0) -T >commutative_plus
  32 /3 width=6 by le_S_S, ex4_2_intro/
  33 qed.
  34
  35 lemma scpds_cprs_trans: ∀h,g,G,L,T1,T,T2,d.
  36                         ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d] T2.
  37 #h #g #G #L #T1 #T #T2 #d * /3 width=8 by cprs_trans, ex4_2_intro/
  38 qed-.
  39
  40 lemma lstas_scpds_trans: ∀h,g,G,L,T1,T,T2,d1,d2,d.
  41                          d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] d1 →
  42                          ⦃G, L⦄ ⊢ T1 •*[h, d2] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, d] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d2+d] T2.
  43 #h #g #G #L #T1 #T #T2 #d1 #d2 #d #Hd21 #HTd1 #HT1 * #T0 #d0 #Hd0 #HTd0 #HT0 #HT02
  44 lapply (lstas_da_conf … HT1 … HTd1) #HTd12
  45 lapply (da_mono … HTd12 … HTd0) -HTd12 -HTd0 #H destruct
  46 lapply (le_minus_to_plus_r … Hd21 Hd0) -Hd21 -Hd0
  47 /3 width=7 by lstas_trans, ex4_2_intro/
  48 qed-.
  49
  50 (* Advanced inversion lemmas ************************************************)
  51
  52 lemma scpds_inv_abst1: ∀h,g,a,G,L,V1,T1,U2,d. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, g, d] U2 →
  53                        ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, g, d] T2 &
  54                                 U2 = ⓛ{a}V2.T2.
  55 #h #g #a #G #L #V1 #T1 #U2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
  56 lapply (da_inv_bind … Hd1) -Hd1 #Hd1
  57 elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
  58 elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
  59 /3 width=6 by ex4_2_intro, ex3_2_intro/
  60 qed-.
  61
  62 lemma scpds_inv_abbr_abst: ∀h,g,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, g, d] ⓛ{a2}W2.T2 →
  63                            ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, g, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true.
  64 #h #g #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
  65 lapply (da_inv_bind … Hd1) -Hd1 #Hd1
  66 elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
  67 elim (cprs_inv_abbr1 … H2) -H2 *
  68 [ #V2 #U2 #HV12 #HU12 #H destruct
  69 | /3 width=6 by ex4_2_intro, ex3_intro/
  70 ]
  71 qed-.
  72
  73 lemma scpds_inv_lstas_eq: ∀h,g,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d] T2 →
  74                           ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d] T → ⦃G, L⦄ ⊢ T ➡* T2.
  75 #h #g #G #L #T1 #T2 #d2 *
  76 #T0 #d1 #_ #_ #HT10 #HT02 #T #HT1
  77 lapply (lstas_mono … HT10 … HT1) #H destruct //
  78 qed-.
  79
  80 (* Advanced forward lemmas **************************************************)
  81
  82 lemma scpds_fwd_cpxs: ∀h,g,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, d] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
  83 #h #g #G #L #T1 #T2 #d * /3 width=5 by cpxs_trans, lstas_cpxs, cprs_cpxs/
  84 qed-.
  85
  86 (* Main properties **********************************************************)
  87
  88 theorem scpds_conf_eq: ∀h,g,G,L,T0,T1,d. ⦃G, L⦄ ⊢ T0 •*➡*[h, g, d] T1 →
  89                        ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, g, d] T2 →
  90                        ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
  91 #h #g #G #L #T0 #T1 #d0 * #U1 #d1 #_ #_ #H1 #HUT1 #T2 * #U2 #d2 #_ #_ #H2 #HUT2 -d1 -d2
  92 lapply (lstas_mono … H1 … H2) #H destruct -h -d0 /2 width=3 by cprs_conf/
  93 qed-.