elim (fpr_bind2_minus … HU2) -HU2 /3 width=4/
qed-.
+lemma fprs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡* ⦃K2, T2⦄ →
+ ∀d,e,L1. ⇩[d, e] L1 ≡ K1 →
+ ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
+ ∃∃L2. ⦃L1, U1⦄ ➡* ⦃L2, U2⦄ & ⇩[d, e] L2 ≡ K2.
+#K1 #K2 #T1 #T2 #HT12 @(fprs_ind … HT12) -K2 -T2
+[ #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2
+ >(lift_mono … HTU2 … HTU1) -U2 /2 width=3/
+| #K #K2 #T #T2 #_ #HT2 #IHT1 #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2
+ elim (lift_total T d e) #U #HTU
+ elim (IHT1 … HLK1 … HTU1 HTU) -K1 -T1 #L #HU1 #HKL
+ elim (fpr_lift … HT2 … HKL … HTU HTU2) -K -T -T2 /3 width=4/
+]
+qed-.
+
(* Advanced inversion lemmas ************************************************)
lemma fprs_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
(* *)
(**************************************************************************)
-
-include "basic_2/reducibility/ltpr.ma".
+include "basic_2/static/ssta_ltpss_dx.ma".
include "basic_2/computation/xprs_lift.ma".
-include "basic_2/equivalence/cpcs_cpcs.ma".
include "basic_2/equivalence/lsubse_ssta.ma".
include "basic_2/equivalence/fpcs_cpcs.ma".
-include "basic_2/equivalence/fpcs_fpcs.ma".
+include "basic_2/equivalence/lfpcs_fpcs.ma".
include "basic_2/dynamic/snv_ssta.ma".
(*
-include "basic_2/static/ssta_ltpss_dx.ma".
-include "basic_2/dynamic/snv_lift.ma".
+anclude "basic_2/dynamic/snv_lift.ma".
*)
(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************)
∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L1⦄ ⊩ T1 :[g] →
∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄.
#h #g #n #IH3 #IH2 #IH1 #L1 * * [|||| *]
-[
-|
-|
-|
+[ #k #_ #Y #l #H1 #L2 #HL12 #X #H2 #_ -IH3 -IH1
+ elim (ssta_inv_sort1 … H1) -H1 #Hkl #H destruct
+ >(tpr_inv_atom1 … H2) -X /4 width=6/
+| #i #Hn #U1 #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3
+ elim (ssta_inv_lref1 … H1) -H1 * #K1
+ >(tpr_inv_atom1 … H2) -X
+ elim (snv_inv_lref … H3) -H3 #I0 #K0 #V0 #H #HV1
+ [ #V1 #W1 #HLK1 #HVW1 #HWU1
+ lapply (ldrop_mono … H … HLK1) -H #H destruct
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
+ elim (ltpr_ldrop_conf … HLK1 … HL12) #X #H #HLK2
+ elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ elim (IH1 … HVW1 K2 … HV12) -IH1 -HVW1 -HV12 // -HV1 -HKV1 #W2 #HVW2 #HW12
+ lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #H1
+ lapply (ldrop_fwd_ldrop2 … HLK2) #H2
+ elim (lift_total W2 0 (i+1)) #U2 #HWU2
+ lapply (fpcs_lift … HW12 … H1 H2 … HWU1 … HWU2) -H1 -H2 -W1 [ /3 width=1/ ] /3 width=6/
+ | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct
+ lapply (ldrop_mono … H … HLK1) -H #H destruct
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
+ elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2
+ elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ elim (IH1 … HVW1 K2 … HV12) -IH1 -HVW1 // -HV1 -HK12 -HKV1 #W2 #HVW2 #_ -W1
+ elim (lift_total V2 0 (i+1)) #U2 #HVU2
+ lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/
+ ]
+| #p #Hn #U1 #l #H1 -IH3 -IH1
+ elim (ssta_inv_gref1 … H1)
+| #a #I #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct -IH3
+ elim (ssta_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
+ elim (snv_inv_bind … H3) -H3 #_ #HT1
+ elim (tpr_inv_bind1 … H2) -H2 *
+ [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
+ elim (IH1 … HTU1 (L2.ⓑ{I}V2) … HT10) -IH1 -HTU1 -HT10 // -T1 /3 width=1/ #U0 #HTU0 #HU10
+ lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02
+ elim (ssta_tps_conf … HTU0 … HT02) -T0 #U2 #HTU2 #HU02
+ lapply (cpr_intro … U0 … HU02) -HU02 // #HU02
+ lapply (fpcs_fpr_strap1 … HU10 (L2.ⓑ{I}V2) U2 ?) [ /2 width=1/ ] -U0 #HU12
+ lapply (fpcs_fwd_shift … HU12 a) -HU12 /3 width=3/
+ | #T2 #HT12 #HT2 #H1 #H2 destruct
+ elim (IH1 … HTU1 (L2.ⓓV1) … HT12) -IH1 -HTU1 -HT12 // -T1 [2: /3 width=1/ ] #U2 #HTU2 #HU12
+ lapply (fpcs_fwd_shift … HU12 true) -HU12 #HU12
+ elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2
+ lapply (fpcs_fpr_strap1 … HU12 L2 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/
+ ]
| #V1 #T1 #Hn #Y #l #H1 #L2 #HL12 #X #H2 #H3 destruct
elim (ssta_inv_appl1 … H1) -H1 #U1 #HTU1 #H destruct
elim (snv_inv_appl … H3) -H3 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10
--- /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/fprs_cprs.ma".
+include "basic_2/computation/lfprs_fprs.ma".
+include "basic_2/equivalence/fpcs_fpcs.ma".
+include "basic_2/equivalence/lfpcs_lfpcs.ma".
+
+(* FOCALIZED PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *********************)
+
+(* Inversion lemmas on context-free parallel equivalence for closures *******)
+
+lemma lfpcs_inv_fpcs: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ⬌* ⦃L2, T⦄.
+#L1 #L2 #HL12 #T
+elim (lfpcs_inv_lfprs … HL12) -HL12 #L #HL1 #HL2
+lapply (lfprs_inv_fprs … HL1 T) -HL1
+lapply (lfprs_inv_fprs … HL2 T) -HL2 /2 width=4/
+qed-.
+
+(* Properties on context-free parallel equivalence for closures *************)
+
+lemma fpcs_lfpcs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄.
+#L1 #L2 #T1 #T2 #HT12
+elim (fpcs_inv_fprs … HT12) -HT12 /3 width=5 by fprs_lfprs, lfprs_div/ (**) (* auto too slow without trace *)
+qed.
+
+lemma fpcs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ⬌* ⦃K2, T2⦄ →
+ ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ →
+ ∀d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+ ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
+ ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄.
+#K1 #K2 #T1 #T2 #HT12 #L1 #L2 #HL12 #d #e #HLK1 #HLK2 #U1 #U2 #HTU1 #HTU2
+elim (fpcs_inv_fprs … HT12) -HT12 #K #T #HT1 #HT2
+elim (lift_total T d e) #U #HTU
+elim (fprs_lift … HT1 … HLK1 … HTU1 HTU) -K1 -T1 #K1 #HU1 #_
+elim (fprs_lift … HT2 … HLK2 … HTU2 HTU) -K2 -T2 -T #K2 #HU2 #_ -K -d -e
+lapply (lfpcs_lfprs_conf K1 … HL12) -HL12 /2 width=3/ #H
+lapply (lfpcs_lfprs_strap1 … H K2 ?) -H /2 width=3/ #HK12
+lapply (lfpcs_inv_fpcs … HK12 U) -HK12 #HU
+/3 width=4 by fpcs_fprs_strap2, fpcs_fprs_div/
+qed.
(* Properties on context-sensitive parallel reduction for terms *************)
+lemma ltpr_tpr_fpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 → ⦃L1, T1⦄ ➡ ⦃L2, T2⦄.
+/3 width=4/ qed.
+
lemma cpr_fpr: ∀L,T1,T2. L ⊢ T1 ➡ T2 → ⦃L, T1⦄ ➡ ⦃L, T2⦄.
/2 width=4/ qed.
+lemma fpr_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡ ⦃K2, T2⦄ →
+ ∀d,e,L1. ⇩[d, e] L1 ≡ K1 →
+ ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
+ ∃∃L2. ⦃L1, U1⦄ ➡ ⦃L2, U2⦄ & ⇩[d, e] L2 ≡ K2.
+#K1 #K2 #T1 #T2 #HT12 #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2
+elim (fpr_inv_all … HT12) -HT12 #K #HK1 #HT12 #HK2
+elim (ldrop_ltpr_trans … HLK1 … HK1) -K1 #L #HL1 #HLK
+lapply (cpr_lift … HLK … HTU1 … HTU2 HT12) -T1 -T2 #HU12
+elim (le_or_ge (|K|) d) #Hd
+[ elim (ldrop_ltpss_sn_trans_ge … HLK … HK2 …)
+| elim (ldrop_ltpss_sn_trans_be … HLK … HK2 …)
+] // -Hd #L2 #HL2 #HLK2
+lapply (ltpss_sn_weak_all … HL2) -K /3 width=4/
+qed-.
+
(* Advanced properties ******************************************************)
lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →
).
/2 width=3/ qed-.
+fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀p0. T = §p0 → ⊥.
+#h #g #L #T #U #l * -L -T -U -l
+[ #L #k #l #_ #p0 #H destruct
+| #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct
+| #L #K #W #V #U #i #l #_ #_ #_ #p0 #H destruct
+| #a #I #L #V #T #U #l #_ #p0 #H destruct
+| #L #V #T #U #l #_ #p0 #H destruct
+| #L #W #T #U #l #_ #p0 #H destruct
+qed.
+
+lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃h, L⦄ ⊢ §p •[g, l] U → ⊥.
+/2 width=9/ qed-.
+
fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U →
∀a,I,X,Y. T = ⓑ{a,I}Y.X →
∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g, l] Z & U = ⓑ{a,I}Y.Z.
(* *)
(**************************************************************************)
+include "basic_2/unfold/tpss_lift.ma".
include "basic_2/unfold/ltpss_sn.ma".
(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
]
]
qed.
+
+lemma ldrop_ltpss_sn_trans_be: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+ ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 →
+ d2 ≤ d1 → d1 ≤ d2 + e2 →
+ ∃∃L2. L1 ⊢ ▶* [d2, e1 + e2] L2 &
+ ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_ #_
+ >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H #_
+ lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H1 #H2
+ elim (IHLK1 … HK12 H1 H2) -K1 -H2
+ lapply (le_n_O_to_eq … H1) -H1 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21 #Hd12
+ elim (eq_or_gt d2) #Hd2 [ -Hd21 elim (eq_or_gt e2) #He2 ] destruct
+ [ lapply (le_n_O_to_eq … Hd12) -Hd12 <plus_n_Sm #H destruct
+ | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 …) -IHLK1 // /2 width=1/ >plus_minus_commutative // #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 // /2 width=1/
+ >plus_minus // >commutative_plus /4 width=5/
+ | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // ] /2 width=1/ #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_be … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // ] /2 width=1/
+ >commutative_plus /3 width=5/
+ ]
+]
+qed-.
+
+lemma ldrop_ltpss_sn_trans_ge: ∀L1,K1,d1,e1. ⇩[d1, e1] L1 ≡ K1 →
+ ∀K2,d2,e2. K1 ⊢ ▶* [d2, e2] K2 → d2 + e2 ≤ d1 →
+ ∃∃L2. L1 ⊢ ▶* [d2, e2] L2 & ⇩[d1, e1] L2 ≡ K2.
+#L1 #K1 #d1 #e1 #H elim H -L1 -K1 -d1 -e1
+[ #d1 #e1 #K2 #d2 #e2 #H #_
+ >(ltpss_sn_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #K2 #d2 #e2 #HK12 #H
+ elim (plus_le_0 … H) -H #H1 #H2 destruct /2 width=3/
+| #L1 #K1 #I #V #e1 #_ #IHLK1 #K2 #d2 #e2 #HK12 #H
+ elim (IHLK1 … HK12 H) -K1
+ elim (plus_le_0 … H) -H #H1 #H2 destruct #L2 #HL12
+ >(ltpss_sn_inv_refl_O2 … HL12) -L1 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d1 #e1 #HLK1 #HWV1 #IHLK1 #X #d2 #e2 #H #Hd21
+ elim (eq_or_gt d2) #Hd2 [ elim (eq_or_gt e2) #He2 ] destruct
+ [ -IHLK1 -Hd21 <(ltpss_sn_inv_refl_O2 … H) -X /3 width=5/
+ | elim (ltpss_sn_inv_tpss21 … H He2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 …) -IHLK1 /2 width=1/ #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 /2 width=1/ /3 width=5/
+ | elim (ltpss_sn_inv_tpss11 … H Hd2) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (IHLK1 … HK12 …) -IHLK1 [2: >plus_minus // /2 width=1/ ] #L2 #HL12 #HLK2
+ elim (lift_total W2 d1 e1) #V2 #HWV2
+ lapply (tpss_lift_le … HW12 … HLK1 HWV1 … HWV2) -HLK1 -W1 [ >plus_minus // /2 width=1/ ] /3 width=5/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/unfold/tpss_lift.ma".
include "basic_2/unfold/ltpss_sn_tps.ma".
(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
(* *)
(**************************************************************************)
-include "basic_2/substitution/ldrop_ldrop.ma".
include "basic_2/unfold/ltpss_sn_ldrop.ma".
include "basic_2/unfold/thin.ma".
elim (not_le_Sn_n x) #H0 elim (H0 ?) //
qed-.
+lemma plus_le_0: ∀x,y. x + y ≤ 0 → x = 0 ∧ y = 0.
+#x #y #H elim (le_inv_plus_l … H) -H #H1 #H2 /3 width=1/
+qed-.
+
(* Still more equalities ****************************************************)
theorem eq_minus_O: ∀n,m:nat.
projects / helm.git / commitdiff