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/unfold/ltpss_ltpss.ma".
16 include "Basic_2/reducibility/cpr.ma".
18 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
20 (* Advanced inversion lemmas ************************************************)
22 (* Basic_1: was pr2_gen_abbr *)
23 lemma cpr_inv_abbr1: ∀L,V1,T1,U2. L ⊢ ⓓV1. T1 ➡ U2 →
24 (∃∃V2,T2,T. L ⊢ V1 ➡ V2 & L. ⓓV2 ⊢ T1 ➡ T2 &
25 L. ⓓV2 ⊢ T [1, |L|] ▶* T2 &
28 ∃∃T. ⇧[0,1] T ≡ T1 & L ⊢ T ➡ U2.
29 #L #V1 #T1 #Y * #X #H1 #H2
30 elim (tpr_inv_abbr1 … H1) -H1 *
31 [ #V #T0 #T #HV1 #HT10 #HT0 #H destruct
32 elim (tpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct
33 lapply (tps_lsubs_conf … HT0 (L. ⓓV) ?) -HT0 /2 width=1/ #HT0
34 elim (ltpss_tps_conf … HT0 (L. ⓓV2) 1 (|L|) ?) -HT0 /2 width=1/ #V0 #HV20 #HV0
35 lapply (tpss_weak_all … HV20) -HV20 #HV20
36 lapply (tpss_lsubs_conf … HV0 (L. ⓓV2) ?) -HV0 /2 width=1/ #HV0
37 elim (tpss_conf_eq … HT2 … HV0) -T #T3 #HT23 #HVT3
38 lapply (tpss_weak_all … HVT3) -HVT3 #HVT3
39 lapply (tpss_trans_eq … HV20 … HVT3) -V0 /4 width=7/
44 (* Properties concerning partial unfold on local environments ***************)
46 lemma ltpss_cpr_trans: ∀L1,L2,d,e. L1 [d, e] ▶* L2 →
47 ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
48 #L1 #L2 #d #e #HL12 #T1 #T2 *
49 lapply (ltpss_weak_all … HL12)
50 <(ltpss_fwd_length … HL12) -HL12 /3 width=5/