1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/multiple/lleq_ldrop.ma".
16 include "basic_2/reduction/lpx_ldrop.ma".
17 include "basic_2/computation/lsx.ma".
19 (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
21 (* Advanced properties ******************************************************)
23 lemma lsx_lref_free: ∀h,g,G,L,d,i. |L| ≤ i → G ⊢ ⬊*[h, g, #i, d] L.
24 #h #g #G #L1 #d #i #HL1 @lsx_intro
25 #L2 #HL12 #H elim H -H
26 /4 width=6 by lpx_fwd_length, lleq_free, le_repl_sn_conf_aux/
29 lemma lsx_lref_skip: ∀h,g,G,L,d,i. yinj i < d → G ⊢ ⬊*[h, g, #i, d] L.
30 #h #g #G #L1 #d #i #HL1 @lsx_intro
31 #L2 #HL12 #H elim H -H
32 /3 width=4 by lpx_fwd_length, lleq_skip/
35 (* Advanced forward lemmas **************************************************)
37 lemma lsx_fwd_lref_be: ∀h,g,I,G,L,d,i. d ≤ yinj i → G ⊢ ⬊*[h, g, #i, d] L →
38 ∀K,V. ⇩[i] L ≡ K.ⓑ{I}V → G ⊢ ⬊*[h, g, V, 0] K.
39 #h #g #I #G #L #d #i #Hdi #H @(lsx_ind … H) -L
40 #L1 #_ #IHL1 #K1 #V #HLK1 @lsx_intro
41 #K2 #HK12 #HnK12 lapply (ldrop_fwd_drop2 … HLK1)
42 #H2LK1 elim (ldrop_lpx_trans … H2LK1 … HK12) -H2LK1 -HK12
43 #L2 #HL12 #H2LK2 #H elim (leq_ldrop_conf_be … H … HLK1) -H /2 width=1 by ylt_inj/
44 #Y #_ #HLK2 lapply (ldrop_fwd_drop2 … HLK2)
45 #HY lapply (ldrop_mono … HY … H2LK2) -HY -H2LK2 #H destruct
46 /4 width=10 by lleq_inv_lref_ge/
49 (* Properties on relocation *************************************************)
51 lemma lsx_lift_le: ∀h,g,G,K,T,U,dt,d,e. dt ≤ yinj d →
52 ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, T, dt] K →
53 ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, U, dt] L.
54 #h #g #G #K #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -K
55 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
56 #L2 #HL12 #HnU elim (lpx_ldrop_conf … HLK1 … HL12) -HL12
57 /4 width=10 by lleq_lift_le/
60 lemma lsx_lift_ge: ∀h,g,G,K,T,U,dt,d,e. yinj d ≤ dt →
61 ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, T, dt] K →
62 ∀L. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, U, dt + e] L.
63 #h #g #G #K #T #U #dt #d #e #Hddt #HTU #H @(lsx_ind … H) -K
64 #K1 #_ #IHK1 #L1 #HLK1 @lsx_intro
65 #L2 #HL12 #HnU elim (lpx_ldrop_conf … HLK1 … HL12) -HL12
66 /4 width=9 by lleq_lift_ge/
69 (* Inversion lemmas on relocation *******************************************)
71 lemma lsx_inv_lift_le: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d →
72 ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L →
73 ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, T, dt] K.
74 #h #g #G #L #T #U #dt #d #e #Hdtd #HTU #H @(lsx_ind … H) -L
75 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
76 #K2 #HK12 #HnT elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
77 /4 width=10 by lleq_inv_lift_le/
80 lemma lsx_inv_lift_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e →
81 ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L →
82 ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, T, d] K.
83 #h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L
84 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
85 #K2 #HK12 #HnT elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
86 /4 width=11 by lleq_inv_lift_be/
89 lemma lsx_inv_lift_ge: ∀h,g,G,L,T,U,dt,d,e. yinj d + yinj e ≤ dt →
90 ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L →
91 ∀K. ⇩[Ⓕ, d, e] L ≡ K → G ⊢ ⬊*[h, g, T, dt-e] K.
92 #h #g #G #L #T #U #dt #d #e #Hdedt #HTU #H @(lsx_ind … H) -L
93 #L1 #_ #IHL1 #K1 #HLK1 @lsx_intro
94 #K2 #HK12 #HnT elim (ldrop_lpx_trans … HLK1 … HK12) -HK12
95 /4 width=9 by lleq_inv_lift_ge/