module E = Engine
let is_obj path =
- F.check_suffix path ".con.ng" &
- F.check_suffix path ".ind.ng" &
+ F.check_suffix path ".con.ng" ||
+ F.check_suffix path ".ind.ng" ||
F.check_suffix path ".var.ng"
let src_exists path = !O.no_devel || Y.file_exists path
include "basic_2/unfold/sstas_sstas.ma".
include "basic_2/computation/lprs_cprs.ma".
+include "basic_2/computation/cpxs_cpxs.ma".
include "basic_2/computation/cpds.ma".
(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
| /3 width=3/
]
qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpds_fwd_cpxs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+#h #g #L #T1 #T2 * /3 width=3 by cpxs_trans, sstas_cpxs, cprs_cpxs/
+qed-.
L ⊢ T1 ➡ T → L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
normalize /2 width=3/ qed.
-lemma lsubx_cprs_trans: lsub_trans … cprs lsubx.
-/3 width=5 by lsubx_cpr_trans, TC_lsub_trans/
+lemma lsubr_cprs_trans: lsub_trans … cprs lsubr.
+/3 width=5 by lsubr_cpr_trans, TC_lsub_trans/
qed-.
(* Basic_1: was: pr3_pr1 *)
lemma tprs_cprs: ∀L,T1,T2. ⋆ ⊢ T1 ➡* T2 → L ⊢ T1 ➡* T2.
-#L #T1 #T2 #H @(lsubx_cprs_trans … H) -H //
+#L #T1 #T2 #H @(lsubr_cprs_trans … H) -H //
qed.
lemma cprs_bind_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 →
[ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
| #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12
- lapply (lsubx_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2
+ lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2
@or3_intro1 @(ex2_3_intro … HT10) -HT10 /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
| #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
@or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
(**************************************************************************)
include "basic_2/notation/relations/predstar_5.ma".
+include "basic_2/unfold/sstas.ma".
include "basic_2/reduction/cnx.ma".
include "basic_2/computation/cprs.ma".
∀T2. ⦃h, L⦄ ⊢ T ➡*[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
normalize /2 width=3/ qed.
-lemma lsubx_cpxs_trans: ∀h,g. lsub_trans … (cpxs h g) lsubx.
-/3 width=5 by lsubx_cpx_trans, TC_lsub_trans/
+lemma lsubr_cpxs_trans: ∀h,g. lsub_trans … (cpxs h g) lsubr.
+/3 width=5 by lsubr_cpx_trans, TC_lsub_trans/
qed-.
+lemma sstas_cpxs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •* [g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 //
+/3 width=4 by cpxs_strap1, ssta_cpx/
+qed.
+
lemma cprs_cpxs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
qed.
[ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
| #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
lapply (cpxs_strap1 … HV10 … HV02) -V0 #HV12
- lapply (lsubx_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2
+ lapply (lsubr_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 /2 width=1/ #HT2
@or3_intro1 @(ex2_3_intro … HT10) -HT10 /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
| #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
@or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
[ #V0 #T0 #_ #_ #H destruct /2 width=1/
| #b #W0 #T0 #HT0 #HU
elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
- lapply (lsubx_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 /2 width=1/ #HT1
+ lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 /2 width=1/ #HT1
@or_intror @(cpxs_trans … HU) -U /3 width=1/ (**) (* explicit constructor *)
| #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/ ] -H2
- lapply (lsubx_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 [ /2 width=1/ ] /3 width=1/
+ lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 [ /2 width=1/ ] /3 width=1/
| -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct
- lapply (lsubx_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 [ /2 width=1/ ] #HT02
+ lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 [ /2 width=1/ ] #HT02
@(csn_cpx_trans … HT1) -HT1 /3 width=1/
| -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct
]
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/crsubeq_3.ma".
+include "basic_2/notation/relations/lrsubeq_3.ma".
include "basic_2/static/aaa.ma".
include "basic_2/computation/acp_cr.ma".
inductive lsubc (RP:lenv→predicate term): relation lenv ≝
| lsubc_atom: lsubc RP (⋆) (⋆)
-| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V)
+| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1.ⓑ{I}V) (L2.ⓑ{I}V)
| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ ϵ[RP] 〚A〛 → ⦃L1, W⦄ ϵ[RP] 〚A〛 → L2 ⊢ W ⁝ A →
- lsubc RP L1 L2 → lsubc RP (L1. ⓓⓝW.V) (L2. ⓛW)
+ lsubc RP L1 L2 → lsubc RP (L1. ⓓⓝW.V) (L2.ⓛW)
.
interpretation
"local environment refinement (abstract candidates of reducibility)"
- 'CrSubEq L1 RP L2 = (lsubc RP L1 L2).
+ 'LRSubEq RP L1 L2 = (lsubc RP L1 L2).
(* Basic inversion lemmas ***************************************************)
/2 width=4 by lsubc_inv_atom1_aux/ qed-.
fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
- (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I}X) ∨
+ (∃∃K2. K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &
L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
(∃∃K2. K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &
- L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
+ L2 = K2.ⓛW & X = ⓝW.V & I = Abbr.
/2 width=3 by lsubc_inv_pair1_aux/ qed-.
fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → L2 = ⋆ → L1 = ⋆.
lemma lsubc_inv_atom2: ∀RP,L1. L1 ⊑[RP] ⋆ → L1 = ⋆.
/2 width=4 by lsubc_inv_atom2_aux/ qed-.
-fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
+fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2.ⓑ{I} W →
(∃∃K1. K1 ⊑[RP] K2 & L1 = K1. ⓑ{I} W) ∨
∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &
- L1 = K1. ⓓⓝW.V & I = Abst.
+ L1 = K1.ⓓⓝW.V & I = Abst.
#RP #L1 #L2 * -L1 -L2
[ #I #K2 #W #H destruct
| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
qed-.
(* Basic_1: was just: csubc_gen_head_l *)
-lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2. ⓑ{I} W →
+lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 ⊑[RP] K2.ⓑ{I} W →
(∃∃K1. K1 ⊑[RP] K2 & L1 = K1.ⓑ{I} W) ∨
∃∃K1,V,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
K1 ⊑[RP] K2 &
(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
(* properties concerning lenv refinement for atomic arity assignment ********)
-(*
-lamma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+
+lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L1,L2. L1 ⁝⊑ L2 → L1 ⊑[RP] L2.
-#RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2
-// /2 width=1/ /3 width=4/
+#RR #RS #RP #H1RP #H2RP #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.
-*)
\ No newline at end of file
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/crsubeqv_4.ma".
+include "basic_2/notation/relations/lrsubeqv_4.ma".
include "basic_2/dynamic/snv.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
interpretation
"local environment refinement (stratified native validity)"
- 'CrSubEqV h g L1 L2 = (lsubsv h g L1 L2).
+ 'LRSubEqV h g L1 L2 = (lsubsv h g L1 L2).
(* Basic inversion lemmas ***************************************************)
(* Basic_forward lemmas *****************************************************)
-lemma lsubsv_fwd_lsubx: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ⓝ⊑ L2.
+lemma lsubsv_fwd_lsubr: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ⊑ L2.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
qed-.
lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-/3 width=5 by lsubsv_fwd_lsubx, lsubx_cprs_trans/
+/3 width=5 by lsubsv_fwd_lsubr, lsubr_cprs_trans/
qed-.
lemma lsubsv_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 →
∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
-/3 width=5 by lsubsv_fwd_lsubx, lsubx_cpcs_trans/
+/3 width=5 by lsubsv_fwd_lsubr, lsubr_cpcs_trans/
qed-.
(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************)
-(* Properties on local environment refinement for atomic arity assignment ***)
-(*
-lamma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ⁝⊑ L2.
+(* Forward lemmas on lenv refinement for atomic arity assignment ************)
+
+lemma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ⁝⊑ L2.
#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
-#L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #_ #_ #HL12
-elim (snv_fwd_aaa … HV1) -HV1 #A #HV1
-elim (snv_fwd_aaa … HW2) -HW2 #B #HW2
-lapply (ssta_aaa … HV1 … HVW1) -HVW1 #H1
-lapply (lsuba_aaa_trans … HW2 … HL12) #H2
-lapply (aaa_cpcs_mono … HW12 … H1 … H2) -W1 -H2 #H destruct /2 width=3/
+#L1 #L2 #W #V #W1 #V2 #l #HV #HW #_ #_ #_ #IHL12 -W1 -V2
+elim (snv_fwd_aaa … HV) -HV #A #HV
+elim (snv_fwd_aaa … HW) -HW #B #HW
+elim (aaa_inv_cast … HV) #HWA #_
+lapply (lsuba_aaa_trans … HW … IHL12) #HWB
+lapply (aaa_mono … HWB … HWA) -HWB -HWA #H destruct /2 width=3/
qed-.
-*)
elim (cpcs_inv_cprs … HV12) -HV12 /3 width=5 by cprs_div, cprs_bind/ (**) (* /3 width=5/ is a bit slow *)
qed.
-lemma lsubx_cpcs_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
- â\88\80L2. L2 â\93\9dâ\8a\91 L1 â\86\92 L2 â\8a¢ T1 â¬\8c* T2.
+lemma lsubr_cpcs_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
+ ∀L2. L2 ⊑ L1 → L2 ⊢ T1 ⬌* T2.
#L1 #T1 #T2 #HT12
elim (cpcs_inv_cprs … HT12) -HT12
-/3 width=5 by cprs_div, lsubx_cprs_trans/ (**) (* /3 width=5/ is a bit slow *)
+/3 width=5 by cprs_div, lsubr_cprs_trans/ (**) (* /3 width=5/ is a bit slow *)
qed-.
(* Basic_1: was: pc3_lift *)
@(cpcs_trans … (ⓑ{a,I}V2.T1)) /2 width=1/
qed.
-lemma cpcs_beta_dx: ∀a,L,V1,V2,W1,W2,T1,T2.
- L ⊢ V1 ⬌* V2 → L ⊢ W1 ⬌* W2 → L.ⓛW2 ⊢ T1 ⬌* T2 →
- L ⊢ ⓐV1.ⓛ{a}W1.T1 ⬌* ⓓ{a}ⓝW2.V2.T2.
-#a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12
-@(cpcs_cpr_strap1 … (ⓐV2.ⓛ{a}W2.T2)) /2 width=1/ /3 width=1/
-qed.
-
-lemma cpcs_beta_sn: ∀a,L,V1,V2,W1,W2,T1,T2.
- L ⊢ V1 ⬌* V2 → L ⊢ W1 ⬌* W2 → L.ⓛW1 ⊢ T1 ⬌* T2 →
- L ⊢ ⓐV1.ⓛ{a}W1.T1 ⬌* ⓓ{a}ⓝW2.V2.T2.
-#a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12
-lapply (lsubx_cpcs_trans … HT12 (L.ⓓⓝW1.V1) ?) /2 width=1/ #H2T12
-@(cpcs_cpr_strap2 … (ⓓ{a}ⓝW1.V1.T1)) /2 width=1/ -HT12 /3 width=1/
-qed.
-
(* Basic_1: was: pc3_wcpr0 *)
lemma lpr_cpcs_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
#L1 #L2 #HL12 #T1 #T2 #H
--- /dev/null
+lemma cpcs_beta_dx: ∀a,L,V1,V2,W1,W2,T1,T2.
+ L ⊢ V1 ⬌* V2 → L ⊢ W1 ⬌* W2 → L.ⓛW2 ⊢ T1 ⬌* T2 →
+ L ⊢ ⓐV1.ⓛ{a}W1.T1 ⬌* ⓓ{a}ⓝW2.V2.T2.
+#a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12
+@(cpcs_cpr_strap1 … (ⓐV2.ⓛ{a}W2.T2)) /2 width=1/ /3 width=1/
+qed.
+
+lemma cpcs_beta_sn: ∀a,L,V1,V2,W1,W2,T1,T2.
+ L ⊢ V1 ⬌* V2 → L ⊢ W1 ⬌* W2 → L.ⓛW1 ⊢ T1 ⬌* T2 →
+ L ⊢ ⓐV1.ⓛ{a}W1.T1 ⬌* ⓓ{a}ⓝW2.V2.T2.
+#a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12
+lapply (lsubr_cpcs_trans … HT12 (L.ⓓⓝW1.V1) ?) /2 width=1/ #H2T12
+@(cpcs_cpr_strap2 … (ⓓ{a}ⓝW1.V1.T1)) /2 width=1/ -HT12 /3 width=1/
+qed.
(* *)
(**************************************************************************)
-notation "hvbox( L1 ⊑ break term 46 L2 )"
+notation "hvbox( L1 â\93\9d â\8a\91 break term 46 L2 )"
non associative with precedence 45
- for @{ 'CrSubEq $L1 $L2 }.
+ for @{ 'LRSubEqT $L1 $L2 }.
include "basic_2/relocation/ldrop.ma".
notation "hvbox( h ⊢ break term 46 L1 ÷ ⊑ break term 46 L2 )"
non associative with precedence 45
- for @{ 'CrSubEqB $h $L1 $L2 }.
+ for @{ 'LRSubEqB $h $L1 $L2 }.
notation "hvbox( L1 ⊢ ⬌ break term 46 L2 )"
non associative with precedence 45
+++ /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( T1 ⊑ break [ term 46 R ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'CrSubEq $T1 $R $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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( T1 ⁝ ⊑ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'CrSubEqA $T1 $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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 ⓝ ⊑ break term 46 L2 )"
- non associative with precedence 45
- for @{ 'CrSubEqT $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( h ⊢ break term 46 L1 ¡ ⊑ break [ term 46 g ] break term 46 L2 )"
- non associative with precedence 45
- for @{ 'CrSubEqV $h $g $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( L1 ⊑ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LRSubEq $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( T1 ⊑ break [ term 46 R ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'LRSubEq $R $T1 $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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( T1 ⁝ ⊑ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'LRSubEqA $T1 $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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( h ⊢ break term 46 L1 ¡ ⊑ break [ term 46 g ] break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LRSubEqV $h $g $L1 $L2 }.
include "basic_2/notation/relations/pred_3.ma".
include "basic_2/grammar/cl_shift.ma".
include "basic_2/relocation/ldrop_append.ma".
-include "basic_2/reduction/lsubx.ma".
+include "basic_2/substitution/lsubr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
(* Basic properties *********************************************************)
-lemma lsubx_cpr_trans: lsub_trans … cpr lsubx.
+lemma lsubr_cpr_trans: lsub_trans … cpr lsubr.
#L1 #T1 #T2 #H elim H -L1 -T1 -T2
[ //
| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsubx_fwd_ldrop2_abbr … HL12 … HLK1) -L1 * /3 width=6/
+ elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -L1 * /3 width=6/
|3,7: /4 width=1/
|4,6: /3 width=1/
|5,8: /4 width=3/
(* Basic_1: was by definition: pr2_free *)
lemma tpr_cpr: ∀T1,T2. ⋆ ⊢ T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2.
#T1 #T2 #HT12 #L
-lapply (lsubx_cpr_trans … HT12 L ?) //
+lapply (lsubr_cpr_trans … HT12 L ?) //
qed.
(* Basic_1: includes by definition: pr0_refl *)
(* Basic properties *********************************************************)
-lemma lsubx_cpx_trans: ∀h,g. lsub_trans … (cpx h g) lsubx.
+lemma lsubr_cpx_trans: ∀h,g. lsub_trans … (cpx h g) lsubr.
#h #g #L1 #T1 #T2 #H elim H -L1 -T1 -T2
[ //
| /2 width=2/
| #I #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsubx_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
+ elim (lsubr_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
[ /3 width=7/ | /4 width=7/ ]
|4,9: /4 width=1/
|5,7,8: /3 width=1/
elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #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/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
-lapply (lsubx_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1/
+lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1/
/4 width=5 by cpr_bind, cpr_flat, cpr_beta, ex2_intro/ (**) (* auto too slow without trace *)
qed-.
elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #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/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
-lapply (lsubx_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1/
-lapply (lsubx_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1/
+lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1/
+lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1/
/4 width=5 by cpr_bind, cpr_flat, 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/notation/relations/crsubeqt_2.ma".
-include "basic_2/relocation/ldrop.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED REDUCTION **********************)
-
-inductive lsubx: relation lenv ≝
-| lsubx_sort: ∀L. lsubx L (⋆)
-| lsubx_bind: ∀I,L1,L2,V. lsubx L1 L2 → lsubx (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsubx_abst: ∀L1,L2,V,W. lsubx L1 L2 → lsubx (L1.ⓓⓝW.V) (L2.ⓛW)
-.
-
-interpretation
- "local environment refinement (reduction)"
- 'CrSubEqT L1 L2 = (lsubx L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma lsubx_refl: ∀L. L ⓝ⊑ L.
-#L elim L -L // /2 width=1/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lsubx_inv_atom1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 * -L1 -L2 //
-[ #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #_ #H destruct
-]
-qed-.
-
-lemma lsubx_inv_atom1: ∀L2. ⋆ ⓝ⊑ L2 → L2 = ⋆.
-/2 width=3 by lsubx_inv_atom1_aux/ qed-.
-
-fact lsubx_inv_abst1_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀K1,W. L1 = K1.ⓛW →
- L2 = ⋆ ∨ ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓛW.
-#L1 #L2 * -L1 -L2
-[ #L #K1 #W #H destruct /2 width=1/
-| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3/
-| #L1 #L2 #V1 #V2 #_ #K1 #W #H destruct
-]
-qed-.
-
-lemma lsubx_inv_abst1: ∀K1,L2,W. K1.ⓛW ⓝ⊑ L2 →
- L2 = ⋆ ∨ ∃∃K2. K1 ⓝ⊑ K2 & L2 = K2.ⓛW.
-/2 width=3 by lsubx_inv_abst1_aux/ qed-.
-
-fact lsubx_inv_abbr2_aux: ∀L1,L2. L1 ⓝ⊑ L2 → ∀K2,W. L2 = K2.ⓓW →
- ∃∃K1. K1 ⓝ⊑ K2 & L1 = K1.ⓓW.
-#L1 #L2 * -L1 -L2
-[ #L #K2 #W #H destruct
-| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3/
-| #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
-]
-qed-.
-
-lemma lsubx_inv_abbr2: ∀L1,K2,W. L1 ⓝ⊑ K2.ⓓW →
- ∃∃K1. K1 ⓝ⊑ K2 & L1 = K1.ⓓW.
-/2 width=3 by lsubx_inv_abbr2_aux/ qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lsubx_fwd_length: ∀L1,L2. L1 ⓝ⊑ L2 → |L2| ≤ |L1|.
-#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
-qed-.
-
-lemma lsubx_fwd_ldrop2_bind: ∀L1,L2. L1 ⓝ⊑ L2 →
- ∀I,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I}W →
- (∃∃K1. K1 ⓝ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I}W) ∨
- ∃∃K1,V. K1 ⓝ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
-#L1 #L2 #H elim H -L1 -L2
-[ #L #I #K2 #W #i #H
- elim (ldrop_inv_atom1 … H) -H #H destruct
-| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #i #H
- elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
- [ /3 width=3/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
- ]
-| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #i #H
- elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
- [ /3 width=4/
- | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
- ]
-]
-qed-.
-
-lemma lsubx_fwd_ldrop2_abbr: ∀L1,L2. L1 ⓝ⊑ L2 →
- ∀K2,V,i. ⇩[0, i] L2 ≡ K2.ⓓV →
- ∃∃K1. K1 ⓝ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓV.
-#L1 #L2 #HL12 #K2 #V #i #HLK2 elim (lsubx_fwd_ldrop2_bind … HL12 … HLK2) -L2 // *
-#K1 #W #_ #_ #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/reduction/lsubx.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR EXTENDED REDUCTION **********************)
-
-(* Auxiliary inversion lemmas ***********************************************)
-
-fact lsubx_inv_bind1_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 &
- I = Abbr & X = ⓝW.V.
-#L1 #L2 * -L1 -L2
-[ #L #J #K1 #X #H destruct /2 width=1/
-| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
-| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6/
-]
-qed-.
-
-lemma lsubx_inv_bind1: ∀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 lsubx_inv_bind1_aux/ qed-.
-
-(* Main properties **********************************************************)
-
-theorem lsubx_trans: Transitive … lsubx.
-#L1 #L #H elim H -L1 -L
-[ #L1 #X #H
- lapply (lsubx_inv_atom1 … H) -H //
-| #I #L1 #L #V #_ #IHL1 #X #H
- elim (lsubx_inv_bind1 … H) -H // *
- #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1/
-| #L1 #L #V1 #W #_ #IHL1 #X #H
- elim (lsubx_inv_abst1 … H) -H // *
- #L2 #HL2 #H destruct /3 width=1/
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/crsubeqa_2.ma".
+include "basic_2/notation/relations/lrsubeqa_2.ma".
+include "basic_2/substitution/lsubr.ma".
include "basic_2/static/aaa.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
inductive lsuba: relation lenv ≝
| lsuba_atom: lsuba (⋆) (⋆)
-| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. ⓑ{I} V) (L2. ⓑ{I} V)
-| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ⁝ A → L2 ⊢ W ⁝ A →
- lsuba L1 L2 → lsuba (L1. ⓓV) (L2. ⓛW)
+| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsuba_abbr: ∀L1,L2,W,V,A. L1 ⊢ ⓝW.V ⁝ A → L2 ⊢ W ⁝ A →
+ lsuba L1 L2 → lsuba (L1.ⓓⓝW.V) (L2.ⓛW)
.
interpretation
"local environment refinement (atomic arity assigment)"
- 'CrSubEqA L1 L2 = (lsuba L1 L2).
+ 'LRSubEqA L1 L2 = (lsuba L1 L2).
(* Basic inversion lemmas ***************************************************)
#L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+| #L1 #L2 #W #V #A #_ #_ #_ #H destruct
]
-qed.
+qed-.
lemma lsuba_inv_atom1: ∀L2. ⋆ ⁝⊑ L2 → L2 = ⋆.
-/2 width=3/ qed-.
+/2 width=3 by lsuba_inv_atom1_aux/ qed-.
-fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
- (∃∃K2. K1 ⁝⊑ K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
- L2 = K2. ⓛW & I = Abbr.
+fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+ (∃∃K2. K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,W,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
+ I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
#L1 #L2 * -L1 -L2
-[ #I #K1 #V #H destruct
-| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
-| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K1 #V #H destruct /3 width=7/
+[ #J #K1 #X #H destruct
+| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
+| #L1 #L2 #W #V #A #HV #HW #HL12 #J #K1 #X #H destruct /3 width=9/
]
-qed.
+qed-.
-lemma lsuba_inv_pair1: ∀I,K1,L2,V. K1. ⓑ{I} V ⁝⊑ L2 →
- (∃∃K2. K1 ⁝⊑ K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
- L2 = K2. ⓛW & I = Abbr.
-/2 width=3/ qed-.
+lemma lsuba_inv_pair1: ∀I,K1,L2,X. K1.ⓑ{I}X ⁝⊑ L2 →
+ (∃∃K2. K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,W,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
+ I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+/2 width=3 by lsuba_inv_pair1_aux/ qed-.
fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ⁝⊑ L2 → L2 = ⋆ → L1 = ⋆.
#L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
-| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+| #L1 #L2 #W #V #A #_ #_ #_ #H destruct
]
-qed.
+qed-.
lemma lsubc_inv_atom2: ∀L1. L1 ⁝⊑ ⋆ → L1 = ⋆.
-/2 width=3/ qed-.
+/2 width=3 by lsuba_inv_atom2_aux/ qed-.
-fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
- (∃∃K1. K1 ⁝⊑ K2 & L1 = K1. ⓑ{I} W) ∨
- ∃∃K1,V,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
- L1 = K1. ⓓV & I = Abst.
+fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →
+ (∃∃K1. K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
+ ∃∃K1,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
+ I = Abst & L1 = K1.ⓓⓝW.V.
#L1 #L2 * -L1 -L2
-[ #I #K2 #W #H destruct
-| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
-| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K2 #W #H destruct /3 width=7/
+[ #J #K2 #U #H destruct
+| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3/
+| #L1 #L2 #W #V #A #HV #HW #HL12 #J #K2 #U #H destruct /3 width=7/
]
-qed.
+qed-.
+
+lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ⁝⊑ K2.ⓑ{I}W →
+ (∃∃K1. K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
+ ∃∃K1,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
+ I = Abst & L1 = K1.ⓓⓝW.V.
+/2 width=3 by lsuba_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
-lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ⁝⊑ K2. ⓑ{I} W →
- (∃∃K1. K1 ⁝⊑ K2 & L1 = K1. ⓑ{I} W) ∨
- ∃∃K1,V,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
- L1 = K1. ⓓV & I = Abst.
-/2 width=3/ qed-.
+lemma lsuba_fwd_lsubr: ∀L1,L2. L1 ⁝⊑ L2 → L1 ⊑ L2.
+#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
(* Basic properties *********************************************************)
lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ⁝ A → ∀L2. L1 ⁝⊑ L2 → L2 ⊢ V ⁝ A.
#L1 #V #A #H elim H -L1 -V -A
[ //
-| #I #L1 #K1 #V1 #B #i #HLK1 #HV1B #IHV1 #L2 #HL12
+| #I #L1 #K1 #V #A #i #HLK1 #HV #IHV #L2 #HL12
elim (lsuba_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
elim (lsuba_inv_pair1 … H) -H * #K2
[ #HK12 #H destruct /3 width=5/
- | #V2 #A1 #HV1A1 #HV2 #_ #H1 #H2 destruct
- >(aaa_mono … HV1B … HV1A1) -B -HV1A1 /2 width=5/
+ | #W0 #V0 #A0 #HV0 #HW0 #_ #H1 #H2 #H3 destruct
+ lapply (aaa_mono … HV0 … HV) #H destruct -V0 /2 width=5/
]
| /4 width=2/
| /4 width=1/
| /3 width=3/
| /3 width=1/
]
-qed.
+qed-.
lemma lsuba_aaa_trans: ∀L2,V,A. L2 ⊢ V ⁝ A → ∀L1. L1 ⁝⊑ L2 → L1 ⊢ V ⁝ A.
#L2 #V #A #H elim H -L2 -V -A
[ //
-| #I #L2 #K2 #V2 #B #i #HLK2 #HV2B #IHV2 #L1 #HL12
+| #I #L2 #K2 #V #A #i #HLK2 #H1V #IHV #L1 #HL12
elim (lsuba_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
elim (lsuba_inv_pair2 … H) -H * #K1
[ #HK12 #H destruct /3 width=5/
- | #V1 #A1 #HV1 #HV2A1 #_ #H1 #H2 destruct
- >(aaa_mono … HV2B … HV2A1) -B -HV2A1 /2 width=5/
+ | #V0 #A0 #HV0 #H2V #_ #H1 #H2 destruct
+ lapply (aaa_mono … H2V … H1V) #H destruct -K2 /2 width=5/
]
| /4 width=2/
| /4 width=1/
| /3 width=3/
| /3 width=1/
]
-qed.
+qed-.
<(ldrop_inv_O2 … H) in HL12; -H /3 width=3/
| elim (IHL12 … HLK1) -L1 /3 width=3/
]
-| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #K1 #e #H
+| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K1 #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1
[ destruct
elim (IHL12 L1 0) -IHL12 // #X #HL12 #H
<(ldrop_inv_O2 … H) in HL12; -H /3 width=3/
| elim (IHL12 … HLK2) -L2 /3 width=3/
]
-| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #K2 #e #H
+| #L1 #L2 #W #V #A #HV #HW #_ #IHL12 #K2 #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2
[ destruct
elim (IHL12 L2 0) -IHL12 // #X #HL12 #H
theorem lsuba_trans: ∀L1,L. L1 ⁝⊑ L → ∀L2. L ⁝⊑ L2 → L1 ⁝⊑ L2.
#L1 #L #H elim H -L1 -L
[ #X #H >(lsuba_inv_atom1 … H) -H //
-| #I #L1 #L #V #HL1 #IHL1 #X #H
+| #I #L1 #L #Y #HL1 #IHL1 #X #H
elim (lsuba_inv_pair1 … H) -H * #L2
[ #HL2 #H destruct /3 width=1/
- | #V #A #HLV #HL2V #HL2 #H1 #H2 destruct /3 width=3/
+ | #W #V #A #HV #HW #HL2 #H1 #H2 #H3 destruct
+ /3 width=3 by lsuba_abbr, lsuba_aaa_trans/
]
-| #L1 #L #V1 #W #A1 #HV1 #HW #HL1 #IHL1 #X #H
+| #L1 #L #W #V #A #HV #HW #HL1 #IHL1 #X #H
elim (lsuba_inv_pair1 … H) -H * #L2
- [ #HL2 #H destruct /3 width=5/
- | #V #A2 #_ #_ #_ #_ #H destruct
+ [ #HL2 #H destruct /3 width=5 by lsuba_abbr, lsuba_aaa_conf/
+ | #W0 #V0 #A0 #_ #_ #_ #H destruct
]
]
-qed.
+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/lrsubeq_2.ma".
+include "basic_2/relocation/ldrop.ma".
+
+(* 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)
+.
+
+interpretation
+ "local environment refinement (restricted)"
+ 'LRSubEq L1 L2 = (lsubr L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma lsubr_refl: ∀L. L ⊑ L.
+#L elim L -L // /2 width=1/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubr_inv_atom1_aux: ∀L1,L2. L1 ⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#L1 #L2 * -L1 -L2 //
+[ #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #_ #H destruct
+]
+qed-.
+
+lemma lsubr_inv_atom1: ∀L2. ⋆ ⊑ L2 → L2 = ⋆.
+/2 width=3 by lsubr_inv_atom1_aux/ qed-.
+
+fact lsubr_inv_abst1_aux: ∀L1,L2. L1 ⊑ L2 → ∀K1,W. L1 = K1.ⓛW →
+ L2 = ⋆ ∨ ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓛW.
+#L1 #L2 * -L1 -L2
+[ #L #K1 #W #H destruct /2 width=1/
+| #I #L1 #L2 #V #HL12 #K1 #W #H destruct /3 width=3/
+| #L1 #L2 #V1 #V2 #_ #K1 #W #H destruct
+]
+qed-.
+
+lemma lsubr_inv_abst1: ∀K1,L2,W. K1.ⓛW ⊑ L2 →
+ L2 = ⋆ ∨ ∃∃K2. K1 ⊑ K2 & L2 = K2.ⓛW.
+/2 width=3 by lsubr_inv_abst1_aux/ qed-.
+
+fact lsubr_inv_abbr2_aux: ∀L1,L2. L1 ⊑ L2 → ∀K2,W. L2 = K2.ⓓW →
+ ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
+#L1 #L2 * -L1 -L2
+[ #L #K2 #W #H destruct
+| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3/
+| #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
+]
+qed-.
+
+lemma lsubr_inv_abbr2: ∀L1,K2,W. L1 ⊑ K2.ⓓW →
+ ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
+/2 width=3 by lsubr_inv_abbr2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsubr_fwd_length: ∀L1,L2. L1 ⊑ L2 → |L2| ≤ |L1|.
+#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+qed-.
+
+lemma lsubr_fwd_ldrop2_bind: ∀L1,L2. L1 ⊑ L2 →
+ ∀I,K2,W,i. ⇩[0, i] L2 ≡ K2.ⓑ{I}W →
+ (∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓑ{I}W) ∨
+ ∃∃K1,V. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst.
+#L1 #L2 #H elim H -L1 -L2
+[ #L #I #K2 #W #i #H
+ elim (ldrop_inv_atom1 … H) -H #H destruct
+| #J #L1 #L2 #V #HL12 #IHL12 #I #K2 #W #i #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+ [ /3 width=3/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
+ ]
+| #L1 #L2 #V1 #V2 #HL12 #IHL12 #I #K2 #W #i #H
+ elim (ldrop_inv_O1_pair1 … H) -H * #Hi #HLK2 destruct [ -IHL12 | -HL12 ]
+ [ /3 width=4/
+ | elim (IHL12 … HLK2) -IHL12 -HLK2 * /4 width=3/ /4 width=4/
+ ]
+]
+qed-.
+
+lemma lsubr_fwd_ldrop2_abbr: ∀L1,L2. L1 ⊑ L2 →
+ ∀K2,V,i. ⇩[0, i] L2 ≡ K2.ⓓV →
+ ∃∃K1. K1 ⊑ K2 & ⇩[0, i] L1 ≡ K1.ⓓV.
+#L1 #L2 #HL12 #K2 #V #i #HLK2 elim (lsubr_fwd_ldrop2_bind … HL12 … HLK2) -L2 // *
+#K1 #W #_ #_ #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/substitution/lsubr.ma".
+
+(* RESTRICTED LOCAL ENVIRONMENT REFINEMENT **********************************)
+
+(* Auxiliary inversion lemmas ***********************************************)
+
+fact lsubr_inv_bind1_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 &
+ I = Abbr & X = ⓝW.V.
+#L1 #L2 * -L1 -L2
+[ #L #J #K1 #X #H destruct /2 width=1/
+| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
+| #L1 #L2 #V #W #HL12 #J #K1 #X #H destruct /3 width=6/
+]
+qed-.
+
+lemma lsubr_inv_bind1: ∀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-.
+
+(* Main properties **********************************************************)
+
+theorem lsubr_trans: Transitive … lsubr.
+#L1 #L #H elim H -L1 -L
+[ #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/
+| #L1 #L #V1 #W #_ #IHL1 #X #H
+ elim (lsubr_inv_abst1 … H) -H // *
+ #L2 #HL2 #H destruct /3 width=1/
+]
+qed-.
[ "crr ( ? ⊢ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ]
}
]
- [ { "local env. ref. for extended reduction" * } {
- [ "lsubx ( ? ⓝ⊑ ? )" "lsubx_lsubx" * ]
- }
- ]
}
]
class "green"
]
class "yellow"
[ { "substitution" * } {
+ [ { "restricted local env. ref." * } {
+ [ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ]
+ }
+ ]
[ { "iterated structural successor for closures" * } {
[ "fsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ )" "fsups_fsups" * ]
[ "fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )" "fsupp_fsupp" * ]
projects / helm.git / commitdiff