(* *)
(**************************************************************************)
+include "basic_2/relocation/ldrop_lsuby.ma".
include "basic_2/reduction/lpr_ldrop.ma".
include "basic_2/computation/lprs.ma".
(* *)
(**************************************************************************)
+include "basic_2/relocation/ldrop_lsuby.ma".
include "basic_2/reduction/lpx_ldrop.ma".
include "basic_2/computation/lpxs.ma".
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/substitution/lleq_ldrop.ma".
+include "basic_2/computation/lsx.ma".
+
+(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+
+(* Advanced properties ******************************************************)
+
+lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⋕⬊*[h, g, #i, d] L.
+#h #g #G #L1 #d #i #HL1 @lsx_intro
+#L2 #HL12 #H elim H -H
+/4 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_aux/
+qed.
+
+lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⋕⬊*[h, g, #i, d] L.
+#h #g #G #L1 #d #i #HL1 @lsx_intro
+#L2 #HL12 #H elim H -H
+/3 width=4 by lpxs_fwd_length, lleq_skip/
+qed.
(* Advanced forward lemmas **************************************************)
+lemma lsx_fwd_lref_be: ∀h,g,I,G,L,d,i. d ≤ yinj i → G ⊢ ⋕⬊*[h, g, #i, d] L →
+ ∀K,V. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, V, 0] K.
+#h #g #I #G #L #d #i #Hdi #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro
+#K2 #HK12 #HnK12 lapply (ldrop_fwd_drop2 … HLK1)
+#H2LK1 elim (ldrop_lpxs_trans … H2LK1 … HK12) -H2LK1 -HK12
+#L2 #HL12 #H2LK2 #HL21 elim (lsuby_ldrop_trans_be … HL21 … HLK1) -HL21 /2 width=1 by ylt_inj/
+#J #Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2)
+#HY lapply (ldrop_mono … HY … H2LK2) -HY -H2LK2 #H destruct
+elim (lpxs_ldrop_conf … HLK1 … HL12) #Y #H #HY
+elim (lpxs_inv_pair1 … H) -H #Z #X #_ #_ #H destruct
+lapply (ldrop_mono … HY … HLK2) -HY #H destruct
+/4 width=10 by lleq_inv_lref_ge/
+qed-.
+
lemma lsx_fwd_bind_dx: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L →
G ⊢ ⋕⬊*[h, g, T, ⫯d] L.ⓑ{I}V.
#h #g #a #I #G #L #V1 #T #d #H @(lsx_ind … H) -L
[ //
| /2 width=2 by cpx_sort/
| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
+ elim (lsuby_ldrop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/
|4,9: /4 width=1 by cpx_bind, cpx_beta, lsuby_pair_O_Y/
|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsuby_pair_O_Y/
include "ground_2/ynat/ynat_max.ma".
include "basic_2/notation/relations/psubst_6.ma".
include "basic_2/grammar/genv.ma".
-include "basic_2/relocation/lsuby.ma".
+include "basic_2/relocation/ldrop.ma".
(* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
#G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e
[ //
| #I #G #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
- elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/
+ elim (lsuby_ldrop_trans_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/
| /4 width=1 by lsuby_succ, cpy_bind/
| /3 width=1 by cpy_flat/
]
include "basic_2/notation/relations/rdrop_5.ma".
include "basic_2/notation/relations/rdrop_4.ma".
include "basic_2/notation/relations/rdrop_3.ma".
-include "basic_2/grammar/lenv_length.ma".
include "basic_2/grammar/cl_restricted_weight.ma".
include "basic_2/relocation/lift.ma".
+include "basic_2/relocation/lsuby.ma".
(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
definition dedropable_sn: predicate (relation lenv) ≝
λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀K2. R K1 K2 →
- ∃∃L2. R L1 L2 & ⇩[s, d, e] L2 ≡ K2.
+ ∃∃L2. R L1 L2 & ⇩[s, d, e] L2 ≡ K2 & L2 ⊑×[d, e] L1.
definition dropable_dx: predicate (relation lenv) ≝
λR. ∀L1,L2. R L1 L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 →
]
qed-.
-lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R).
-#R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2
-[ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1
- /3 width=3 by inj, ex2_intro/
-| #K #K2 #_ #HK2 * #L #HL1 #HLK elim (HR … HLK … HK2) -HR -K
- /3 width=3 by step, ex2_intro/
-]
-qed-.
-
lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R).
#R #HR #L1 #L2 #H elim H -L2
[ #L2 #HL12 #K2 #s #e #HLK2 elim (HR … HL12 … HLK2) -HR -L2
]
qed-.
+lemma lsuby_ldrop_trans_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
+ ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W →
+ d ≤ i → i < d + e →
+ ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #L1 #d #e #J2 #K2 #W #s #i #H
+ elim (ldrop_inv_atom1 … H) -H #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #s #i #_ #_ #H
+ elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #s #i #H #_ >yplus_O1
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ]
+ [ #_ destruct -I2 >ypred_succ
+ /2 width=4 by ldrop_pair, ex2_2_intro/
+ | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/
+ #H <H -H #H lapply (ylt_inv_succ … H) -H
+ #Hie elim (IHL12 … HLK1) -IHL12 -HLK1 // -Hie
+ >yminus_succ <yminus_inj /3 width=4 by ldrop_drop_lt, ex2_2_intro/
+ ]
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #J2 #K2 #W #s #i #HLK2 #Hdi
+ elim (yle_inv_succ1 … Hdi) -Hdi
+ #Hdi #Hi <Hi >yplus_succ1 #H lapply (ylt_inv_succ … H) -H
+ #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/
+ #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 <yminus_inj >yminus_SO2
+ /4 width=4 by ylt_O, ldrop_drop_lt, ex2_2_intro/
+]
+qed-.
+
(* Basic forvard lemmas *****************************************************)
(* Basic_1: was: drop_S *)
l_liftable R → dedropable_sn (lpx_sn R).
#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e
[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H
- /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/
+ /4 width=4 by ldrop_atom, lpx_sn_atom, ex3_intro/
| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
#K2 #V2 #HK12 #HV12 #H destruct
- /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/
+ lapply (lpx_sn_fwd_length … HK12)
+ #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *)
+ /3 width=1 by lsuby_O1, lpx_sn_pair, monotonic_le_plus_l/
| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
- /3 width=5 by ldrop_drop, lpx_sn_pair, ex2_intro/
+ /3 width=5 by ldrop_drop, lsuby_pair, lpx_sn_pair, ex3_intro/
| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
elim (lift_total W2 d e) #V2 #HWV2
lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1
- elim (IHLK1 … HK12) -K1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/
+ elim (IHLK1 … HK12) -K1
+ /3 width=6 by ldrop_skip, lsuby_succ, lpx_sn_pair, ex3_intro/
]
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/relocation/lsuby_lsuby.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
+
+(* Properties on local environment refinement for extended substitution *****)
+
+lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R).
+#R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2
+[ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1
+ /3 width=4 by inj, ex3_intro/
+| #K #K2 #_ #HK2 * #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2) -HR -K
+ /3 width=6 by lsuby_trans, step, ex3_intro/
+]
+qed-.
include "ground_2/ynat/ynat_plus.ma".
include "basic_2/notation/relations/extlrsubeq_4.ma".
-include "basic_2/relocation/ldrop.ma".
+include "basic_2/grammar/lenv_length.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
lemma lsuby_fwd_length: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → |L2| ≤ |L1|.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize /2 width=1 by le_S_S/
qed-.
-
-lemma lsuby_fwd_ldrop2_be: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 →
- ∀I2,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I2}W →
- d ≤ i → i < d + e →
- ∃∃I1,K1. K1 ⊑×[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I1}W.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #L1 #d #e #J2 #K2 #W #s #i #H
- elim (ldrop_inv_atom1 … H) -H #H destruct
-| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J2 #K2 #W #s #i #_ #_ #H
- elim (ylt_yle_false … H) //
-| #I1 #I2 #L1 #L2 #V #e #HL12 #IHL12 #J2 #K2 #W #s #i #H #_ >yplus_O1
- elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ]
- [ #_ destruct -I2 >ypred_succ
- /2 width=4 by ldrop_pair, ex2_2_intro/
- | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/
- #H <H -H #H lapply (ylt_inv_succ … H) -H
- #Hie elim (IHL12 … HLK1) -IHL12 -HLK1 // -Hie
- >yminus_succ <yminus_inj /3 width=4 by ldrop_drop_lt, ex2_2_intro/
- ]
-| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #J2 #K2 #W #s #i #HLK2 #Hdi
- elim (yle_inv_succ1 … Hdi) -Hdi
- #Hdi #Hi <Hi >yplus_succ1 #H lapply (ylt_inv_succ … H) -H
- #Hide lapply (ldrop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/
- #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 <yminus_inj >yminus_SO2
- /4 width=4 by ylt_O, ldrop_drop_lt, ex2_2_intro/
-]
-qed-.
#G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e
[ //
| #I #G #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) -HL12 -HLK1 /3 width=7 by cpysa_subst/
+ elim (lsuby_ldrop_trans_be … HL12 … HLK1) -HL12 -HLK1 /3 width=7 by cpysa_subst/
| /4 width=1 by lsuby_succ, cpysa_bind/
| /3 width=1 by cpysa_flat/
]
/3 width=4 by lleq_sym, ex2_2_intro/
qed-.
+lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
+ ∀I1,I2,K1,K2,V.
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V → K1 ⋕[V, 0] K2.
+#L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V #HLK1 #HLK2
+elim (lleq_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d
+#J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct //
+qed-.
+
(* Advanced properties ******************************************************)
lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[T, d] L2).
}
]
[ { "strongly normalizing extended computation" * } {
- [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ]
+ [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_cpxs" + "lsx_csx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ]
}
[ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
}
]
- [ { "local env. ref. for extended substitution" * } {
- [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ]
- }
- ]
[ { "restricted local env. ref." * } {
[ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ]
}
}
]
[ { "basic local env. slicing" * } {
- [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ]
+ [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_lsuby" + "ldrop_ldrop" * ]
+ }
+ ]
+ [ { "local env. ref. for extended substitution" * } {
+ [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ]
}
]
[ { "basic term relocation" * } {
projects / helm.git / commitdiff