%.stats:
@printf '\x1B[1;40;37m'
- @printf '%-15s %-42s' 'Statistics for:' $*
+ @printf '%-15s %-43s' 'Statistics for:' $*
@printf '\x1B[0m\n'
@printf '\x1B[1;40;35m'
@printf '%-8s %6i' Chars $(CHARS)
@printf ' %-8s %5i' Lines `cat $(MAS) | wc -l`
@printf ' %-6s %3i' Pages `echo $$(($(CHARS) / 5120))`
- @printf ' %-10s' ''
+ @printf ' %-11s' ''
@printf '\x1B[0m\n'
@printf '\x1B[1;40;36m'
@printf '%-8s %6i' Sources `ls $(MAS) | wc -l`
- @printf ' %-40s' ''
+ @printf ' %-41s' ''
# @printf ' %-8s %5i' Objs `ls *.vo | wc -l`
# @printf ' %-6s %3i' Files `ls *.v | wc -l`
@printf '\x1B[0m\n'
@printf '%-8s %6i' Theorems `grep "theorem " $(MAS) | wc -l`
@printf ' %-8s %5i' Lemmas `grep "lemma " $(MAS) | wc -l`
@printf ' %-6s %3i' Facts `grep "fact " $(MAS) | wc -l`
- @printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l`
+ @printf ' %-6s %4i' Proofs `grep qed $(MAS) | wc -l`
@printf '\x1B[0m\n'
@printf '\x1B[1;40;33m'
@printf '%-8s %6i' Defs `grep "definition\|let rec\|inductive\|record" $(MAS) | wc -l`
- @printf ' %-40s' ''
+ @printf ' %-41s' ''
# @printf ' %-8s %5i' Local `grep "Local" *.v | wc -l`
@printf '\x1B[0m\n'
@printf '\x1B[1;40;31m'
@printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l`
@printf ' %-8s %5i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l`
@printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
- @printf ' %-10s' ''
+ @printf ' %-11s' ''
@printf '\x1B[0m\n'
# summary ####################################################################
--- /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/cpr_aaa.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A.
+#L #T1 #A #HT1 #T2 #HT12
+@(TC_Conf3 … HT1 ? HT12) /2 width=3/
+qed.
include "basic_2/reducibility/cpr_lift.ma".
include "basic_2/reducibility/cpr_cpr.ma".
-include "basic_2/reducibility/lcpr_cpr.ma".
-include "basic_2/computation/cprs_lcpr.ma".
+include "basic_2/reducibility/lfpr_cpr.ma".
+include "basic_2/computation/cprs_lfpr.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T2 →
∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
#L #V1 #V2 #HV12 #T1 #T2 #HT12
-lapply (lcpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/
+lapply (lfpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/
qed.
(* Basic_1: was: pr3_strip *)
#L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1
[ /2 width=1/
| #T1 #T #HT1 #_ #IHT1
- lapply (lcpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1
+ lapply (lfpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1
@(cprs_trans … IHT1) -IHT1 /2 width=1/
]
qed.
qed.
(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
-lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
+lemma lcpr_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ →
∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT2
+++ /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_ltpss.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/computation/cprs_cprs.ma".
-include "basic_2/computation/lcprs_lcprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties exploiting context-senstive computation on local environments *)
-
-(* Basic_1: was just: pr3_pr3_pr3_t *)
-lemma lcprs_cprs_trans: ∀L1,L2. L1 ⊢ ➡* L2 →
- ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-#L1 #L2 #HL12 @(lcprs_ind … HL12) -L2 // /3 width=3/
-qed.
-
-lemma lcprs_cpr_trans: ∀L1,L2. L1 ⊢ ➡* L2 →
- ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
-/3 width=3 by lcprs_cprs_trans, inj/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-(* Basic_1: was pr3_gen_abbr *)
-lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡* U2 →
- (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
- U2 = ⓓ{a}V2. T2
- ) ∨
- ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
-#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
-#U0 #U2 #_ #HU02 * *
-[ #V0 #T0 #HV10 #HT10 #H destruct
- elim (cpr_inv_abbr1 … HU02) -HU02 *
- [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct
- lapply (cpr_intro … HV0 … HV2) -HV2 #HV02
- lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02
- lapply (lcprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/
- | #T2 #HT02 #HUT2
- lapply (lcprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02
- lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/
- ]
-| #U1 #HTU1 #HU01
- elim (lift_total U2 0 1) #U #HU2
- lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 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/reducibility/ltpr_tps.ma".
+include "basic_2/reducibility/cpr_ltpss.ma".
+include "basic_2/reducibility/lfpr.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties concerning focalized parallel reduction on local environments *)
+
+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 lfpr_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/computation/cprs_cprs.ma".
+include "basic_2/computation/lfprs_lfprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties on focalized computation for local environments ***************)
+
+(* Basic_1: was just: pr3_pr3_pr3_t *)
+lemma lfprs_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ →
+ ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #HL12 @(lfprs_ind … HL12) -L2 // /3 width=3/
+qed.
+
+lemma lfprs_cpr_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ →
+ ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
+/3 width=3 by lfprs_cprs_trans, inj/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was pr3_gen_abbr *)
+lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡* U2 →
+ (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
+ U2 = ⓓ{a}V2. T2
+ ) ∨
+ ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
+#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpr_inv_abbr1 … HU02) -HU02 *
+ [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct
+ lapply (cpr_intro … HV0 … HV2) -HV2 #HV02
+ lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02
+ lapply (lfprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/
+ | #T2 #HT02 #HUT2
+ lapply (lfprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02
+ lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/
+ ]
+| #U1 #HTU1 #HU01
+ elim (lift_total U2 0 1) #U #HU2
+ lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=3/
+]
+qed-.
include "basic_2/grammar/tstc.ma".
include "basic_2/computation/cprs_lift.ma".
-include "basic_2/computation/cprs_lcprs.ma".
+include "basic_2/computation/cprs_lfprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION 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/grammar/tstc_tstc.ma".
-include "basic_2/computation/cprs_cprs.ma".
-include "basic_2/computation/csn_lift.ma".
-include "basic_2/computation/csn_cpr.ma".
-include "basic_2/computation/csn_alt.ma".
-
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T.
-#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
-@csn_intro #T0 #HLT0 #HT0
-@IHT /2 width=2/ -IHT -HT0 /2 width=3/
-qed.
-
-lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T.
-#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
-@csn_intro #X #H1 #H2
-elim (cpr_inv_abbr1 … H1) -H1 *
-[ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct
- lapply (cpr_intro … HLV0 HLV01) -HLV01 #HLV1
- lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1
- elim (eq_false_inv_tpair_sn … H2) -H2
- [ #HV1 @IHV // /2 width=1/ -HV1
- @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
- | -IHV -HLV1 * #H destruct /3 width=1/
- ]
-| -IHV -IHT -H2 #T0 #HLT0 #HT0
- lapply (csn_cpr_trans … HT … HLT0) -T #HLT0
- lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/
-]
-qed.
-
-fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U →
- ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
-#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct
-lapply (csn_fwd_pair_sn … HVT) #HV
-lapply (csn_fwd_bind_dx … HVT) #HT -HVT
-@csn_intro #X #H #H2
-elim (cpr_inv_appl1 … H) -H *
-[ #V0 #Y #HLV0 #H #H0 destruct
- elim (cpr_inv_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct
- elim (eq_false_inv_beta … H2) -H2
- [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0
- @csn_abbr /2 width=3/ -HV
- @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
- | -IHW -HLW0 -HV -HT * #H #HVT0 destruct
- @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/
- ]
-| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct
- lapply (lcpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01
- @csn_abbr /2 width=3/ -HV
- @(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
-| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct
-]
-qed.
-
-(* Basic_1: was: sn3_beta *)
-lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T →
- L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
-/2 width=3/ qed.
-
-fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
-#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
-lapply (csn_fwd_pair_sn … HVT) #HV
-lapply (csn_fwd_bind_dx … HVT) -HVT #HVT
-@csn_intro #X #HL #H
-elim (cpr_inv_appl1 … HL) -HL *
-[ -HV #V0 #Y #HLV10 #HL #H0 destruct
- elim (cpr_inv_abbr1 … HL) -HL *
- [ #V3 #V4 #T3 #HV3 #HLV34 #HLT3 #H0 destruct
- lapply (cpr_intro … HV3 HLV34) -HLV34 #HLV34
- elim (lift_total V0 0 1) #V5 #HV05
- elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V4.ⓐV5.T3))
- [ -IHVT #H0 destruct
- elim (eq_false_inv_tpair_sn … H) -H
- [ -HLV10 -HLV34 -HV3 -HLT3 -HVT
- >(lift_inj … HV12 … HV05) -V5
- #H elim (H ?) //
- | * #_ #H elim (H ?) //
- ]
- | -H -HVT #H
- lapply (cpr_lift (L. ⓓV) … HV12 … HV05 HLV10) -HLV10 -HV12 /2 width=1/ #HV25
- lapply (ltpr_cpr_trans (L. ⓓV) … HLT3) /2 width=1/ -HLT3 #HLT3
- @(IHVT … H … HV05) -IHVT // -H -HV05 /3 width=1/
- ]
- | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
- lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0
- lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
- @(csn_cpr_trans … HVY) /2 width=1/
- ]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct
-| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct
- lapply (cpr_lift (L. ⓓW0) … HV12 … HV03 HLV10) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23
- lapply (lcpr_cpr_trans (L. ⓓW0) … HLT01) -HLT01 /2 width=1/ #HLT01
- @csn_abbr /2 width=3/ -HV
- @(csn_lcpr_conf (L. ⓓW0)) /2 width=1/ -W1
- @(csn_cprs_trans … HVT) -HVT /2 width=1/
-]
-qed.
-
-lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
-/2 width=5/ qed.
-
-(* Basic_1: was only: sn3_appl_appl *)
-lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1.
- L ⊢ ⬊* T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) →
- 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1.
-#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
-@csn_intro #X #HL #H
-elim (cpr_inv_appl1_simple … HL ?) -HL //
-#V0 #T0 #HLV0 #HLT10 #H0 destruct
-elim (eq_false_inv_tpair_sn … H) -H
-[ -IHT1 #HV0
- @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10
- @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0
- #T2 #HLT12 #HT12
- @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
- @H2T1 -H2T1 // -HLT12 /2 width=1/
-| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
- elim (tstc_dec T1 T0) #H2T10
- [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1
- #T2 #HLT02 #HT02
- @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/
- | -IHT1 -H3T1 -H1T10
- @H2T1 -H2T1 /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/grammar/tstc_tstc.ma".
+include "basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/csn_lift.ma".
+include "basic_2/computation/csn_cpr.ma".
+include "basic_2/computation/csn_alt.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma csn_lfpr_conf: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T.
+#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
+@csn_intro #T0 #HLT0 #HT0
+@IHT /2 width=2/ -IHT -HT0 /2 width=3/
+qed.
+
+lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T.
+#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
+@csn_intro #X #H1 #H2
+elim (cpr_inv_abbr1 … H1) -H1 *
+[ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct
+ lapply (cpr_intro … HLV0 HLV01) -HLV01 #HLV1
+ lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1
+ elim (eq_false_inv_tpair_sn … H2) -H2
+ [ #HV1 @IHV // /2 width=1/ -HV1
+ @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
+ | -IHV -HLV1 * #H destruct /3 width=1/
+ ]
+| -IHV -IHT -H2 #T0 #HLT0 #HT0
+ lapply (csn_cpr_trans … HT … HLT0) -T #HLT0
+ lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/
+]
+qed.
+
+fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U →
+ ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
+#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct
+lapply (csn_fwd_pair_sn … HVT) #HV
+lapply (csn_fwd_bind_dx … HVT) #HT -HVT
+@csn_intro #X #H #H2
+elim (cpr_inv_appl1 … H) -H *
+[ #V0 #Y #HLV0 #H #H0 destruct
+ elim (cpr_inv_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct
+ elim (eq_false_inv_beta … H2) -H2
+ [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0
+ @csn_abbr /2 width=3/ -HV
+ @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
+ | -IHW -HLW0 -HV -HT * #H #HVT0 destruct
+ @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/
+ ]
+| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct
+ lapply (lfpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01
+ @csn_abbr /2 width=3/ -HV
+ @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
+| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct
+]
+qed.
+
+(* Basic_1: was: sn3_beta *)
+lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T →
+ L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
+/2 width=3/ qed.
+
+fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
+ ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
+#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
+lapply (csn_fwd_pair_sn … HVT) #HV
+lapply (csn_fwd_bind_dx … HVT) -HVT #HVT
+@csn_intro #X #HL #H
+elim (cpr_inv_appl1 … HL) -HL *
+[ -HV #V0 #Y #HLV10 #HL #H0 destruct
+ elim (cpr_inv_abbr1 … HL) -HL *
+ [ #V3 #V4 #T3 #HV3 #HLV34 #HLT3 #H0 destruct
+ lapply (cpr_intro … HV3 HLV34) -HLV34 #HLV34
+ elim (lift_total V0 0 1) #V5 #HV05
+ elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V4.ⓐV5.T3))
+ [ -IHVT #H0 destruct
+ elim (eq_false_inv_tpair_sn … H) -H
+ [ -HLV10 -HLV34 -HV3 -HLT3 -HVT
+ >(lift_inj … HV12 … HV05) -V5
+ #H elim (H ?) //
+ | * #_ #H elim (H ?) //
+ ]
+ | -H -HVT #H
+ lapply (cpr_lift (L. ⓓV) … HV12 … HV05 HLV10) -HLV10 -HV12 /2 width=1/ #HV25
+ lapply (ltpr_cpr_trans (L. ⓓV) … HLT3) /2 width=1/ -HLT3 #HLT3
+ @(IHVT … H … HV05) -IHVT // -H -HV05 /3 width=1/
+ ]
+ | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
+ lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0
+ lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
+ @(csn_cpr_trans … HVY) /2 width=1/
+ ]
+| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct
+| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct
+ lapply (cpr_lift (L. ⓓW0) … HV12 … HV03 HLV10) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23
+ lapply (lfpr_cpr_trans (L. ⓓW0) … HLT01) -HLT01 /2 width=1/ #HLT01
+ @csn_abbr /2 width=3/ -HV
+ @(csn_lfpr_conf (L. ⓓW0)) /2 width=1/ -W1
+ @(csn_cprs_trans … HVT) -HVT /2 width=1/
+]
+qed.
+
+lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
+ ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
+/2 width=5/ qed.
+
+(* Basic_1: was only: sn3_appl_appl *)
+lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1.
+ L ⊢ ⬊* T1 →
+ (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) →
+ 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1.
+#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
+@csn_intro #X #HL #H
+elim (cpr_inv_appl1_simple … HL ?) -HL //
+#V0 #T0 #HLV0 #HLT10 #H0 destruct
+elim (eq_false_inv_tpair_sn … H) -H
+[ -IHT1 #HV0
+ @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10
+ @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0
+ #T2 #HLT12 #HT12
+ @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
+ @H2T1 -H2T1 // -HLT12 /2 width=1/
+| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
+ elim (tstc_dec T1 T0) #H2T10
+ [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1
+ #T2 #HLT02 #HT02
+ @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/
+ | -IHT1 -H3T1 -H1T10
+ @H2T1 -H2T1 /2 width=1/
+ ]
+]
+qed.
include "basic_2/computation/acp_cr.ma".
include "basic_2/computation/cprs_tstc_vector.ma".
-include "basic_2/computation/csn_lcpr.ma".
+include "basic_2/computation/csn_lfpr.ma".
include "basic_2/computation/csn_vector.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
+++ /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 COMPUTATION ON LOCAL ENVIRONMENTS *************)
-
-definition lcprs: relation lenv ≝ TC … lcpr.
-
-interpretation
- "context-sensitive parallel computation (environment)"
- 'CPRedStar L1 L2 = (lcprs L1 L2).
-
-(* Basic eliminators ********************************************************)
-
-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) //
-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 *********************************************************)
-
-lemma lcprs_refl: ∀L. L ⊢ ➡* L.
-/2 width=1/ qed.
-
-lemma lcprs_strap1: ∀L1,L,L2.
- L1 ⊢ ➡* L → L ⊢ ➡ L2 → L1 ⊢ ➡* L2.
-/2 width=3/ qed.
-
-lemma lcprs_strap2: ∀L1,L,L2.
- L1 ⊢ ➡ L → L ⊢ ➡* L2 → 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/reducibility/lcpr_aaa.ma".
-include "basic_2/computation/cprs.ma".
-include "basic_2/computation/lcprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
-
-(* Properties about atomic arity assignment on terms ************************)
-
-lemma aaa_lcprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A.
-#L1 #T #A #HT #L2 #HL12
-@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/
-qed.
-
-lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A.
-#L #T1 #A #HT1 #T2 #HT12
-@(TC_Conf3 … HT1 ? HT12) /2 width=3/
-qed.
-
-lemma aaa_lcprs_cprs_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/reducibility/lcpr_cpr.ma".
-include "basic_2/computation/cprs.ma".
-include "basic_2/computation/lcprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
-
-(* Advanced properties ******************************************************)
-
-lemma lcprs_pair_dx: ∀I,L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
- L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2.
-#I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2
-/3 width=1/ /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/lcpr_lcpr.ma".
-include "basic_2/computation/lcprs_cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
-
-(* Advanced properties ******************************************************)
-
-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.
-
-lemma lcprs_pair: ∀L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
- ∀I. L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2.
-#L1 #L2 #H @(lcprs_ind … H) -L2 /2 width=1/
-#L #L2 #_ #HL2 #IHL1 #V1 #V2 #HV12 #I
-@(lcprs_trans … (L.ⓑ{I}V1)) /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/reducibility/lfpr.ma".
+
+(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
+
+definition lfprs: relation lenv ≝ TC … lfpr.
+
+interpretation
+ "focalized parallel computation (environment)"
+ 'FocalizedPRedStar L1 L2 = (lfprs L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma lfprs_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 lfprs_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 lfprs_refl: ∀L. ⦃L⦄ ➡* ⦃L⦄.
+/2 width=1/ qed.
+
+lemma lfprs_strap1: ∀L1,L,L2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
+/2 width=3/ qed.
+
+lemma lfprs_strap2: ∀L1,L,L2. ⦃L1⦄ ➡ ⦃L⦄ → ⦃L⦄ ➡* ⦃L2⦄ → ⦃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/reducibility/lfpr_aaa.ma".
+include "basic_2/computation/lfprs.ma".
+
+(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_lfprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ → L2 ⊢ T ⁝ A.
+#L1 #T #A #HT #L2 #HL12
+@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/
+qed.
+(*
+(* Note: this should be rephrased in terms of fprs *)
+lemma aaa_lfprs_cprs_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/reducibility/lfpr_cpr.ma".
+include "basic_2/computation/cprs.ma".
+include "basic_2/computation/lfprs.ma".
+
+(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
+
+(* Advanced properties ******************************************************)
+
+lemma lfprs_pair_dx: ∀I,L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
+ ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄.
+#I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2
+/3 width=1/ /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/lfpr_lfpr.ma".
+include "basic_2/computation/lfprs_cprs.ma".
+
+(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
+
+(* Advanced properties ******************************************************)
+
+lemma lfprs_strip: ∀L,L1. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ➡ ⦃L2⦄ →
+ ∃∃L0. ⦃L1⦄ ➡ ⦃L0⦄ & ⦃L2⦄ ➡* ⦃L0⦄.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+theorem lfprs_conf: ∀L,L1. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ →
+ ∃∃L0. ⦃L1⦄ ➡* ⦃L0⦄ & ⦃L2⦄ ➡* ⦃L0⦄.
+/3 width=3/ qed.
+
+theorem lfprs_trans: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
+/2 width=3/ qed.
+
+lemma lfprs_pair: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
+ ∀I. ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄.
+#L1 #L2 #H @(lfprs_ind … H) -L2 /2 width=1/
+#L #L2 #_ #HL2 #IHL1 #V1 #V2 #HV12 #I
+@(lfprs_trans … (L.ⓑ{I}V1)) /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/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.
--- /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/lfpr.ma".
+
+(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************)
+
+definition lfpc: relation lenv ≝
+ λL1,L2. ⦃L1⦄ ➡ ⦃L2⦄ ∨ ⦃L2⦄ ➡ ⦃L1⦄.
+
+interpretation
+ "focalized parallel conversion (local environment)"
+ 'FocalizedPConv L1 L2 = (lfpc L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lfpc_refl: ∀L. ⦃L⦄ ⬌ ⦃L⦄.
+/2 width=1/ qed.
+
+lemma lfpc_sym: ∀L1,L2. ⦃L1⦄ ⬌ ⦃L2⦄ → ⦃L2⦄ ⬌ ⦃L1⦄.
+#L1 #L2 * /2 width=1/
+qed.
+
+lemma lfpc_lfpr: ∀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/lfpc.ma".
+
+(* FOCALIZED PARALLEL CONVERSION ON LOCAL ENVIRONMENTS **********************)
+
+(* Main properties **********************************************************)
+
+theorem lfpc_conf: ∀L0,L1,L2. ⦃L0⦄ ⬌ ⦃L1⦄ → ⦃L0⦄ ⬌ ⦃L2⦄ →
+ ∃∃L. ⦃L1⦄ ⬌ ⦃L⦄ & ⦃L2⦄ ⬌ ⦃L⦄.
+/3 width=3/ qed.
include "basic_2/computation/csn_aaa.ma".
include "basic_2/computation/xprs_aaa.ma".
include "basic_2/computation/xprs_cprs.ma".
-include "basic_2/equivalence/lcpcs_aaa.ma".
+include "basic_2/equivalence/cpcs_aaa.ma".
include "basic_2/dynamic/snv.ma".
(* STRATIFIED NATIVE VALIDITY FOR 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/computation/cprs_aaa.ma".
+include "basic_2/equivalence/cpcs_cpcs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
+
+(* Main properties about atomic arity assignment on terms *******************)
+
+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/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 by lcpcs_trans, lcprs_comm/ qed.
-
-theorem lcpcs_canc_dx: ∀L,L1,L2. L1 ⊢ ⬌* L → L2 ⊢ ⬌* L → L1 ⊢ ⬌* L2.
-/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/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.
--- /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/lfpc.ma".
+
+(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************)
+
+definition lfpcs: relation lenv ≝ TC … lfpc.
+
+interpretation "focalized parallel equivalence (local environment)"
+ 'FocalizedPConvStar L1 L2 = (lfpcs L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma lfpcs_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 lfpcs_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 lfpcs_refl: ∀L. ⦃L⦄ ⬌* ⦃L⦄.
+/2 width=1/ qed.
+
+lemma lfpcs_strap1: ∀L1,L,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/2 width=3/ qed.
+
+lemma lfpcs_strap2: ∀L1,L,L2. ⦃L1⦄ ⬌ ⦃L⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/2 width=3/ qed.
+
+lemma lfpcs_lfpr_dx: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/3 width=1/ qed.
+
+lemma lfpcs_lfpr_sn: ∀L1,L2. ⦃L2⦄ ➡ ⦃L1⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/3 width=1/ qed.
+
+lemma lfpcs_lfpr_strap1: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/3 width=3/ qed.
+
+lemma lfpcs_lfpr_strap2: ∀L1,L. ⦃L1⦄ ➡ ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/3 width=3/ qed.
+
+lemma lfpcs_lfpr_div: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡ ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/3 width=3/ qed.
+
+lemma lfpcs_lfpr_conf: ∀L1,L. ⦃L⦄ ➡ ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/3 width=3/ qed.
+
+lemma lfprs_comm: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ⦃L2⦄ ⬌* ⦃L1⦄.
+#L1 #L2 #H @(lfpcs_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/lfprs_aaa.ma".
+include "basic_2/equivalence/lfpcs_lfpcs.ma".
+
+(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************)
+
+(* Main properties about atomic arity assignment on terms *******************)
+
+theorem aaa_lfpcs_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 (lfpcs_inv_lfprs … HL12) -HL12 #L #HL1 #HL2
+lapply (aaa_lfprs_conf … HT1 … HL1) -L1 #HT1
+lapply (aaa_lfprs_conf … HT2 … HL2) -L2 #HT2
+lapply (aaa_mono … HT1 … HT2) -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/lfprs_lfprs.ma".
+include "basic_2/conversion/lfpc_lfpc.ma".
+include "basic_2/equivalence/lfpcs_lfprs.ma".
+
+(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lfpcs_inv_lfprs: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ →
+ ∃∃L. ⦃L1⦄ ➡* ⦃L⦄ & ⦃L2⦄ ➡* ⦃L⦄.
+#L1 #L2 #H @(lfpcs_ind … H) -L2
+[ /3 width=3/
+| #L #L2 #_ #HL2 * #L0 #HL10 elim HL2 -HL2 #HL2 #HL0
+ [ elim (lfprs_strip … HL0 … HL2) -L #L #HL0 #HL2
+ lapply (lfprs_strap1 … HL10 … HL0) -L0 /2 width=3/
+ | lapply (lfprs_strap2 … HL2 … HL0) -L /2 width=3/
+ ]
+]
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma lfpcs_strip: ∀L,L1. ⦃L⦄ ⬌* ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌ ⦃L2⦄ →
+ ∃∃L0. ⦃L1⦄ ⬌ ⦃L0⦄ & ⦃L2⦄ ⬌* ⦃L0⦄.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+theorem lfpcs_trans: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/2 width=3/ qed.
+
+theorem lfpcs_canc_sn: ∀L,L1,L2. ⦃L⦄ ⬌* ⦃L1⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/3 width=3 by lfpcs_trans, lfprs_comm/ qed.
+
+theorem lfpcs_canc_dx: ∀L,L1,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L2⦄ ⬌* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+/3 width=3 by lfpcs_trans, lfprs_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/computation/lfprs.ma".
+include "basic_2/equivalence/lfpcs.ma".
+
+(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************)
+
+(* Properties on focalized computation for local environments ***************)
+
+lemma lfpcs_lfprs_dx: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+#L1 #L2 #H @(lfprs_ind … H) -L2 /width=1/ /3 width=3/
+qed.
+
+lemma lfpcs_lfprs_sn: ∀L1,L2. ⦃L2⦄ ➡* ⦃L1⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+#L1 #L2 #H @(lfprs_ind_dx … H) -L2 /width=1/ /3 width=3/
+qed.
+
+lemma lfpcs_lfprs_strap1: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+#L1 #L #HL1 #L2 #H @(lfprs_ind … H) -L2 /width=1/ /2 width=3/
+qed.
+
+lemma lfpcs_lfprs_strap2: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+#L1 #L #H #L2 #HL2 @(lfprs_ind_dx … H) -L1 /width=1/ /2 width=3/
+qed.
+
+lemma lfpcs_lfprs_div: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+#L1 #L #HL1 #L2 #H @(lfprs_ind_dx … H) -L2 /width=1/ /2 width=3/
+qed.
+
+lemma lfpcs_lfprs_conf: ∀L1,L. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+#L1 #L #H #L2 #HL2 @(lfprs_ind … H) -L1 /width=1/ /2 width=3/
+qed.
+
+lemma lfprs_div: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+#L1 #L #HL1 #L2 #H @(lfprs_ind_dx … H) -L2 /2 width=1/ /2 width=3/
+qed.
(* Basic properties *********************************************************)
lemma shift_append_assoc: ∀L,K. ∀T:term. (L @@ K) @@ T = L @@ K @@ T.
-#L #K elim K -K normalize //
+#L #K elim K -K // normalize //
qed.
(* Basic inversion lemmas ***************************************************)
| #K1 #I1 #V1 #IH * normalize
[ #L1 #L2 #_ <plus_n_Sm #H destruct
| #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
- elim (IH … e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+ -H1 (**) (* destruct: the destucted equality is not erased *)
+ elim (IH … e0 ?) -IH /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
]
]
qed-.
normalize in H2; >append_length in H2; #H
elim (plus_xySz_x_false … (sym_eq … H))
| #K2 #I2 #V2 #L1 #L2 #H1 #H2 destruct (**) (* destruct does not simplify well *)
- elim (IH … e0 ?) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+ -H1 (**) (* destruct: the destucted equality is not erased *)
+ elim (IH … e0 ?) -IH // -H2 #H1 #H2 destruct /2 width=1/
]
]
qed-.
(∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
∀L. R L.
/3 width=2 by lenv_ind_dx_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma length_inv_pos_sn_append: ∀d,L. 1 + d = |L| →
+ ∃∃I,K,V. d = |K| & L = ⋆. ⓑ{I}V @@ K.
+#d >commutative_plus @(nat_ind_plus … d) -d
+[ #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
+ >(length_inv_zero_sn … H1) -K
+ @(ex2_3_intro … (⋆)) // (**) (* explicit constructor *)
+| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
+ >H1 in IHd; -H1 #IHd
+ elim (IHd K ?) -IHd // #J #L #W #H1 #H2 destruct
+ @(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *)
+ >append_length /2 width=1/
+]
+qed-.
#R #L1 #L2 #H elim H -L1 -L2 normalize //
qed-.
+(* Advanced inversion lemmas ************************************************)
+
+lemma lpx_inv_append1: ∀R,L1,K1,L. lpx R (K1 @@ L1) L →
+ ∃∃K2,L2. lpx R K1 K2 & lpx R L1 L2 & L = K2 @@ L2.
+#R #L1 elim L1 -L1 normalize
+[ #K1 #K2 #HK12
+ @(ex3_2_intro … K2 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *)
+| #L1 #I #V1 #IH #K1 #X #H
+ elim (lpx_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct
+ elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #HL12 #H destruct
+ @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *)
+]
+qed-.
+
+lemma lpx_inv_append2: ∀R,L2,K2,L. lpx R L (K2 @@ L2) →
+ ∃∃K1,L1. lpx R K1 K2 & lpx R L1 L2 & L = K1 @@ L1.
+#R #L2 elim L2 -L2 normalize
+[ #K2 #K1 #HK12
+ @(ex3_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=5/ does not work *)
+| #L2 #I #V2 #IH #K2 #X #H
+ elim (lpx_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct
+ elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #HL12 #H destruct
+ @(ex3_2_intro … HK12) [2: /2 width=2/ | skip | // ] (* explicit constructor, /3 width=5/ does not work *)
+]
+qed-.
+
(* Basic properties *********************************************************)
lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R).
/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *)
qed.
-lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2.
+lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2.
#R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/
qed.
non associative with precedence 45
for @{ 'PRed $L $T1 $T2 }.
-notation "hvbox( L1 ⊢ ➡ break term 46 L2 )"
- non associative with precedence 45
- for @{ 'CPRed $L1 $L2 }.
-
notation "hvbox( ⦃ L1 ⦄ ➡ break ⦃ L2 ⦄ )"
non associative with precedence 45
for @{ 'FocalizedPRed $L1 $L2 }.
non associative with precedence 45
for @{ 'FocalizedPRed $L1 $T1 $L2 $T2 }.
+notation "hvbox( L ⊢ break ⦃ L1, break T1 ⦄ ➡ break ⦃ L2 , break T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'FocalizedPRed $L $L1 $T1 $L2 $T2 }.
+
notation "hvbox( ⦃ L1 ⦄ ➡ ➡ break ⦃ L2 ⦄ )"
non associative with precedence 45
for @{ 'FocalizedPRedAlt $L1 $L2 }.
(* Computation **************************************************************)
-notation "hvbox( T1 ➡* break term 46 T2 )"
+notation "hvbox( T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $T1 $T2 }.
-notation "hvbox( L ⊢ break term 46 T1 ➡* break term 46 T2 )"
+notation "hvbox( L ⊢ break term 46 T1 ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStar $L $T1 $T2 }.
-notation "hvbox( T1 ➡➡* break term 46 T2 )"
+notation "hvbox( T1 ➡ ➡ * break term 46 T2 )"
non associative with precedence 45
for @{ 'PRedStarAlt $T1 $T2 }.
-notation "hvbox( L1 ⊢ ➡* break term 46 L2 )"
+notation "hvbox( ⦃ L1 ⦄ ➡ * ⦃ L2 ⦄ )"
non associative with precedence 45
- for @{ 'CPRedStar $L1 $L2 }.
+ for @{ 'FocalizedPRedStar $L1 $L2 }.
-notation "hvbox( L ⊢ break term 46 T1 ➡* break 𝐍 ⦃ T2 ⦄ )"
+notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ T2 ⦄ )"
non associative with precedence 45
for @{ 'PEval $L $T1 $T2 }.
-notation "hvbox( ⬊ * term 46 T )"
+notation "hvbox( ⬊ * term 46 T )"
non associative with precedence 45
for @{ 'SN $T }.
non associative with precedence 45
for @{ 'PConv $L $T1 $T2 }.
-notation "hvbox( T1 ⊢ ⬌ break term 46 T2 )"
+notation "hvbox( ⦃ L1 ⦄ ⬌ ⦃ L2 ⦄ )"
non associative with precedence 45
- for @{ 'CPConv $T1 $T2 }.
+ for @{ 'FocalizedPConv $L1 $L2 }.
(* Equivalence **************************************************************)
non associative with precedence 45
for @{ 'PConvStar $L $T1 $T2 }.
-notation "hvbox( T1 ⊢ ⬌* break term 46 T2 )"
+notation "hvbox( ⦃ L1 ⦄ ⬌ * ⦃ L2 ⦄ )"
non associative with precedence 45
- for @{ 'CPConvStar $T1 $T2 }.
+ for @{ 'FocalizedPConvStar $L1 $L2 }.
(* Dynamic typing ***********************************************************)
--- /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/cpr.ma".
+include "basic_2/reducibility/fpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************)
+
+definition cfpr: lenv → bi_relation lenv term ≝
+ λL,L1,T1,L2,T2. |L1| = |L2| ∧ L ⊢ L1 @@ T1 ➡ L2 @@ T2.
+
+interpretation
+ "context-sensitive parallel reduction (closure)"
+ 'FocalizedPRed L L1 T1 L2 T2 = (cfpr L L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma cfpr_refl: ∀L. bi_reflexive … (cfpr L).
+/2 width=1/ qed.
+
+lemma fpr_cfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⋆ ⊢ ⦃L1, T1⦄ ➡ ⦃L2, T2⦄.
+#L1 #L2 #T1 #T2 * /3 width=1/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cfpr_inv_atom1: ∀L,L2,T1,T2. L ⊢ ⦃⋆, T1⦄ ➡ ⦃L2, T2⦄ → L ⊢ T1 ➡ T2 ∧ L2 = ⋆.
+#L #L2 #T1 #T2 * #H >(length_inv_zero_sn … H) /2 width=1/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma fpr_inv_pair1_sn: ∀I,K1,L2,V1,T1,T2. ⦃⋆.ⓑ{I}V1@@K1, T1⦄ ➡ ⦃L2, T2⦄ →
+ ∃∃K2,V2. V1 ➡ V2 &
+ ⋆.ⓑ{I}V2 ⊢ ⦃K1, T1⦄ ➡ ⦃K2, T2⦄ &
+ L2 = ⋆.ⓑ{I}V2@@K2.
+#I1 #K1 #L2 #V1 #T1 #T2 * >append_length #H
+elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct
+>shift_append_assoc >shift_append_assoc normalize in ⊢ (%→?); #H
+elim (tpr_inv_bind1 … H) -H *
+[ #V0 #T #T0 #HV10 #HT1 #HT0 #H destruct /5 width=5/
+| #T0 #_ #_ #H destruct
+]
+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_ltpss_sn.ma".
+include "basic_2/reducibility/ltpr_aaa.ma".
+include "basic_2/reducibility/cpr_aaa.ma".
+include "basic_2/reducibility/cfpr_cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_fpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A →
+ ∀L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A.
+#L1 #T1 #A #HT1 #L2 #T2 #H
+elim (fpr_inv_all … H) -H
+/4 width=5 by aaa_cpr_conf, aaa_ltpr_conf, aaa_ltpss_sn_conf/
+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_sn_alt.ma".
+include "basic_2/reducibility/ltpr.ma".
+include "basic_2/reducibility/cpr_tpss.ma".
+include "basic_2/reducibility/cpr_cpr.ma".
+include "basic_2/reducibility/cfpr_ltpss.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************)
+
+(* Advanced properties ******************************************************)
+
+lemma fpr_all: ∀L1,L. L1 ➡ L → ∀L2,T1,T2. L ⊢ T1 ➡ T2 →
+ L ⊢ ▶* [0, |L|] L2 → ⦃L1, T1⦄ ➡ ⦃L2, T2⦄.
+#L1 #L #H elim H -L1 -L
+[ #L2 #T1 #T2 #HT12 #HL2
+ lapply (ltpss_sn_inv_atom1 … HL2) -HL2 #H destruct
+ lapply (cpr_inv_atom … HT12) -HT12 /2 width=1/
+| #I #L1 #L #V1 #V #_ #HV1 #IH #X #T1 #T2 #HT12 #H
+ elim (ltpss_sn_inv_tpss21 … H ?) -H // <minus_plus_m_m #L2 #V2 #HL2 #HV2 #H destruct
+ lapply (cpr_bind_dx false … HV1 HT12) -HV1 -HT12 #HT12
+ lapply (cpr_tpss_trans … HT12 (-ⓑ{I}V2.T2) ?) -HT12 /2 width=1/ -HV2 /3 width=1/
+]
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cfpr_inv_all: ∀L1,L2,L0,T1,T2. L0 ⊢ ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ →
+ ∃∃L. L0 @@ L1 ➡ L0 @@ L & L0 @@ L ⊢ T1 ➡ T2 &
+ L0 @@ L ⊢ ▶* [0, |L0| + |L|] L0 @@ L2.
+#L1 @(lenv_ind_dx … L1) -L1
+[ #L2 #L0 #T1 #T2 #H
+ elim (cfpr_inv_atom1 … H) -H #HT12 #H destruct /3 width=4/
+| #I #L1 #V1 #IH #X #L0 #T1 #T2 #H
+ elim (cfpr_inv_pair1 … H) -H #L2 #V #V2 #HV1 #HV2 #HT12 #H destruct
+ elim (IH … HT12) -IH -HT12 #L #HL1 #HT12 #HL2
+ elim (ltpr_inv_append1 … HL1) -HL1 #X #Y #HX #HY #H
+ lapply (ltpr_fwd_length … HX) -HX #HX
+ elim (append_inj_dx … H ?) -H // -HX #_ #H destruct -X
+ lapply (ltpss_sn_fwd_length … HL2) >append_length >append_length #H
+ lapply (injective_plus_r … H) -H #H
+ @(ex3_1_intro … (⋆.ⓑ{I}V@@Y)) <append_assoc // -HT12
+ <append_assoc [ /3 width=1/ ] -HV1 -HY
+ >append_length <associative_plus
+ @(ltpss_sn_dx_trans_eq … HL2) -HL2 >H -H >commutative_plus /3 width=1/
+]
+qed-.
+
+lemma fpr_inv_all: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ →
+ ∃∃L. L1 ➡ L & L ⊢ T1 ➡ T2 & L ⊢ ▶* [0, |L|] L2.
+#L1 #L2 #T1 #T2 #H
+lapply (fpr_cfpr … H) -H #H
+elim (cfpr_inv_all … H) -H /2 width=4/
+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/cpr_lift.ma".
+include "basic_2/reducibility/cpr_ltpss.ma".
+include "basic_2/reducibility/cfpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cfpr_inv_pair1: ∀I,L,K1,L2,V1,T1,T2. L ⊢ ⦃⋆.ⓑ{I}V1@@K1, T1⦄ ➡ ⦃L2, T2⦄ →
+ ∃∃K2,V,V2. V1 ➡ V & L ⊢ V ▶* [0, |L|] V2 &
+ L.ⓑ{I}V ⊢ ⦃K1, T1⦄ ➡ ⦃K2, T2⦄ &
+ L2 = ⋆.ⓑ{I}V2@@K2.
+* #L #K1 #L2 #V1 #T1 #T2 * >append_length #H
+elim (length_inv_pos_sn_append … H) -H #I2 #K2 #V2 #HK12 #H destruct
+>shift_append_assoc >shift_append_assoc normalize in ⊢ (??%%→?); #H
+[ elim (cpr_inv_abbr1 … H) -H *
+ [ #V #V0 #T0 #HV1 #HV0 #HT10 #H destruct /3 width=7/
+ | #T0 #_ #_ #H destruct
+ ]
+| elim (cpr_inv_abst1 … H Abst V2) -H
+ #V #T * #V0 #HV10 #HV0 #HT1 #H destruct
+ lapply (ltpss_sn_cpr_trans (L.ⓛV0) … 0 (|L|+1) … HT1) -HT1 /2 width=1/ #HT12
+ /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/static/aaa_ltpss_sn.ma".
+include "basic_2/reducibility/ltpr_aaa.ma".
+include "basic_2/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+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.
elim (simple_inv_bind … HT1)
]
qed-.
-
+
(* Relocation properties ****************************************************)
(* Basic_1: was: pr2_lift *)
--- /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_tpss.ma".
+include "basic_2/reducibility/cpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
+
+(* Properties on partial unfold for terms ***********************************)
+
+lemma cpr_tpss_trans: ∀L,T1,T. L ⊢ T1 ➡ T →
+ ∀T2. L ⊢ T ▶* [O, |L|] T2 → L ⊢ T1 ➡ T2.
+#L #T1 #T * #T0 #HT10 #HT0 #T2 #HT2
+lapply (tpss_trans_eq … HT0 HT2) -T /2 width=3/
+qed.
+
+lemma cpr_tps_trans: ∀L,T1,T. L ⊢ T1 ➡ T →
+ ∀T2. L ⊢ T ▶ [O, |L|] T2 → L ⊢ T1 ➡ T2.
+/3 width=3/ qed.
include "basic_2/reducibility/tpr.ma".
-(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************)
+(* CONTEXT-FREE PARALLEL REDUCTION ON CLOSURES ******************************)
definition fpr: bi_relation lenv term ≝
λL1,T1,L2,T2. |L1| = |L2| ∧ L1 @@ T1 ➡ L2 @@ T2.
interpretation
- "focalized parallel reduction (closure)"
+ "context-free parallel reduction (closure)"
'FocalizedPRed L1 T1 L2 T2 = (fpr L1 T1 L2 T2).
(* Basic properties *********************************************************)
lemma fpr_refl: bi_reflexive … fpr.
/2 width=1/ qed.
+lemma fpr_shift: ∀I1,I2,L1,L2,V1,V2,T1,T2.
+ ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ →
+ ⦃L1.ⓑ{I1}V1, T1⦄ ➡ ⦃L2.ⓑ{I2}V2, T2⦄.
+#I1 #I2 #L1 #L2 #V1 #V2 #T1 #T2 * #HL12 #HT12
+@conj // normalize // (**) (* explicit constructor *)
+qed.
+
(* Basic inversion lemmas ***************************************************)
lemma fpr_inv_atom1: ∀L2,T1,T2. ⦃⋆, T1⦄ ➡ ⦃L2, T2⦄ → T1 ➡ T2 ∧ L2 = ⋆.
#L2 #T1 #T2 * #H
lapply (length_inv_zero_sn … H) -H #H destruct /2 width=1/
qed-.
-(*
-lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ →
- ∃∃K2,V2. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ &
- L2 = K2.ⓑ{I}V2.
-#I1 #K1 #L2 #V1 #T1 #T2 * #H
-elim (length_inv_pos_sn … H) -H #I2 #K2 #V2 #HK12 #H destruct #H
-elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/
-qed-.
-*)
+
lemma fpr_inv_atom3: ∀L1,T1,T2. ⦃L1,T1⦄ ➡ ⦃⋆,T2⦄ → T1 ➡ T2 ∧ L1 = ⋆.
#L1 #T1 #T2 * #H
lapply (length_inv_zero_dx … H) -H #H destruct /2 width=1/
qed-.
-(*
-lemma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ →
- ∃∃K1,V1. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ &
- L1 = K1.ⓑ{I}V1.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fpr_fwd_pair1: ∀I1,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I1}V1, T1⦄ ➡ ⦃L2, T2⦄ →
+ ∃∃I2,K2,V2. ⦃K1, -ⓑ{I1}V1.T1⦄ ➡ ⦃K2, -ⓑ{I2}V2.T2⦄ &
+ L2 = K2.ⓑ{I2}V2.
+#I1 #K1 #L2 #V1 #T1 #T2 * #H
+elim (length_inv_pos_sn … H) -H #I2 #K2 #V2 #HK12 #H destruct /3 width=5/
+qed-.
+
+lemma fpr_fwd_pair3: ∀I2,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I2}V2, T2⦄ →
+ ∃∃I1,K1,V1. ⦃K1, -ⓑ{I1}V1.T1⦄ ➡ ⦃K2, -ⓑ{I2}V2.T2⦄ &
+ L1 = K1.ⓑ{I1}V1.
#I2 #L1 #K2 #V2 #T1 #T2 * #H
-elim (length_inv_pos_dx … H) -H #I1 #K1 #V1 #HK12 #H destruct #H
-elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/
+elim (length_inv_pos_dx … H) -H #I1 #K1 #V1 #HK12 #H destruct /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/cfpr_cpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************)
+
+(* Advanced propertis *******************************************************)
+
+lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →
+ ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄.
+#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I
+elim (fpr_inv_all … H) /3 width=4/
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2.
+ ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ →
+ ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2.
+* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H
+elim (fpr_inv_all … H) -H #L #HL1 #H #HL2
+[ elim (cpr_inv_abbr1 … H) -H *
+ [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/
+ | #T #_ #_ #H destruct
+ ]
+| elim (cpr_inv_abst1 … H Abst V2) -H
+ #V #T #HV1 #_ #H destruct /3 width=4/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ →
+ ∃∃K2,V2. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ &
+ ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ &
+ L2 = K2.ⓑ{I}V2.
+#I1 #K1 #X #V1 #T1 #T2 #H
+elim (fpr_fwd_pair1 … H) -H #I2 #K2 #V2 #HT12 #H destruct
+elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/
+qed-.
+
+lemma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ →
+ ∃∃K1,V1. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ &
+ ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ &
+ L1 = K1.ⓑ{I}V1.
+#I2 #X #K2 #V2 #T1 #T2 #H
+elim (fpr_fwd_pair3 … H) -H #I1 #K1 #V1 #HT12 #H destruct
+elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /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/unfold/ltpss_sn.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.
-
-lemma ltpss_sn_lcpr: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ➡ L2.
-/3 width=5/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆.
-#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_sn_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_ltpss_sn.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/ltpss_sn_ltpss_sn.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 *
-<(ltpss_sn_fwd_length … HL2) #V #HV1 #HV2 #I
-lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2
-@(ex2_1_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *)
-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_ltpss_sn.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_sn_fwd_length … HKL1) #H1
-lapply (ltpss_sn_fwd_length … HKL2) #H2
->H1 in HKL1 H; -H1 #HKL1
->H2 in HKL2; -H2 #HKL2 #H
-elim (ltpr_ltpss_sn_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
-elim (ltpr_ltpss_sn_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
-elim (ltpss_sn_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/ltpss_sn.ma".
+include "basic_2/reducibility/ltpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************)
+
+definition lfpr: relation lenv ≝
+ λL1,L2. ∃∃L. L1 ➡ L & L ⊢ ▶* [0, |L|] L2
+.
+
+interpretation
+ "focalized parallel reduction (environment)"
+ 'FocalizedPRed L1 L2 = (lfpr L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lfpr_refl: ∀L. ⦃L⦄ ➡ ⦃L⦄.
+/2 width=3/ qed.
+
+lemma ltpss_sn_lfpr: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → ⦃L1⦄ ➡ ⦃L2⦄.
+/3 width=5/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lfpr_inv_atom1: ∀L2. ⦃⋆⦄ ➡ ⦃L2⦄ → L2 = ⋆.
+#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_sn_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_ltpss_sn.ma".
+include "basic_2/reducibility/ltpr_aaa.ma".
+include "basic_2/reducibility/lfpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_lfpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡ ⦃L2⦄ → L2 ⊢ T ⁝ A.
+#L1 #T #A #HT #L2 * /3 width=5/
+qed.
(**************************************************************************)
include "basic_2/grammar/lenv_px_bi.ma".
-include "basic_2/reducibility/fpr.ma".
+include "basic_2/reducibility/fpr_cpr.ma".
+include "basic_2/reducibility/lfpr_fpr.ma".
(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************)
lemma lfpra_refl: reflexive … lfpra.
/2 width=1/ qed.
+lemma fpr_lfpra: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄.
+#L1 elim L1 -L1
+[ #L2 #T1 #T2 #H
+ elim (fpr_inv_atom1 … H) -H #_ #H destruct //
+| #L1 #I #V1 #IH #L2 #T1 #T2 #H
+ elim (fpr_inv_pair1 … H) -H #L #V #HV1 #HL1 #H destruct /3 width=3/
+]
+qed.
+
(* Basic inversion lemmas ***************************************************)
lemma lfpra_inv_atom1: ∀L2. ⦃⋆⦄ ➡➡ ⦃L2⦄ → L2 = ⋆.
L1 = K1. ⓑ{I} V1.
/2 width=1 by lpx_bi_inv_pair2/ qed-.
+lemma lfpra_inv_fpr: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → ∀T.⦃L1, T⦄ ➡ ⦃L2, T⦄.
+#L1 #L2 * -L1 -L2 // /3 width=1/
+qed-.
+
(* Basic forward lemmas *****************************************************)
lemma lfpra_fwd_length: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → |L1| = |L2|.
/2 width=2 by lpx_bi_fwd_length/ qed-.
-(****************************************************************************)
-(*
-lemma fpr_lfpra: ∀L1,T1,L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄.
-#L1 #T1 @(cw_wf_ind … L1 T1) -L1 -T1 *
-[ #T1 #_ #L2 #T2 #H
- elim (fpr_inv_atom1 … H) -H #_ #H destruct //
-| #L1 #I #V1 #T1 #IH #Y #X #H
- elim (fpr_inv_pair1 … H) -H #L2 #V2 #HL12 #H destruct
- @lpx_bi_pair
- [ @(IH … HL12)
- | @IH
-
- /3 width=4/
+(* Main properties **********************************************************)
-lemma fpr_lfpra: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄.
-#L1 elim L1 -L1
-[ #L2 #T1 #T2 #H
- elim (fpr_inv_atom1 … H) -H #_ #H destruct //
-| #L1 #I #V1 #IH #L2 #T1 #T2 #H
- elim (fpr_inv_pair1 … H) -H #L #V #HL1 #H destruct
- @lpx_bi_pair /2 width=3/
-
- /4 width=3/
-
-(*
-include "basic_2/reducibility/lcpr.ma".
-
-lemma lcpr_pair2: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ →
- ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2.
-#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
-#H1 #H2 #I
-@(ex2_1_intro … (L.ⓑ{I}V1)) /2 width=1/
-@tpss_
-
-(*
-<(ltpss_fwd_length … HL2) /4 width=5/
+theorem lfpr_lfpra: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄.
+#L1 #L2 #H
+lapply (lfpr_inv_fpr … H (⋆0)) -H /2 width=3/
qed.
-*)
-*)
-*)
\ No newline at end of file
+
+theorem lfpra_lfpr: ∀L1,L2. ⦃L1⦄ ➡➡ ⦃L2⦄ → ⦃L1⦄ ➡ ⦃L2⦄.
+#L1 #L2 #H
+lapply (lfpra_inv_fpr … H (⋆0)) -H /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_sn_ltpss_sn.ma".
+include "basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/lfpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS **********************)
+
+(* Advanced properties ****************************************************)
+
+lemma lfpr_pair_cpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡ V2 →
+ ∀I. ⦃L1. ⓑ{I} V1⦄ ➡ ⦃L2. ⓑ{I} V2⦄.
+#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
+<(ltpss_sn_fwd_length … HL2) #V #HV1 #HV2 #I
+lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2
+@(ex2_1_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *)
+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/lfpr.ma".
+include "basic_2/reducibility/cfpr_cpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************)
+
+(* Inversion lemmas on context-free parallel reduction for closures *********)
+
+lemma fpr_lfpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡ ⦃L2⦄.
+#L1 #L2 #T1 #T2 #H
+elim (fpr_inv_all … H) -H /2 width=3/
+qed.
+
+(* Inversion lemmas on context-free parallel reduction for closures *********)
+
+lemma lfpr_inv_fpr: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T. ⦃L1, T⦄ ➡ ⦃L2, T⦄.
+#L1 #L2 * /2 width=4/
+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_ltpss_sn.ma".
+include "basic_2/reducibility/ltpr_ltpr.ma".
+include "basic_2/reducibility/lfpr.ma".
+
+(* FOCALIZED PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***********************)
+
+(* Main properties **********************************************************)
+
+theorem lfpr_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_sn_fwd_length … HKL1) #H1
+lapply (ltpss_sn_fwd_length … HKL2) #H2
+>H1 in HKL1 H; -H1 #HKL1
+>H2 in HKL2; -H2 #HKL2 #H
+elim (ltpr_ltpss_sn_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
+elim (ltpr_ltpss_sn_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
+elim (ltpss_sn_conf … HK1 … HK2) -K #K #HK1 #HK2
+lapply (ltpr_fwd_length … HLK1) #H1
+lapply (ltpr_fwd_length … HLK2) #H2
+/3 width=5/
+qed.
lemma ltpr_refl: reflexive … ltpr.
/2 width=1/ qed.
+lemma ltpr_append: ∀K1,K2. K1 ➡ K2 → ∀L1,L2:lenv. L1 ➡ L2 → K1 @@ L1 ➡ K2 @@ L2.
+/2 width=1/ qed.
+
(* Basic inversion lemmas ***************************************************)
(* Basic_1: was: wcpr0_gen_sort *)
lemma ltpr_fwd_length: ∀L1,L2. L1 ➡ L2 → |L1| = |L2|.
/2 width=2 by lpx_fwd_length/ qed-.
+(* Advanced inversion lemmas ************************************************)
+
+lemma ltpr_inv_append1: ∀K1,L1. ∀L:lenv. K1 @@ L1 ➡ L →
+ ∃∃K2,L2. K1 ➡ K2 & L1 ➡ L2 & L = K2 @@ L2.
+/2 width=1 by lpx_inv_append1/ qed-.
+
+lemma ltpr_inv_append2: ∀L:lenv. ∀K2,L2. L ➡ K2 @@ L2 →
+ ∃∃K1,L1. K1 ➡ K2 & L1 ➡ L2 & L = K1 @@ L1.
+/2 width=1 by lpx_inv_append2/ qed-.
+
(* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)
]
]
qed-.
-
-lemma tpr_fwd_shift_bind_minus: ∀L1,L2. |L1| = |L2| → ∀I1,I2,V1,V2,T1,T2.
- L1 @@ -ⓑ{I1}V1.T1 ➡ L2 @@ -ⓑ{I2}V2.T2 →
- L1 𝟙 L2 ∧ I1 = I2.
-#L1 #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H
+*)
+
+
+(*
+ >shift_append_assoc >shift_append_assoc >shift_append_assoc >shift_append_assoc normalize #H
+ elim (tpr_inv_bind1 … H) -H *
+ [ #V #T #T0 #HV1 #HT1 #HT0 #H destruct /2 width=1/
+ | #T #_ #_ #H destruct
+ ]
+
+ lapply (IH … HT12)
+
+
+ >shift_append_assoc >shift_append_assoc >shift_append_assoc #HT12
+ lapply (shift_inj … HT12) -HT12
+
+
+
+ #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H
elim (tpr_fwd_shift1 (L1.ⓑ{I1}V1) … H) -H #Y #X #HY #HX
elim (ltop_inv_pair1 … HY) -HY #L #V #HL1 #H destruct
elim (shift_inj (L2.ⓑ{I2}V2) … HX ?) -HX
(**************************************************************************)
include "basic_2/static/ssta_aaa.ma".
-include "basic_2/reducibility/lcpr_aaa.ma".
+include "basic_2/reducibility/cpr_aaa.ma".
include "basic_2/reducibility/xpr.ma".
(* EXTENDED PARALLEL REDUCTION ON TERMS *************************************)
L1 @@ K1 ▶* [d, |K1| - d + e] L2 @@ K2.
/2 width=1 by ltpss_dx_append_le_aux/ qed.
+lemma ltpss_dx_append_zero: ∀K1,K2. K1 ▶* [0, |K1|] K2 →
+ ∀L1,L2,e. L1 ▶* [0, e] L2 →
+ L1 @@ K1 ▶* [0, |K1| + e] L2 @@ K2.
+/2 width=1/ qed.
+
lemma ltpss_dx_append_ge: ∀K1,K2,d,e. K1 ▶* [d, e] K2 →
∀L1,L2. L1 ▶* [d - |K1|, e] L2 → |K1| ≤ d →
L1 @@ K1 ▶* [d, e] L2 @@ K2.
(* Advanced forward lemmas **************************************************)
lemma tps_fwd_shift1: ∀L1,L,T1,T,d,e. L ⊢ L1 @@ T1 ▶ [d, e] T →
- ∃∃L2,T2. L @@ L1 ⊢ ▶* [d + |L1|, e] L @@ L2 & T = L2 @@ T2.
+ ∃∃L2,T2. L @@ L1 ⊢ ▶* [d + |L1|, e] L @@ L2 &
+ L @@ L2 ⊢ T1 ▶ [d + |L1|, e] T2 &
+ T = L2 @@ T2.
#L1 @(lenv_ind_dx … L1) -L1
-[ #L #T1 #T #d #e #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+[ #L #T1 #T #d #e #HT1
+ @ex3_2_intro [3: // |5: // |4: normalize /2 width=1/ |1,2: skip ] (**) (* /2 width=4/ does not work *)
| #I #L1 #V1 #IH #L #T1 #T #d #e >shift_append_assoc #H
elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- elim (IH … HT12) -IH -T1 #L2 #T #HL12 #H destruct
+ elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
<append_assoc >append_length <associative_plus
lapply (ltpss_sn_trans_eq (L.ⓑ{I}V1@@L1) … HL12) -HL12 /3 width=1/ #HL12
- @(ex
2_2_intro … (⋆.ⓑ{I}V2@@L2)) /2 width=4/ <append_assoc // (**) (* explicit constructor *)
+ @(ex
3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3/ | skip ] <append_assoc // (**) (* explicit constructor *)
]
qed-.
projects / helm.git / commitdiff