matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cpxs.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 "ground/xoa/ex_4_5.ma".
  16 include "basic_2/rt_transition/cpx_lsubr.ma".
  17 include "basic_2/rt_computation/cpxs.ma".
  18
  19 (* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************)
  20
  21 (* Main properties **********************************************************)
  22
  23 theorem cpxs_trans (G) (L):
  24         Transitive … (cpxs G L).
  25 normalize /2 width=3 by trans_TC/ qed-.
  26
  27 theorem cpxs_bind (G) (L):
  28         ∀p,I,V1,V2,T1,T2. ❪G,L.ⓑ[I]V1❫ ⊢ T1 ⬈* T2 →
  29         ❪G,L❫ ⊢ V1 ⬈* V2 →
  30         ❪G,L❫ ⊢ ⓑ[p,I]V1.T1 ⬈* ⓑ[p,I]V2.T2.
  31 #G #L #p #I #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2
  32 /3 width=5 by cpxs_trans, cpxs_bind_dx/
  33 qed.
  34
  35 theorem cpxs_flat (G) (L):
  36         ∀I,V1,V2,T1,T2. ❪G,L❫ ⊢ T1 ⬈* T2 →
  37         ❪G,L❫ ⊢ V1 ⬈* V2 →
  38         ❪G,L❫ ⊢ ⓕ[I]V1.T1 ⬈* ⓕ[I]V2.T2.
  39 #G #L #I #V1 #V2 #T1 #T2 #HT12 #H @(cpxs_ind … H) -V2
  40 /3 width=5 by cpxs_trans, cpxs_flat_dx/
  41 qed.
  42
  43 theorem cpxs_beta_rc (G) (L):
  44         ∀p,V1,V2,W1,W2,T1,T2.
  45         ❪G,L❫ ⊢ V1 ⬈ V2 → ❪G,L.ⓛW1❫ ⊢ T1 ⬈* T2 → ❪G,L❫ ⊢ W1 ⬈* W2 →
  46         ❪G,L❫ ⊢ ⓐV1.ⓛ[p]W1.T1 ⬈* ⓓ[p]ⓝW2.V2.T2.
  47 #G #L #p #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cpxs_ind … H) -W2
  48 /4 width=5 by cpxs_trans, cpxs_beta_dx, cpxs_bind_dx, cpx_pair_sn/
  49 qed.
  50
  51 theorem cpxs_beta (G) (L):
  52         ∀p,V1,V2,W1,W2,T1,T2.
  53         ❪G,L.ⓛW1❫ ⊢ T1 ⬈* T2 → ❪G,L❫ ⊢ W1 ⬈* W2 → ❪G,L❫ ⊢ V1 ⬈* V2 →
  54         ❪G,L❫ ⊢ ⓐV1.ⓛ[p]W1.T1 ⬈* ⓓ[p]ⓝW2.V2.T2.
  55 #G #L #p #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cpxs_ind … H) -V2
  56 /4 width=5 by cpxs_trans, cpxs_beta_rc, cpxs_bind_dx, cpx_flat/
  57 qed.
  58
  59 theorem cpxs_theta_rc (G) (L):
  60         ∀p,V1,V,V2,W1,W2,T1,T2.
  61         ❪G,L❫ ⊢ V1 ⬈ V → ⇧[1] V ≘ V2 →
  62         ❪G,L.ⓓW1❫ ⊢ T1 ⬈* T2 → ❪G,L❫ ⊢ W1 ⬈* W2 →
  63         ❪G,L❫ ⊢ ⓐV1.ⓓ[p]W1.T1 ⬈* ⓓ[p]W2.ⓐV2.T2.
  64 #G #L #p #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H @(cpxs_ind … H) -W2
  65 /3 width=5 by cpxs_trans, cpxs_theta_dx, cpxs_bind_dx/
  66 qed.
  67
  68 theorem cpxs_theta (G) (L):
  69         ∀p,V1,V,V2,W1,W2,T1,T2.
  70         ⇧[1] V ≘ V2 → ❪G,L❫ ⊢ W1 ⬈* W2 →
  71         ❪G,L.ⓓW1❫ ⊢ T1 ⬈* T2 → ❪G,L❫ ⊢ V1 ⬈* V →
  72         ❪G,L❫ ⊢ ⓐV1.ⓓ[p]W1.T1 ⬈* ⓓ[p]W2.ⓐV2.T2.
  73 #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1
  74 /3 width=5 by cpxs_trans, cpxs_theta_rc, cpxs_flat_dx/
  75 qed.
  76
  77 (* Advanced inversion lemmas ************************************************)
  78
  79 lemma cpxs_inv_appl1 (G) (L):
  80       ∀V1,T1,U2. ❪G,L❫ ⊢ ⓐV1.T1 ⬈* U2 →
  81       ∨∨ ∃∃V2,T2. ❪G,L❫ ⊢ V1 ⬈* V2 & ❪G,L❫ ⊢ T1 ⬈* T2 & U2 = ⓐV2.T2
  82        | ∃∃p,W,T. ❪G,L❫ ⊢ T1 ⬈* ⓛ[p]W.T & ❪G,L❫ ⊢ ⓓ[p]ⓝW.V1.T ⬈* U2
  83        | ∃∃p,V0,V2,V,T. ❪G,L❫ ⊢ V1 ⬈* V0 & ⇧[1] V0 ≘ V2 & ❪G,L❫ ⊢ T1 ⬈* ⓓ[p]V.T & ❪G,L❫ ⊢ ⓓ[p]V.ⓐV2.T ⬈* U2.
  84 #G #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5 by or3_intro0, ex3_2_intro/ ]
  85 #U #U2 #_ #HU2 * *
  86 [ #V0 #T0 #HV10 #HT10 #H destruct
  87   elim (cpx_inv_appl1 … HU2) -HU2 *
  88   [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5 by cpxs_strap1, or3_intro0, ex3_2_intro/
  89   | #p #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
  90     lapply (cpxs_strap1 … HV10 … HV02) -V0 #HV12
  91     lapply (lsubr_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2
  92     /5 width=5 by cpxs_bind, cpxs_flat_dx, cpx_cpxs, lsubr_beta, ex2_3_intro, or3_intro1/
  93   | #p #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
  94     /5 width=10 by cpxs_flat_sn, cpxs_bind_dx, cpxs_strap1, ex4_5_intro, or3_intro2/
  95   ]
  96 | /4 width=9 by cpxs_strap1, or3_intro1, ex2_3_intro/
  97 | /4 width=11 by cpxs_strap1, or3_intro2, ex4_5_intro/
  98 ]
  99 qed-.