1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
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".
19 (* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************)
21 (* Main properties **********************************************************)
23 theorem cpxs_trans (G) (L):
24 Transitive … (cpxs G L).
25 normalize /2 width=3 by trans_TC/ qed-.
27 theorem cpxs_bind (G) (L):
28 ∀p,I,V1,V2,T1,T2. ❨G,L.ⓑ[I]V1❩ ⊢ T1 ⬈* T2 →
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/
35 theorem cpxs_flat (G) (L):
36 ∀I,V1,V2,T1,T2. ❨G,L❩ ⊢ T1 ⬈* T2 →
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/
43 theorem cpxs_beta_rc (G) (L):
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/
51 theorem cpxs_beta (G) (L):
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/
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/
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/
77 (* Advanced inversion lemmas ************************************************)
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/ ]
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/
96 | /4 width=9 by cpxs_strap1, or3_intro1, ex2_3_intro/
97 | /4 width=11 by cpxs_strap1, or3_intro2, ex4_5_intro/