From: Ferruccio Guidi Date: Sat, 27 Jul 2013 16:10:57 +0000 (+0000) Subject: - probe: critical bug fixed (all objects were deleted due to wrong test) X-Git-Tag: make_still_working~1126 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ebc33b6d5b68400bc8411973ed4c9ed50d0c52a6;p=helm.git - probe: critical bug fixed (all objects were deleted due to wrong test) - lambdadelta: lenv refinement for atomic arity assignment updated, some renaming and notational change reaxiomatization of beta-reduction complete! (milestone) --- diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index 99f6d193e..9f6248c0f 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -22,8 +22,8 @@ module O = Options 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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma index 847b8f62a..ec3d035f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma @@ -14,6 +14,7 @@ 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 ************************) @@ -51,3 +52,9 @@ elim (cprs_inv_abbr1 … H2) -H2 * | /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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index d74134167..1bcc38d80 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -58,13 +58,13 @@ lemma cprs_strap2: ∀L,T1,T,T2. 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 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma index cdd0bc64b..7e8723fb1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma @@ -94,7 +94,7 @@ lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1.T1 ➡* U2 → [ #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 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma index c8f64f148..635aff910 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma @@ -13,6 +13,7 @@ (**************************************************************************) 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". @@ -56,10 +57,15 @@ lemma cpxs_strap2: ∀h,g,L,T1,T. ⦃h, L⦄ ⊢ T1 ➡[g] T → ∀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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma index 8017af6bf..2399ca665 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -87,7 +87,7 @@ lemma cpxs_inv_appl1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡*[g] U2 → [ #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 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma index 115a366f9..87ae419aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma @@ -48,7 +48,7 @@ elim (cpxs_inv_appl1 … H) -H * [ #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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma index 9a57a2ca5..3f97c882a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma @@ -67,9 +67,9 @@ elim (cpx_inv_appl1 … H1) -H1 * [ -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 ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma index ee9d5df16..0af4368e3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -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". @@ -20,14 +20,14 @@ 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 ***************************************************) @@ -44,7 +44,7 @@ lemma lsubc_inv_atom1: ∀RP,L2. ⋆ ⊑[RP] L2 → L2 = ⋆. /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. @@ -60,7 +60,7 @@ lemma lsubc_inv_pair1: ∀RP,I,K1,L2,X. K1.ⓑ{I}X ⊑[RP] L2 → (∃∃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 = ⋆. @@ -75,11 +75,11 @@ qed-. 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/ @@ -88,7 +88,7 @@ fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K2,W. L2 = K2. ⓑ 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 & diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma index b77900e2f..255de428b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma @@ -18,10 +18,9 @@ include "basic_2/computation/acp_aaa.ma". (* 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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index 537a97d1e..8d4e9b67a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -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 **************) @@ -29,7 +29,7 @@ inductive lsubsv (h:sh) (g:sd h): relation lenv ≝ 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 ***************************************************) @@ -99,7 +99,7 @@ lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 ¡⊑[g] K2.ⓑ{I}W → (* 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-. @@ -111,5 +111,5 @@ 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma index ec6c1e343..a66322d66 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma @@ -21,5 +21,5 @@ include "basic_2/dynamic/lsubsv.ma". 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma index d542b686b..100c34da2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma @@ -17,15 +17,14 @@ include "basic_2/dynamic/lsubsv.ma". (* 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-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma index 7d60ed1b9..44cbd7491 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma @@ -140,11 +140,11 @@ lemma cpcs_bind_sn: ∀a,I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{a,I}V1. T 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 → - ∀L2. L2 ⓝ⊑ L1 → L2 ⊢ T1 ⬌* 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 *) @@ -206,21 +206,6 @@ lemma cpcs_bind2: ∀a,I,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓑ{I}V2 ⊢ @(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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpcs/cpcs_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpcs/cpcs_cpcs.etc new file mode 100644 index 000000000..1647052e1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpcs/cpcs_cpcs.etc @@ -0,0 +1,14 @@ +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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubr/lsubr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubr/lsubr.etc index 93c31e5af..c41ab19f5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubr/lsubr.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubr/lsubr.etc @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -notation "hvbox( L1 ⊑ break term 46 L2 )" +notation "hvbox( L1 ⓝ ⊑ break term 46 L2 )" non associative with precedence 45 - for @{ 'CrSubEq $L1 $L2 }. + for @{ 'LRSubEqT $L1 $L2 }. include "basic_2/relocation/ldrop.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma index e7b98b07e..d131ad872 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma @@ -24,7 +24,7 @@ notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T ÷ brea 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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeq_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeq_3.ma deleted file mode 100644 index 4af339681..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeq_3.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeqa_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeqa_2.ma deleted file mode 100644 index 157579006..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeqa_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeqt_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeqt_2.ma deleted file mode 100644 index 4b40069ad..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeqt_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeqv_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeqv_4.ma deleted file mode 100644 index 2e5f4b473..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/crsubeqv_4.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_2.ma new file mode 100644 index 000000000..185bce94b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_3.ma new file mode 100644 index 000000000..704b6b4ba --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_2.ma new file mode 100644 index 000000000..c45cdebdc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_4.ma new file mode 100644 index 000000000..1124b8b8f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma index a8fe7b1c3..2f263f76c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma @@ -15,7 +15,7 @@ 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 ***************************) @@ -48,11 +48,11 @@ interpretation "context-sensitive parallel reduction (term)" (* 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/ @@ -62,7 +62,7 @@ qed-. (* 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 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma index 3d116e292..6e1a50a65 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma @@ -49,12 +49,12 @@ interpretation (* 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/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index ab7ac0d18..d87242057 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -194,7 +194,7 @@ elim (cpr_inv_abst1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct 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-. @@ -247,8 +247,8 @@ fact cpr_conf_lpr_beta_beta: 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx.ma deleted file mode 100644 index 3b3d7953d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx.ma +++ /dev/null @@ -1,105 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx_lsubx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx_lsubx.ma deleted file mode 100644 index 4c9d0ef09..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx_lsubx.ma +++ /dev/null @@ -1,53 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma index eeeb35651..f3e13c105 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma @@ -12,21 +12,22 @@ (* *) (**************************************************************************) -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 ***************************************************) @@ -34,57 +35,63 @@ fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ⁝⊑ L2 → L1 = ⋆ → L2 = ⋆. #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 *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma index 66e802aae..8539db3db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma @@ -22,33 +22,33 @@ include "basic_2/static/lsuba_ldrop.ma". 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma index b32e6ba93..863ad74d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma @@ -30,7 +30,7 @@ lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ <(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 @@ -52,7 +52,7 @@ lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ <(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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma index 5d64516a5..2738570ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma @@ -21,15 +21,16 @@ include "basic_2/static/lsuba_aaa.ma". 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma new file mode 100644 index 000000000..faf254e36 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma new file mode 100644 index 000000000..e8b7b5e0f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma @@ -0,0 +1,53 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index b365cee9e..e6b3e1709 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -148,10 +148,6 @@ table { [ "crr ( ? ⊢ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ] } ] - [ { "local env. ref. for extended reduction" * } { - [ "lsubx ( ? ⓝ⊑ ? )" "lsubx_lsubx" * ] - } - ] } ] class "green" @@ -188,6 +184,10 @@ table { ] class "yellow" [ { "substitution" * } { + [ { "restricted local env. ref." * } { + [ "lsubr ( ? ⊑ ? )" "lsubr_lsubr" * ] + } + ] [ { "iterated structural successor for closures" * } { [ "fsups ( ⦃?,?⦄ ⊃* ⦃?,?⦄ )" "fsups_fsups" * ] [ "fsupp ( ⦃?,?⦄ ⊃+ ⦃?,?⦄ )" "fsupp_fsupp" * ]