elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
@(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA
- /3 width=5 by lsubc_abbr, drops_trans, drops_skip, lifts_trans/
+ /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
/3 width=10 by drops_nil, lifts_nil/
| #H @(cp2 … H1RP … k) @(s1 … IHA) //
]
| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H
- elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
+ elim (lifts_inv_appls1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
lapply (s1 … IHB … HB) #HV0
@(s2 … IHA … (V0 @ V0s))
/3 width=14 by rp_liftsv_all, acp_lifts, cp0, lifts_simple_dx, conj/
| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H
- elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
- @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
+ @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_appls, lifts_flat, lifts_bind/
| #G #L #Vs #HVs #k #L0 #V0 #X #des #HB #HL0 #H
- elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct
>(lifts_inv_sort1 … HY) -Y
lapply (s1 … IHB … HB) #HV0
@(s4 … IHA … (V0 @ V0s)) /3 width=7 by rp_liftsv_all, conj/
| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
- elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
>(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
>(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
- @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/
+ @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_appls/
| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
- elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
+ elim (lifts_inv_appls1 … H) -H #V10s #Y #HV10s #HY #H destruct
elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
elim (lift_total V10 0 1) #V20 #HV120
elim (liftv_total 0 1 V10s) #V20s #HV120s
@(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/
@(HA … (des + 1)) /2 width=2 by drops_skip/
[ @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/
- | @lifts_applv //
+ | @lifts_appls //
elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
>(liftv_mono … HV12s … HV10s) -V1s //
]
| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
- elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
- @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/
+ @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_appls/
]
qed.
interpretation "evaluation for context-sensitive parallel reduction (term)"
'PRedEval G L T1 T2 = (cpre G L T1 T2).
-(* Basic_properties *********************************************************)
+(* Basic properties *********************************************************)
(* Basic_1: was just: nf2_sn3 *)
lemma csx_cpre: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄.
| #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12
lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2
- /5 width=5 by cprs_bind, cprs_flat_dx, cpr_cprs, lsubr_abst, ex2_3_intro, or3_intro1/
+ /5 width=5 by cprs_bind, cprs_flat_dx, cpr_cprs, lsubr_beta, ex2_3_intro, or3_intro1/
| #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
/5 width=10 by cprs_flat_sn, cprs_bind_dx, cprs_strap1, ex4_5_intro, or3_intro2/
]
interpretation "evaluation for context-sensitive extended parallel reduction (term)"
'PRedEval h g G L T1 T2 = (cpxe h g G L T1 T2).
-(* Basic_properties *********************************************************)
+(* Basic properties *********************************************************)
lemma csx_cpxe: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] 𝐍⦃T2⦄.
#h #g #G #L #T1 #H @(csx_ind … H) -T1
| #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
lapply (cpxs_strap1 … HV10 … HV02) -V0 #HV12
lapply (lsubr_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2
- /5 width=5 by cpxs_bind, cpxs_flat_dx, cpx_cpxs, lsubr_abst, ex2_3_intro, or3_intro1/
+ /5 width=5 by cpxs_bind, cpxs_flat_dx, cpx_cpxs, lsubr_beta, ex2_3_intro, or3_intro1/
| #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
/5 width=10 by cpxs_flat_sn, cpxs_bind_dx, cpxs_strap1, ex4_5_intro, or3_intro2/
]
| #b #W0 #T0 #HT0 #HU
elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
- /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_abst, or_intror/
+ /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/
| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
]
[ -HT1 #V0 #Y #HLV0 #H #H0 destruct
elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct
@IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2
- lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/
+ lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_beta/
| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02
- /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/
+ /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_beta/
| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
]
qed-.
(* Advanced properties ******************************************************)
(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
+lemma csx_appls_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T.
#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
elim (csxv_inv_cons … H) -H #HV #HVs
-@csx_appl_simple_tstc /2 width=1 by applv_simple/ -IHV -HV -HVs
+@csx_appl_simple_tstc /2 width=1 by appls_simple/ -IHV -HV -HVs
#X #H #H0
lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H
elim (H0) -H0 //
qed.
-lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
+lemma csx_appls_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
#h #g #G #L #k elim (deg_total h g k)
-#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ]
+#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_appls_cnx, cnx_sort, simple_atom/ ]
#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
#Hkl #Vs elim Vs -Vs /2 width=1 by/
#V #Vs #IHVs #HVVs
elim (csxv_inv_cons … HVVs) #HV #HVs
-@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs
+@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_atom/ -IHVs -HV -HVs
#X #H #H0
elim (cpxs_fwd_sort_vector … H) -H #H
[ elim H0 -H0 //
qed.
(* Basic_1: was just: sn3_appls_beta *)
-lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
+lemma csx_appls_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T.
#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
#V0 #Vs #IHV #V #W #T #H1T
lapply (csx_fwd_pair_sn … H1T) #HV0
lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
+@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_flat/ -IHV -HV0 -H2T
#X #H #H0
elim (cpxs_fwd_beta_vector … H) -H #H
[ -H1T elim H0 -H0 //
]
qed.
-lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
+lemma csx_appls_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
∀V2. ⇧[0, i + 1] V1 ≡ V2 →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
| #V #Vs #IHV #H1T
lapply (csx_fwd_pair_sn … H1T) #HV
lapply (csx_fwd_flat_dx … H1T) #H2T
- @csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T
+ @csx_appl_simple_tstc /2 width=1 by appls_simple, simple_atom/ -IHV -HV -H2T
#X #H #H0
elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
[ -H1T elim H0 -H0 //
qed.
(* Basic_1: was just: sn3_appls_abbr *)
-lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+lemma csx_appls_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T.
#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/
qed.
(* Basic_1: was just: sn3_appls_cast *)
-lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
+lemma csx_appls_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T.
#h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/
#V #Vs #IHV #W #T #H1W #H1T
lapply (csx_fwd_pair_sn … H1W) #HV
lapply (csx_fwd_flat_dx … H1W) #H2W
lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T
+@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_flat/ -IHV -HV -H2W -H2T
#X #H #H0
elim (cpxs_fwd_cast_vector … H) -H #H
[ -H1W -H1T elim H0 -H0 //
theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T).
#h #g @mk_acr //
[ /2 width=8 by csx_lift/
-| /3 width=1 by csx_applv_cnx/
-|3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/
-| /2 width=7 by csx_applv_delta/
+| /3 width=1 by csx_appls_cnx/
+|3,4,7: /2 width=1 by csx_appls_beta, csx_appls_sort, csx_appls_cast/
+| /2 width=7 by csx_appls_delta/
| #G #L #V1s #V2s #HV12s #a #V #T #H #HV
- @(csx_applv_theta … HV12s) -HV12s
+ @(csx_appls_theta … HV12s) -HV12s
@csx_abbr //
]
qed.
(* Basic forward lemmas *****************************************************)
-lemma csx_fwd_applv: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T →
+lemma csx_fwd_appls: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T →
⦃G, L⦄ ⊢ ⬊*[h, g] Vs ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] T.
#h #g #G #L #T #Vs elim Vs -Vs /2 width=1/
#V #Vs #IHVs #HVs
(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
-(* Advanced propreties on context-senstive extended bormalizing terms *******)
+(* Advanced propreties on context-sensitive extended normalizing terms *******)
lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥[h, g] T2.
(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
-(* Properies on local environment slicing ***********************************)
+(* Properties on local environment slicing ***********************************)
lemma lprs_drop_conf: ∀G. dropable_sn (lprs G).
/3 width=3 by dropable_sn_TC, lpr_drop_conf/ qed-.
(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************)
-(* Properies on local environment slicing ***********************************)
+(* Properties on local environment slicing ***********************************)
lemma lpxs_drop_conf: ∀h,g,G. dropable_sn (lpxs h g G).
/3 width=3 by dropable_sn_TC, lpx_drop_conf/ qed-.
inductive lsubc (RP) (G): relation lenv ≝
| lsubc_atom: lsubc RP G (⋆) (⋆)
| lsubc_pair: ∀I,L1,L2,V. lsubc RP G L1 L2 → lsubc RP G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubc_abbr: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A →
+| lsubc_beta: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A →
lsubc RP G L1 L2 → lsubc RP G (L1. ⓓⓝW.V) (L2.ⓛW)
.
| #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #s #e #H
elim (drop_inv_O1_pair1 … H) -H * #He #H destruct
[ elim (IHL12 L2 s 0) -IHL12 // #X #H <(drop_inv_O2 … H) -H
- /3 width=8 by lsubc_abbr, drop_pair, ex2_intro/
+ /3 width=8 by lsubc_beta, drop_pair, ex2_intro/
| elim (IHL12 … H) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
]
]
elim (lsubc_inv_pair1 … H) -H *
[ #K1 #HLK1 #H destruct /3 width=3 by lsubc_pair, drop_pair, ex2_intro/
| #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct
- /3 width=4 by lsubc_abbr, drop_pair, ex2_intro/
+ /3 width=4 by lsubc_beta, drop_pair, ex2_intro/
]
| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12
elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, drop_drop, ex2_intro/
lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
lapply (s0 … HA … HV2 … HLK1 HV3) -HV2
lapply (s0 … HA … H1W2 … HLK1 HW23) -H1W2
- /4 width=11 by lsubc_abbr, aaa_lift, drop_skip, ex2_intro/
+ /4 width=11 by lsubc_beta, aaa_lift, drop_skip, ex2_intro/
]
]
qed-.
(* properties concerning lenv refinement for atomic arity assignment ********)
lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
- â\88\80G,L1,L2. G â\8a¢ L1 â\81\9dâ«\83 L2 → G ⊢ L1 ⫃[RP] L2.
+ â\88\80G,L1,L2. G â\8a¢ L1 â«\83â\81\9d L2 → G ⊢ L1 ⫃[RP] L2.
#RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4/
qed.
| lsubsv_atom: lsubsv h g G (⋆) (⋆)
| lsubsv_pair: ∀I,L1,L2,V. lsubsv h g G L1 L2 →
lsubsv h g G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubsv_abbr: ∀L1,L2,W,V,l. ⦃G, L1⦄ ⊢ W ¡[h, g] → ⦃G, L1⦄ ⊢ V ¡[h, g] →
+| lsubsv_beta: ∀L1,L2,W,V,l. ⦃G, L1⦄ ⊢ W ¡[h, g] → ⦃G, L1⦄ ⊢ V ¡[h, g] →
scast h g l G L1 V W → ⦃G, L2⦄ ⊢ W ¡[h, g] →
⦃G, L1⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] l →
lsubsv h g G L1 L2 → lsubsv h g G (L1.ⓓⓝW.V) (L2.ⓛW)
(* Basic inversion lemmas ***************************************************)
-fact lsubsv_inv_atom1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → L1 = ⋆ → L2 = ⋆.
+fact lsubsv_inv_atom1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → L1 = ⋆ → L2 = ⋆.
#h #g #G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
]
qed-.
-lemma lsubsv_inv_atom1: ∀h,g,G,L2. G ⊢ ⋆ ¡⫃[h, g] L2 → L2 = ⋆.
+lemma lsubsv_inv_atom1: ∀h,g,G,L2. G ⊢ ⋆ ⫃¡[h, g] L2 → L2 = ⋆.
/2 width=6 by lsubsv_inv_atom1_aux/ qed-.
-fact lsubsv_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 →
+fact lsubsv_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 →
∀I,K1,X. L1 = K1.ⓑ{I}X →
- (∃∃K2. G ⊢ K1 ¡⫃[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
+ (∃∃K2. G ⊢ K1 ⫃¡[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] &
scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] &
⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G ⊢ K1 ¡⫃[h, g] K2 &
+ G ⊢ K1 ⫃¡[h, g] K2 &
I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
#h #g #G #L1 #L2 * -L1 -L2
[ #J #K1 #X #H destruct
]
qed-.
-lemma lsubsv_inv_pair1: ∀h,g,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ¡⫃[h, g] L2 →
- (∃∃K2. G ⊢ K1 ¡⫃[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
+lemma lsubsv_inv_pair1: ∀h,g,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃¡[h, g] L2 →
+ (∃∃K2. G ⊢ K1 ⫃¡[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] &
scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] &
⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G ⊢ K1 ¡⫃[h, g] K2 &
+ G ⊢ K1 ⫃¡[h, g] K2 &
I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
/2 width=3 by lsubsv_inv_pair1_aux/ qed-.
-fact lsubsv_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → L2 = ⋆ → L1 = ⋆.
+fact lsubsv_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → L2 = ⋆ → L1 = ⋆.
#h #g #G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
]
qed-.
-lemma lsubsv_inv_atom2: ∀h,g,G,L1. G ⊢ L1 ¡⫃[h, g] ⋆ → L1 = ⋆.
+lemma lsubsv_inv_atom2: ∀h,g,G,L1. G ⊢ L1 ⫃¡[h, g] ⋆ → L1 = ⋆.
/2 width=6 by lsubsv_inv_atom2_aux/ qed-.
-fact lsubsv_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 →
+fact lsubsv_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 →
∀I,K2,W. L2 = K2.ⓑ{I}W →
- (∃∃K1. G ⊢ K1 ¡⫃[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
+ (∃∃K1. G ⊢ K1 ⫃¡[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
∃∃K1,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] &
scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] &
⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G ⊢ K1 ¡⫃[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
+ G ⊢ K1 ⫃¡[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
#h #g #G #L1 #L2 * -L1 -L2
[ #J #K2 #U #H destruct
| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3/
]
qed-.
-lemma lsubsv_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ¡⫃[h, g] K2.ⓑ{I}W →
- (∃∃K1. G ⊢ K1 ¡⫃[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
+lemma lsubsv_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ⫃¡[h, g] K2.ⓑ{I}W →
+ (∃∃K1. G ⊢ K1 ⫃¡[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
∃∃K1,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] &
scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] &
⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G ⊢ K1 ¡⫃[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
+ G ⊢ K1 ⫃¡[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
/2 width=3 by lsubsv_inv_pair2_aux/ qed-.
-(* Basic_forward lemmas *****************************************************)
+(* Basic forward lemmas *****************************************************)
-lemma lsubsv_fwd_lsubr: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → L1 ⫃ L2.
+lemma lsubsv_fwd_lsubr: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → L1 ⫃ L2.
#h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
qed-.
(* Basic properties *********************************************************)
-lemma lsubsv_refl: ∀h,g,G,L. G ⊢ L ¡⫃[h, g] L.
+lemma lsubsv_refl: ∀h,g,G,L. G ⊢ L ⫃¡[h, g] L.
#h #g #G #L elim L -L // /2 width=1/
qed.
-lemma lsubsv_cprs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 →
+lemma lsubsv_cprs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 →
∀T1,T2. ⦃G, L2⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ T1 ➡* T2.
/3 width=6 by lsubsv_fwd_lsubr, lsubr_cprs_trans/
qed-.
(* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_drop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 →
+lemma lsubsv_drop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 →
∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 →
- ∃∃K2. G ⊢ K1 ¡⫃[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2.
+ ∃∃K2. G ⊢ K1 ⫃¡[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2.
#h #g #G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
| #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H
elim (drop_inv_O1_pair1 … H) -H * #He #HLK1
[ destruct
elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, drop_pair, ex2_intro/
+ <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
| elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
]
]
qed-.
(* Note: the constant 0 cannot be generalized *)
-lemma lsubsv_drop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 →
+lemma lsubsv_drop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 →
∀K2,s, e. ⇩[s, 0, e] L2 ≡ K2 →
- ∃∃K1. G ⊢ K1 ¡⫃[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1.
+ ∃∃K1. G ⊢ K1 ⫃¡[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1.
#h #g #G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
| #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H
elim (drop_inv_O1_pair1 … H) -H * #He #HLK2
[ destruct
elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, drop_pair, ex2_intro/
+ <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/
| elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
]
]
(* Properties on context-sensitive parallel equivalence for terms ***********)
-lemma lsubsv_cpcs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 →
+lemma lsubsv_cpcs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 →
∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2.
/3 width=6 by lsubsv_fwd_lsubr, lsubr_cpcs_trans/
qed-.
(* Properties on decomposed extended parallel computation on terms **********)
lemma lsubsv_cpds_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g] T2 →
- ∀L1. G ⊢ L1 ¡⫃[h, g] L2 →
+ ∀L1. G ⊢ L1 ⫃¡[h, g] L2 →
∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] T & ⦃G, L1⦄ ⊢ T2 ➡* T.
#h #g #G #L2 #T1 #T2 * #T #l1 #l2 #Hl21 #Hl1 #HT1 #HT2 #L1 #HL12
lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2
lemma lsubsv_lstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, l1] U2 →
∀l2. l1 ≤ l2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l2 →
- ∀L1. G ⊢ L1 ¡⫃[h, g] L2 →
+ ∀L1. G ⊢ L1 ⫃¡[h, g] L2 →
∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, l1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
#h #g #G #L2 #T #U #l1 #H @(lstas_ind_alt … H) -G -L2 -T -U -l1
[1,2: /2 width=3 by ex2_intro/
lemma lsubsv_sta_trans: ∀h,g,G,L2,T,U2. ⦃G, L2⦄ ⊢ T •[h] U2 →
∀l. ⦃G, L2⦄ ⊢ T ▪[h, g] l+1 →
- ∀L1. G ⊢ L1 ¡⫃[h, g] L2 →
+ ∀L1. G ⊢ L1 ⫃¡[h, g] L2 →
∃∃U1. ⦃G, L1⦄ ⊢ T •[h] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2.
#h #g #G #L2 #T #U2 #H #l #HTl #L1 #HL12
elim (lsubsv_lstas_trans … U2 1 … HTl … HL12)
(* Forward lemmas on lenv refinement for atomic arity assignment ************)
-lemma lsubsv_fwd_lsuba: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → G ⊢ L1 ⁝⫃ L2.
+lemma lsubsv_fwd_lsuba: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → G ⊢ L1 ⫃⁝ L2.
#h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
#L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #_ #_ #IHL12
lapply (snv_scast … HV H1W HVW H1l) -HV -H1W -HVW -H1l #HV
(* Forward lemmas on lenv refinement for degree assignment ******************)
-lemma lsubsv_fwd_lsubd: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → G ⊢ L1 ▪⫃[h, g] L2.
+lemma lsubsv_fwd_lsubd: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → G ⊢ L1 ⫃▪[h, g] L2.
#h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=3/
qed-.
(* Properties concerning stratified native validity *************************)
lemma lsubsv_snv_trans: ∀h,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] →
- ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g].
+ ∀L1. G ⊢ L1 ⫃¡[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g].
#h #g #G #L2 #T #H elim H -G -L2 -T //
[ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12
elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fqup_fpbg/ ] #Hl0
lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fqup_fpbg/ -HW
lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2
- /4 width=6 by da_bind, lsubd_da_trans, lsubd_abbr/
+ /4 width=6 by da_bind, lsubd_da_trans, lsubd_beta/
| #b #V #V2 #W #W2 #U1 #U2 #HV1 #HV2 #HW2 #HU12 #H1 #H2 destruct -IH3 -IH2 -V -W0 -T0 -l0 -HV1 -HVW1
elim (snv_inv_bind … HT1) -HT1 #_
lapply (da_inv_bind … Hl) -Hl
lapply (snv_sta_aux … IH4 … HlV2 … HV2W3)
/3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW3
lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/
- @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
+ @(lsubsv_beta … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20
lapply (lstas_sta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
@(lstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
[ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_sta_fpbs/
@(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/
/4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/
| -U3
- @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/
+ @(lsubsv_beta … l) /3 width=7 by fqup_fpbg/
#W #W0 #l0 #Hl0 #HV2W #HW30
lapply (lstas_sta_conf_pos … HV2W4 … HV2W) -HV2W #HW4W
@(lstas_cpcs_lpr_aux … IH3 IH2 IH1 … Hl0 … HW4W … Hl0 … HW30 … HW43) //
| APair: aarity → aarity → aarity (* binary aarity construction *)
.
-interpretation "aarity construction (atomic)"
+interpretation "atomic arity construction (atomic)"
'Item0 = AAtom.
-interpretation "aarity construction (binary)"
+interpretation "atomic arity construction (binary)"
'SnItem2 A1 A2 = (APair A1 A2).
(* Basic inversion lemmas ***************************************************)
#A #B elim B -B
[ #H destruct
| #Y #X #IHY #_ #H destruct
- -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
+ -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destructed equality is not erased *)
/2 width=1/
]
qed-.
#B #A elim A -A
[ #H destruct
| #Y #X #_ #IHX #H destruct
- -H (**) (* destruct: the destucted equality is not erased *)
+ -H (**) (* destruct: the destructed equality is not erased *)
/2 width=1/
]
qed-.
elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/
qed-.
-(* Basic_eliminators ********************************************************)
+(* Basic eliminators ********************************************************)
(* Basic_1: was: c_tail_ind *)
lemma lenv_ind_alt: ∀R:predicate lenv.
(**************************************************************************)
include "ground_2/lib/list.ma".
-include "basic_2/notation/functions/snapplv_2.ma".
+include "basic_2/notation/functions/snappls_2.ma".
include "basic_2/grammar/term_simple.ma".
(* TERMS ********************************************************************)
-let rec applv Vs T on Vs ≝
+let rec appls Vs T on Vs ≝
match Vs with
[ nil ⇒ T
- | cons hd tl ⇒ ⓐhd. (applv tl T)
+ | cons hd tl ⇒ ⓐhd. (appls tl T)
].
-interpretation "application o vevtor (term)"
- 'SnApplV Vs T = (applv Vs T).
+interpretation "application to vector (term)"
+ 'SnApplStar Vs T = (appls Vs T).
(* properties concerning simple terms ***************************************)
-lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄.
+lemma appls_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄.
#T * //
qed.
@(cpys_subst … HLK … HU12) >yminus_Y_inj //
qed.
-(* Advanced inverion lemmas *************************************************)
+(* Advanced inversion lemmas *************************************************)
lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*[d, e] T2 →
T2 = ⓪{I} ∨
"lazy equivalence (closure)"
'LazyEq d G1 L1 T1 G2 L2 T2 = (fleq d G1 L1 T1 G2 L2 T2).
-(* Basic_properties *********************************************************)
+(* Basic properties *********************************************************)
lemma fleq_refl: ∀d. tri_reflexive … (fleq d).
/2 width=1 by fleq_intro/ qed.
(* Basic inversion lemmas ***************************************************)
(* Basic_1: was: lifts1_flat (left to right) *)
-lemma lifts_inv_applv1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 →
+lemma lifts_inv_appls1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 →
∃∃V2s,U2. ⇧*[des] V1s ≡ V2s & ⇧*[des] U1 ≡ U2 &
T2 = Ⓐ V2s. U2.
#V1s elim V1s -V1s normalize
(* Basic properties *********************************************************)
(* Basic_1: was: lifts1_flat (right to left) *)
-lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s →
+lemma lifts_appls: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s →
∀T1,T2. ⇧*[des] T1 ≡ T2 →
⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
#V1s #V2s #des #H elim H -V1s -V2s /3 width=1 by lifts_flat/
L1 ≡[ⓑ{a,I}V.T, 0] L2.
/2 width=1 by llpx_sn_bind_O/ qed-.
-(* Advancded properties on lazy pointwise exyensions ************************)
+(* Advanceded properties on lazy pointwise extensions ************************)
lemma llpx_sn_lrefl: ∀R. (∀L. reflexive … (R L)) →
∀L1,L2,T,d. L1 ≡[T, d] L2 → llpx_sn R d T L1 L2.
(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
-(* Properties on poinwise union for local environments **********************)
+(* Properties on pointwise union for local environments **********************)
lemma llpx_sn_llor_dx: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) →
∀L1,L2,T,d. llpx_sn R d T L1 L2 → ∀L. L1 ⩖[T, d] L2 ≡ L → L2 ≡[T, d] L.
#R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/
qed-.
-(* Basic_properties *********************************************************)
+(* Basic properties *********************************************************)
lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,d. llpx_sn R d T L L.
#R #HR #T #L @(f2_ind … rfw … L T) -L -T
(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
-(* Inversion lemmas on poinwise union for local environments ****************)
+(* Inversion lemmas on pointwise union for local environments ****************)
lemma llpx_sn_llor_fwd_sn: ∀R. (∀L. reflexive … (R L)) →
∀L1,L2,T,d. llpx_sn R d T 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( Ⓐ term 55 T1 . break term 55 T )"
+ non associative with precedence 55
+ for @{ 'SnApplStar $T1 $T }.
+++ /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( Ⓐ term 55 T1 . break term 55 T )"
- non associative with precedence 55
- for @{ 'SnApplV $T1 $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G â\8a¢ break term 46 L1 â\81\9d â«\83 break term 46 L2 )"
+notation "hvbox( G â\8a¢ break term 46 L1 â«\83 â\81\9d break term 46 L2 )"
non associative with precedence 45
for @{ 'LRSubEqA $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G â\8a¢ break term 46 L1 â\96ª â«\83 break [ term 46 h, break term 46 g ] break term 46 L2 )"
+notation "hvbox( G â\8a¢ break term 46 L1 â«\83 â\96ª break [ term 46 h, break term 46 g ] break term 46 L2 )"
non associative with precedence 45
for @{ 'LRSubEqD $h $g $G $L1 $L2 }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( G ⊢ break term 46 L1 ¡ ⫃ break [ term 46 h, break term 46 g ] break term 46 L2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ break [ term 46 h, break term 46 g ] break term 46 L2 )"
non associative with precedence 45
for @{ 'LRSubEqV $h $g $G $L1 $L2 }.
| #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
elim (lsubr_fwd_drop2_abbr … HL12 … HLK1) -L1 *
/3 width=6 by cpr_delta/
-|3,7: /4 width=1 by lsubr_bind, cpr_bind, cpr_beta/
+|3,7: /4 width=1 by lsubr_pair, cpr_bind, cpr_beta/
|4,6: /3 width=1 by cpr_flat, cpr_eps/
-|5,8: /4 width=3 by lsubr_bind, cpr_zeta, cpr_theta/
+|5,8: /4 width=3 by lsubr_pair, cpr_zeta, cpr_theta/
]
qed-.
[ //
| /2 width=2 by cpx_st/
| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsubr_fwd_drop2_bind … HL12 … HLK1) -HL12 -HLK1 *
+ elim (lsubr_fwd_drop2_pair … HL12 … HLK1) -HL12 -HLK1 *
/4 width=7 by cpx_delta, cpx_ct/
-|4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_bind/
+|4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_pair/
|5,7,8: /3 width=1 by cpx_flat, cpx_eps, cpx_ct/
-|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsubr_bind/
+|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsubr_pair/
]
qed-.
(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
-(* Properies on local environment slicing ***********************************)
+(* Properties on local environment slicing ***********************************)
(* Basic_1: includes: wcpr0_drop *)
lemma lpr_drop_conf: ∀G. dropable_sn (lpr G).
elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ #W #HW1 #HW2
elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
-lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/ (**) (* full auto not tried *)
+lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ (**) (* full auto not tried *)
/4 width=5 by cpr_bind, cpr_flat, cpr_beta, ex2_intro/
qed-.
elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2
elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
-lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_abst/
-lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/
+lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/
+lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/
/4 width=5 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
qed-.
lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
- /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/
+ /5 width=6 by lsuba_aaa_trans, lsuba_beta, aaa_abbr, aaa_cast/
| #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by drop_drop/ #HV2
lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H
(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-(* Properies on local environment slicing ***********************************)
+(* Properties on local environment slicing ***********************************)
lemma lpx_drop_conf: ∀h,g,G. dropable_sn (lpx h g G).
/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
inductive lsuba (G:genv): relation lenv ≝
| lsuba_atom: lsuba G (⋆) (⋆)
| lsuba_pair: ∀I,L1,L2,V. lsuba G L1 L2 → lsuba G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsuba_abbr: ∀L1,L2,W,V,A. ⦃G, L1⦄ ⊢ ⓝW.V ⁝ A → ⦃G, L2⦄ ⊢ W ⁝ A →
+| lsuba_beta: ∀L1,L2,W,V,A. ⦃G, L1⦄ ⊢ ⓝW.V ⁝ A → ⦃G, L2⦄ ⊢ W ⁝ A →
lsuba G L1 L2 → lsuba G (L1.ⓓⓝW.V) (L2.ⓛW)
.
interpretation
- "local environment refinement (atomic arity assigment)"
+ "local environment refinement (atomic arity assignment)"
'LRSubEqA G L1 L2 = (lsuba G L1 L2).
(* Basic inversion lemmas ***************************************************)
-fact lsuba_inv_atom1_aux: â\88\80G,L1,L2. G â\8a¢ L1 â\81\9dâ«\83 L2 → L1 = ⋆ → L2 = ⋆.
+fact lsuba_inv_atom1_aux: â\88\80G,L1,L2. G â\8a¢ L1 â«\83â\81\9d L2 → L1 = ⋆ → L2 = ⋆.
#G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
]
qed-.
-lemma lsuba_inv_atom1: â\88\80G,L2. G â\8a¢ â\8b\86 â\81\9dâ«\83 L2 → L2 = ⋆.
+lemma lsuba_inv_atom1: â\88\80G,L2. G â\8a¢ â\8b\86 â«\83â\81\9d L2 → L2 = ⋆.
/2 width=4 by lsuba_inv_atom1_aux/ qed-.
-fact lsuba_inv_pair1_aux: â\88\80G,L1,L2. G â\8a¢ L1 â\81\9dâ«\83 L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
- (â\88\83â\88\83K2. G â\8a¢ K1 â\81\9dâ«\83 K2 & L2 = K2.ⓑ{I}X) ∨
+fact lsuba_inv_pair1_aux: â\88\80G,L1,L2. G â\8a¢ L1 â«\83â\81\9d L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+ (â\88\83â\88\83K2. G â\8a¢ K1 â«\83â\81\9d K2 & L2 = K2.ⓑ{I}X) ∨
∃∃K2,W,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A &
- G â\8a¢ K1 â\81\9dâ«\83 K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+ G â\8a¢ K1 â«\83â\81\9d K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
#G #L1 #L2 * -L1 -L2
[ #J #K1 #X #H destruct
| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by ex2_intro, or_introl/
]
qed-.
-lemma lsuba_inv_pair1: â\88\80I,G,K1,L2,X. G â\8a¢ K1.â\93\91{I}X â\81\9dâ«\83 L2 →
- (â\88\83â\88\83K2. G â\8a¢ K1 â\81\9dâ«\83 K2 & L2 = K2.ⓑ{I}X) ∨
- â\88\83â\88\83K2,W,V,A. â¦\83G, K1â¦\84 â\8a¢ â\93\9dW.V â\81\9d A & â¦\83G, K2â¦\84 â\8a¢ W â\81\9d A & G â\8a¢ K1 â\81\9dâ«\83 K2 &
+lemma lsuba_inv_pair1: â\88\80I,G,K1,L2,X. G â\8a¢ K1.â\93\91{I}X â«\83â\81\9d L2 →
+ (â\88\83â\88\83K2. G â\8a¢ K1 â«\83â\81\9d K2 & L2 = K2.ⓑ{I}X) ∨
+ â\88\83â\88\83K2,W,V,A. â¦\83G, K1â¦\84 â\8a¢ â\93\9dW.V â\81\9d A & â¦\83G, K2â¦\84 â\8a¢ W â\81\9d A & G â\8a¢ K1 â«\83â\81\9d K2 &
I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
/2 width=3 by lsuba_inv_pair1_aux/ qed-.
-fact lsuba_inv_atom2_aux: â\88\80G,L1,L2. G â\8a¢ L1 â\81\9dâ«\83 L2 → L2 = ⋆ → L1 = ⋆.
+fact lsuba_inv_atom2_aux: â\88\80G,L1,L2. G â\8a¢ L1 â«\83â\81\9d L2 → L2 = ⋆ → L1 = ⋆.
#G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
]
qed-.
-lemma lsubc_inv_atom2: â\88\80G,L1. G â\8a¢ L1 â\81\9dâ«\83 ⋆ → L1 = ⋆.
+lemma lsubc_inv_atom2: â\88\80G,L1. G â\8a¢ L1 â«\83â\81\9d ⋆ → L1 = ⋆.
/2 width=4 by lsuba_inv_atom2_aux/ qed-.
-fact lsuba_inv_pair2_aux: â\88\80G,L1,L2. G â\8a¢ L1 â\81\9dâ«\83 L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →
- (â\88\83â\88\83K1. G â\8a¢ K1 â\81\9dâ«\83 K2 & L1 = K1.ⓑ{I}W) ∨
+fact lsuba_inv_pair2_aux: â\88\80G,L1,L2. G â\8a¢ L1 â«\83â\81\9d L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →
+ (â\88\83â\88\83K1. G â\8a¢ K1 â«\83â\81\9d K2 & L1 = K1.ⓑ{I}W) ∨
∃∃K1,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A &
- G â\8a¢ K1 â\81\9dâ«\83 K2 & I = Abst & L1 = K1.ⓓⓝW.V.
+ G â\8a¢ K1 â«\83â\81\9d K2 & I = Abst & L1 = K1.ⓓⓝW.V.
#G #L1 #L2 * -L1 -L2
[ #J #K2 #U #H destruct
| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3 by ex2_intro, or_introl/
]
qed-.
-lemma lsuba_inv_pair2: â\88\80I,G,L1,K2,W. G â\8a¢ L1 â\81\9dâ«\83 K2.ⓑ{I}W →
- (â\88\83â\88\83K1. G â\8a¢ K1 â\81\9dâ«\83 K2 & L1 = K1.ⓑ{I}W) ∨
- â\88\83â\88\83K1,V,A. â¦\83G, K1â¦\84 â\8a¢ â\93\9dW.V â\81\9d A & â¦\83G, K2â¦\84 â\8a¢ W â\81\9d A & G â\8a¢ K1 â\81\9dâ«\83 K2 &
+lemma lsuba_inv_pair2: â\88\80I,G,L1,K2,W. G â\8a¢ L1 â«\83â\81\9d K2.ⓑ{I}W →
+ (â\88\83â\88\83K1. G â\8a¢ K1 â«\83â\81\9d K2 & L1 = K1.ⓑ{I}W) ∨
+ â\88\83â\88\83K1,V,A. â¦\83G, K1â¦\84 â\8a¢ â\93\9dW.V â\81\9d A & â¦\83G, K2â¦\84 â\8a¢ W â\81\9d A & G â\8a¢ K1 â«\83â\81\9d K2 &
I = Abst & L1 = K1.ⓓⓝW.V.
/2 width=3 by lsuba_inv_pair2_aux/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma lsuba_fwd_lsubr: â\88\80G,L1,L2. G â\8a¢ L1 â\81\9dâ«\83 L2 → L1 ⫃ L2.
-#G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_abst/
+lemma lsuba_fwd_lsubr: â\88\80G,L1,L2. G â\8a¢ L1 â«\83â\81\9d L2 → L1 ⫃ L2.
+#G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
qed-.
(* Basic properties *********************************************************)
-lemma lsuba_refl: â\88\80G,L. G â\8a¢ L â\81\9dâ«\83 L.
+lemma lsuba_refl: â\88\80G,L. G â\8a¢ L â«\83â\81\9d L.
#G #L elim L -L /2 width=1 by lsuba_atom, lsuba_pair/
qed.
(* Note: the constant 0 cannot be generalized *)
-lemma lsuba_drop_O1_conf: â\88\80G,L1,L2. G â\8a¢ L1 â\81\9dâ«\83 L2 → ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 →
- â\88\83â\88\83K2. G â\8a¢ K1 â\81\9dâ«\83 K2 & ⇩[s, 0, e] L2 ≡ K2.
+lemma lsuba_drop_O1_conf: â\88\80G,L1,L2. G â\8a¢ L1 â«\83â\81\9d L2 → ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 →
+ â\88\83â\88\83K2. G â\8a¢ K1 â«\83â\81\9d K2 & ⇩[s, 0, e] L2 ≡ K2.
#G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
| #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H
elim (drop_inv_O1_pair1 … H) -H * #He #HLK1
[ destruct
elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_abbr, drop_pair, ex2_intro/
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/
| elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
]
]
qed-.
(* Note: the constant 0 cannot be generalized *)
-lemma lsuba_drop_O1_trans: â\88\80G,L1,L2. G â\8a¢ L1 â\81\9dâ«\83 L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 →
- â\88\83â\88\83K1. G â\8a¢ K1 â\81\9dâ«\83 K2 & ⇩[s, 0, e] L1 ≡ K1.
+lemma lsuba_drop_O1_trans: â\88\80G,L1,L2. G â\8a¢ L1 â«\83â\81\9d L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 →
+ â\88\83â\88\83K1. G â\8a¢ K1 â«\83â\81\9d K2 & ⇩[s, 0, e] L1 ≡ K1.
#G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
| #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H
elim (drop_inv_O1_pair1 … H) -H * #He #HLK2
[ destruct
elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_abbr, drop_pair, ex2_intro/
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/
| elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
]
]
(* Properties concerning atomic arity assignment ****************************)
lemma lsuba_aaa_conf: ∀G,L1,V,A. ⦃G, L1⦄ ⊢ V ⁝ A →
- â\88\80L2. G â\8a¢ L1 â\81\9dâ«\83 L2 → ⦃G, L2⦄ ⊢ V ⁝ A.
+ â\88\80L2. G â\8a¢ L1 â«\83â\81\9d L2 → ⦃G, L2⦄ ⊢ V ⁝ A.
#G #L1 #V #A #H elim H -G -L1 -V -A
[ //
| #I #G #L1 #K1 #V #A #i #HLK1 #HV #IHV #L2 #HL12
qed-.
lemma lsuba_aaa_trans: ∀G,L2,V,A. ⦃G, L2⦄ ⊢ V ⁝ A →
- â\88\80L1. G â\8a¢ L1 â\81\9dâ«\83 L2 → ⦃G, L1⦄ ⊢ V ⁝ A.
+ â\88\80L1. G â\8a¢ L1 â«\83â\81\9d L2 → ⦃G, L1⦄ ⊢ V ⁝ A.
#G #L2 #V #A #H elim H -G -L2 -V -A
[ //
| #I #G #L2 #K2 #V #A #i #HLK2 #H1V #IHV #L1 #HL12
(* Main properties **********************************************************)
-theorem lsuba_trans: â\88\80G,L1,L. G â\8a¢ L1 â\81\9dâ«\83 L â\86\92 â\88\80L2. G â\8a¢ L â\81\9dâ«\83 L2 â\86\92 G â\8a¢ L1 â\81\9dâ«\83 L2.
+theorem lsuba_trans: â\88\80G,L1,L. G â\8a¢ L1 â«\83â\81\9d L â\86\92 â\88\80L2. G â\8a¢ L â«\83â\81\9d L2 â\86\92 G â\8a¢ L1 â«\83â\81\9d L2.
#G #L1 #L #H elim H -L1 -L
[ #X #H >(lsuba_inv_atom1 … H) -H //
| #I #L1 #L #Y #HL1 #IHL1 #X #H
elim (lsuba_inv_pair1 … H) -H * #L2
[ #HL2 #H destruct /3 width=1/
| #W #V #A #HV #HW #HL2 #H1 #H2 #H3 destruct
- /3 width=3 by lsuba_abbr, lsuba_aaa_trans/
+ /3 width=3 by lsuba_beta, lsuba_aaa_trans/
]
| #L1 #L #W #V #A #HV #HW #HL1 #IHL1 #X #H
elim (lsuba_inv_pair1 … H) -H * #L2
- [ #HL2 #H destruct /3 width=5 by lsuba_abbr, lsuba_aaa_conf/
+ [ #HL2 #H destruct /3 width=5 by lsuba_beta, lsuba_aaa_conf/
| #W0 #V0 #A0 #_ #_ #_ #H destruct
]
]
| lsubd_atom: lsubd h g G (⋆) (⋆)
| lsubd_pair: ∀I,L1,L2,V. lsubd h g G L1 L2 →
lsubd h g G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubd_abbr: ∀L1,L2,W,V,l. ⦃G, L1⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] l →
+| lsubd_beta: ∀L1,L2,W,V,l. ⦃G, L1⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] l →
lsubd h g G L1 L2 → lsubd h g G (L1.ⓓⓝW.V) (L2.ⓛW)
.
"local environment refinement (degree assignment)"
'LRSubEqD h g G L1 L2 = (lsubd h g G L1 L2).
-(* Basic_forward lemmas *****************************************************)
+(* Basic forward lemmas *****************************************************)
-lemma lsubd_fwd_lsubr: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â\96ªâ«\83[h, g] L2 → L1 ⫃ L2.
-#h #g #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_abst/
+lemma lsubd_fwd_lsubr: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â«\83â\96ª[h, g] L2 → L1 ⫃ L2.
+#h #g #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
qed-.
(* Basic inversion lemmas ***************************************************)
-fact lsubd_inv_atom1_aux: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â\96ªâ«\83[h, g] L2 → L1 = ⋆ → L2 = ⋆.
+fact lsubd_inv_atom1_aux: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â«\83â\96ª[h, g] L2 → L1 = ⋆ → L2 = ⋆.
#h #g #G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
]
qed-.
-lemma lsubd_inv_atom1: â\88\80h,g,G,L2. G â\8a¢ â\8b\86 â\96ªâ«\83[h, g] L2 → L2 = ⋆.
+lemma lsubd_inv_atom1: â\88\80h,g,G,L2. G â\8a¢ â\8b\86 â«\83â\96ª[h, g] L2 → L2 = ⋆.
/2 width=6 by lsubd_inv_atom1_aux/ qed-.
-fact lsubd_inv_pair1_aux: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â\96ªâ«\83[h, g] L2 →
+fact lsubd_inv_pair1_aux: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â«\83â\96ª[h, g] L2 →
∀I,K1,X. L1 = K1.ⓑ{I}X →
- (â\88\83â\88\83K2. G â\8a¢ K1 â\96ªâ«\83[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
+ (â\88\83â\88\83K2. G â\8a¢ K1 â«\83â\96ª[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G â\8a¢ K1 â\96ªâ«\83[h, g] K2 &
+ G â\8a¢ K1 â«\83â\96ª[h, g] K2 &
I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
#h #g #G #L1 #L2 * -L1 -L2
[ #J #K1 #X #H destruct
]
qed-.
-lemma lsubd_inv_pair1: â\88\80h,g,I,G,K1,L2,X. G â\8a¢ K1.â\93\91{I}X â\96ªâ«\83[h, g] L2 →
- (â\88\83â\88\83K2. G â\8a¢ K1 â\96ªâ«\83[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
+lemma lsubd_inv_pair1: â\88\80h,g,I,G,K1,L2,X. G â\8a¢ K1.â\93\91{I}X â«\83â\96ª[h, g] L2 →
+ (â\88\83â\88\83K2. G â\8a¢ K1 â«\83â\96ª[h, g] K2 & L2 = K2.ⓑ{I}X) ∨
∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G â\8a¢ K1 â\96ªâ«\83[h, g] K2 &
+ G â\8a¢ K1 â«\83â\96ª[h, g] K2 &
I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
/2 width=3 by lsubd_inv_pair1_aux/ qed-.
-fact lsubd_inv_atom2_aux: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â\96ªâ«\83[h, g] L2 → L2 = ⋆ → L1 = ⋆.
+fact lsubd_inv_atom2_aux: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â«\83â\96ª[h, g] L2 → L2 = ⋆ → L1 = ⋆.
#h #g #G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
]
qed-.
-lemma lsubd_inv_atom2: â\88\80h,g,G,L1. G â\8a¢ L1 â\96ªâ«\83[h, g] ⋆ → L1 = ⋆.
+lemma lsubd_inv_atom2: â\88\80h,g,G,L1. G â\8a¢ L1 â«\83â\96ª[h, g] ⋆ → L1 = ⋆.
/2 width=6 by lsubd_inv_atom2_aux/ qed-.
-fact lsubd_inv_pair2_aux: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â\96ªâ«\83[h, g] L2 →
+fact lsubd_inv_pair2_aux: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â«\83â\96ª[h, g] L2 →
∀I,K2,W. L2 = K2.ⓑ{I}W →
- (â\88\83â\88\83K1. G â\8a¢ K1 â\96ªâ«\83[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
+ (â\88\83â\88\83K1. G â\8a¢ K1 â«\83â\96ª[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
∃∃K1,V,l. ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G â\8a¢ K1 â\96ªâ«\83[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
+ G â\8a¢ K1 â«\83â\96ª[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
#h #g #G #L1 #L2 * -L1 -L2
[ #J #K2 #U #H destruct
| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3 by ex2_intro, or_introl/
]
qed-.
-lemma lsubd_inv_pair2: â\88\80h,g,I,G,L1,K2,W. G â\8a¢ L1 â\96ªâ«\83[h, g] K2.ⓑ{I}W →
- (â\88\83â\88\83K1. G â\8a¢ K1 â\96ªâ«\83[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
+lemma lsubd_inv_pair2: â\88\80h,g,I,G,L1,K2,W. G â\8a¢ L1 â«\83â\96ª[h, g] K2.ⓑ{I}W →
+ (â\88\83â\88\83K1. G â\8a¢ K1 â«\83â\96ª[h, g] K2 & L1 = K1.ⓑ{I}W) ∨
∃∃K1,V,l. ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l &
- G â\8a¢ K1 â\96ªâ«\83[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
+ G â\8a¢ K1 â«\83â\96ª[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V.
/2 width=3 by lsubd_inv_pair2_aux/ qed-.
(* Basic properties *********************************************************)
-lemma lsubd_refl: â\88\80h,g,G,L. G â\8a¢ L â\96ªâ«\83[h, g] L.
+lemma lsubd_refl: â\88\80h,g,G,L. G â\8a¢ L â«\83â\96ª[h, g] L.
#h #g #G #L elim L -L /2 width=1 by lsubd_pair/
qed.
(* Note: the constant 0 cannot be generalized *)
-lemma lsubd_drop_O1_conf: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â\96ªâ«\83[h, g] L2 →
+lemma lsubd_drop_O1_conf: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â«\83â\96ª[h, g] L2 →
∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 →
- â\88\83â\88\83K2. G â\8a¢ K1 â\96ªâ«\83[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2.
+ â\88\83â\88\83K2. G â\8a¢ K1 â«\83â\96ª[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2.
#h #g #G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
| #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H
elim (drop_inv_O1_pair1 … H) -H * #He #HLK1
[ destruct
elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubd_abbr, drop_pair, ex2_intro/
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubd_beta, drop_pair, ex2_intro/
| elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/
]
]
qed-.
(* Note: the constant 0 cannot be generalized *)
-lemma lsubd_drop_O1_trans: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â\96ªâ«\83[h, g] L2 →
+lemma lsubd_drop_O1_trans: â\88\80h,g,G,L1,L2. G â\8a¢ L1 â«\83â\96ª[h, g] L2 →
∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 →
- â\88\83â\88\83K1. G â\8a¢ K1 â\96ªâ«\83[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1.
+ â\88\83â\88\83K1. G â\8a¢ K1 â«\83â\96ª[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1.
#h #g #G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3 by ex2_intro/
| #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H
elim (drop_inv_O1_pair1 … H) -H * #He #HLK2
[ destruct
elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H
- <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubd_abbr, drop_pair, ex2_intro/
+ <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubd_beta, drop_pair, ex2_intro/
| elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
]
]
(* Properties on degree assignment ******************************************)
lemma lsubd_da_trans: ∀h,g,G,L2,T,l. ⦃G, L2⦄ ⊢ T ▪[h, g] l →
- â\88\80L1. G â\8a¢ L1 â\96ªâ«\83[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] l.
+ â\88\80L1. G â\8a¢ L1 â«\83â\96ª[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] l.
#h #g #G #L2 #T #l #H elim H -G -L2 -T -l
[ /2 width=1/
| #G #L2 #K2 #V #i #l #HLK2 #_ #IHV #L1 #HL12
qed-.
lemma lsubd_da_conf: ∀h,g,G,L1,T,l. ⦃G, L1⦄ ⊢ T ▪[h, g] l →
- â\88\80L2. G â\8a¢ L1 â\96ªâ«\83[h, g] L2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l.
+ â\88\80L2. G â\8a¢ L1 â«\83â\96ª[h, g] L2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l.
#h #g #G #L1 #T #l #H elim H -G -L1 -T -l
[ /2 width=1/
| #G #L1 #K1 #V #i #l #HLK1 #HV #IHV #L2 #HL12
elim (lsubd_inv_pair1 … H) -H * #L2
[ #HL2 #H destruct /3 width=1/
| #W #V #l #HV #HW #HL2 #H1 #H2 #H3 destruct
- /3 width=3 by lsubd_abbr, lsubd_da_trans/
+ /3 width=3 by lsubd_beta, lsubd_da_trans/
]
| #L1 #L #W #V #l #HV #HW #HL1 #IHL1 #X #H
elim (lsubd_inv_pair1 … H) -H * #L2
- [ #HL2 #H destruct /3 width=5 by lsubd_abbr, lsubd_da_conf/
+ [ #HL2 #H destruct /3 width=5 by lsubd_beta, lsubd_da_conf/
| #W0 #V0 #l0 #_ #_ #_ #H destruct
]
]
(* RESTRICTED LOCAL ENVIRONMENT REFINEMENT **********************************)
inductive lsubr: relation lenv ≝
-| lsubr_sort: ∀L. lsubr L (⋆)
-| lsubr_bind: ∀I,L1,L2,V. lsubr L1 L2 → lsubr (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubr_abst: ∀L1,L2,V,W. lsubr L1 L2 → lsubr (L1.ⓓⓝW.V) (L2.ⓛW)
+| lsubr_atom: ∀L. lsubr L (⋆)
+| lsubr_pair: ∀I,L1,L2,V. lsubr L1 L2 → lsubr (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsubr_beta: ∀L1,L2,V,W. lsubr L1 L2 → lsubr (L1.ⓓⓝW.V) (L2.ⓛW)
.
interpretation
(* Basic properties *********************************************************)
lemma lsubr_refl: ∀L. L ⫃ L.
-#L elim L -L /2 width=1 by lsubr_sort, lsubr_bind/
+#L elim L -L /2 width=1 by lsubr_atom, lsubr_pair/
qed.
(* Basic inversion lemmas ***************************************************)
#L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/
qed-.
-lemma lsubr_fwd_drop2_bind: ∀L1,L2. L1 ⫃ L2 →
+lemma lsubr_fwd_drop2_pair: ∀L1,L2. L1 ⫃ L2 →
∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W →
(∃∃K1. K1 ⫃ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W) ∨
∃∃K1,V. K1 ⫃ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
lemma lsubr_fwd_drop2_abbr: ∀L1,L2. L1 ⫃ L2 →
∀K2,V,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓓV →
∃∃K1. K1 ⫃ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓV.
-#L1 #L2 #HL12 #K2 #V #s #i #HLK2 elim (lsubr_fwd_drop2_bind … HL12 … HLK2) -L2 // *
+#L1 #L2 #HL12 #K2 #V #s #i #HLK2 elim (lsubr_fwd_drop2_pair … HL12 … HLK2) -L2 // *
#K1 #W #_ #_ #H destruct
qed-.
(* Auxiliary inversion lemmas ***********************************************)
-fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+fact lsubr_inv_pair1_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
∨∨ L2 = ⋆
| ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓑ{I}X
| ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW &
]
qed-.
-lemma lsubr_inv_bind1: ∀I,K1,L2,X. K1.ⓑ{I}X ⫃ L2 →
+lemma lsubr_inv_pair1: ∀I,K1,L2,X. K1.ⓑ{I}X ⫃ L2 →
∨∨ L2 = ⋆
| ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓑ{I}X
| ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW &
I = Abbr & X = ⓝW.V.
-/2 width=3 by lsubr_inv_bind1_aux/ qed-.
+/2 width=3 by lsubr_inv_pair1_aux/ qed-.
(* Main properties **********************************************************)
[ #L1 #X #H
lapply (lsubr_inv_atom1 … H) -H //
| #I #L1 #L #V #_ #IHL1 #X #H
- elim (lsubr_inv_bind1 … H) -H // *
- #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1 by lsubr_bind, lsubr_abst/
+ elim (lsubr_inv_pair1 … H) -H // *
+ #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1 by lsubr_pair, lsubr_beta/
| #L1 #L #V1 #W #_ #IHL1 #X #H
elim (lsubr_inv_abst1 … H) -H // *
- #L2 #HL2 #H destruct /3 width=1 by lsubr_abst/
+ #L2 #HL2 #H destruct /3 width=1 by lsubr_beta/
]
qed-.
]
qed-.
-(* Advanced forvard lemmas **************************************************)
+(* Advanced forward lemmas **************************************************)
(* Basic_1: was: sty0_correct *)
lemma sta_fwd_correct: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •[h] U → ∃T0. ⦃G, L⦄ ⊢ U •[h] T0.
]
qed-.
-(* Advancd inversion lemmas on relocation ***********************************)
+(* Advanced inversion lemmas on relocation ***********************************)
lemma cpy_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 →
∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
]
qed-.
-(* Basic forvard lemmas *****************************************************)
+(* Basic forward lemmas *****************************************************)
(* Basic_1: was: drop_S *)
lemma drop_fwd_drop2: ∀L1,I2,K2,V2,s,e. ⇩[s, O, e] L1 ≡ K2. ⓑ{I2} V2 →
(* BASIC TERM RELOCATION ****************************************************)
-(* Main properies ***********************************************************)
+(* Main properties ***********************************************************)
(* Basic_1: was: lift_inj *)
theorem lift_inj: ∀d,e,T1,U. ⇧[d,e] T1 ≡ U → ∀T2. ⇧[d,e] T2 ≡ U → T1 = T2.
(* BASIC TERM VECTOR RELOCATION *********************************************)
-(* Main properies ***********************************************************)
+(* Main properties ***********************************************************)
theorem liftv_mono: ∀Ts,U1s,d,e. ⇧[d,e] Ts ≡ U1s →
∀U2s:list term. ⇧[d,e] Ts ≡ U2s → U1s = U2s.
(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
-(* Properies on dropping ****************************************************)
+(* Properties on dropping ****************************************************)
lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 →
∀I,K1,V1,i. ⇩[i] L1 ≡ K1.ⓑ{I}V1 →
]
*)
[ { "local env. ref. for stratified native validity" * } {
- [ "lsubsv ( ? ⊢ ? ¡⫃[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
+ [ "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
}
]
[ { "stratified native validity" * } {
class "grass"
[ { "static typing" * } {
[ { "local env. ref. for degree assignment" * } {
- [ "lsubd ( ? â\8a¢ ? â\96ªâ«\83 ? )" "lsubd_da" + "lsubd_lsubd" * ]
+ [ "lsubd ( ? â\8a¢ ? â«\83â\96ª[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ]
}
]
[ { "degree assignment" * } {
}
]
[ { "local env. ref. for atomic arity assignment" * } {
- [ "lsuba ( ? â\8a¢ ? â\81\9dâ«\83 ? )" "lsuba_aaa" + "lsuba_lsuba" * ]
+ [ "lsuba ( ? â\8a¢ ? â«\83â\81\9d ? )" "lsuba_aaa" + "lsuba_lsuba" * ]
}
]
[ { "atomic arity assignment" * } {
}
]
[ { "local env. ref. for extended substitution" * } {
- [ "lsuby ( ? â\8a\91Ã\97[?,?] ? )" "lsuby_lsuby" * ]
+ [ "lsuby ( ? â\8a\86[?,?] ? )" "lsuby_lsuby" * ]
}
]
[ { "pointwise extension of a relation" * } {
(* Iterators ****************************************************************)
-(* Note: see also: lib/arithemetcs/bigops.ma *)
+(* Note: see also: lib/arithemetics/bigops.ma *)
let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝
match n with
[ O ⇒ nil
projects / helm.git / commitdiff