- long awaited equivalence for local environments is now set up (coequivalence is in etc in case of need)
- unused results on append parked in etc
- some additions to ynat
include "basic_2/computation/fsb_alt.ma".
axiom lsx_fqup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
- G1 ⊢ ⋕⬊*[h, g, T1] L1 → G2 ⊢ ⋕⬊*[h, g, T2] L2.
+ G1 ⊢ ⋕⬊*[h, g, T1, 0] L1 → G2 ⊢ ⋕⬊*[h, g, T2, 0] L2.
axiom fqup_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ →
∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[T2, 0] L2 →⊥) →
lemma csx_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T.
#h #g #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1
-#T1 #HT1 @(lsx_ind h g T1 G1 … L1) /2 width=1 by csx_lsx/ -L1
+#T1 #HT1 @(lsx_ind h g G1 T1 0 … L1) /2 width=1 by csx_lsx/ -L1
#L1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1
#G1 #L1 #T1 #IHu #H1 #IHl #IHc @fsb_intro
#G2 #L2 #T2 * -G2 -L2 -T2
--- /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/notation/relations/lazycosn_5.ma".
+include "basic_2/computation/lsx.ma".
+
+(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
+
+inductive lcosx (h) (g) (G): relation2 ynat lenv ≝
+| lcosx_sort: ∀d. lcosx h g G d (⋆)
+| lcosx_skip: ∀I,L,T. lcosx h g G 0 L → lcosx h g G 0 (L.ⓑ{I}T)
+| lcosx_pair: ∀I,L,T,d. G ⊢ ⋕⬊*[h, g, T, d] L →
+ lcosx h g G d L → lcosx h g G (⫯d) (L.ⓑ{I}T)
+.
+
+interpretation
+ "sn extended strong conormalization (local environment)"
+ 'LazyCoSN h g d G L = (lcosx h g G d L).
+
+(* Basic properties *********************************************************)
+
+lemma lcosx_O: ∀h,g,G,L. G ⊢ ⧤⬊*[h, g, 0] L.
+#h #g #G #L elim L /2 width=1 by lcosx_skip/
+qed.
+
+lemma lcosx_ldrop_trans_lt: ∀h,g,G,L,d. G ⊢ ⧤⬊*[h, g, d] L →
+ ∀I,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → i < d →
+ G ⊢ ⧤⬊*[h, g, ⫰(d-i)] K ∧ G ⊢ ⋕⬊*[h, g, V, ⫰(d-i)] K.
+#h #g #G #L #d #H elim H -L -d
+[ #d #J #K #V #i #H elim (ldrop_inv_atom1 … H) -H #H destruct
+| #I #L #T #_ #_ #J #K #V #i #_ #H elim (ylt_yle_false … H) -H //
+| #I #L #T #d #HT #HL #IHL #J #K #V #i #H #Hid
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK destruct
+ [ >ypred_succ /2 width=1 by conj/
+ | lapply (ylt_pred … Hid ?) -Hid /2 width=1 by ylt_inj/ >ypred_succ #Hid
+ elim (IHL … HLK ?) -IHL -HLK <yminus_inj >yminus_SO2 //
+ <(ypred_succ d) in ⊢ (%→%→?); >yminus_pred /2 width=1 by ylt_inj, conj/
+ ]
+]
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lcosx_inv_succ_aux: ∀h,g,G,L,x. G ⊢ ⧤⬊*[h, g, x] L → ∀d. x = ⫯d →
+ L = ⋆ ∨
+ ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ⧤⬊*[h, g, d] K &
+ G ⊢ ⋕⬊*[h, g, V, d] K.
+#h #g #G #L #d * -L -d /2 width=1 by or_introl/
+[ #I #L #T #_ #x #H elim (ysucc_inv_O_sn … H)
+| #I #L #T #d #HT #HL #x #H <(ysucc_inj … H) -x
+ /3 width=6 by ex3_3_intro, or_intror/
+]
+qed-.
+
+lemma lcosx_inv_succ: ∀h,g,G,L,d. G ⊢ ⧤⬊*[h, g, ⫯d] L → L = ⋆ ∨
+ ∃∃I,K,V. L = K.ⓑ{I}V & G ⊢ ⧤⬊*[h, g, d] K &
+ G ⊢ ⋕⬊*[h, g, V, d] K.
+/2 width=3 by lcosx_inv_succ_aux/ qed-.
+
+lemma lcosx_inv_pair: ∀h,g,I,G,L,T,d. G ⊢ ⧤⬊*[h, g, ⫯d] L.ⓑ{I}T →
+ G ⊢ ⧤⬊*[h, g, d] L ∧ G ⊢ ⋕⬊*[h, g, T, d] L.
+#h #g #I #G #L #T #d #H elim (lcosx_inv_succ … H) -H
+[ #H destruct
+| * #Z #Y #X #H destruct /2 width=1 by conj/
+]
+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/lsx_ldrop.ma".
+include "basic_2/computation/lsx_lpxs.ma".
+include "basic_2/computation/lcosx.ma".
+
+(* SN EXTENDED STRONGLY CONORMALIZING LOCAL ENVIRONMENTS ********************)
+
+(* Properties on extended context-sensitive parallel computation for term ***)
+
+lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+ ∀d. G ⊢ ⧤⬊*[h, g, d] L →
+ G ⊢ ⋕⬊*[h, g, T1, d] L → G ⊢ ⋕⬊*[h, g, T2, d] L.
+#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 //
+[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H
+ elim (ylt_split i d) #Hdi [ -H | -HL ]
+ [ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/
+ elim (lcosx_ldrop_trans_lt … HL … HLK) // -HL -Hdi
+ lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7 by lsx_lift_ge/
+ | lapply (lsx_fwd_lref_be … H … HLK) // -H -Hdi
+ lapply (ldrop_fwd_drop2 … HLK) -HLK
+ /4 width=10 by lsx_ge, lsx_lift_le/
+ ]
+| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H
+ elim (lsx_inv_bind … H) -H #HV1 #HT1
+ @lsx_bind /2 width=2 by/ (**) (* explicit constructor *)
+ @(lsx_leqy_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, lsuby_succ/
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H
+ elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/
+| #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H
+ elim (lsx_inv_bind … H) -H
+ /4 width=9 by lcosx_pair, lsx_inv_lift_ge, ldrop_drop/
+| #G #L #V #T1 #T2 #_ #IHT12 #d #HL #H
+ elim (lsx_inv_flat … H) -H /2 width=1 by/
+| #G #L #V1 #V2 #T #_ #IHV12 #d #HL #H
+ elim (lsx_inv_flat … H) -H /2 width=1 by/
+| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H
+ elim (lsx_inv_flat … H) -H #HV1 #H
+ elim (lsx_inv_bind … H) -H #HW1 #HT1
+ @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *)
+ @(lsx_leqy_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, lsuby_succ/
+| #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H
+ elim (lsx_inv_flat … H) -H #HV1 #H
+ elim (lsx_inv_bind … H) -H #HW1 #HT1
+ @lsx_bind /2 width=1 by/ (**) (* explicit constructor *)
+ @lsx_flat [ /3 width=7 by lsx_lift_ge, ldrop_drop/ ]
+ @(lsx_leqy_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, lsuby_succ/
+]
+qed-.
+
+lemma lsx_cpx_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+ G ⊢ ⋕⬊*[h, g, T1, 0] L → G ⊢ ⋕⬊*[h, g, T2, 0] L.
+/2 width=3 by lsx_cpx_trans_lcosx/ qed-.
+
+lemma lsx_cpxs_trans_O: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 →
+ G ⊢ ⋕⬊*[h, g, T1, 0] L → G ⊢ ⋕⬊*[h, g, T2, 0] L.
+#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2
+/3 width=3 by lsx_cpx_trans_O, cpxs_strap1/
+qed-.
(* *)
(**************************************************************************)
-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".
/3 width=4 by lpxs_fwd_length, lleq_gref/
qed.
+lemma lsx_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e →
+ ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → G ⊢ ⋕⬊*[h, g, U, d] L.
+#h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L
+/5 width=7 by lsx_intro, lleq_be/
+qed-.
+
(* Basic forward lemmas *****************************************************)
lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L →
(* *)
(**************************************************************************)
-include "basic_2/reduction/cpx_cpys.ma".
-include "basic_2/computation/lpxs_llneq.ma".
include "basic_2/computation/csx_alt.ma".
-include "basic_2/computation/lsx_lpxs.ma".
+include "basic_2/computation/csx_lift.ma".
+include "basic_2/computation/lcosx_cpxs.ma".
(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
(* Advanced properties ******************************************************)
-lemma lpxs_cpys_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U →
- ∀T. ⦃G, L1⦄ ⊢ T ▶*[0, ∞] U →
- G ⊢ ⋕⬊*[h, g, T] L1.
-#h #g #G #L1 #U #H @(csx_ind_alt … H) -U
-#U #_ #IHU #T #HTU @lsx_intro
-#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT
-#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0)
-#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct
-[ -HUX
-| -HnU02 @(lsx_lpxs_trans … HL02) @(IHU … HnUX)
- [ /3 width=3 by cpys_cpx, cpx_cpxs/
- | /2 width=3 by cpys_trans_eq/
- ]
-]
-
-lemma lpxs_cpys_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U →
- ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀T. ⦃G, L2⦄ ⊢ T ▶*[0, ∞] U →
- G ⊢ ⋕⬊*[h, g, T] L2.
-#h #g #G #L1 #U #H @(csx_ind_alt … H) -U
-#U #_ #IHU #L0 #HL10 #T #HTU @lsx_intro
-#L2 #HL02 #HnT elim (lpxs_nlleq_fwd_cpxs … HL02 HnT) -HnT
-#U0 #U2 #H0 #H2 #HU02 #HnU02 elim (cpys_conf_eq … HTU … H0)
-#X #HUX #H0X elim (eq_term_dec U X) #HnUX destruct
-[ -HUX
-| -HnU02 @(IHU … HnUX)
-
-
--HnT /4 width=9 by lpxs_trans, lpxs_cpxs_trans, cpx_cpye_fwd_lpxs/
+lemma lsx_lref_be_lpxs: ∀h,g,I,G,K1,V,i,d. d ≤ yinj i → ⦃G, K1⦄ ⊢ ⬊*[h, g] V →
+ ∀K2. G ⊢ ⋕⬊*[h, g, V, 0] K2 → ⦃G, K1⦄ ⊢ ➡*[h, g] K2 →
+ ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L2.
+#h #g #I #G #K1 #V #i #d #Hdi #H @(csx_ind_alt … H) -V
+#V0 #_ #IHV0 #K2 #H @(lsx_ind … H) -K2
+#K0 #HK0 #IHK0 #HK10 #L0 #HLK0 @lsx_intro
+#L2 #HL02 #HnL02 elim (lpxs_ldrop_conf … HLK0 … HL02) -HL02
+#Y #H #HLK2 elim (lpxs_inv_pair1 … H) -H
+#K2 #V2 #HK02 #HV02 #H destruct
+lapply (lpxs_trans … HK10 … HK02) #HK12
+elim (eq_term_dec V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 -HK10 | -IHK0 -HnL02 -HLK0 ]
+[ /4 width=8 by lleq_lref/
+| @(IHV0 … HnV02 … HK12 … HLK2) -IHV0 -HnV02 -HK12 -HLK2
+ /3 width=4 by lsx_cpxs_trans_O, lsx_lpxs_trans, lpxs_cpxs_trans/ (**) (* full auto too slow *)
]
-
-
-
-
-
-
-
-include "basic_2/reduction/cpx_cpys.ma".
-include "basic_2/computation/lpxs_cpye.ma".
-include "basic_2/computation/csx_alt.ma".
-include "basic_2/computation/lsx_lpxs.ma".
-
-(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
+qed.
-(* Advanced properties ******************************************************)
+lemma lsx_lref_be: ∀h,g,I,G,K,V,i,d. d ≤ yinj i → ⦃G, K⦄ ⊢ ⬊*[h, g] V →
+ G ⊢ ⋕⬊*[h, g, V, 0] K →
+ ∀L. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⋕⬊*[h, g, #i, d] L.
+/2 width=8 by lsx_lref_be_lpxs/ qed.
-axiom lpxs_cpye_csx_lsx: ∀h,g,G,L1,U. ⦃G, L1⦄ ⊢ ⬊*[h, g] U →
- ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ∀T. ⦃G, L2⦄ ⊢ T ▶*[0, ∞] 𝐍⦃U⦄ →
- G ⊢ ⋕⬊*[h, g, T] L2.
-(*
-#h #g #G #L1 #U #H @(csx_ind_alt … H) -U
-#U0 #_ #IHU0 #L0 #HL10 #T #H0 @lsx_intro
-#L2 #HL02 #HnT elim (cpye_total G L2 T 0 (∞))
-#U2 #H2 elim (eq_term_dec U0 U2) #H destruct
-[ -IHU0
-| -HnT /4 width=9 by lpxs_trans, lpxs_cpxs_trans, cpx_cpye_fwd_lpxs/
-]
-*)
(* Main properties **********************************************************)
-lemma csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → G ⊢ ⋕⬊*[h, g, T] L.
-#h #g #G #L #T #HT elim (cpye_total G L T 0 (∞))
-#U #HTU elim HTU
-/4 width=5 by lpxs_cpye_csx_lsx, csx_cpx_trans, cpys_cpx/
+theorem csx_lsx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀d. G ⊢ ⋕⬊*[h, g, T, d] L.
+#h #g #G #L #T @(fqup_wf_ind_eq … G L T) -G -L -T
+#Z #Y #X #IH #G #L * * //
+[ #i #HG #HL #HT #H #d destruct
+ elim (lt_or_ge i (|L|)) /2 width=1 by lsx_lref_free/
+ elim (ylt_split i d) /2 width=1 by lsx_lref_skip/
+ #Hdi #Hi elim (ldrop_O1_lt … Hi) -Hi
+ #I #K #V #HLK lapply (csx_inv_lref_bind … HLK … H) -H
+ /4 width=6 by lsx_lref_be, fqup_lref/
+| #a #I #V #T #HG #HL #HT #H #d destruct
+ elim (csx_fwd_bind … H) -H /3 width=1 by lsx_bind/
+| #I #V #T #HG #HL #HT #H #d destruct
+ elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/
+]
qed.
(**************************************************************************)
include "basic_2/substitution/lleq_ldrop.ma".
+include "basic_2/computation/lpxs_ldrop.ma".
include "basic_2/computation/lsx.ma".
(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
#L2 #HL12 #H elim H -H
/3 width=4 by lpxs_fwd_length, lleq_skip/
qed.
+
+(* Properties on relocation *************************************************)
+
+lemma lsx_lift_le: ∀h,g,G,K,T,U,dt,d,e. dt ≤ yinj d →
+ ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K →
+ ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt] L.
+#h #g #G #K #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -K
+#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
+#L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12
+/4 width=10 by lleq_lift_le/
+qed-.
+
+lemma lsx_lift_ge: ∀h,g,G,K,T,U,dt,d,e. yinj d ≤ dt →
+ ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, T, dt] K →
+ ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, U, dt + e] L.
+#h #g #G #K #T #U #dt #d #e #Hddt #HTU #H @(lsx_ind … H) -K
+#K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
+#L2 #HL12 #HnU elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12
+/4 width=9 by lleq_lift_ge/
+qed-.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d →
+ ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
+ ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt] K.
+#h #g #G #L #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
+#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
+/4 width=10 by lleq_inv_lift_le/
+qed-.
+
+lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e →
+ ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
+ ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, d] K.
+#h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
+#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
+/4 width=11 by lleq_inv_lift_be/
+qed-.
+
+lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,dt,d,e. yinj d + yinj e ≤ dt →
+ ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L →
+ ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⋕⬊*[h, g, T, dt-e] K.
+#h #g #G #L #T #U #dt #d #e #Hdedt #HTU #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
+#K2 #HK12 #HnT elim (ldrop_lpxs_trans … HLK1 … HK12) -HK12
+/4 width=9 by lleq_inv_lift_ge/
+qed-.
#_ #H @(IHL1 … H1L10) -IHL1 -H1L10 /3 width=1 by/
qed-.
+lemma lsx_ge: ∀h,g,G,L,T,d1,d2. d1 ≤ d2 →
+ G ⊢ ⋕⬊*[h, g, T, d1] L → G ⊢ ⋕⬊*[h, g, T, d2] L.
+#h #g #G #L #T #d1 #d2 #Hd12 #H @(lsx_ind … H) -L
+/5 width=7 by lsx_intro, lleq_ge/
+qed-.
+
lemma lsx_lleq_trans: ∀h,g,T,G,L1,d. G ⊢ ⋕⬊*[h, g, T, d] L1 →
∀L2. L1 ⋕[T, d] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2.
#h #g #T #G #L1 #d #H @(lsx_ind … H) -L1
#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)
+#L2 #HL12 #H2LK2 #H elim (leq_ldrop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/
+#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-.
--- /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/reduction/crr_append.ma".
+include "basic_2/reduction/cir.ma".
+
+(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************)
+
+(* Advanved properties ******************************************************)
+
+lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐈⦃T⦄.
+/3 width=2 by crr_inv_labst_last/ qed.
+
+lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄.
+/3 width=2 by crr_inv_trr/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄.
+/3 width=1/ qed-.
+
+lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄.
+/3 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/reduction/crx_append.ma".
+include "basic_2/reduction/cix.ma".
+
+(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ***************)
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cix_inv_append_sn: ∀h,g,G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
+/3 width=1 by crx_append_sn/ qed-.
+
+lemma cix_inv_tix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
+/3 width=1 by trx_crx/ 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/lenv_append.ma".
+
+(* SHIFT OF A CLOSURE *******************************************************)
+
+let rec shift L T on L ≝ match L with
+[ LAtom ⇒ T
+| LPair L I V ⇒ shift L (-ⓑ{I} V. T)
+].
+
+interpretation "shift (closure)" 'Append L T = (shift L T).
+
+(* Basic properties *********************************************************)
+
+lemma shift_append_assoc: ∀L,K. ∀T:term. (L @@ K) @@ T = L @@ K @@ T.
+#L #K elim K -K // normalize //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma shift_inj: ∀L1,L2. ∀T1,T2:term. L1 @@ T1 = L2 @@ T2 → |L1| = |L2| →
+ L1 = L2 ∧ T1 = T2.
+#L1 elim L1 -L1
+[ * normalize /2 width=1/
+ #L2 #I2 #V2 #T1 #T2 #_ <plus_n_Sm #H destruct
+| #L1 #H1 #V1 #IH * normalize
+ [ #T1 #T2 #_ <plus_n_Sm #H destruct
+ | #L2 #I2 #V2 #T1 #T2 #H1 #H2
+ elim (IH … H1) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /2 width=1/
+ ]
+]
+qed-.
--- /dev/null
+include "basic_2/grammar/cl_shift.ma".
+include "basic_2/relocation/ldrop_append.ma".
+
+lemma cpr_append: ∀G. l_appendable_sn … (cpr G).
+#G #K #T1 #T2 #H elim H -G -K -T1 -T2
+/2 width=3 by cpr_bind, cpr_flat, cpr_zeta, cpr_tau, cpr_beta, cpr_theta/
+#G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_length_lt2 … HK0) #H
+@(cpr_delta … (L@@K0) V1 … HVW2) //
+@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
+qed.
+
+lemma cpr_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡ T →
+ ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#G #L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #L #T1 #T #HT1
+ @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #L #T1 #X
+ >shift_append_assoc normalize #H
+ elim (cpr_inv_bind1 … H) -H *
+ [ #V0 #T0 #_ #HT10 #H destruct
+ elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
+ >append_length >HL12 -HL12
+ @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *)
+ | #T #_ #_ #H destruct
+ ]
+]
+qed-.
+
--- /dev/null
+lemma cpx_append: ∀h,g,G. l_appendable_sn … (cpx h g G).
+#h #g #G #K #T1 #T2 #H elim H -G -K -T1 -T2
+/2 width=3 by cpx_sort, cpx_bind, cpx_flat, cpx_zeta, cpx_tau, cpx_ti, cpx_beta, cpx_theta/
+#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_length_lt2 … HK0) #H
+@(cpx_delta … I … (L@@K0) V1 … HVW2) //
+@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
+qed.
+
+lemma cpx_fwd_shift1: ∀h,g,G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡[h, g] T →
+ ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#h #g #G #L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #L #T1 #T #HT1
+ @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #L #T1 #X
+ >shift_append_assoc normalize #H
+ elim (cpx_inv_bind1 … H) -H *
+ [ #V0 #T0 #_ #HT10 #H destruct
+ elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
+ >append_length >HL12 -HL12
+ @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by refl, trans_eq/ (**) (* explicit constructor *)
+ | #T #_ #_ #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/relocation/ldrop_append.ma".
+include "basic_2/reduction/crr.ma".
+
+(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION **************************)
+
+(* Advanved properties ******************************************************)
+
+lemma crr_append_sn: ∀G,L,K,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡ 𝐑⦃T⦄.
+#G #L #K0 #T #H elim H -L -T /2 width=1/
+#L #K #V #i #HLK
+lapply (ldrop_fwd_length_lt2 … HLK) #Hi
+lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=3/
+qed.
+
+lemma trr_crr: ∀G,L,T. ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄.
+#G #L #T #H lapply (crr_append_sn … H) //
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact crr_inv_labst_last_aux: ∀G,L1,T,W. ⦃G, L1⦄ ⊢ ➡ 𝐑⦃T⦄ →
+ ∀L2. L1 = ⋆.ⓛW @@ L2 → ⦃G, L2⦄ ⊢ ➡ 𝐑⦃T⦄.
+#G #L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/
+[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct
+ lapply (ldrop_fwd_length_lt2 … HLK1)
+ >append_length >commutative_plus normalize in ⊢ (??% → ?); #H
+ elim (le_to_or_lt_eq i (|L2|)) /2 width=1/ -H #Hi destruct
+ [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2
+ lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi
+ normalize #H destruct /2 width=3/
+ | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // <minus_n_n #H
+ lapply (ldrop_inv_O2 … H) -H #H destruct
+ ]
+| #a #I #L1 #V #T #HI #_ #IHT #L2 #H destruct /3 width=1/
+]
+qed.
+
+lemma crr_inv_labst_last: ∀G,L,T,W. ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄.
+/2 width=4/ qed-.
+
+lemma crr_inv_trr: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄.
+/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/relocation/ldrop_append.ma".
+include "basic_2/reduction/crx.ma".
+
+(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION *****************)
+
+(* Advanved properties ******************************************************)
+
+lemma crx_append_sn: ∀h,g,G,L,K,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
+#h #g #G #L #K0 #T #H elim H -L -T
+/2 width=2 by crx_sort, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/
+#I #L #K #V #i #HLK
+lapply (ldrop_fwd_length_lt2 … HLK) #Hi
+lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=4 by crx_delta, lt_to_le/
+qed.
+
+lemma trx_crx: ∀h,g,G,L,T. ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
+#h #g #G #L #T #H lapply (crx_append_sn … H) //
+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/lenv_append.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* DROPPING *****************************************************************)
+
+(* Properties on append for local environments ******************************)
+
+fact ldrop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 →
+ d = 0 → e ≤ |L1| →
+ ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize
+[2,3,4: /4 width=1 by ldrop_skip_lt, ldrop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
+#d #e #_ #_ #H <(le_n_O_to_eq … H) -H //
+qed-.
+
+lemma ldrop_O1_append_sn_le: ∀L1,L2,s,e. ⇩[s, 0, e] L1 ≡ L2 → e ≤ |L1| →
+ ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
+/2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
+
+(* Inversion lemmas on append for local environments ************************)
+
+lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K →
+ |L2| ≤ e → ⇩[s, 0, e - |L2|] L1 ≡ K.
+#K #L1 #L2 elim L2 -L2 normalize //
+#L2 #I #V #IHL2 #s #e #H #H1e
+elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct
+[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2
+ >commutative_plus normalize #H destruct
+| <minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
+]
+qed-.
+
+lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
+ ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2.
+#K #L1 #L2 elim L2 -L2 normalize
+[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2
+ #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct
+ >(ldrop_inv_O2 … H1) -H1 //
+| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ]
+ [ #H1 #_ #K2 #H2
+ lapply (ldrop_inv_O2 … H1) -H1 #H1
+ lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct //
+ | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/
+ ]
+]
+qed-.
--- /dev/null
+lemma lpr_append: ∀G,K1,K2. ⦃G, K1⦄ ⊢ ➡ K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
+ ⦃G, L1 @@ K1⦄ ⊢ ➡ L2 @@ K2.
+/3 width=1 by lpx_sn_append, cpr_append/ qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpr_fwd_append1: ∀G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ➡ L →
+ ∃∃K2,L2. ⦃G, K1⦄ ⊢ ➡ K2 & L = K2 @@ L2.
+/2 width=2 by lpx_sn_fwd_append1/ qed-.
+
+lemma lpr_fwd_append2: ∀G,L,K2,L2. ⦃G, L⦄ ⊢ ➡ K2 @@ L2 →
+ ∃∃K1,L1. ⦃G, K1⦄ ⊢ ➡ K2 & L = K1 @@ L1.
+/2 width=2 by lpx_sn_fwd_append2/ qed-.
--- /dev/null
+lemma lpx_append: ∀h,g,G,K1,K2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ⦃G, L1 @@ K1⦄ ⊢ ➡[h, g] L2 @@ K2.
+/3 width=1 by lpx_sn_append, cpx_append/ qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpx_fwd_append1: ∀h,g,G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ➡[h, g] L →
+ ∃∃K2,L2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & L = K2 @@ L2.
+/2 width=2 by lpx_sn_fwd_append1/ qed-.
+
+lemma lpx_fwd_append2: ∀h,g,G,L,K2,L2. ⦃G, L⦄ ⊢ ➡[h, g] K2 @@ L2 →
+ ∃∃K1,L1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & L = K1 @@ L1.
+/2 width=2 by lpx_sn_fwd_append2/ qed-.
--- /dev/null
+lemma lpx_sn_append: ∀R. l_appendable_sn R →
+ ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 →
+ lpx_sn R (L1 @@ K1) (L2 @@ K2).
+#R #HR #K1 #K2 #H elim H -K1 -K2 /3 width=1 by lpx_sn_pair/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpx_sn_fwd_append1: ∀R,L1,K1,L. lpx_sn R (K1 @@ L1) L →
+ ∃∃K2,L2. lpx_sn R K1 K2 & L = K2 @@ L2.
+#R #L1 elim L1 -L1
+[ #K1 #K2 #HK12
+ @(ex2_2_intro … K2 (⋆)) // (* explicit constructor, /2 width=4/ does not work *)
+| #L1 #I #V1 #IH #K1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct
+ elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #H destruct
+ @(ex2_2_intro … (L2.ⓑ{I}V2) HK12) // (* explicit constructor, /2 width=4/ does not work *)
+]
+qed-.
+
+lemma lpx_sn_fwd_append2: ∀R,L2,K2,L. lpx_sn R L (K2 @@ L2) →
+ ∃∃K1,L1. lpx_sn R K1 K2 & L = K1 @@ L1.
+#R #L2 elim L2 -L2
+[ #K2 #K1 #HK12
+ @(ex2_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=4/ does not work *)
+| #L2 #I #V2 #IH #K2 #X #H
+ elim (lpx_sn_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct
+ elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #H destruct
+ @(ex2_2_intro … (L1.ⓑ{I}V1) HK12) // (* explicit constructor, /2 width=4/ does not work *)
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ≅ break [ term 46 d , break term 46 e ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'CoEq $d $e $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/ynat/ynat_lt.ma".
+include "basic_2/notation/relations/coeq_4.ma".
+include "basic_2/grammar/lenv_length.ma".
+
+(* COEQUIVALENCE FOR LOCAL ENVIRONMENTS *************************************)
+
+inductive lcoeq: relation4 ynat ynat lenv lenv ≝
+| lcoeq_atom: ∀d,e. lcoeq d e (⋆) (⋆)
+| lcoeq_zero: ∀I,L1,L2,V.
+ lcoeq 0 0 L1 L2 → lcoeq 0 0 (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lcoeq_pair: ∀I1,I2,L1,L2,V1,V2,e. lcoeq 0 e L1 L2 →
+ lcoeq 0 (⫯e) (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
+| lcoeq_succ: ∀I,L1,L2,V,d,e.
+ lcoeq d e L1 L2 → lcoeq (⫯d) e (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+.
+
+interpretation
+ "coequivalence (local environment)"
+ 'CoEq d e L1 L2 = (lcoeq d e L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lcoeq_pair_lt: ∀I1,I2,L1,L2,V1,V2,e. L1 ≅[0, ⫰e] L2 → 0 < e →
+ L1.ⓑ{I1}V1 ≅[0, e] L2.ⓑ{I2}V2.
+#I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 #He <(ylt_inv_O1 … He) /2 width=1 by lcoeq_pair/
+qed.
+
+lemma lcoeq_succ_lt: ∀I,L1,L2,V,d,e. L1 ≅[⫰d, e] L2 → 0 < d →
+ L1.ⓑ{I}V ≅[d, e] L2. ⓑ{I}V.
+#I #L1 #L2 #V #d #e #HL12 #Hd <(ylt_inv_O1 … Hd) /2 width=1 by lcoeq_succ/
+qed.
+
+lemma lcoeq_pair_O_Y: ∀L1,L2. L1 ≅[0, ∞] L2 →
+ ∀I1,I2,V1,V2. L1.ⓑ{I1}V1 ≅[0,∞] L2.ⓑ{I2}V2.
+#L1 #L2 #HL12 #I1 #I2 #V1 #V2 lapply (lcoeq_pair I1 I2 … V1 V2 … HL12) -HL12 //
+qed.
+
+lemma lcoeq_refl: ∀L,d,e. L ≅[d, e] L.
+#L elim L -L //
+#L #I #V #IHL #d elim (ynat_cases … d) [| * #x ]
+#Hd destruct /2 width=1 by lcoeq_succ/
+#e elim (ynat_cases … e) [| * #x ]
+#He destruct /2 width=1 by lcoeq_zero, lcoeq_pair/
+qed.
+
+lemma lcoeq_O_Y: ∀L1,L2. |L1| = |L2| → L1 ≅[0, ∞] L2.
+#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ]
+* [2,4: #L2 #I2 #V1 ] normalize /3 width=2 by lcoeq_pair_O_Y/
+<plus_n_Sm #H destruct
+qed.
+
+lemma lcoeq_sym: ∀d,e. symmetric … (lcoeq d e).
+#d #e #L1 #L2 #H elim H -L1 -L2
+/2 width=1 by lcoeq_zero, lcoeq_pair, lcoeq_succ/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lcoeq_inv_atom1_aux: ∀L1,L2,d,e. L1 ≅[d, e] L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 #d #e * -L1 -L2 -d -e //
+[ #I #L1 #L2 #V #_ #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #H destruct
+| #I #L1 #L2 #V #d #e #_ #H destruct
+]
+qed-.
+
+lemma lcoeq_inv_atom1: ∀L2,d,e. ⋆ ≅[d, e] L2 → L2 = ⋆.
+/2 width=5 by lcoeq_inv_atom1_aux/ qed-.
+
+fact lcoeq_inv_zero1_aux: ∀L1,L2,d,e. L1 ≅[d, e] L2 →
+ ∀J,K1,W. L1 = K1.ⓑ{J}W → d = 0 → e = 0 →
+ ∃∃K2. K1 ≅[0, 0] K2 & L2 = K2.ⓑ{J}W.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #J #K1 #W #H destruct
+| #I #L1 #L2 #V #HL12 #J #K1 #W #H destruct /2 width=3 by ex2_intro/
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #J #K1 #W #_ #_ #H elim (ysucc_inv_O_dx … H)
+| #I #L1 #L2 #V #d #e #_ #J #K1 #W #_ #H elim (ysucc_inv_O_dx … H)
+]
+qed-.
+
+lemma lcoeq_inv_zero1: ∀I,K1,L2,V. K1.ⓑ{I}V ≅[0, 0] L2 →
+ ∃∃K2. K1 ≅[0, 0] K2 & L2 = K2.ⓑ{I}V.
+/2 width=7 by lcoeq_inv_zero1_aux/ qed-.
+
+fact lcoeq_inv_pair1_aux: ∀L1,L2,d,e. L1 ≅[d, e] L2 →
+ ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → d = 0 → 0 < e →
+ ∃∃J2,K2,W2. K1 ≅[0, ⫰e] K2 & L2 = K2.ⓑ{J2}W2.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #J1 #K1 #W1 #H destruct
+| #I #L1 #L2 #V #_ #J1 #K1 #W1 #_ #_ #H elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 #J1 #K1 #W1 #H #_ #_ destruct
+ /2 width=5 by ex2_3_intro/
+| #I #L1 #L2 #V #d #e #_ #J1 #K1 #W1 #_ #H elim (ysucc_inv_O_dx … H)
+]
+qed-.
+
+lemma lcoeq_inv_pair1: ∀I1,K1,L2,V1,e. K1.ⓑ{I1}V1 ≅[0, e] L2 → 0 < e →
+ ∃∃I2,K2,V2. K1 ≅[0, ⫰e] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=7 by lcoeq_inv_pair1_aux/ qed-.
+
+fact lcoeq_inv_succ1_aux: ∀L1,L2,d,e. L1 ≅[d, e] L2 →
+ ∀J,K1,W. L1 = K1.ⓑ{J}W → 0 < d →
+ ∃∃K2. K1 ≅[⫰d, e] K2 & L2 = K2.ⓑ{J}W.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #J #K1 #W #H destruct
+| #I #L1 #L2 #V #_ #J #K1 #W #_ #H elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #J #K1 #W #_ #H elim (ylt_yle_false … H) //
+| #I #L1 #L2 #V #d #e #HL12 #J #K1 #W #H destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma lcoeq_inv_succ1: ∀I,K1,L2,V,d,e. K1.ⓑ{I}V ≅[d, e] L2 → 0 < d →
+ ∃∃K2. K1 ≅[⫰d, e] K2 & L2 = K2.ⓑ{I}V.
+/2 width=3 by lcoeq_inv_succ1_aux/ qed-.
+
+lemma lcoeq_inv_atom2: ∀L1,d,e. L1 ≅[d, e] ⋆ → L1 = ⋆.
+/3 width=3 by lcoeq_inv_atom1, lcoeq_sym/ qed-.
+
+lemma lcoeq_inv_zero2: ∀I,K2,L1,V. L1 ≅[0, 0] K2.ⓑ{I}V →
+ ∃∃K1. K1 ≅[0, 0] K2 & L1 = K1.ⓑ{I}V.
+#I #K2 #L1 #V #H elim (lcoeq_inv_zero1 … (lcoeq_sym … H)) -H
+/3 width=3 by lcoeq_sym, ex2_intro/
+qed-.
+
+lemma lcoeq_inv_pair2: ∀I2,K2,L1,V2,e. L1 ≅[0, e] K2.ⓑ{I2}V2 → 0 < e →
+ ∃∃I1,K1,V1. K1 ≅[0, ⫰e] K2 & L1 = K1.ⓑ{I1}V1.
+#I2 #K2 #L1 #V2 #e #H #He elim (lcoeq_inv_pair1 … (lcoeq_sym … H)) -H
+/3 width=5 by lcoeq_sym, ex2_3_intro/
+qed-.
+
+lemma lcoeq_inv_succ2: ∀I,K2,L1,V,d,e. L1 ≅[d, e] K2.ⓑ{I}V → 0 < d →
+ ∃∃K1. K1 ≅[⫰d, e] K2 & L1 = K1.ⓑ{I}V.
+#I #K2 #L1 #V #d #e #H #Hd elim (lcoeq_inv_succ1 … (lcoeq_sym … H)) -H
+/3 width=3 by lcoeq_sym, ex2_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lcoeq_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-.
+
+(* Advanced inversionn lemmas ***********************************************)
+
+fact lcoeq_inv_O2_aux: ∀L1,L2,d,e. L1 ≅[d, e] L2 → e = 0 → L1 = L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/
+#I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H elim (ysucc_inv_O_dx … H)
+qed-.
+
+lemma lcoeq_inv_O2: ∀L1,L2,d. L1 ≅[d, 0] L2 → L1 = L2.
+/2 width=4 by lcoeq_inv_O2_aux/ 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/lcoeq.ma".
+
+(* COEQUIVALENCE FOR LOCAL ENVIRONMENTS *************************************)
+
+(* Main properties **********************************************************)
+
+theorem lcoeq_trans: ∀d,e. Transitive … (lcoeq d e).
+#d #e #L1 #L2 #H elim H -L1 -L2 -d -e //
+[ #I #L1 #L #V #HL1 #_ #X #H >(lcoeq_inv_O2 … HL1) -HL1 //
+| #I1 #I #L1 #L #V1 #V #e #_ #IHL1 #X #H elim (lcoeq_inv_pair1 … H) -H //
+ #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by lcoeq_pair/
+| #I #L1 #L #V #d #e #_ #IHL1 #X #H elim (lcoeq_inv_succ1 … H) -H //
+ #L2 #HL2 #H destruct /3 width=1 by lcoeq_succ/
+]
+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 "ground_2/ynat/ynat_minus.ma".
+include "basic_2/grammar/lcoeq.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
+
+(* Properties on coequivalence **********************************************)
+
+lemma lcoeq_ldrop_trans_lt: ∀L1,L2,d,e. L1 ≅[d, e] L2 →
+ ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W → i < d →
+ ∃∃K1. K1 ≅[⫰(d-i), e] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #J #K2 #W #s #i #H
+ elim (ldrop_inv_atom1 … H) -H #H destruct
+| #I #L1 #L2 #V #_ #_ #J #K2 #W #s #i #_ #H
+ elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K2 #W #s #i #_ #H
+ elim (ylt_yle_false … H) //
+| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K2 #W #s #i #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ]
+ [ #_ destruct >ypred_succ
+ /2 width=3 by ldrop_pair, ex2_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=3 by ldrop_drop_lt, ex2_intro/
+ ]
+]
+qed-.
+
+lemma lcoeq_ldrop_conf_lt: ∀L1,L2,d,e. L1 ≅[d, e] L2 →
+ ∀I,K1,W,s,i. ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W → i < d →
+ ∃∃K2. K1 ≅[⫰(d-i), e] K2 & ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W.
+#L1 #L2 #d #e #HL12 #I #K1 #W #s #i #HLK1 #Hid
+elim (lcoeq_ldrop_trans_lt … (lcoeq_sym … HL12) … HLK1) // -L1 -Hid
+/3 width=3 by lcoeq_sym, ex2_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/ldrop_leq.ma".
-include "basic_2/relocation/lleq_lleq.ma".
-include "basic_2/reduction/cpx.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
-
-(* Properties on lazy equivalence for local environments ********************)
-
-lemma lleq_cpx_trans_leq: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L1,d. L1 ⋕[d, T1] L2 → L1 ≃[d, ∞] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_sort/
-[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #d #H #HL12 elim (lleq_inv_lref_dx … H … HLK2) -H *
- [ #K1 #HLK1 #HV1 #Hdi elim (ldrop_leq_conf_be … HL12 … HLK1) -HL12 /2 width=1 by yle_inj/
- >yminus_Y_inj #J #Y #X #HK12 #H lapply (ldrop_mono … H … HLK2) -L2
- #H destruct /3 width=7 by cpx_delta/
- | #J #K1 #V #HLK1 #_ #HV1 #Hid elim (ldrop_leq_conf_lt … HL12 … HLK1) -HL12 /2 width=1 by ylt_inj/
- <yminus_SO2 >yminus_inj #Y #HK12 #H lapply (ldrop_mono … H … HLK2) -L2
- #H destruct /3 width=7 by cpx_delta/
- ]
-| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_bind … H) -H
- /4 width=3 by cpx_bind, leq_succ/
-| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
- /3 width=3 by cpx_flat/
-| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #H elim (lleq_inv_bind … H) -H
- /4 width=3 by cpx_zeta, leq_succ/
-| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
- /3 width=3 by cpx_tau/
-| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #d #H elim (lleq_inv_flat … H) -H
- /3 width=3 by cpx_ti/
-| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
- #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_beta, leq_succ/
-| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H
- #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_theta, leq_succ/
-]
-qed-.
-
-(* Note: this can be proved directly *)
-lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L1. L1 ⋕[0, T1] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2.
-/4 width=6 by lleq_cpx_trans_leq, lleq_fwd_length, leq_O_Y/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 ≃ break [ term 46 d , break term 46 e ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'Iso $d $e $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/ynat/ynat_plus.ma".
-include "basic_2/grammar/leq.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************)
-
-lemma ldrop_leq_conf_ge: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
- ∀I,K,V,i. ⇩[O, i]L1 ≡ K.ⓑ{I}V → d + e ≤ i →
- ⇩[O, i]L2 ≡ K.ⓑ{I}V.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #d #e #J #K #W #i #H elim (ldrop_inv_atom1 … H) -H
- #H destruct
-| #I #L1 #L2 #V #HL12 #IHL12 #J #K #W #i #H #_ elim (ldrop_inv_O1_pair1 … H) -H
- * #H1 #H2
- [ -IHL12 lapply (leq_inv_O2 … HL12) -HL12
- #H3 destruct //
- | -HL12 /4 width=1 by ldrop_ldrop_lt, yle_inj/
- ]
-| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #IHL12 #J #K #W #i #H1 >yplus_succ_swap
- #Hei elim (yle_inv_inj2 … Hei) -Hei
- #x #Hei #H elim (yplus_inv_inj … H) -H normalize
- #y #z >commutative_plus
- #H1 #H2 #H3 destruct elim (le_inv_plus_l … Hei) -Hei
- #Hzi #Hi lapply (ldrop_inv_ldrop1_lt … H1 ?) -H1
- /4 width=1 by ldrop_ldrop_lt, yle_inj/
-| #I #L1 #L2 #V #d #e #_ #IHL12 #J #K #W #i #H0 #Hdei elim (yle_inv_inj2 … Hdei) -Hdei
- #x #Hdei #H elim (yplus_inv_inj … H) -H
- #y #z >commutative_plus
- #H1 #H2 #H3 destruct elim (ysucc_inv_inj_dx … H2) -H2
- #x #H1 #H2 destruct elim (le_inv_plus_l … Hdei)
- #_ #Hi lapply (ldrop_inv_ldrop1_lt … H0 ?) -H0
- [2: #H0 @ldrop_ldrop_lt ] [2,3: /2 width=3 by lt_to_le_to_lt/ ]
- /4 width=3 by yle_inj, monotonic_pred/
-]
-qed-.
-
-lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
- ∀I1,K1,V1,i. ⇩[O, i]L1 ≡ K1.ⓑ{I1}V1 → d ≤ i → i < d + e →
- ∃∃I2,K2,V2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I2}V2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H
- #H destruct
-| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) //
-| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O1 >yplus_O1
- #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
- [ #_ lapply (ldrop_inv_O2 … H) -H
- #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/
- | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
- #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
- #Hie lapply (ylt_inv_succ … Hie) -Hie
- #Hie elim (IHL12 … H) -IHL12 -H //
- >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
- ]
-| #I #L1 #L2 #V #d #e #_ #IHL12 #J1 #K1 #W1 #i #H #Hdi lapply (ylt_yle_trans 0 … Hdi ?) //
- #Hi <(ylt_inv_O1 … Hi) >yplus_succ1 >yminus_succ elim (yle_inv_succ1 … Hdi) -Hdi
- #Hdi #_ #Hide lapply (ylt_inv_succ … Hide)
- #Hide lapply (ylt_inv_inj … Hi) -Hi
- #Hi lapply (ldrop_inv_ldrop1_lt … H ?) -H //
- #H elim (IHL12 … H) -IHL12 -H
- /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/
-]
-qed-.
-
-lemma ldrop_leq_conf_lt: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
- ∀I,K1,V,i. ⇩[O, i]L1 ≡ K1.ⓑ{I}V → i < d →
- ∃∃K2. K1 ≃[⫰(d-i), e] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I}V.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-[ #d #e #J #K1 #W #i #H elim (ldrop_inv_atom1 … H) -H
- #H destruct
-| #I #L1 #L2 #V #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
-| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) //
-| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K1 #W #i #H elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
- [ #_ lapply (ldrop_inv_O2 … H) -H
- #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_intro/
- | lapply (ldrop_inv_ldrop1_lt … H ?) -H //
- #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/
- #Hie lapply (ylt_inv_succ … Hie) -Hie
- #Hie elim (IHL12 … H) -IHL12 -H
- >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_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 "ground_2/ynat/ynat_succ.ma".
-include "basic_2/notation/relations/iso_4.ma".
-include "basic_2/grammar/lenv_length.ma".
-
-(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
-
-inductive leq: ynat → ynat → relation lenv ≝
-| leq_atom: ∀d,e. leq d e (⋆) (⋆)
-| leq_zero: ∀I,L1,L2,V. leq 0 0 L1 L2 → leq 0 0 (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| leq_pair: ∀I1,I2,L1,L2,V1,V2,e.
- leq 0 e L1 L2 → leq 0 (⫯e) (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
-| leq_succ: ∀I,L1,L2,V,d,e. leq d e L1 L2 → leq (⫯d) e (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-.
-
-interpretation
- "equivalence (local environment)"
- 'Iso d e L1 L2 = (leq d e L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma leq_refl: ∀L,d,e. L ≃[d, e] L.
-#L elim L -L /2 width=1 by/
-#L #I #V #IHL #d #e elim (ynat_cases … d) [ | * /2 width=1 by leq_succ/ ]
-elim (ynat_cases … e) [ | * ]
-/2 width=1 by leq_zero, leq_pair/
-qed.
-
-lemma leq_sym: ∀L1,L2,d,e. L1 ≃[d, e] L2 → L2 ≃[d, e] L1.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-/2 width=1 by leq_atom, leq_zero, leq_pair, leq_succ/
-qed-.
-
-lemma leq_O_Y: ∀L1,L2. |L1| = |L2| → L1 ≃[0, ∞] L2.
-#L1 elim L1 -L1
-[ #X #H lapply (length_inv_zero_sn … H) -H //
-| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H
- #L2 #I2 #V2 #HL12 #H destruct
- @(leq_pair … (∞)) /2 width=1 by/ (**) (* explicit constructor *)
-]
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L1| = |L2|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize //
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact leq_inv_O2_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → e = 0 → L1 = L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/
-#I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H elim (ysucc_inv_O_dx … H)
-qed-.
-
-lemma leq_inv_O2: ∀L1,L2,d. L1 ≃[d, 0] L2 → L1 = L2.
-/2 width=4 by leq_inv_O2_aux/ qed-.
-
-fact leq_inv_Y1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → d = ∞ → L1 = L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/
-[ #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H destruct
-| #I #L1 #L2 #V #d #e #_ #IHL12 #H lapply (ysucc_inv_Y_dx … H) -H
- /3 width=1 by eq_f3/
-]
-qed-.
-
-lemma leq_inv_Y1: ∀L1,L2,e. L1 ≃[∞, e] L2 → L1 = L2.
-/2 width=4 by leq_inv_Y1_aux/ 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/lenv_length.ma".
-
-(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
-
-notation "hvbox( T1 break [ d , break e ] ≈ break T2 )"
- non associative with precedence 45
- for @{ 'Eq $T1 $d $e $T2 }.
-
-inductive leq: nat → nat → relation lenv ≝
-| leq_sort: ∀d,e. leq d e (⋆) (⋆)
-| leq_OO: ∀L1,L2. leq 0 0 L1 L2
-| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 →
- leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V)
-| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
- leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
-.
-
-interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2).
-
-definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R.
- ∀L1,s1,s2. R L1 s1 s2 →
- ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2.
-
-(* Basic properties *********************************************************)
-
-lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))).
-#S #R #HR #L1 #s1 #s2 #H elim H -H s2
-[ /3 width=5/
-| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12
- lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/
-]
-qed.
-
-lemma leq_refl: ∀d,e,L. L [d, e] ≈ L.
-#d elim d -d
-[ #e elim e -e // #e #IHe #L elim L -L /2/
-| #d #IHd #e #L elim L -L /2/
-]
-qed.
-
-lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/
-qed.
-
-lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d →
- ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2.
-
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
+++ /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 *)
-(* *)
-(**************************************************************************)
-
-axiom- lleq_inv_lref_lt_bi: ∀L1,L2,i,d. L1 ⋕[d, #i] L2 → i < d →
- ∀I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 →
- K1 ⋕[d-i-1, V1] K2 ∧ K1 ⋕[d-i-1, V2] K2.
-
-include "Basic-2/grammar/lenv_length.ma".
-
-(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
-
-interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2).
-
-(* Basic properties *********************************************************)
-
-| leq_comp: ∀L1,L2,I1,I2,V1,V2.
- leq L1 0 0 L2 → leq (L1. 𝕓{I1} V1) 0 0 (L2. 𝕓{I2} V2)
-
-lemma leq_fwd_length: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → |L1| = |L2|.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e; normalize //
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma leq_inv_sort1_aux: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e
-[ //
-| #L1 #L2 #I1 #I2 #V1 #V2 #_ #_ #H destruct
-| #L1 #L2 #I #V #e #_ #_ #H destruct
-| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #_ #H destruct
-qed.
-
-lemma leq_inv_sort1: ∀L2,d,e. ⋆ [d, e] ≈ L2 → L2 = ⋆.
-/2 width=5/ qed.
-
-lemma leq_inv_sort2: ∀L1,d,e. L1 [d, e] ≈ ⋆ → L1 = ⋆.
-/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/notation/relations/leqdx_3.ma".
-include "basic_2/grammar/lenv_length.ma".
-
-(* DX GUARDED EQUIVALENCE FOR LOCAL ENVIRONMENTS ****************************)
-
-inductive leqdx: nat → relation lenv ≝
-| leqdx_atom: ∀d. leqdx d (⋆) (⋆)
-| leqdx_zero: ∀I1,I2,L1,L2,V1,V2.
- leqdx 0 L1 L2 → leqdx 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
-| leqdx_succ: ∀I,L1,L2,V,d.
- leqdx d L1 L2 → leqdx (d+1) (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-.
-
-interpretation
- "guarded equivalence (local environment, dx variant)"
- 'LEqDx d L1 L2 = (leqdx d L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma leqdx_O: ∀L1,L2. |L1| = |L2| → L1 ≚[0] L2.
-#L1 elim L1 -L1
-[ #L2 #H >(length_inv_zero_sn … H) -L2 //
-| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H
- #I2 #L2 #V2 #HL12 #H destruct /3 width=1 by leqdx_zero/
-]
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact leqdx_inv_succ2_aux: ∀L1,L2,d. L1 ≚[d] L2 →
- ∀I,K2,V,e. L2 = K2.ⓑ{I}V → d = e + 1 →
- ∃∃K1. K1 ≚[e] K2 & L1 = K1.ⓑ{I}V.
-#L1 #L2 #d * -L1 -L2 -d
-[ #d #J #K2 #W #e #H destruct
-| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K2 #W #e #_
- >commutative_plus normalize #H destruct
-| #I #L1 #L2 #V #d #HL12 #J #K2 #W #e #H1 #H2 destruct
- /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma leqdx_inv_succ2: ∀I,L1,K2,V,d. L1 ≚[d+1] K2.ⓑ{I}V →
- ∃∃K1. K1 ≚[d] K2 & L1 = K1.ⓑ{I}V.
-/2 width=5 by leqdx_inv_succ2_aux/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 ≚ break [ term 46 d ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'LEqDx $d $L1 $L2 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/reduction/cpx_leq.ma".
-include "basic_2/reduction/lpx_ldrop.ma".
-
-(**) (* to be proved later *)
-axiom- lleq_beta: ∀L2s,L2d,V2,W2,T2,d.
- L2s.ⓛW2 ⋕[d+1, T2] L2d.ⓛW2 →
- L2s.ⓓⓝW2.V2 ⋕[d+1, T2] L2d.ⓓⓝW2.V2.
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties using equivalences for local environments *********************)
-
-lemma lleq_cpx_conf_leq_dx: ∀h,g,G,L1s,L1d,T1,d. L1s ⋕[d, T1] L1d → L1s ≃[d, ∞] L1d →
- ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s → L1s ≃[0, d] L2s →
- ∀L2d. ⦃G, L1d⦄ ⊢ ➡[h, g] L2d → L1d ≃[0, d] L2d →
- L2s ≃[d, ∞] L2d → L2s ⋕[d, T2] L2d.
-#h #g #G #L1s #L1d #T1 #d #H elim H -L1s -L1d -T1 -d
-[ #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3
- lapply (leq_fwd_length … H3) -H3 #HL2sd
- elim (cpx_inv_sort1 … H2) -H2 [| * #l #_ ]
- #H destruct /2 width=1 by lleq_sort/
-| #Is #Id #L1s #L1d #K1s #K1d #V1s #V1d #d #i #Hid #HLK1s #HLK1d #_ #_ #_ #IHV1d #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
- elim (ldrop_leq_conf_lt … H1 … HLK1s) -H1 /2 width=1 by ylt_inj/
- <yminus_SO2 >yminus_inj #Y #H1 #HY
- lapply (ldrop_mono … HY … HLK1d) -HY #H destruct
- elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s
- elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct
- elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d
- elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct
- elim (ldrop_leq_conf_be … H2s … HLK1s) -H2s /2 width=1 by ylt_inj/
- >yplus_O1 <yminus_SO2 >yminus_inj #Z #Y #X #HK12s #H
- lapply (ldrop_mono … H … HLK2s) -H #H destruct
- elim (ldrop_leq_conf_be … H2d … HLK1d) -H2d /2 width=1 by ylt_inj/
- >yplus_O1 <yminus_SO2 >yminus_inj #Z #Y #X #HK12d #H
- lapply (ldrop_mono … H … HLK2d) -H #H destruct
- elim (ldrop_leq_conf_lt … H3 … HLK2s) -H3 /2 width=1 by ylt_inj/
- <yminus_SO2 >yminus_inj #Y #H3 #HY
- lapply (ldrop_mono … HY … HLK2d) -HY #H destruct
- elim (cpx_inv_lref1 … H2) -H2 -L1s
- [ -L1d #H destruct /3 width=15 by lleq_skip/
- | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d
- #H destruct >(plus_minus_m_m d (i+1)) //
- lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s
- lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d
- /3 width=9 by lleq_lift_ge/
- ]
-| #I #L1s #L1d #K1s #K1d #V1 #d #i #Hdi #HLK1s #HLK1d #_ #IHV1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
- elim (ldrop_leq_conf_be … H1 … HLK1s) -H1 /2 width=1 by ylt_Y, yle_inj/ #Z #Y #X #H1 #HY
- lapply (ldrop_mono … HY … HLK1d) -HY #H destruct
- elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s
- elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct
- elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d
- elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct
- lapply (ldrop_leq_conf_ge … H2s … HLK1s ?) /2 width=1 by yle_inj/ #H
- lapply (ldrop_mono … H … HLK2s) -H #H destruct
- lapply (ldrop_leq_conf_ge … H2d … HLK1d ?) /2 width=1 by yle_inj/ #H
- lapply (ldrop_mono … H … HLK2d) -H #H destruct
- elim (ldrop_leq_conf_be … H3 … HLK2s) -H3 /2 width=1 by ylt_Y, yle_inj/
- >yminus_Y_inj #Z #Y #X #H3 #HY
- lapply (ldrop_mono … HY … HLK2d) -HY #H destruct
- elim (cpx_inv_lref1 … H2) -H2 -L1s
- [ -L1d #H destruct /3 width=12 by lleq_lref/
- | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d
- #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s #HLK2s
- lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d #HLK2d
- @(lleq_ge … 0) /3 width=10 by lleq_lift_le/ (**) (* full auto too slow *)
- ]
-| #L1s #L1d #d #i #HL1s #HL1d #_ #_ #X #H2 #L2s #_ #_ #L2s #_ #H2d #H3
- lapply (leq_fwd_length … H2d) -H2d
- lapply (leq_fwd_length … H3) -H3
- elim (cpx_inv_lref1 … H2) -H2
- [ #H destruct /2 width=1 by lleq_free/
- | -L1s * #I #K1d #V1 #V2 #HLK1d
- lapply (ldrop_fwd_length_lt2 … HLK1d) -HLK1d #H
- elim (lt_refl_false … i) /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *)
- ]
-| #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3
- lapply (leq_fwd_length … H3) -H3 #HL2sd
- lapply (cpx_inv_gref1 … H2) -H2
- #H destruct /2 width=1 by lleq_gref/
-| #a #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
- elim (cpx_inv_bind1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct
- /5 width=5 by lpx_pair, lleq_cpx_trans_leq, lleq_bind, leq_pair, leq_succ/
- | #T2 #HT12 #HT2X #H1 #H2 destruct >(minus_plus_m_m d 1)
- /4 width=9 by lpx_pair, lleq_inv_lift_ge, ldrop_ldrop, leq_pair, leq_succ/
- ]
-| #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3
- elim (cpx_inv_flat1 … H2) -H2 *
- [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by lleq_flat/
- | #HT1X #H destruct /2 width=1 by/
- | #HV1X #H destruct /2 width=1 by/
- | #a #V2 #W1 #W2 #T0 #T2 #HV12 #HW12 #HT02 #H1 #H2 #H3 destruct
- lapply (IHT1 … (ⓛ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H
- elim (lleq_inv_bind … H) -H -HW12 -HT02 #HW2 #HT2
- /4 width=1 by lleq_beta, lleq_flat, lleq_bind/
- | #a #V0 #V2 #W1 #W2 #T0 #T2 #HV10 #HV02 #HW12 #HT02 #H1 #H2 #H3 destruct
- lapply (IHT1 … (ⓓ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H
- elim (lleq_inv_bind … H) -H -HW12 -HT02
- /5 width=9 by lleq_lift_ge, lleq_flat, lleq_bind, ldrop_ldrop/
- ]
-]
-qed-.
-
-lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
- ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2.
-#h #g #G #L2 #T1 #T2 #HT12 #L1 #HT1 lapply (lleq_fwd_length … HT1)
-/3 width=13 by lleq_cpx_conf_leq_dx, leq_O_Y/
-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/lenv_append.ma".
-
-(* SHIFT OF A CLOSURE *******************************************************)
-
-let rec shift L T on L ≝ match L with
-[ LAtom ⇒ T
-| LPair L I V ⇒ shift L (-ⓑ{I} V. T)
-].
-
-interpretation "shift (closure)" 'Append L T = (shift L T).
-
-(* Basic properties *********************************************************)
-
-lemma shift_append_assoc: ∀L,K. ∀T:term. (L @@ K) @@ T = L @@ K @@ T.
-#L #K elim K -K // normalize //
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma shift_inj: ∀L1,L2. ∀T1,T2:term. L1 @@ T1 = L2 @@ T2 → |L1| = |L2| →
- L1 = L2 ∧ T1 = T2.
-#L1 elim L1 -L1
-[ * normalize /2 width=1/
- #L2 #I2 #V2 #T1 #T2 #_ <plus_n_Sm #H destruct
-| #L1 #H1 #V1 #IH * normalize
- [ #T1 #T2 #_ <plus_n_Sm #H destruct
- | #L2 #I2 #V2 #T1 #T2 #H1 #H2
- elim (IH … H1) -IH -H1 /2 width=1/ -H2 #H1 #H2 destruct /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 "ground_2/ynat/ynat_lt.ma".
+include "basic_2/notation/relations/iso_4.ma".
+include "basic_2/grammar/lenv_length.ma".
+
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
+
+inductive leq: relation4 ynat ynat lenv lenv ≝
+| leq_atom: ∀d,e. leq d e (⋆) (⋆)
+| leq_zero: ∀I1,I2,L1,L2,V1,V2.
+ leq 0 0 L1 L2 → leq 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
+| leq_pair: ∀I,L1,L2,V,e. leq 0 e L1 L2 →
+ leq 0 (⫯e) (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| leq_succ: ∀I1,I2,L1,L2,V1,V2,d,e.
+ leq d e L1 L2 → leq (⫯d) e (L1. ⓑ{I1}V1) (L2. ⓑ{I2} V2)
+.
+
+interpretation
+ "equivalence (local environment)"
+ 'Iso d e L1 L2 = (leq d e L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma leq_pair_lt: ∀I,L1,L2,V,e. L1 ≃[0, ⫰e] L2 → 0 < e →
+ L1.ⓑ{I}V ≃[0, e] L2.ⓑ{I}V.
+#I #L1 #L2 #V #e #HL12 #He <(ylt_inv_O1 … He) /2 width=1 by leq_pair/
+qed.
+
+lemma leq_succ_lt: ∀I1,I2,L1,L2,V1,V2,d,e. L1 ≃[⫰d, e] L2 → 0 < d →
+ L1.ⓑ{I1}V1 ≃[d, e] L2. ⓑ{I2}V2.
+#I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #Hd <(ylt_inv_O1 … Hd) /2 width=1 by leq_succ/
+qed.
+
+lemma leq_pair_O_Y: ∀L1,L2. L1 ≃[0, ∞] L2 →
+ ∀I,V. L1.ⓑ{I}V ≃[0, ∞] L2.ⓑ{I}V.
+#L1 #L2 #HL12 #I #V lapply (leq_pair I … V … HL12) -HL12 //
+qed.
+
+lemma leq_refl: ∀L,d,e. L ≃[d, e] L.
+#L elim L -L //
+#L #I #V #IHL #d elim (ynat_cases … d) [| * #x ]
+#Hd destruct /2 width=1 by leq_succ/
+#e elim (ynat_cases … e) [| * #x ]
+#He destruct /2 width=1 by leq_zero, leq_pair/
+qed.
+
+lemma leq_O2: ∀L1,L2,d. |L1| = |L2| → L1 ≃[d, yinj 0] L2.
+#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ]
+* // [1,3: #L2 #I2 #V2 ] #d normalize
+[1,3: <plus_n_Sm #H destruct ]
+#H lapply (injective_plus_l … H) -H #HL12
+elim (ynat_cases d) /3 width=1 by leq_zero/
+* /3 width=1 by leq_succ/
+qed.
+
+lemma leq_sym: ∀d,e. symmetric … (leq d e).
+#d #e #L1 #L2 #H elim H -L1 -L2 -d -e
+/2 width=1 by leq_zero, leq_pair, leq_succ/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact leq_inv_atom1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 #d #e * -L1 -L2 -d -e //
+[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #H destruct
+| #I #L1 #L2 #V #e #_ #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #H destruct
+]
+qed-.
+
+lemma leq_inv_atom1: ∀L2,d,e. ⋆ ≃[d, e] L2 → L2 = ⋆.
+/2 width=5 by leq_inv_atom1_aux/ qed-.
+
+fact leq_inv_zero1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → d = 0 → e = 0 →
+ ∃∃J2,K2,W2. K1 ≃[0, 0] K2 & L2 = K2.ⓑ{J2}W2.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #J1 #K1 #W1 #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J1 #K1 #W1 #H #_ #_ destruct
+ /2 width=5 by ex2_3_intro/
+| #I #L1 #L2 #V #e #_ #J1 #K1 #W1 #_ #_ #H
+ elim (ysucc_inv_O_dx … H)
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #J1 #K1 #W1 #_ #H
+ elim (ysucc_inv_O_dx … H)
+]
+qed-.
+
+lemma leq_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ≃[0, 0] L2 →
+ ∃∃I2,K2,V2. K1 ≃[0, 0] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=9 by leq_inv_zero1_aux/ qed-.
+
+fact leq_inv_pair1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀J,K1,W. L1 = K1.ⓑ{J}W → d = 0 → 0 < e →
+ ∃∃K2. K1 ≃[0, ⫰e] K2 & L2 = K2.ⓑ{J}W.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #J #K1 #W #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K1 #W #_ #_ #H
+ elim (ylt_yle_false … H) //
+| #I #L1 #L2 #V #e #HL12 #J #K1 #W #H #_ #_ destruct
+ /2 width=3 by ex2_intro/
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #J #K1 #W #_ #H
+ elim (ysucc_inv_O_dx … H)
+]
+qed-.
+
+lemma leq_inv_pair1: ∀I,K1,L2,V,e. K1.ⓑ{I}V ≃[0, e] L2 → 0 < e →
+ ∃∃K2. K1 ≃[0, ⫰e] K2 & L2 = K2.ⓑ{I}V.
+/2 width=6 by leq_inv_pair1_aux/ qed-.
+
+fact leq_inv_succ1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < d →
+ ∃∃J2,K2,W2. K1 ≃[⫰d, e] K2 & L2 = K2.ⓑ{J2}W2.
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ #d #e #J1 #K1 #W1 #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W1 #_ #H
+ elim (ylt_yle_false … H) //
+| #I #L1 #L2 #V #e #_ #J1 #K1 #W1 #_ #H
+ elim (ylt_yle_false … H) //
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #HL12 #J1 #K1 #W1 #H #_ destruct
+ /2 width=5 by ex2_3_intro/
+]
+qed-.
+
+lemma leq_inv_succ1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≃[d, e] L2 → 0 < d →
+ ∃∃I2,K2,V2. K1 ≃[⫰d, e] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=5 by leq_inv_succ1_aux/ qed-.
+
+lemma leq_inv_atom2: ∀L1,d,e. L1 ≃[d, e] ⋆ → L1 = ⋆.
+/3 width=3 by leq_inv_atom1, leq_sym/
+qed-.
+
+lemma leq_inv_zero2: ∀I2,K2,L1,V2. L1 ≃[0, 0] K2.ⓑ{I2}V2 →
+ ∃∃I1,K1,V1. K1 ≃[0, 0] K2 & L1 = K1.ⓑ{I1}V1.
+#I2 #K2 #L1 #V2 #H elim (leq_inv_zero1 … (leq_sym … H)) -H
+/3 width=5 by leq_sym, ex2_3_intro/
+qed-.
+
+lemma leq_inv_pair2: ∀I,K2,L1,V,e. L1 ≃[0, e] K2.ⓑ{I}V → 0 < e →
+ ∃∃K1. K1 ≃[0, ⫰e] K2 & L1 = K1.ⓑ{I}V.
+#I #K2 #L1 #V #e #H #He elim (leq_inv_pair1 … (leq_sym … H)) -H
+/3 width=3 by leq_sym, ex2_intro/
+qed-.
+
+lemma leq_inv_succ2: ∀I2,K2,L1,V2,d,e. L1 ≃[d, e] K2.ⓑ{I2}V2 → 0 < d →
+ ∃∃I1,K1,V1. K1 ≃[⫰d, e] K2 & L1 = K1.ⓑ{I1}V1.
+#I2 #K2 #L1 #V2 #d #e #H #Hd elim (leq_inv_succ1 … (leq_sym … H)) -H
+/3 width=5 by leq_sym, ex2_3_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma leq_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-.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact leq_inv_O_Y_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → d = 0 → e = ∞ → L1 = L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e //
+[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #_ #H destruct
+| /4 width=1 by eq_f3, ysucc_inv_Y_dx/
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #_ #H elim (ysucc_inv_O_dx … H)
+]
+qed-.
+
+lemma leq_inv_O_Y: ∀L1,L2. L1 ≃[0, ∞] L2 → L1 = L2.
+/2 width=5 by leq_inv_O_Y_aux/ 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/leq.ma".
+
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
+
+(* Main properties **********************************************************)
+
+theorem leq_trans: ∀d,e. Transitive … (leq d e).
+#d #e #L1 #L2 #H elim H -L1 -L2 -d -e
+[ #d #e #X #H lapply (leq_inv_atom1 … H) -H
+ #H destruct //
+| #I1 #I #L1 #L #V1 #V #_ #IHL1 #X #H elim (leq_inv_zero1 … H) -H
+ #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by leq_zero/
+| #I #L1 #L #V #e #_ #IHL1 #X #H elim (leq_inv_pair1 … H) -H //
+ #L2 #HL2 #H destruct /3 width=1 by leq_pair/
+| #I1 #I #L1 #L #V1 #V #d #e #_ #IHL1 #X #H elim (leq_inv_succ1 … H) -H //
+ #I2 #L2 #V2 #HL2 #H destruct /3 width=1 by leq_succ/
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/grammar/lenv_append.ma".
+include "basic_2/grammar/lenv_length.ma".
(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
.
+(* Basic properties *********************************************************)
+
+lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R).
+#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/
+qed-.
+
(* Basic inversion lemmas ***************************************************)
fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆.
lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|.
#R #L1 #L2 #H elim H -L1 -L2 normalize //
qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma lpx_sn_fwd_append1: ∀R,L1,K1,L. lpx_sn R (K1 @@ L1) L →
- ∃∃K2,L2. lpx_sn R K1 K2 & L = K2 @@ L2.
-#R #L1 elim L1 -L1
-[ #K1 #K2 #HK12
- @(ex2_2_intro … K2 (⋆)) // (* explicit constructor, /2 width=4/ does not work *)
-| #L1 #I #V1 #IH #K1 #X #H
- elim (lpx_sn_inv_pair1 … H) -H #L #V2 #H1 #HV12 #H destruct
- elim (IH … H1) -IH -H1 #K2 #L2 #HK12 #H destruct
- @(ex2_2_intro … (L2.ⓑ{I}V2) HK12) // (* explicit constructor, /2 width=4/ does not work *)
-]
-qed-.
-
-lemma lpx_sn_fwd_append2: ∀R,L2,K2,L. lpx_sn R L (K2 @@ L2) →
- ∃∃K1,L1. lpx_sn R K1 K2 & L = K1 @@ L1.
-#R #L2 elim L2 -L2
-[ #K2 #K1 #HK12
- @(ex2_2_intro … K1 (⋆)) // (**) (* explicit constructor, /2 width=4/ does not work *)
-| #L2 #I #V2 #IH #K2 #X #H
- elim (lpx_sn_inv_pair2 … H) -H #L #V1 #H1 #HV12 #H destruct
- elim (IH … H1) -IH -H1 #K1 #L1 #HK12 #H destruct
- @(ex2_2_intro … (L1.ⓑ{I}V1) HK12) // (* explicit constructor, /2 width=4/ does not work *)
-]
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R).
-#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/
-qed-.
-
-lemma lpx_sn_append: ∀R. l_appendable_sn R →
- ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 →
- lpx_sn R (L1 @@ K1) (L2 @@ K2).
-#R #HR #K1 #K2 #H elim H -K1 -K2 /3 width=1 by lpx_sn_pair/
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ≃ break [ term 46 d , break term 46 e ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'Iso $d $e $L1 $L2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( G ⊢ ⧤ ⬊ * break [ term 46 h , break term 46 g , break term 46 d ] break term 46 L )"
+ non associative with precedence 45
+ for @{ 'LazyCoSN $h $g $d $G $L }.
+++ /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/reduction/crr_append.ma".
-include "basic_2/reduction/cir.ma".
-
-(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************)
-
-(* Advanved properties ******************************************************)
-
-lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐈⦃T⦄.
-/3 width=2 by crr_inv_labst_last/ qed.
-
-lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄.
-/3 width=2 by crr_inv_trr/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄.
-/3 width=1/ qed-.
-
-lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄.
-/3 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/reduction/crx_append.ma".
-include "basic_2/reduction/cix.ma".
-
-(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ***************)
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma cix_inv_append_sn: ∀h,g,G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
-/3 width=1 by crx_append_sn/ qed-.
-
-lemma cix_inv_tix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
-/3 width=1 by trx_crx/ qed-.
include "basic_2/notation/relations/pred_4.ma".
include "basic_2/grammar/genv.ma".
-include "basic_2/grammar/cl_shift.ma".
-include "basic_2/relocation/ldrop_append.ma".
include "basic_2/relocation/lsubr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
]
qed-.
-lemma cpr_append: ∀G. l_appendable_sn … (cpr G).
-#G #K #T1 #T2 #H elim H -G -K -T1 -T2
-/2 width=3 by cpr_bind, cpr_flat, cpr_zeta, cpr_tau, cpr_beta, cpr_theta/
-#G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
-lapply (ldrop_fwd_length_lt2 … HK0) #H
-@(cpr_delta … (L@@K0) V1 … HVW2) //
-@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
-qed.
-
(* Basic inversion lemmas ***************************************************)
fact cpr_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀I. T1 = ⓪{I} →
]
qed-.
-lemma cpr_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡ T →
- ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
-#G #L1 @(lenv_ind_dx … L1) -L1 normalize
-[ #L #T1 #T #HT1
- @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
-| #I #L1 #V1 #IH #L #T1 #X
- >shift_append_assoc normalize #H
- elim (cpr_inv_bind1 … H) -H *
- [ #V0 #T0 #_ #HT10 #H destruct
- elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
- >append_length >HL12 -HL12
- @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by trans_eq/ (**) (* explicit constructor *)
- | #T #_ #_ #H destruct
- ]
-]
-qed-.
-
(* Basic_1: removed theorems 11:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
pr2_head_2 pr2_cflat clear_pr2_trans
]
qed-.
-lemma cpx_append: ∀h,g,G. l_appendable_sn … (cpx h g G).
-#h #g #G #K #T1 #T2 #H elim H -G -K -T1 -T2
-/2 width=3 by cpx_sort, cpx_bind, cpx_flat, cpx_zeta, cpx_tau, cpx_ti, cpx_beta, cpx_theta/
-#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
-lapply (ldrop_fwd_length_lt2 … HK0) #H
-@(cpx_delta … I … (L@@K0) V1 … HVW2) //
-@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
-qed.
-
(* Basic inversion lemmas ***************************************************)
fact cpx_inv_atom1_aux: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ∀J. T1 = ⓪{J} →
| #T2 #_ #_ #H destruct
]
qed-.
-
-lemma cpx_fwd_shift1: ∀h,g,G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡[h, g] T →
- ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
-#h #g #G #L1 @(lenv_ind_dx … L1) -L1 normalize
-[ #L #T1 #T #HT1
- @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
-| #I #L1 #V1 #IH #L #T1 #X
- >shift_append_assoc normalize #H
- elim (cpx_inv_bind1 … H) -H *
- [ #V0 #T0 #_ #HT10 #H destruct
- elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
- >append_length >HL12 -HL12
- @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by refl, trans_eq/ (**) (* explicit constructor *)
- | #T #_ #_ #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/relocation/ldrop_append.ma".
-include "basic_2/reduction/crr.ma".
-
-(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION **************************)
-
-(* Advanved properties ******************************************************)
-
-lemma crr_append_sn: ∀G,L,K,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡ 𝐑⦃T⦄.
-#G #L #K0 #T #H elim H -L -T /2 width=1/
-#L #K #V #i #HLK
-lapply (ldrop_fwd_length_lt2 … HLK) #Hi
-lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=3/
-qed.
-
-lemma trr_crr: ∀G,L,T. ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄.
-#G #L #T #H lapply (crr_append_sn … H) //
-qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-fact crr_inv_labst_last_aux: ∀G,L1,T,W. ⦃G, L1⦄ ⊢ ➡ 𝐑⦃T⦄ →
- ∀L2. L1 = ⋆.ⓛW @@ L2 → ⦃G, L2⦄ ⊢ ➡ 𝐑⦃T⦄.
-#G #L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/
-[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct
- lapply (ldrop_fwd_length_lt2 … HLK1)
- >append_length >commutative_plus normalize in ⊢ (??% → ?); #H
- elim (le_to_or_lt_eq i (|L2|)) /2 width=1/ -H #Hi destruct
- [ elim (ldrop_O1_lt … Hi) #I2 #K2 #V2 #HLK2
- lapply (ldrop_O1_inv_append1_le … HLK1 … HLK2) -HLK1 /2 width=2/ -Hi
- normalize #H destruct /2 width=3/
- | lapply (ldrop_O1_inv_append1_ge … HLK1 ?) -HLK1 // <minus_n_n #H
- lapply (ldrop_inv_O2 … H) -H #H destruct
- ]
-| #a #I #L1 #V #T #HI #_ #IHT #L2 #H destruct /3 width=1/
-]
-qed.
-
-lemma crr_inv_labst_last: ∀G,L,T,W. ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄.
-/2 width=4/ qed-.
-
-lemma crr_inv_trr: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄.
-/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/relocation/ldrop_append.ma".
-include "basic_2/reduction/crx.ma".
-
-(* REDUCIBLE TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION *****************)
-
-(* Advanved properties ******************************************************)
-
-lemma crx_append_sn: ∀h,g,G,L,K,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
-#h #g #G #L #K0 #T #H elim H -L -T
-/2 width=2 by crx_sort, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/
-#I #L #K #V #i #HLK
-lapply (ldrop_fwd_length_lt2 … HLK) #Hi
-lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=4 by crx_delta, lt_to_le/
-qed.
-
-lemma trx_crx: ∀h,g,G,L,T. ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
-#h #g #G #L #T #H lapply (crx_append_sn … H) //
-qed.
⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ K2.ⓑ{I}V2.
/2 width=1/ qed.
-lemma lpr_append: ∀G,K1,K2. ⦃G, K1⦄ ⊢ ➡ K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 →
- ⦃G, L1 @@ K1⦄ ⊢ ➡ L2 @@ K2.
-/3 width=1 by lpx_sn_append, cpr_append/ qed.
-
(* Basic forward lemmas *****************************************************)
lemma lpr_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → |L1| = |L2|.
/2 width=2 by lpx_sn_fwd_length/ qed-.
-(* Advanced forward lemmas **************************************************)
-
-lemma lpr_fwd_append1: ∀G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ➡ L →
- ∃∃K2,L2. ⦃G, K1⦄ ⊢ ➡ K2 & L = K2 @@ L2.
-/2 width=2 by lpx_sn_fwd_append1/ qed-.
-
-lemma lpr_fwd_append2: ∀G,L,K2,L2. ⦃G, L⦄ ⊢ ➡ K2 @@ L2 →
- ∃∃K1,L1. ⦃G, K1⦄ ⊢ ➡ K2 & L = K1 @@ L1.
-/2 width=2 by lpx_sn_fwd_append2/ qed-.
-
(* Basic_1: removed theorems 3: wcpr0_getl wcpr0_getl_back
pr0_subst1_back
*)
⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2.
/2 width=1 by lpx_sn_pair/ qed.
-lemma lpx_append: ∀h,g,G,K1,K2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
- ⦃G, L1 @@ K1⦄ ⊢ ➡[h, g] L2 @@ K2.
-/3 width=1 by lpx_sn_append, cpx_append/ qed.
-
lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2.
#h #g #G #L1 #L2 #H elim H -L1 -L2 /3 width=1 by lpx_pair, cpr_cpx/
qed.
lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|.
/2 width=2 by lpx_sn_fwd_length/ qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma lpx_fwd_append1: ∀h,g,G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ➡[h, g] L →
- ∃∃K2,L2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & L = K2 @@ L2.
-/2 width=2 by lpx_sn_fwd_append1/ qed-.
-
-lemma lpx_fwd_append2: ∀h,g,G,L,K2,L2. ⦃G, L⦄ ⊢ ➡[h, g] K2 @@ L2 →
- ∃∃K1,L1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & L = K1 @@ L1.
-/2 width=2 by lpx_sn_fwd_append2/ qed-.
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/ldrop.ma".
+include "basic_2/relocation/lsuby.ma".
(* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
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 *************************************)
λR. ∀L1,K1,s,d,e. ⇩[s, d, e] L1 ≡ K1 → ∀L2. R L1 L2 →
∃∃K2. R K1 K2 & ⇩[s, d, e] L2 ≡ K2.
-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 ⊑×[d, e] L1.
-
definition dropable_dx: predicate (relation lenv) ≝
λR. ∀L1,L2. R L1 L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 →
∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & R K1 K2.
]
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 *)
+++ /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/lenv_append.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* DROPPING *****************************************************************)
-
-(* Properties on append for local environments ******************************)
-
-fact ldrop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 →
- d = 0 → e ≤ |L1| →
- ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
-#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize
-[2,3,4: /4 width=1 by ldrop_skip_lt, ldrop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
-#d #e #_ #_ #H <(le_n_O_to_eq … H) -H //
-qed-.
-
-lemma ldrop_O1_append_sn_le: ∀L1,L2,s,e. ⇩[s, 0, e] L1 ≡ L2 → e ≤ |L1| →
- ∀L. ⇩[s, 0, e] L @@ L1 ≡ L @@ L2.
-/2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
-
-(* Inversion lemmas on append for local environments ************************)
-
-lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K →
- |L2| ≤ e → ⇩[s, 0, e - |L2|] L1 ≡ K.
-#K #L1 #L2 elim L2 -L2 normalize //
-#L2 #I #V #IHL2 #s #e #H #H1e
-elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HL12 destruct
-[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2
- >commutative_plus normalize #H destruct
-| <minus_plus >minus_minus_comm /3 width=1 by monotonic_pred/
-]
-qed-.
-
-lemma ldrop_O1_inv_append1_le: ∀K,L1,L2,s,e. ⇩[s, 0, e] L1 @@ L2 ≡ K → e ≤ |L2| →
- ∀K2. ⇩[s, 0, e] L2 ≡ K2 → K = L1 @@ K2.
-#K #L1 #L2 elim L2 -L2 normalize
-[ #s #e #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2
- #H2 elim (ldrop_inv_atom1 … H3) -H3 #H3 #_ destruct
- >(ldrop_inv_O2 … H1) -H1 //
-| #L2 #I #V #IHL2 #s #e @(nat_ind_plus … e) -e [ -IHL2 ]
- [ #H1 #_ #K2 #H2
- lapply (ldrop_inv_O2 … H1) -H1 #H1
- lapply (ldrop_inv_O2 … H2) -H2 #H2 destruct //
- | /4 width=7 by ldrop_inv_drop1, le_plus_to_le_r/
- ]
-]
-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 "ground_2/ynat/ynat_plus.ma".
+include "basic_2/grammar/leq_leq.ma".
+include "basic_2/relocation/ldrop.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 & L1 ≃[d, e] L2.
+
+(* Properties on equivalence ************************************************)
+
+lemma leq_ldrop_trans_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W →
+ d ≤ i → i < d + e →
+ ∃∃K1. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #J #K2 #W #s #i #H
+ elim (ldrop_inv_atom1 … H) -H #H destruct
+| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J #K2 #W #s #i #_ #_ #H
+ elim (ylt_yle_false … H) //
+| #I #L1 #L2 #V #e #HL12 #IHL12 #J #K2 #W #s #i #H #_ >yplus_O1
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ]
+ [ #_ destruct >ypred_succ
+ /2 width=3 by ldrop_pair, ex2_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=3 by ldrop_drop_lt, ex2_intro/
+ ]
+| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #J #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=3 by ylt_O, ldrop_drop_lt, ex2_intro/
+]
+qed-.
+
+lemma leq_ldrop_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 →
+ ∀I,K1,W,s,i. ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W →
+ d ≤ i → i < d + e →
+ ∃∃K2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W.
+#L1 #L2 #d #e #HL12 #I #K1 #W #s #i #HLK1 #Hdi #Hide
+elim (leq_ldrop_trans_be … (leq_sym … HL12) … HLK1) // -L1 -Hdi -Hide
+/3 width=3 by leq_sym, ex2_intro/
+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=4 by inj, ex3_intro/
+| #K #K2 #_ #HK2 * #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2) -HR -K
+ /3 width=6 by leq_trans, step, ex3_intro/
+]
+qed-.
(**************************************************************************)
include "basic_2/grammar/lpx_sn.ma".
-include "basic_2/relocation/ldrop.ma".
+include "basic_2/relocation/ldrop_leq.ma".
(* DROPPING *****************************************************************)
| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H
#K2 #V2 #HK12 #HV12 #H destruct
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/
+ #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *)
+ /3 width=1 by lpx_sn_pair, monotonic_le_plus_l/
+ @leq_O2 normalize //
| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1
- /3 width=5 by ldrop_drop, lsuby_pair, lpx_sn_pair, ex3_intro/
+ /3 width=5 by ldrop_drop, leq_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=6 by ldrop_skip, lsuby_succ, lpx_sn_pair, ex3_intro/
+ /3 width=6 by ldrop_skip, leq_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/grammar/lenv_length.ma".
+include "basic_2/relocation/ldrop.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED SUBSTITUTION *******************)
#He destruct /2 width=1 by lsuby_zero, lsuby_pair/
qed.
-lemma lsuby_O1: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊑×[d, yinj 0] L2.
+lemma lsuby_O2: ∀L2,L1,d. |L2| ≤ |L1| → L1 ⊑×[d, yinj 0] L2.
#L2 elim L2 -L2 // #L2 #I2 #V2 #IHL2 * normalize
[ #d #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
| #L1 #I1 #V1 #d #H lapply (le_plus_to_le_r … H) -H #HL12
lemma lsuby_sym: ∀d,e,L1,L2. L1 ⊑×[d, e] L2 → |L1| = |L2| → L2 ⊑×[d, e] L1.
#d #e #L1 #L2 #H elim H -d -e -L1 -L2
[ #L1 #d #e #H >(length_inv_zero_dx … H) -L1 //
-| /2 width=1 by lsuby_O1/
+| /2 width=1 by lsuby_O2/
| #I1 #I2 #L1 #L2 #V #e #_ #IHL12 #H lapply (injective_plus_l … H)
/3 width=1 by lsuby_pair/
| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #H lapply (injective_plus_l … H)
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-.
+
+(* Properties on basic slicing **********************************************)
+
+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-.
}
]
[ { "strongly normalizing extended computation" * } {
- [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_cpxs" + "lsx_csx" * ]
+ [ "lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )" "lcosx_cpxs" * ]
+ [ "lsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_cpxs" + "lsx_csx" * ]
[ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ]
}
}
]
[ { "irreducible forms for context-sensitive extended reduction" * } {
- [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_append" + "cix_lift" * ]
+ [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ]
}
]
[ { "reducible forms for context-sensitive extended reduction" * } {
- [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_append" + "crx_lift" * ]
+ [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ]
}
]
[ { "normal forms for context-sensitive reduction" * } {
}
]
[ { "irreducible forms for context-sensitive reduction" * } {
- [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ]
+ [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ]
}
]
[ { "reducible forms for context-sensitive reduction" * } {
- [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ]
+ [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ]
}
]
}
[ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ]
}
]
+ [ { "local env. ref. for extended substitution" * } {
+ [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ]
+ }
+ ]
[ { "structural successor for closures" * } {
[ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ]
[ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" * ]
}
]
[ { "basic local env. slicing" * } {
- [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_lsuby" + "ldrop_ldrop" * ]
- }
- ]
- [ { "local env. ref. for extended substitution" * } {
- [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ]
+ [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_lpx_sn" + "ldrop_leq" + "ldrop_ldrop" * ]
}
]
[ { "basic term relocation" * } {
]
class "red"
[ { "grammar" * } {
+ [ { "equivalence for local environments" * } {
+ [ "leq ( ? ≃[?,?] ? )" "leq_leq" * ]
+ }
+ ]
[ { "pointwise extension of a relation" * } {
[ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ]
}
}
]
[ { "closures" * } {
- [ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?,?} )" * ]
+ [ "cl_weight ( ♯{?,?,?} )" "cl_restricted_weight ( ♯{?,?} )" * ]
}
]
[ { "internal syntax" * } {
lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
/3 width=1 by monotonic_le_minus_l/ qed.
+(* Note: this might interfere with nat.ma *)
+lemma monotonic_lt_pred: ∀m,n. m < n → O < m → pred m < pred n.
+#m #n #Hmn #Hm whd >(S_pred … Hm)
+@le_S_S_to_le >S_pred /2 width=3 by transitive_lt/
+qed.
+
lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
#H destruct
qed.
+(* Properties on predecessor ************************************************)
+
+lemma ylt_pred: ∀m,n. m < n → 0 < m → ⫰m < ⫰n.
+#m #n * -m -n
+/4 width=1 by ylt_inv_inj, ylt_inj, monotonic_lt_pred/
+qed.
+
(* Properties on successor **************************************************)
lemma ylt_O_succ: ∀n. 0 < ⫯n.
* //
qed.
+lemma yminus_pred: ∀n,m. 0 < m → 0 < n → ⫰m - ⫰n = m - n.
+* // #n *
+[ #m #Hm #Hn >yminus_inj >yminus_inj
+ /4 width=1 by ylt_inv_inj, minus_pred_pred, eq_f/
+| >yminus_Y_inj //
+]
+qed-.
+
(* Properties on successor **************************************************)
lemma yminus_succ: ∀n,m. ⫯m - ⫯n = m - n.
["?"; "¿"; "⸮"; ];
[":"; "⁝"; ];
["."; "•"; "◦"; ];
- ["#"; "♯"; "⋕"; "⌘"; ];
+ ["#"; "â\99¯"; "â\8b\95"; "⧤"; "â\8c\98"; ];
["-"; "÷"; "⊢"; "⊩"; ];
- ["="; "â\89\83"; "â\89\88"; "â\89\9d"; "â\89¡"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; ];
+ ["="; "â\89\9d"; "â\8a\9c"; "â\89¡"; "â\89\83"; "â\89\88"; "≅"; "≐"; "≑"; "≚"; "≙"; "⌆"; ];
["→"; "↦"; "⇝"; "⤞"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
["⇒"; "⤇"; "➾"; "⇨"; "➡"; "➤"; "➸"; "⇉"; "⥰"; ] ;
["^"; "↑"; ] ;
projects / helm.git / commitdiff