(**************************************************************************)
include "basic_2/reducibility/ltpr_tps.ma".
-include "basic_2/reducibility/cpr_ltpss.ma".
+include "basic_2/reducibility/cpr_ltpsss.ma".
include "basic_2/reducibility/lcpr.ma".
include "basic_2/computation/cprs.ma".
(* v GNU General Public License Version 2 *)
(* *)
(**************************************************************************)
-(*
+
include "basic_2/reducibility/lcpr_lcpr.ma".
-*)
include "basic_2/computation/lcprs_cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
(* Advanced properties ******************************************************)
-axiom lcprs_strip: ∀L,L1. L ⊢ ➡* L1 → ∀L2. L ⊢ ➡ L2 →
+lemma lcprs_strip: ∀L,L1. L ⊢ ➡* L1 → ∀L2. L ⊢ ➡ L2 →
∃∃L0. L1 ⊢ ➡ L0 & L2 ⊢ ➡* L0.
-(*
/3 width=3/ qed.
-*)
+
(* Main properties **********************************************************)
+theorem lcprs_conf: ∀L,L1. L ⊢ ➡* L1 → ∀L2. L ⊢ ➡* L2 →
+ ∃∃L0. L1 ⊢ ➡* L0 & L2 ⊢ ➡* L0.
+/3 width=3/ qed.
+
theorem lcprs_trans: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ➡* L2 → L1 ⊢ ➡* L2.
/2 width=3/ qed.
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss_tpss.ma".
+include "basic_2/unfold/ltpss_ltpss.ma".
include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/ltpsss.ma".
+include "basic_2/reducibility/cpr_ltpss.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Properties on iterated partial unfold on local environments **************)
+
+lemma ltpsss_cpr_trans: ∀L1,L2,d,e. L1 [d, e] ▶** L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
+#L1 #L2 #d #e #HL12 #T1 #T2 #HT12 @(ltpsss_ind_dx … HL12) -L1 // /2 width=5/
+qed.
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss.ma".
+include "basic_2/unfold/ltpsss.ma".
include "basic_2/reducibility/ltpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
definition lcpr: relation lenv ≝
- λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶* L2
+ λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶** L2
.
interpretation
(* Basic inversion lemmas ***************************************************)
lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆.
-#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 //
+#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpsss_inv_atom1 … HL2) -HL2 //
qed-.
(* *)
(**************************************************************************)
-include "basic_2/static/aaa_ltpss.ma".
+include "basic_2/static/aaa_ltpsss.ma".
include "basic_2/reducibility/ltpr_aaa.ma".
include "basic_2/reducibility/cpr.ma".
include "basic_2/reducibility/lcpr.ma".
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/unfold/ltpsss_ltpsss.ma".
include "basic_2/reducibility/cpr.ma".
include "basic_2/reducibility/lcpr.ma".
lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 →
∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2.
#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
-<(ltpss_fwd_length … HL2) /4 width=5/
+<(ltpsss_fwd_length … HL2) /4 width=5/
qed.
(* *)
(**************************************************************************)
-include "basic_2/reducibility/ltpr_ltpss.ma".
+include "basic_2/unfold/ltpsss_ltpsss.ma".
+include "basic_2/reducibility/ltpr_ltpsss.ma".
include "basic_2/reducibility/ltpr_ltpr.ma".
include "basic_2/reducibility/lcpr.ma".
lapply (ltpr_fwd_length … HK01) #H
>(ltpr_fwd_length … HK02) in H; #H
elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2
-lapply (ltpss_fwd_length … HKL1) #H1
-lapply (ltpss_fwd_length … HKL2) #H2
+lapply (ltpsss_fwd_length … HKL1) #H1
+lapply (ltpsss_fwd_length … HKL2) #H2
>H1 in HKL1 H; -H1 #HKL1
>H2 in HKL2; -H2 #HKL2 #H
-elim (ltpr_ltpss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
-elim (ltpr_ltpss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
-elim (ltpss_conf … HK1 … HK2) -K #K #HK1 #HK2
+elim (ltpr_ltpsss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
+elim (ltpr_ltpsss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
+elim (ltpsss_conf … HK1 … HK2) -K #K #HK1 #HK2
lapply (ltpr_fwd_length … HLK1) #H1
lapply (ltpr_fwd_length … HLK2) #H2
/3 width=5/
(* *)
(**************************************************************************)
-include "basic_2/static/aaa_ltps.ma".
+include "basic_2/static/aaa_ltpss.ma".
include "basic_2/static/lsuba_aaa.ma".
include "basic_2/reducibility/ltpr_ldrop.ma".
(* Properties concerning parallel unfold on local environments **************)
-lemma ltpr_ltps_conf: ∀L1,K1,d,e. L1 [d, e] ▶ K1 → ∀L2. L1 ➡ L2 →
- ∃∃K2. L2 [d, e] ▶* K2 & K1 ➡ K2.
+lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 [d, e] ▶* K1 → ∀L2. L1 ➡ L2 →
+ ∃∃K2. L2 [d, e] ▶* K2 & K1 ➡ K2.
#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
[ /2 width=3/
| #L1 #I #V1 #X #H
| #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H
elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
- elim (tpr_tps_ltpr … HV12 … HVW1 … HK12) -V1 /3 width=5/
+ elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
| #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H
elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
- elim (tpr_tps_ltpr … HV12 … HVW1 … HK12) -V1 /3 width=5/
+ elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
]
qed.
-
-lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 [d, e] ▶* K1 → ∀L2. L1 ➡ L2 →
- ∃∃K2. L2 [d, e] ▶* K2 & K1 ➡ K2.
-#L1 #K1 #d #e #H @(ltpss_ind … H) -K1 /2 width=3/
-#K #K1 #_ #HK1 #IHK #L2 #HL12
-elim (IHK … HL12) -L1 #K2 #HLK2 #HK2
-elim (ltpr_ltps_conf … HK1 … HK2) -K #K #HK2 #HK1
-lapply (ltpss_trans_eq … HLK2 HK2) -K2 /2 width=3/
-qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/ltpsss.ma".
+include "basic_2/reducibility/ltpr_ltpss.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* Properties on iterated parallel unfold on local environments *************)
+
+lemma ltpr_ltpsss_conf: ∀L1,K1,d,e. L1 [d, e] ▶** K1 → ∀L2. L1 ➡ L2 →
+ ∃∃K2. L2 [d, e] ▶** K2 & K1 ➡ K2.
+#L1 #K1 #d #e #H @(ltpsss_ind … H) -K1 /2 width=3/
+#K #K1 #_ #HK1 #IHK #L2 #HL12
+elim (IHK … HL12) -L1 #K2 #HLK2 #HK2
+elim (ltpr_ltpss_conf … HK1 … HK2) -K /3 width=3/
+qed.
elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2
lapply (tps_lsubs_conf … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2
elim (ltpss_tps_conf … HTT2 (L2. ⓑ{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
- lapply (tpss_lsubs_conf … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
- lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
+ lapply (tps_lsubs_conf … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
lapply (tpss_lsubs_conf … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/substitution/ltps_ldrop.ma".
-include "basic_2/static/aaa_lift.ma".
-
-(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
-
-(* Properties about parallel substitution ***********************************)
-
-(* Note: lemma 500 *)
-lemma aaa_ltps_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶ L2 →
- ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A.
-#L1 #T1 #A #H elim H -L1 -T1 -A
-[ #L1 #k #L2 #d #e #_ #T2 #H
- >(tps_inv_sort1 … H) -H //
-| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #L2 #d #e #HL12 #T2 #H
- elim (tps_inv_lref1 … H) -H
- [ #H destruct
- elim (lt_or_ge i d) #Hdi
- [ elim (ltps_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
- elim (ltps_inv_tps11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct
- /3 width=8/
- | elim (lt_or_ge i (d + e)) #Hide
- [ elim (ltps_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
- elim (ltps_inv_tps21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct
- /3 width=8/
- | -Hdi
- lapply (ltps_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide #HLK2
- /3 width=8/
- ]
- ]
- | * #K2 #V2 #Hdi #Hide #HLK2 #HVT2
- elim (ltps_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
- elim (ltps_inv_tps21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct
- lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /3 width=7/
- ]
-| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
- elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/
-| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
- elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/
-| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
- elim (tps_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
-| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
- elim (tps_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
-]
-qed.
-
-lemma aaa_ltps_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2,d,e. L1 [d, e] ▶ L2 → L2 ⊢ T ÷ A.
-/2 width=7/ qed.
-
-lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ÷ A.
-/2 width=7/ qed.
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss.ma".
-include "basic_2/static/aaa_ltps.ma".
+include "basic_2/unfold/tpss_tpss.ma".
+include "basic_2/unfold/ltpss_ldrop.ma".
+include "basic_2/static/aaa_lift.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* Properties about parallel unfold *****************************************)
-lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ÷ A.
-#L1 #T #A #HT #L2 #d #e #HL12
-@(TC_Conf3 … (λL,A. L ⊢ T ÷ A) … HT ? HL12) /2 width=5/
+(* Note: lemma 500 *)
+lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
+ ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A.
+#L1 #T1 #A #H elim H -L1 -T1 -A
+[ #L1 #k #L2 #d #e #_ #T2 #H
+ >(tpss_inv_sort1 … H) -H //
+| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #L2 #d #e #HL12 #T2 #H
+ elim (tpss_inv_lref1 … H) -H
+ [ #H destruct
+ elim (lt_or_ge i d) #Hdi
+ [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct
+ /3 width=8/
+ | elim (lt_or_ge i (d + e)) #Hide
+ [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct
+ /3 width=8/
+ | -Hdi
+ lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=8/
+ ]
+ ]
+ | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2
+ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0
+ elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct
+ lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
+ lapply (tpss_trans_eq … HV12 HVW2) -V2 /3 width=7/
+ ]
+| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/
+| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=4/
+| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
+| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #L2 #d #e #HL12 #X #H
+ elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
+]
qed.
-lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ÷ A.
-#L #T1 #A #HT1 #T2 #d #e #HT12
-@(TC_Conf3 … HT1 ? HT12) /2 width=5/
-qed.
+lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
+ ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A.
+/3 width=7/ qed.
-lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
- ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A.
-/3 width=5/ qed.
+lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ÷ A →
+ ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ÷ A.
+/2 width=7/ qed.
+
+lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ÷ A →
+ ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ÷ A.
+/2 width=7/ qed.
+
+lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ÷ A →
+ ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ÷ A.
+/2 width=7/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/ltpsss.ma".
+include "basic_2/static/aaa_ltpss.ma".
+
+(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
+
+(* Properties about iterated parallel unfold ********************************)
+
+lemma aaa_ltpsss_conf: ∀L1,T,A. L1 ⊢ T ÷ A →
+ ∀L2,d,e. L1 [d, e] ▶** L2 → L2 ⊢ T ÷ A.
+#L1 #T #A #HT #L2 #d #e #HL12
+@(TC_Conf3 … (λL,A. L ⊢ T ÷ A) … HT ? HL12) /2 width=5/
+qed.
+
+lemma aaa_ltpsss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶** L2 →
+ ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A.
+/3 width=5/ qed.
+
+lemma aaa_ltpsss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶** L2 →
+ ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A.
+/3 width=5/ qed.
(* Basic properties *********************************************************)
+lemma ltpss_tps2: ∀L1,L2,I,V1,V2,e.
+ L1 [0, e] ▶* L2 → L2 ⊢ V1 [0, e] ▶ V2 →
+ L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+lemma ltpss_tps1: ∀L1,L2,I,V1,V2,d,e.
+ L1 [d, e] ▶* L2 → L2 ⊢ V1 [d, e] ▶ V2 →
+ L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
>(plus_minus_m_m d 1) /2 width=1/
qed.
+lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e.
+ L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
+ 0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
+ L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
+ 0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
(* Basic_1: was by definition: csubst1_refl *)
lemma ltpss_refl: ∀L,d,e. L [d, e] ▶* L.
#L elim L -L //
(**************************************************************************)
include "basic_2/unfold/tpss_tpss.ma".
+include "basic_2/unfold/tpss_alt.ma".
include "basic_2/unfold/ltpss_tpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
]
qed.
+fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
+ L1 ⊢ T2 [d, e] ▶* U2 → ∀L0. L0 [d, e] ▶* L1 →
+ Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ▶* U2.
+#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
+#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
+[ //
+| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL10 #H1 #H2 destruct
+ lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
+ elim (ltpss_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0
+ elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
+ lapply (tpss_fwd_tw … HV01) #H2
+ lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
+ lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02
+ lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01
+ [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ]
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
+ lapply (tpss_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
+ lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
+ lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
+ lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
+]
+qed.
+
+lemma ltpss_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ▶* U2 →
+ ∀L0. L0 [d, e] ▶* L1 → L0 ⊢ T2 [d, e] ▶* U2.
+/2 width=5/ qed.
+
+lemma ltpss_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ▶* L1 →
+ L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2.
+/3 width=3/ qed.
+
(* Main properties **********************************************************)
fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶* L1 →
elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/
]
qed.
-
-fact ltpss_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
- L1 ⊢ T2 [d, e] ▶ U2 → ∀L0. L0 [d, e] ▶* L1 →
- Y1 = L1 → X2 = T2 → L0 ⊢ T2 [d, e] ▶* U2.
-#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
-#L1 #T2 #U2 #d #e * -L1 -T2 -U2 -d -e
-[ //
-| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L0 #HL10 #H1 #H2 destruct
- lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
- elim (ltpss_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0
- elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
- lapply (tpss_fwd_tw … HV01) #H2
- lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
- lapply (IH … HV01 … HK01 ? ?) -IH -HV01 -HK01
- [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ]
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
- lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
- lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
- lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
- lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
-]
-qed.
-
-lemma ltps_tps_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 [d, e] ▶ U2 →
- ∀L0. L0 [d, e] ▶ L1 → L0 ⊢ T2 [d, e] ▶* U2.
-/2 width=5/ qed.
-
-lemma ltps_tpss_trans_eq: ∀L0,L1,T2,U2,d,e. L0 [d, e] ▶ L1 →
- L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2.
-#L0 #L1 #T2 #U2 #d #e #HL01 #H @(tpss_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU @(tpss_trans_eq … IHU) /2 width=3/
-qed.
-*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/ltpss.ma".
+
+(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
+
+definition ltpsss: nat → nat → relation lenv ≝
+ λd,e. TC … (ltpss d e).
+
+interpretation "repeated partial unfold (local environment)"
+ 'PSubstStars L1 d e L2 = (ltpsss d e L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma ltpsss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. L1 [d, e] ▶** L → L [d, e] ▶* L2 → R L → R L2) →
+ ∀L2. L1 [d, e] ▶** L2 → R L2.
+#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma ltpsss_ind_dx: ∀d,e,L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. L1 [d, e] ▶* L → L [d, e] ▶** L2 → R L → R L1) →
+ ∀L1. L1 [d, e] ▶** L2 → R L1.
+#d #e #L2 #R #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma ltpsss_strap1: ∀L1,L,L2,d,e.
+ L1 [d, e] ▶** L → L [d, e] ▶* L2 → L1 [d, e] ▶** L2.
+/2 width=3/ qed.
+
+lemma ltpsss_strap2: ∀L1,L,L2,d,e.
+ L1 [d, e] ▶* L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2.
+/2 width=3/ qed.
+
+lemma ltpsss_refl: ∀L,d,e. L [d, e] ▶** L.
+/2 width=1/ qed.
+
+lemma ltpsss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → L1 [0, |L2|] ▶** L2.
+#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 //
+#L #L2 #_ #HL2
+>(ltpss_fwd_length … HL2) /3 width=5/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltpsss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → |L1| = |L2|.
+#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL12 >IHL12 -IHL12
+/2 width=3 by ltpss_fwd_length/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltpsss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶** L2 → L1 = L2.
+#d #L1 #L2 #H @(ltpsss_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL <(ltpss_inv_refl_O2 … HL2) -HL2 //
+qed-.
+
+lemma ltpsss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶** L2 → L2 = ⋆.
+#d #e #L2 #H @(ltpsss_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL destruct
+>(ltpss_inv_atom1 … HL2) -HL2 //
+qed-.
+
+lemma ltpsss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶** ⋆ → L1 = ⋆.
+#d #e #L1 #H @(ltpsss_ind_dx … H) -L1 //
+#L1 #L #HL1 #_ #IHL2 destruct
+>(ltpss_inv_atom2 … HL1) -HL1 //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/ltpss_ldrop.ma".
+include "basic_2/unfold/ltpsss.ma".
+
+(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
+
+lemma ltpsss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
+#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 // /3 width=6/
+qed.
+
+lemma ltpsss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
+#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // /3 width=6/
+qed.
+
+lemma ltpsss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L2 [0, d1 + e1 - e2] ▶** L & ⇩[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1
+[ /2 width=3/
+| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
+ elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0
+ elim (ltpss_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3 width=3/
+]
+qed.
+
+lemma ltpsss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L [0, d1 + e1 - e2] ▶** L2 & ⇩[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0
+[ /2 width=3/
+| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
+ elim (ltpss_ldrop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0
+ elim (IHL … HL0 Hd1e2 He2de1) -L /3 width=3/
+]
+qed.
+
+lemma ltpsss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L2 [d1 - e2, e1] ▶** L & ⇩[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1
+[ /2 width=3/
+| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
+ elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0
+ elim (ltpss_ldrop_conf_le … HL1 … HL0 He2d1) -L /3 width=3/
+]
+qed.
+
+lemma ltpsss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L [d1 - e2, e1] ▶** L2 & ⇩[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0
+[ /2 width=3/
+| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1
+ elim (ltpss_ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0
+ elim (IHL … HL0 He2d1) -L /3 width=3/
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/unfold/ltpsss_tpss.ma".
+
+(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma ltpsss_strip: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
+ ∀L2,d2,e2. L0 [d2, e2] ▶* L2 →
+ ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶** L.
+/3 width=3/ qed.
+
+lemma ltpsss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 →
+ ∀T2,U2. L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2.
+#L0 #L1 #d #e #H @(ltpsss_ind … H) -L1
+[ /2 width=1/
+| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2
+ lapply (ltpss_tpss_trans_eq … HTU2 … HL1) -HL1 -HTU2 /2 width=1/
+]
+qed.
+
+lemma ltpsss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 →
+ ∀T2,U2. L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2.
+/3 width=3/ qed.
+
+lemma ltpsss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 →
+ ∀L2,ds,es. L1 [ds, es] ▶** L2 →
+ ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T.
+#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpsss_ind … H) -L2
+[ /2 width=3/
+| -HT12 #L #L2 #HL1 #HL2 * #T #HT1 #HT2
+ lapply (ltpsss_strap1 … HL1 HL2) -HL1 #HL12
+ elim (ltpss_tpss_conf … HT1 … HL2) -L #T0 #HT10 #HT0
+ lapply (ltpsss_tpss_trans_eq … HL12 … HT0) -HL12 -HT0 #HT0
+ lapply (tpss_trans_eq … HT2 HT0) -T /2 width=3/
+]
+qed.
+
+lemma ltpsss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 →
+ ∀L2,ds,es. L1 [ds, es] ▶** L2 →
+ ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T.
+/3 width=1/ qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma ltpsss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶** L2 →
+ ∃∃K2,V2. K1 [0, e - 1] ▶** K2 &
+ K1 ⊢ V1 [0, e - 1] ▶* V2 &
+ L2 = K2. ⓑ{I} V2.
+#e #K1 #I #V1 #L2 #He #H @(ltpsss_ind … H) -L2
+[ /2 width=5/
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
+ elim (ltpss_inv_tpss21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
+ lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2
+ lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/
+]
+qed-.
+
+lemma ltpsss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶** L2 →
+ ∃∃K2,V2. K1 [d - 1, e] ▶** K2 &
+ K1 ⊢ V1 [d - 1, e] ▶* V2 &
+ L2 = K2. ⓑ{I} V2.
+#d #e #K1 #I #V1 #L2 #Hd #H @(ltpsss_ind … H) -L2
+[ /2 width=5/
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
+ elim (ltpss_inv_tpss11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
+ lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2
+ lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/
+]
+qed-.
+
+lemma ltpsss_fwd_tpss22: ∀I,L1,K2,V2,e. L1 [0, e] ▶** K2. ⓑ{I} V2 → 0 < e →
+ ∃∃K1,V1. K1 [0, e - 1] ▶** K2 &
+ K1 ⊢ V1 [0, e - 1] ▶* V2 &
+ L1 = K1. ⓑ{I} V1.
+#I #L1 #K2 #V2 #e #H #He @(ltpsss_ind_dx … H) -L1
+[ /2 width=5/
+| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
+ elim (ltpss_inv_tpss22 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct
+ lapply (tpss_trans_eq … HV1 HV2) -V #HV12
+ lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/
+]
+qed-.
+
+lemma ltpsss_inv_tpss12: ∀I,L1,K2,V2,d,e. L1 [d, e] ▶** K2. ⓑ{I} V2 → 0 < d →
+ ∃∃K1,V1. K1 [d - 1, e] ▶** K2 &
+ K1 ⊢ V1 [d - 1, e] ▶* V2 &
+ L1 = K1. ⓑ{I} V1.
+#I #L1 #K2 #V2 #d #e #H #Hd @(ltpsss_ind_dx … H) -L1
+[ /2 width=5/
+| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
+ elim (ltpss_inv_tpss12 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct
+ lapply (tpss_trans_eq … HV1 HV2) -V #HV12
+ lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/
+]
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem ltpsss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
+ ∀L2,d2,e2. L0 [d2, e2] ▶** L2 →
+ ∃∃L. L1 [d2, e2] ▶** L & L2 [d1, e1] ▶** L.
+/3 width=3/ qed.
+
+theorem ltpsss_trans_eq: ∀L1,L,L2,d,e.
+ L1 [d, e] ▶** L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2.
+/2 width=3/ qed.
+
+lemma ltpsss_tpss2: ∀L1,L2,I,V1,V2,e.
+ L1 [0, e] ▶** L2 → L2 ⊢ V1 [0, e] ▶* V2 →
+ L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
+[ /2 width=1/
+| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/
+]
+qed.
+
+lemma ltpsss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
+ L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
+ 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) // /2 width=1/
+qed.
+
+lemma ltpsss_tpss1: ∀L1,L2,I,V1,V2,d,e.
+ L1 [d, e] ▶** L2 → L2 ⊢ V1 [d, e] ▶* V2 →
+ L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
+[ /2 width=1/
+| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/
+]
+qed.
+
+lemma ltpsss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
+ L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 →
+ 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) // /2 width=1/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/ltpss_tps.ma".
+include "basic_2/unfold/ltpsss.ma".
+
+(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
+
+(* Properties concerning partial substitution on terms **********************)
+
+lemma ltpsss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
+ ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
+ d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶ U2.
+#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 //
+#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
+lapply (ltpss_tps_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/
+qed.
+
+lemma ltpsss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
+ L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶** L1 →
+ L1 ⊢ T2 [d2, e2] ▶ U2.
+#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 //
+-HTU2 #L #L1 #_ #HL1 #IHL
+lapply (ltpss_tps_conf_ge … IHL … HL1 ?) -HL1 -IHL //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/ltpss_tpss.ma".
+include "basic_2/unfold/ltpsss.ma".
+
+(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
+
+(* Properties concerning partial substitution on terms **********************)
+
+lemma ltpsss_tps2: ∀L1,L2,I,e.
+ L1 [0, e] ▶** L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 →
+ L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2.
+#L1 #L2 #I #e #H @(ltpsss_ind … H) -L2
+[ /3 width=1/
+| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
+ elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
+ lapply (IHL … HV1) -IHL -HV1 /3 width=5/
+]
+qed.
+
+lemma ltpsss_tps2_lt: ∀L1,L2,I,V1,V2,e.
+ L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
+ 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) // /2 width=1/
+qed.
+
+lemma ltpsss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶** L2 →
+ ∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 →
+ L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2.
+#L1 #L2 #I #d #e #H @(ltpsss_ind … H) -L2
+[ /3 width=1/
+| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
+ elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
+ lapply (IHL … HV1) -IHL -HV1 /3 width=5/
+]
+qed.
+
+lemma ltpsss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
+ L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
+ 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) // /2 width=1/
+qed.
+
+(* Properties concerning partial unfold on terms ****************************)
+
+lemma ltpsss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
+ L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶** L1 →
+ L1 ⊢ T2 [d2, e2] ▶* U2.
+#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 //
+-HTU2 #L #L1 #_ #HL1 #IHL
+lapply (ltpss_tpss_conf_ge … IHL … HL1 ?) -HL1 -IHL //
+qed.
+
+lemma ltpsss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
+ ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
+ d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2.
+#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 //
+#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
+lapply (ltpss_tpss_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/unfold/tpss_lift.ma".
+
+(* PARALLEL UNFOLD ON TERMS *************************************************)
+
+(* alternative definition of tpss *)
+inductive tpssa: nat → nat → lenv → relation term ≝
+| tpssa_atom : ∀L,I,d,e. tpssa d e L (⓪{I}) (⓪{I})
+| tpssa_subst: ∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
+ ⇩[0, i] L ≡ K. ⓓV1 → tpssa 0 (d + e - i - 1) K V1 V2 →
+ ⇧[0, i + 1] V2 ≡ W2 → tpssa d e L (#i) W2
+| tpssa_bind : ∀L,I,V1,V2,T1,T2,d,e.
+ tpssa d e L V1 V2 → tpssa (d + 1) e (L. ⓑ{I} V2) T1 T2 →
+ tpssa d e L (ⓑ{I} V1. T1) (ⓑ{I} V2. T2)
+| tpssa_flat : ∀L,I,V1,V2,T1,T2,d,e.
+ tpssa d e L V1 V2 → tpssa d e L T1 T2 →
+ tpssa d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+.
+
+interpretation "parallel unfold (term) alternative"
+ 'PSubstStarAlt L T1 d e T2 = (tpssa d e L T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma tpssa_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶▶* T2 →
+ ∀L2. L1 [d, e] ≼ L2 → L2 ⊢ T1 [d, e] ▶▶* T2.
+#L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e
+[ //
+| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+ elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/
+| /4 width=1/
+| /3 width=1/
+]
+qed.
+
+lemma tpssa_refl: ∀T,L,d,e. L ⊢ T [d, e] ▶▶* T.
+#T elim T -T //
+#I elim I -I /2 width=1/
+qed.
+
+lemma tpssa_tps_trans: ∀L,T1,T,d,e. L ⊢ T1 [d, e] ▶▶* T →
+ ∀T2. L ⊢ T [d, e] ▶ T2 → L ⊢ T1 [d, e] ▶▶* T2.
+#L #T1 #T #d #e #H elim H -L -T1 -T -d -e
+[ #L #I #d #e #X #H
+ elim (tps_inv_atom1 … H) -H // * /2 width=6/
+| #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK #_ #HVW2 #IHV12 #T2 #H
+ lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+ lapply (tps_weak … H 0 (d+e) ? ?) -H // #H
+ elim (tps_inv_lift1_be … H … H0LK … HVW2 ? ?) -H -H0LK -HVW2 // /3 width=6/
+| #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
+ elim (tps_inv_bind1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct
+ lapply (tps_lsubs_conf … HT2 (L.ⓑ{I}V) ?) -HT2 /2 width=1/ #HT2
+ lapply (IHV1 … HV2) -IHV1 -HV2 #HV12
+ lapply (IHT1 … HT2) -IHT1 -HT2 #HT12
+ lapply (tpssa_lsubs_conf … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/
+| #L #I #V1 #V #T1 #T #d #e #_ #_ #IHV1 #IHT1 #X #H
+ elim (tps_inv_flat1 … H) -H #V2 #T2 #HV2 #HT2 #H destruct /3 width=1/
+]
+qed.
+
+lemma tpss_tpssa: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T1 [d, e] ▶▶* T2.
+#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // /2 width=3/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma tpssa_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶▶* T2 → L ⊢ T1 [d, e] ▶* T2.
+#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=6/
+qed-.
+
+lemma tpss_ind_alt: ∀R:ℕ→ℕ→lenv→relation term.
+ (∀L,I,d,e. R d e L (⓪{I}) (⓪{I})) →
+ (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e →
+ ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ▶* V2 →
+ ⇧[O, i + 1] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2
+ ) →
+ (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 →
+ L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ▶* T2 → R d e L V1 V2 →
+ R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2)
+ ) →
+ (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ▶* V2 →
+ L⊢ T1 [d, e] ▶* T2 → R d e L V1 V2 →
+ R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+ ) →
+ ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ▶* T2 → R d e L T1 T2.
+#R #H1 #H2 #H3 #H4 #d #e #L #T1 #T2 #H elim (tpss_tpssa … H) -L -T1 -T2 -d -e
+// /3 width=1 by tpssa_tpss/ /3 width=7 by tpssa_tpss/
+qed-.
projects / helm.git / commitdiff