ty3/fsubst0 ty3_fsubst0
ty3/fsubst0 ty3_csubst0
ty3/fsubst0 ty3_subst0
-ty3/fwd ty3_gen_sort
-ty3/fwd ty3_gen_lref
-ty3/fwd ty3_gen_bind
ty3/fwd ty3_gen_appl
-ty3/fwd ty3_gen_cast
ty3/fwd tys3_gen_nil
ty3/fwd tys3_gen_cons
ty3/fwd_nf2 ty3_gen_appl_nf2
ty3/pr3_props ty3_sconv_pc3
ty3/pr3_props ty3_sred_back
ty3/pr3_props ty3_sconv
-ty3/props ty3_lift
-ty3/props ty3_correct
ty3/props ty3_unique
ty3/props ty3_gen_abst_abst
-ty3/props ty3_typecheck
-ty3/props ty3_getl_subst0
ty3/sty0 ty3_sty0
ty3/subst1 ty3_gen_cabbr
ty3/subst1 ty3_gen_cvoid
(**************************************************************************)
include "basic_2/reducibility/ltpr_tps.ma".
-include "basic_2/reducibility/cpr_ltpsss.ma".
+include "basic_2/reducibility/cpr_ltpss.ma".
include "basic_2/reducibility/lcpr.ma".
include "basic_2/computation/cprs.ma".
/2 width=3/ qed.
theorem lcpcs_canc_sn: ∀L,L1,L2. L ⊢ ⬌* L1 → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2.
-/3 width=3/ qed.
+/3 width=3 by lcpcs_trans, lcprs_comm/ qed.
theorem lcpcs_canc_dx: ∀L,L1,L2. L1 ⊢ ⬌* L → L2 ⊢ ⬌* L → L1 ⊢ ⬌* L2.
-/3 width=3/ qed.
+/3 width=3 by lcpcs_trans, lcprs_comm/ 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.
--- /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.
--- /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/reducibility/ltpr_tps.ma".
+include "basic_2/reducibility/cpr_ltpsss.ma".
+include "basic_2/reducibility/lcpr.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties concerning context-sensitive parallel reduction on lenv's *****)
+
+lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 [d, e] ▶* T2 →
+ ∃∃T. L1 ⊢ T1 [d, e] ▶* T & L1 ⊢ T ➡* T2.
+#L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2
+[ /2 width=3/
+| #T #T2 #_ #HT2 * #T0 #HT10 #HT0
+ elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32
+ @(ex2_1_intro … HT10) -T1 (**) (* explicit constructors *)
+ @(cprs_strap1 … T3 …) /2 width=1/ -HT32
+ @(cprs_strap1 … HT0) -HT0 /3 width=3/
+]
+qed.
+
+(* Basic_1: was just: pr3_pr0_pr2_t *)
+lemma ltpr_cpr_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #HL12 #T1 #T2 * #T #HT1
+<(ltpr_fwd_length … HL12) #HT2
+elim (ltpr_tpss_trans … HL12 … HT2) -L2 /3 width=3/
+qed.
+
+(* Basic_1: was just: pr3_pr2_pr2_t *)
+lemma lcpr_cpr_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 * /3 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/reducibility/ltpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
+
+definition lcpr: relation lenv ≝
+ λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶** L2
+.
+
+interpretation
+ "context-sensitive parallel reduction (environment)"
+ 'CPRed L1 L2 = (lcpr L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lcpr_refl: ∀L. L ⊢ ➡ L.
+/2 width=3/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆.
+#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpsss_inv_atom1 … HL2) -HL2 //
+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/static/aaa_ltpsss.ma".
+include "basic_2/reducibility/ltpr_aaa.ma".
+include "basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/lcpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_lcpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ÷ A.
+#L1 #T #A #HT #L2 * /3 width=5/
+qed.
+
+lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ÷ A.
+#L #T1 #A #HT1 #T2 * /3 width=5/
+qed.
+
+lemma aaa_lcpr_cpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ⊢ ➡ L2 →
+ ∀T2. L2 ⊢ T1 ➡ T2 → L2 ⊢ T2 ÷ A.
+/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/ltpsss_ltpsss.ma".
+include "basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/lcpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
+
+(* Advanced properties ****************************************************)
+
+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 *
+<(ltpsss_fwd_length … HL2) /4 width=5/
+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_ltpsss.ma".
+include "basic_2/reducibility/ltpr_ltpsss.ma".
+include "basic_2/reducibility/ltpr_ltpr.ma".
+include "basic_2/reducibility/lcpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***************)
+
+(* Main properties **********************************************************)
+
+theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 →
+ ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L.
+#K0 #L1 #L2 * #K1 #HK01 #HKL1 * #K2 #HK02 #HKL2
+lapply (ltpr_fwd_length … HK01) #H
+>(ltpr_fwd_length … HK02) in H; #H
+elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2
+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_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/
+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.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+(* Unfold *******************************************************************)
+
+notation "hvbox( T1 break [ d , break e ] ▶** break T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStars $T1 $d $e $T2 }.
(* *)
(**************************************************************************)
-(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
- * Support for abstract candidates of reducibility closed: 2012 January 27
- * Confluence of context-sensitive parallel reduction closed: 2011 September 21
- * Confluence of context-free parallel reduction closed: 2011 September 6
- * Specification started: 2011 April 17
+(* THE FORMAL SYSTEM λδ: MATITA SOURCE FILES
* - Patience on me to gain peace and perfection! -
* [ suggested invocation to start formal specifications with ]
+ * Context-sensitive subject equivalence for atomic arity assignment: 2012 April 16
+ * Context-sensitive strong normalization for simply typed terms: 2012 March 15
+ * Support for abstract candidates of reducibility closed: 2012 January 27
+ * Confluence for context-sensitive parallel reduction: 2011 September 21
+ * Confluence for context-free parallel reduction: 2011 September 6
+ * Specification starts: 2011 April 17
*)
include "ground_2/star.ma".
--- /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/static/sh.ma".
+include "basic_2/equivalence/cpcs.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+inductive nta (h:sh): lenv → relation term ≝
+| nta_sort: ∀L,k. nta h L (⋆k) (⋆(next h k))
+| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W →
+ ⇧[0, i + 1] W ≡ U → nta h L (#i) U
+| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V →
+ ⇧[0, i + 1] W ≡ U → nta h L (#i) U
+| nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U →
+ nta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
+| nta_appl: ∀L,V,W,U,T1,T2. nta h L V W → nta h L W U → nta h (L.ⓛW) T1 T2 →
+ nta h L (ⓐV.ⓛW.T1) (ⓐV.ⓛW.T2)
+| nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
+ nta h L (ⓐV.T) (ⓐV.U)
+| nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓣU. T) U
+| nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 →
+ nta h L T U2
+.
+
+interpretation "native type assignment (term)"
+ 'NativeType h L T U = (nta h L T U).
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: ty3_cast *)
+lemma nta_cast_old: ∀h,L,W,T,U.
+ ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → ⦃h, L⦄ ⊢ ⓣU.T : ⓣW.U.
+/4 width=3/ qed.
+
+(* Basic_1: was: ty3_typecheck *)
+lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓣU.T : T0.
+/3 width=2/ qed.
+
+(* Basic_1: removed theorems 1: ty3_getl_subst0 *)
--- /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/equivalence/cpcs_cpcs.ma".
+include "basic_2/native/nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+fact nta_inv_sort_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
+ L ⊢ ⋆(next h k0) ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #k0 #H destruct //
+| #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #k0 #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
+| #L #T #U #_ #_ #k0 #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct
+ lapply (IHTU1 ??) -IHTU1 [ // | skip ] #Hk0
+ lapply (cpcs_trans … Hk0 … HU12) -U1 //
+]
+qed.
+
+(* Basic_1: was: ty3_gen_sort *)
+lemma nta_inv_sort: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U.
+/2 width=3/ qed-.
+
+fact nta_inv_lref_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
+ (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
+ ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ) ∨
+ (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
+ ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ).
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #j #H destruct
+| #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
+| #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
+| #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #j #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
+| #L #T #U #_ #_ #j #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct
+ elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01
+ lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
+]
+qed.
+
+(* Basic_1: was ty3_gen_lref *)
+lemma nta_inv_lref: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
+ (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
+ ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ) ∨
+ (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
+ ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ).
+/2 width=3/ qed-.
+
+fact nta_inv_bind_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X →
+ ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
+ L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #J #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct
+| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
+| #L #T #U #_ #_ #J #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
+ elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1
+ lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
+]
+qed.
+
+(* Basic_1: was: ty3_gen_bind *)
+lemma nta_inv_bind: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U →
+ ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
+ L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+/2 width=3/ qed-.
+
+fact nta_inv_cast_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X →
+ ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
+ elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1
+ lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/
+]
+qed.
+
+(* Basic_1: was: ty3_gen_cast *)
+lemma nta_inv_cast: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+/2 width=3/ qed-.
+
+(* Properties on relocation *************************************************)
+
+(* Basic_1: was: ty3_lift *)
+lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
+#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
+[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ >(lift_inv_sort1 … H1) -X1
+ >(lift_inv_sort1 … H2) -X2 //
+| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
+ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+ /3 width=8/
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+ lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+ ]
+| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
+ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
+ lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
+ elim (lift_total V1 (d-i-1) e) /3 width=8/
+ | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+ lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+ ]
+| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+ elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+ lapply (lift_mono … H1 … HV12) -H1 #H destruct
+ elim (lift_total W1 d e) /4 width=6/
+| #L1 #V1 #W1 #U1 #T11 #T12 #_ #_ #_ #IHVW1 #IHWU1 #IHT112 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
+ elim (lift_inv_bind1 … H1) -H1 #W2 #T12 #HW12 #HT112 #H destruct
+ elim (lift_inv_flat1 … H2) -H2 #X0 #X #H0 #H2 #H destruct
+ elim (lift_inv_bind1 … H2) -H2 #Y0 #T22 #H2 #HT122 #H destruct
+ lapply (lift_mono … H0 … HV12) -H0 #H destruct
+ lapply (lift_mono … H2 … HW12) -H2 #H destruct
+ elim (lift_total U1 d e) #U2 #HU12
+ @nta_appl [2,3: /2 width=5/ | skip | /3 width=5/ ] (**) (* explicit constructor, /4 width=6/ is too slow *)
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+ elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+ lapply (lift_mono … H1 … HV12) -H1 #H destruct
+ elim (lift_total W1 d e) /4 width=6/
+| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
+ elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
+ lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/
+| #L1 #T1 #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
+ elim (lift_total U11 d e) #U #HU11
+ elim (lift_total V12 d e) #V22 #HV122
+ lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
+]
+qed.
+
+(* Advanced forvard lemmas **************************************************)
+
+(* Basic_1: was: ty3_correct *)
+lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
+#h #L #T #U #H elim H -L -T -U
+[ /2 width=2/
+| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
+ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+ elim (lift_total V0 0 (i+1)) /3 width=10/
+| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
+ lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+ elim (lift_total V 0 (i+1)) /3 width=10/
+| #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/
+| #L #V #W #U #T1 #T2 #HVW #HWU #_ #_ #_ * /3 width=2/
+| #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
+| #L #T #U #_ * /2 width=2/
+| /2 width=2/
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was: ty3_appl *)
+lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T : ⓛW.U →
+ ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U.
+#h #L #V #W #T #U #HVW #HTU
+elim (nta_fwd_correct … HTU) #X #H
+elim (nta_inv_bind … H) -H #V0 #T0 #HWV0 #HUT0 #_ -X /3 width=2/
+qed.
non associative with precedence 45
for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
-notation "hvbox( T1 break [ d , break e ] ▶** break T2 )"
- non associative with precedence 45
- for @{ 'PSubstStars $T1 $d $e $T2 }.
-
notation "hvbox( T1 break [ d , break e ] ≡ break T2 )"
non associative with precedence 45
for @{ 'TSubst $T1 $d $e $T2 }.
notation "hvbox( T1 ⊢ ⬌* break T2 )"
non associative with precedence 45
for @{ 'CPConvStar $T1 $T2 }.
+
+(* Native typing ************************************************************)
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 : break T2 )"
+ non associative with precedence 45
+ for @{ 'NativeType $h $L $T1 $T2 }.
+
+notation "hvbox( h ⊢ break term 90 L1 : ⊑ break L2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEqN $h $L1 $L2 }.
+++ /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/ltpsss.ma".
+include "basic_2/unfold/ltpss.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 >(ltpsss_inv_atom1 … HL2) -HL2 //
+#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 //
qed-.
(* *)
(**************************************************************************)
-include "basic_2/static/aaa_ltpsss.ma".
+include "basic_2/static/aaa_ltpss.ma".
include "basic_2/reducibility/ltpr_aaa.ma".
include "basic_2/reducibility/cpr.ma".
include "basic_2/reducibility/lcpr.ma".
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpsss_ltpsss.ma".
+include "basic_2/unfold/ltpss_ltpss.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 *
-<(ltpsss_fwd_length … HL2) /4 width=5/
+<(ltpss_fwd_length … HL2) /4 width=5/
qed.
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpsss_ltpsss.ma".
-include "basic_2/reducibility/ltpr_ltpsss.ma".
+include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/reducibility/ltpr_ltpss.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 (ltpsss_fwd_length … HKL1) #H1
-lapply (ltpsss_fwd_length … HKL2) #H2
+lapply (ltpss_fwd_length … HKL1) #H1
+lapply (ltpss_fwd_length … HKL2) #H2
>H1 in HKL1 H; -H1 #HKL1
>H2 in HKL2; -H2 #HKL2 #H
-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
+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
lapply (ltpr_fwd_length … HLK1) #H1
lapply (ltpr_fwd_length … HLK2) #H2
/3 width=5/
+++ /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.
+++ /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.
(* SORT HIERARCHY ***********************************************************)
-(* sort hierarchy specifications *)
+(* sort hierarchy specification *)
record sh: Type[0] ≝ {
next: nat → nat; (* next sort in the hierarchy *)
next_lt: ∀k. k < next k (* strict monotonicity condition *)
]
qed.
-(* Note: apparently this was missing in Basic_1 *)
+(* Note: apparently this was missing in basic_1 *)
theorem lift_div_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T →
∀e,e2,T2. ⇧[d1 + e, e2] T2 ≡ T →
e ≤ e1 → e1 ≤ e + e2 →
+++ /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.
projects / helm.git / commitdiff