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 "basic_2/computation/cprs_cprs.ma".
16 include "basic_2/computation/lcprs_lcprs.ma".
18 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
20 (* Properties exploiting context-senstive computation on local environments *)
22 (* Basic_1: was just: pr3_pr3_pr3_t *)
23 lemma lcprs_cprs_trans: ∀L1,L2. L1 ⊢ ➡* L2 →
24 ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
25 #L1 #L2 #HL12 @(lcprs_ind … HL12) -L2 // /3 width=3/
28 (* Advanced inversion lemmas ************************************************)
30 (* Basic_1: was pr3_gen_abbr *)
31 lemma cprs_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡* U2 →
32 (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
35 ∃∃U. ⇧[0, 1] U2 ≡ U & L. ⓓV1 ⊢ T1 ➡* U.
36 #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
38 [ #V0 #T0 #HV10 #HT10 #H destruct
39 elim (cpr_inv_abbr1 … HU02) -HU02 *
40 [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct
41 lapply (cpr_intro … HV0 … HV2) -HV2 #HV02
42 lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02
43 lapply (lcprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/
45 elim (lift_total U2 0 1) #U0 #HU20
46 lapply (cpr_lift (L.ⓓV1) … HT20 … HU20 HTU2) -T2 /2 width=1/ /4 width=5/
49 elim (lift_total U2 0 1) #U #HU2
50 lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=5/