(* Advanced properties ******************************************************)
+lemma cprs_abst_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2.
+ L.ⓛV ⊢ T1 ➡* T2 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2.
+#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HT12) -T2
+[ /3 width=2/
+| /3 width=6 by cprs_strap1, cpr_abst/ (**) (* /3 width=6/ is too slow *)
+]
+qed.
+
lemma cprs_abbr1_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 →
L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
#L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind_dx … HT12) -T1
@(cprs_trans … IHV1) -IHV1 /2 width=1/
qed.
+lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2.
+ L.ⓛV ⊢ T1 ➡* T2 → L ⊢ ⓛV1. T1 ➡* ⓛV2. T2.
+#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 @(cprs_ind … HV12) -V2
+[ lapply (cprs_lsubs_conf … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
+| #V0 #V2 #_ #HV02 #IHV01
+ @(cprs_trans … IHV01) -V1 /2 width=2/
+]
+qed.
+
lemma cprs_abbr1: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 →
L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
#L #V1 #T1 #T2 #HT12 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/
lemma lcprs_ind: ∀L1. ∀R:predicate lenv. R L1 →
(∀L,L2. L1 ⊢ ➡* L → L ⊢ ➡ L2 → R L → R L2) →
∀L2. L1 ⊢ ➡* L2 → R L2.
-#L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
+#L1 #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma lcprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. L1 ⊢ ➡ L → L ⊢ ➡* L2 → R L → R L1) →
+ ∀L1. L1 ⊢ ➡* L2 → R L1.
+#L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
qed-.
(* Basic properties *********************************************************)
(* 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 →
+ ∃∃L0. L1 ⊢ ➡ L0 & L2 ⊢ ➡* L0.
+(*
+/3 width=3/ qed.
+*)
(* Main properties **********************************************************)
theorem lcprs_trans: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ➡* L2 → 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/reducibility/lcpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **************)
+
+definition lcpc: relation lenv ≝
+ λL1,L2. L1 ⊢ ➡ L2 ∨ L2 ⊢ ➡ L1.
+
+interpretation
+ "context-sensitive parallel conversion (local environment)"
+ 'CPConv L1 L2 = (lcpc L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lcpc_refl: ∀L. L ⊢ ⬌ L.
+/2 width=1/ qed.
+
+lemma lcpc_sym: ∀L1,L2. L1 ⊢ ⬌ L2 → L2 ⊢ ⬌ L1.
+#L1 #L2 * /2 width=1/
+qed.
+
+lemma lcpc_lcpr: ∀L1,L2. L1 ⊢ ⬌ L2 → ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L.
+#L1 #L2 * /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/conversion/lcpc.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **************)
+
+(* Main properties **********************************************************)
+
+theorem lcpc_conf: ∀L0,L1,L2. L0 ⊢ ⬌ L1 → L0 ⊢ ⬌ L2 →
+ ∃∃L. L1 ⊢ ⬌ L & L2 ⊢ ⬌ L.
+/3 width=3/ qed.
>(lift_inj … HXU … HTU) -X -U -d -e /2 width=3/
qed-.
-(* advanced properties ******************************************************)
+(* Advanced properties ******************************************************)
(* Basic_1: was only: pc3_thin_dx *)
lemma cpcs_flat: ∀L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L ⊢ T1 ⬌* T2 →
elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_flat, cprs_div/ (**) (* /3 width=5/ is too slow *)
qed.
+lemma cpcs_abst: ∀L,V1,V2. L ⊢ V1 ⬌* V2 →
+ ∀V,T1,T2. L.ⓛV ⊢ T1 ⬌* T2 → L ⊢ ⓛV1. T1 ⬌* ⓛV2. T2.
+#L #V1 #V2 #HV12 #V #T1 #T2 #HT12
+elim (cpcs_inv_cprs … HV12) -HV12
+elim (cpcs_inv_cprs … HT12) -HT12
+/3 width=6 by cprs_div, cprs_abst/ (**) (* /3 width=6/ is a bit slow *)
+qed.
+
lemma cpcs_abbr_dx: ∀L,V,T1,T2. L.ⓓV ⊢ T1 ⬌* T2 → L ⊢ ⓓV. T1 ⬌* ⓓV. T2.
#L #V #T1 #T2 #HT12
elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *)
elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_abbr1/ (**) (* /3 width=5/ is a bit slow *)
qed.
-(* Basic_1: was: pc3_gen_lift *)
+(* Basic_1: was: pc3_lift *)
lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
K ⊢ T1 ⬌* T2 → L ⊢ U1 ⬌* U2.
--- /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/conversion/lcpc.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL EBVIRONMENTS *************)
+
+definition lcpcs: relation lenv ≝ TC … lcpc.
+
+interpretation "context-sensitive parallel equivalence (local environment)"
+ 'CPConvStar L1 L2 = (lcpcs L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma lcpcs_ind: ∀L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. L1 ⊢ ⬌* L → L ⊢ ⬌ L2 → R L → R L2) →
+ ∀L2. L1 ⊢ ⬌* L2 → R L2.
+#L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma lcpcs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. L1 ⊢ ⬌ L → L ⊢ ⬌* L2 → R L → R L1) →
+ ∀L1. L1 ⊢ ⬌* L2 → R L1.
+#L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lcpcs_refl: ∀L. L ⊢ ⬌* L.
+/2 width=1/ qed.
+
+lemma lcpcs_strap1: ∀L1,L,L2. L1 ⊢ ⬌* L → L ⊢ ⬌ L2 → L1 ⊢ ⬌* L2.
+/2 width=3/ qed.
+
+lemma lcpcs_strap2: ∀L1,L,L2. L1 ⊢ ⬌ L → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2.
+/2 width=3/ qed.
+
+lemma lcpcs_lcpr_dx: ∀L1,L2. L1 ⊢ ➡ L2 → L1 ⊢ ⬌* L2.
+/3 width=1/ qed.
+
+lemma lcpcs_lcpr_sn: ∀L1,L2. L2 ⊢ ➡ L1 → L1 ⊢ ⬌* L2.
+/3 width=1/ qed.
+
+lemma lcpcs_lcpr_strap1: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ➡ L2 → L1 ⊢ ⬌* L2.
+/3 width=3/ qed.
+
+lemma lcpcs_lcpr_strap2: ∀L1,L. L1 ⊢ ➡ L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2.
+/3 width=3/ qed.
+
+lemma lcpcs_lcpr_div: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L2 ⊢ ➡ L → L1 ⊢ ⬌* L2.
+/3 width=3/ qed.
+
+lemma lcpcs_lcpr_conf: ∀L1,L. L ⊢ ➡ L1 → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2.
+/3 width=3/ qed.
+
+lemma lcprs_comm: ∀L1,L2. L1 ⊢ ⬌* L2 → L2 ⊢ ⬌* L1.
+#L1 #L2 #H @(lcpcs_ind … H) -L2 // /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/computation/lcprs_aaa.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/equivalence/lcpcs_lcpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL EBVIRONMENTS *************)
+
+(* Main properties about atomic arity assignment on terms *******************)
+
+theorem aaa_lcpcs_mono: ∀L1,L2. L1 ⊢ ⬌* L2 →
+ ∀T,A1. L1 ⊢ T ÷ A1 → ∀A2. L2 ⊢ T ÷ A2 →
+ A1 = A2.
+#L1 #L2 #HL12 #T #A1 #HT1 #A2 #HT2
+elim (lcpcs_inv_lcprs … HL12) -HL12 #L #HL1 #HL2
+lapply (aaa_lcprs_conf … HT1 … HL1) -L1 #HT1
+lapply (aaa_lcprs_conf … HT2 … HL2) -L2 #HT2
+lapply (aaa_mono … HT1 … HT2) -L -T //
+qed-.
+
+theorem aaa_cpcs_mono: ∀L,T1,T2. L ⊢ T1 ⬌* T2 →
+ ∀A1. L ⊢ T1 ÷ A1 → ∀A2. L ⊢ T2 ÷ A2 →
+ A1 = A2.
+#L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2
+elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
+lapply (aaa_cprs_conf … HA1 … HT1) -T1 #HA1
+lapply (aaa_cprs_conf … HA2 … HT2) -T2 #HA2
+lapply (aaa_mono … HA1 … HA2) -L -T //
+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/computation/lcprs_lcprs.ma".
+include "basic_2/conversion/lcpc_lcpc.ma".
+include "basic_2/equivalence/lcpcs_lcprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lcpcs_inv_lcprs: ∀L1,L2. L1 ⊢ ⬌* L2 →
+ ∃∃L. L1 ⊢ ➡* L & L2 ⊢ ➡* L.
+#L1 #L2 #H @(lcpcs_ind … H) -L2
+[ /3 width=3/
+| #L #L2 #_ #HL2 * #L0 #HL10 elim HL2 -HL2 #HL2 #HL0
+ [ elim (lcprs_strip … HL0 … HL2) -L #L #HL0 #HL2
+ lapply (lcprs_strap1 … HL10 … HL0) -L0 /2 width=3/
+ | lapply (lcprs_strap2 … HL2 … HL0) -L /2 width=3/
+ ]
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lcpcs_strip: ∀L,L1. L ⊢ ⬌* L1 → ∀L2. L ⊢ ⬌ L2 →
+ ∃∃L0. L1 ⊢ ⬌ L0 & L2 ⊢ ⬌* L0.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+theorem lcpcs_trans: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2.
+/2 width=3/ qed.
+
+theorem lcpcs_canc_sn: ∀L,L1,L2. L ⊢ ⬌* L1 → L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2.
+/3 width=3/ qed.
+
+theorem lcpcs_canc_dx: ∀L,L1,L2. L1 ⊢ ⬌* L → L2 ⊢ ⬌* L → L1 ⊢ ⬌* L2.
+/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/computation/lcprs.ma".
+include "basic_2/equivalence/lcpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************)
+
+(* Properties about context sensitive computation on local environments *****)
+
+lemma lcpcs_lcprs_dx: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ⬌* L2.
+#L1 #L2 #H @(lcprs_ind … H) -L2 /width=1/ /3 width=3/
+qed.
+
+lemma lcpcs_lcprs_sn: ∀L1,L2. L2 ⊢ ➡* L1 → L1 ⊢ ⬌* L2.
+#L1 #L2 #H @(lcprs_ind_dx … H) -L2 /width=1/ /3 width=3/
+qed.
+
+lemma lcpcs_lcprs_strap1: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L ⊢ ➡* L2 → L1 ⊢ ⬌* L2.
+#L1 #L #HL1 #L2 #H @(lcprs_ind … H) -L2 /width=1/ /2 width=3/
+qed.
+
+lemma lcpcs_lcprs_strap2: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2.
+#L1 #L #H #L2 #HL2 @(lcprs_ind_dx … H) -L1 /width=1/ /2 width=3/
+qed.
+
+lemma lcpcs_lcprs_div: ∀L1,L. L1 ⊢ ⬌* L → ∀L2. L2 ⊢ ➡* L → L1 ⊢ ⬌* L2.
+#L1 #L #HL1 #L2 #H @(lcprs_ind_dx … H) -L2 /width=1/ /2 width=3/
+qed.
+
+lemma lcpcs_lcprs_conf: ∀L1,L. L ⊢ ➡* L1 → ∀L2. L ⊢ ⬌* L2 → L1 ⊢ ⬌* L2.
+#L1 #L #H #L2 #HL2 @(lcprs_ind … H) -L1 /width=1/ /2 width=3/
+qed.
+
+lemma lcprs_div: ∀L1,L. L1 ⊢ ➡* L → ∀L2. L2 ⊢ ➡* L → L1 ⊢ ⬌* L2.
+#L1 #L #HL1 #L2 #H @(lcprs_ind_dx … H) -L2 /2 width=1/ /2 width=3/
+qed.
interpretation "weight (local environment)" 'Weight L = (lw L).
+(* Basic properties *********************************************************)
+
+lemma lw_pair: ∀I,L,V. #[L] < #[(L.ⓑ{I}V)].
+/3 width=1/ qed.
+
+(* Basic eliminators ********************************************************)
+
+axiom lw_wf_ind: ∀R:predicate lenv.
+ (∀L2. (∀L1. #[L1] < #[L2] → R L1) → R L2) →
+ ∀L. R L.
+
(* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *)
(* Basic_1: note: clt_thead should be renamed clt_ctail *)
non associative with precedence 45
for @{ 'PConv $L $T1 $T2 }.
-notation "hvbox( T1 ⬌ break T2 )"
+notation "hvbox( T1 â\8a¢ â¬\8c break T2 )"
non associative with precedence 45
- for @{ 'PConv $T1 $T2 }.
+ for @{ 'CPConv $T1 $T2 }.
(* Equivalence **************************************************************)
non associative with precedence 45
for @{ 'PConvStar $L $T1 $T2 }.
-notation "hvbox( T1 ⬌* break T2 )"
+notation "hvbox( T1 â\8a¢ â¬\8c* break T2 )"
non associative with precedence 45
- for @{ 'PConvStar $T1 $T2 }.
+ for @{ 'CPConvStar $T1 $T2 }.
(* Basic_1: removed theorems 6:
pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
- pr2_gen_ctail pr2_ctail
+ pr2_gen_ctail pr2_ctail
Basic_1: removed local theorems 3:
pr2_free_free pr2_free_delta pr2_delta_delta
*)
@ex2_1_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *)
qed.
+lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2.
+ L.ⓛV ⊢ T1 ➡ T2 → L ⊢ ⓛV1. T1 ➡ ⓛV2. T2.
+#L #V1 #V2 * #V0 #HV10 #HV02 #V #T1 #T2 * #T0 #HT10 #HT02
+lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02
+@(ex2_1_intro … (ⓛV0.T0)) /2 width=1/ -V1 -T1 (**) (* explicit constructors *)
+@tpss_bind // -V0
+@(tpss_lsubs_conf (L.ⓛV)) // -T0 -T2 /2 width=1/
+qed.
+
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was: pr2_gen_lref *)
--- /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_ltpss.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 (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_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/
+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/tpr_tpr.ma".
+include "basic_2/reducibility/ltpr.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* Main properties **********************************************************)
+
+theorem ltpr_conf: ∀L0:lenv. ∀L1. L0 ➡ L1 → ∀L2. L0 ➡ L2 →
+ ∃∃L. L1 ➡ L & L2 ➡ L.
+#L0 #L1 #H elim H -L0 -L1 /2 width=3/
+#K0 #K1 #I #V0 #V1 #_ #HV01 #IHK01 #L2 #H
+elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct
+elim (IHK01 … HK02) -K0 #K #HK1 #HK2
+elim (tpr_conf … HV01 HV02) -V0 /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/reducibility/tpr_tpss.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* 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.
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ /2 width=3/
+| #L1 #I #V1 #X #H
+ elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
+| #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/
+| #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/
+]
+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.
(* Advanced inversion lemmas ************************************************)
-fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → e = 1 →
- ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
-#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
+fact tps_inv_S2_aux: ∀L,T1,T2,d,e1. L ⊢ T1 [d, e1] ▶ T2 → ∀e2. e1 = e2 + 1 →
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e2] ▶ T2.
+#L #T1 #T2 #d #e1 #H elim H -L -T1 -T2 -d -e1
[ //
-| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct
- >(le_to_le_to_eq … Hdi ?) /2 width=1/ -d #K #V #HLK
- lapply (ldrop_mono … HLK0 … HLK) #H destruct
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
- >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 // /2 width=1/
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
- >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 … HLK) -IHT12 //
+| #L #K0 #V0 #W #i #d #e1 #Hdi #Hide1 #HLK0 #HV0 #e2 #He12 #K #V #HLK destruct
+ elim (lt_or_ge i (d+1)) #HiSd
+ [ -Hide1 -HV0
+ lapply (le_to_le_to_eq … Hdi ?) /2 width=1/ #H destruct
+ lapply (ldrop_mono … HLK0 … HLK) #H destruct
+ | -V -Hdi /2 width=4/
+ ]
+| /4 width=3/
+| /3 width=3/
]
qed.
+lemma tps_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 [d, e + 1] ▶ T2 →
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e] ▶ T2.
+/2 width=3/ qed-.
+
lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶ T2 →
∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
-/2 width=8/ qed-.
+#L #T1 #T2 #d #HT12 #K #V #HLK
+lapply (tps_inv_S2 … T1 T2 … 0 … HLK) -K // -HT12 #HT12
+lapply (tps_inv_refl_O2 … HT12) -HT12 //
+qed-.
(* Relocation properties ****************************************************)
#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
qed-.
+lemma ltpss_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 ltpss_strap: ∀L1,L,L2,d,e.
(* *)
(**************************************************************************)
+include "basic_2/unfold/tpss_tpss.ma".
include "basic_2/unfold/ltpss_tpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+(* Advanced properties ******************************************************)
+
(* Main properties **********************************************************)
theorem ltpss_trans_eq: ∀L1,L,L2,d,e.
#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
>(plus_minus_m_m d 1) // /2 width=1/
qed.
+
+fact ltps_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶ L1 →
+ ∀K2,L2,d2,e2. K2 [d2, e2] ▶ L2 → K1 = K → K2 = K →
+ ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
+#K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
+[ -IH /3 width=3/
+| -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
+ [ /2 width=3/
+ | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/
+ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/
+ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/
+ ]
+| #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
+ [ -IH #d2 #e2 #H1 #H2 destruct
+ | -IH #K2 #I2 #V2 #H1 #H2 destruct
+ @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *)
+ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
+ [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
+ | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
+ ]
+ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
+ [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
+ | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
+ ]
+ ]
+| #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
+ [ -IH #d2 #e2 #H1 #H2 destruct
+ | -IH #K2 #I2 #V2 #H1 #H2 destruct
+ @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *)
+ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
+ [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
+ | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
+ ]
+ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
+ [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
+ | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
+ ]
+ ]
+]
+qed.
+
+lemma ltps_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.
+/2 width=7/ qed.
+
+axiom ltpss_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.
+(*
+fact ltpss_conf_aux: ∀K1,L1,d1,e1. K1 [d1, e1] ▶* L1 →
+ ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K2 →
+ ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
+#K1 #L1 #d1 #e1 #H @(ltpss_ind_dx … H) -K1 /2 width=3/
+#X1 #K1 #HXK1 #HKL1 #IHKL1 #K2 #L2 #d2 #e2 #H @(ltpss_ind_dx … H) -K2
+[ -IHKL1 #H destruct
+ lapply (ltpss_strap … HXK1 HKL1) -K1 /2 width=3/
+| #X2 #K2 #HXK2 #HKL2 #_ #H destruct
+ elim (ltps_conf … HXK1 … HXK2) -X2 #K #HK1 #HK2
+ elim (IHKL1 … HK1 ?) // -K1 #L #HL1 #HKL
+ @(ex2_1_intro … K) //
+*)
\ No newline at end of file
* #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/
qed-.
+lemma tpss_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 [d, e + 1] ▶* T2 →
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 [d + 1, e] ▶* T2.
+#L #T1 #T2 #d #e #H #K #V #HLK @(tpss_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT
+lapply (tps_inv_S2 … HT2 … HLK) -HT2 -HLK /2 width=3/
+qed-.
+
lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 →
∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
projects / helm.git / commitdiff