From: Ferruccio Guidi Date: Wed, 7 Aug 2013 21:38:40 +0000 (+0000) Subject: passive support for global environments completed! X-Git-Tag: make_still_working~1117 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d7ccf1bd91637d3c59a285df6f215ecfde2a2450;p=helm.git passive support for global environments completed! --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index 29d6151fe..0d39f32ec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -12,104 +12,104 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lrsubeqv_4.ma". +include "basic_2/notation/relations/lrsubeqv_5.ma". include "basic_2/dynamic/snv.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) (* Note: this is not transitive *) -inductive lsubsv (h:sh) (g:sd h): relation lenv ≝ -| lsubsv_atom: lsubsv h g (⋆) (⋆) -| lsubsv_pair: ∀I,L1,L2,V. lsubsv h g L1 L2 → - lsubsv h g (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lsubsv_abbr: ∀L1,L2,W,V,W1,V2,l. ⦃h, L1⦄ ⊢ ⓝW.V ¡[h, g] → ⦃h, L2⦄ ⊢ W ¡[h, g] → - ⦃h, L1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ → ⦃h, L2⦄ ⊢ W •[h, g] ⦃l, V2⦄ → - lsubsv h g L1 L2 → lsubsv h g (L1.ⓓⓝW.V) (L2.ⓛW) +inductive lsubsv (h) (g) (G): relation lenv ≝ +| 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,W1,V2,l. ⦃G, L1⦄ ⊢ ⓝW.V ¡[h, g] → ⦃G, L2⦄ ⊢ W ¡[h, g] → + ⦃G, L1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ → ⦃G, L2⦄ ⊢ W •[h, g] ⦃l, V2⦄ → + lsubsv h g G L1 L2 → lsubsv h g G (L1.ⓓⓝW.V) (L2.ⓛW) . interpretation "local environment refinement (stratified native validity)" - 'LRSubEqV h g L1 L2 = (lsubsv h g L1 L2). + 'LRSubEqV h g G L1 L2 = (lsubsv h g G L1 L2). (* Basic inversion lemmas ***************************************************) -fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L1 = ⋆ → L2 = ⋆. -#h #g #L1 #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 | #L1 #L2 #W #V #V1 #V2 #l #_ #_ #_ #_ #_ #H destruct ] qed-. -lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ¡⊑[h, g] L2 → L2 = ⋆. -/2 width=5 by lsubsv_inv_atom1_aux/ qed-. +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,L1,L2. h ⊢ 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. h ⊢ K1 ¡⊑[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃K2,W,V,W1,V2,l. ⦃h, K1⦄ ⊢ X ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] & - ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & - h ⊢ K1 ¡⊑[h, g] K2 & + (∃∃K2. G ⊢ K1 ¡⊑[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ + ∃∃K2,W,V,W1,V2,l. ⦃G, K1⦄ ⊢ X ¡[h, g] & ⦃G, K2⦄ ⊢ W ¡[h, g] & + ⦃G, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃G, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & + G ⊢ K1 ¡⊑[h, g] K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. -#h #g #L1 #L2 * -L1 -L2 +#h #g #G #L1 #L2 * -L1 -L2 [ #J #K1 #X #H destruct | #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/ | #L1 #L2 #W #V #W1 #V2 #l #HV #HW #HW1 #HV2 #HL12 #J #K1 #X #H destruct /3 width=12/ ] qed-. -lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,X. h ⊢ K1.ⓑ{I}X ¡⊑[h, g] L2 → - (∃∃K2. h ⊢ K1 ¡⊑[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃K2,W,V,W1,V2,l. ⦃h, K1⦄ ⊢ X ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] & - ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & - h ⊢ K1 ¡⊑[h, g] K2 & +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,W1,V2,l. ⦃G, K1⦄ ⊢ X ¡[h, g] & ⦃G, K2⦄ ⊢ W ¡[h, g] & + ⦃G, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃G, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & + 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,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L2 = ⋆ → L1 = ⋆. -#h #g #L1 #L2 * -L1 -L2 +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 | #L1 #L2 #W #V #V1 #V2 #l #_ #_ #_ #_ #_ #H destruct ] qed-. -lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ¡⊑[h, g] ⋆ → L1 = ⋆. -/2 width=5 by lsubsv_inv_atom2_aux/ qed-. +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,L1,L2. h ⊢ 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. h ⊢ K1 ¡⊑[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ - ∃∃K1,V,W1,V2,l. ⦃h, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] & - ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & - h ⊢ K1 ¡⊑[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. -#h #g #L1 #L2 * -L1 -L2 + (∃∃K1. G ⊢ K1 ¡⊑[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ + ∃∃K1,V,W1,V2,l. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃G, K2⦄ ⊢ W ¡[h, g] & + ⦃G, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃G, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & + 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/ | #L1 #L2 #W #V #W1 #V2 #l #HV #HW #HW1 #HV2 #HL12 #J #K2 #U #H destruct /3 width=10/ ] qed-. -lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W. h ⊢ L1 ¡⊑[h, g] K2.ⓑ{I}W → - (∃∃K1. h ⊢ K1 ¡⊑[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ - ∃∃K1,V,W1,V2,l. ⦃h, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃h, K2⦄ ⊢ W ¡[h, g] & - ⦃h, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃h, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & - h ⊢ K1 ¡⊑[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. +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,W1,V2,l. ⦃G, K1⦄ ⊢ ⓝW.V ¡[h, g] & ⦃G, K2⦄ ⊢ W ¡[h, g] & + ⦃G, K1⦄ ⊢ V •[h, g] ⦃l+1, W1⦄ & ⦃G, K2⦄ ⊢ W •[h, g] ⦃l, V2⦄ & + G ⊢ K1 ¡⊑[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. /2 width=3 by lsubsv_inv_pair2_aux/ qed-. (* Basic_forward lemmas *****************************************************) -lemma lsubsv_fwd_lsubr: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L1 ⊑ L2. -#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +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,L. h ⊢ L ¡⊑[h, g] L. -#h #g #L elim L -L // /2 width=1/ +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,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → - ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -/3 width=5 by lsubsv_fwd_lsubr, lsubr_cprs_trans/ +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-. 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 30e42ea09..03ef9527c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma @@ -19,7 +19,7 @@ include "basic_2/dynamic/lsubsv.ma". (* Properties on context-sensitive parallel equivalence for terms ***********) -lemma lsubsv_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → - ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2. -/3 width=5 by lsubsv_fwd_lsubr, lsubr_cpcs_trans/ +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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma index 55a7e9a13..d9b21a9f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma @@ -19,38 +19,38 @@ include "basic_2/dynamic/lsubsv_ssta.ma". (* Properties for the preservation results **********************************) -fact lsubsv_sstas_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → - ∀L2,T. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L2, T⦄ → ⦃h, L2⦄ ⊢ T ¡[h, g] → - ∀L1. h ⊢ L1 ¡⊑[h, g] L2 → ∀U2. ⦃h, L2⦄ ⊢ T •*[h, g] U2 → - ∃∃U1. ⦃h, L1⦄ ⊢ T •*[h, g] U1 & L1 ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T #HLT0 #HT #L1 #HL12 #U2 #H @(sstas_ind … H) -U2 [ /2 width=3/ ] +fact lsubsv_sstas_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsubsv h g G1 L1 T1) → + ∀G,L2,T. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L2, T⦄ → ⦃G, L2⦄ ⊢ T ¡[h, g] → + ∀L1. G ⊢ L1 ¡⊑[h, g] L2 → ∀U2. ⦃G, L2⦄ ⊢ T •*[h, g] U2 → + ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, g] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2. +#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L2 #T #HLT0 #HT #L1 #HL12 #U2 #H @(sstas_ind … H) -U2 [ /2 width=3/ ] #U2 #W #l #HTU2 #HU2W * #U1 #HTU1 #HU12 lapply (IH1 … HT … HL12) // #H -lapply (snv_sstas_aux … IH2 … HTU1) // /3 width=4 by ygt_yprs_trans, lsubsv_yprs/ -H #HU1 +lapply (snv_sstas_aux … IH2 … HTU1) // /3 width=5 by ygt_yprs_trans, lsubsv_yprs/ -H #HU1 lapply (snv_sstas_aux … IH2 … HTU2) // #H -lapply (IH1 … H … HL12) [ /3 width=4 by ygt_yprs_trans, sstas_yprs/ ] -H #HU2 +lapply (IH1 … H … HL12) [ /3 width=5 by ygt_yprs_trans, sstas_yprs/ ] -H #HU2 elim (snv_fwd_ssta … HU1) #l1 #W1 #HUW1 elim (lsubsv_ssta_trans … HU2W … HL12) -HU2W #W2 #HUW2 #HW2 elim (ssta_cpcs_lpr_aux … IH4 IH3 … HU1 HU2 … HUW1 … HUW2 … HU12 L1) -HU1 -HU2 -HUW2 -HU12 // -[2,3: /4 width=4 by ygt_yprs_trans, sstas_yprs, lsubsv_yprs/ ] -L2 -L0 -T0 -U2 #H #HW12 destruct +[2,3: /4 width=5 by ygt_yprs_trans, sstas_yprs, lsubsv_yprs/ ] -G0 -L2 -L0 -T0 -U2 #H #HW12 destruct lapply (cpcs_trans … HW12 … HW2) -W2 /3 width=4/ qed-. -fact lsubsv_cpds_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → - ∀L2,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L2, T1⦄ → ⦃h, L2⦄ ⊢ T1 ¡[h, g] → - ∀L1. h ⊢ L1 ¡⊑[h, g] L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[h, g] T2 → - ∃∃T. ⦃h, L1⦄ ⊢ T1 •*➡*[h, g] T & L1 ⊢ T2 ➡* T. -#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2 +fact lsubsv_cpds_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsubsv h g G1 L1 T1) → + ∀G,L2,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G,L2, T1⦄ → ⦃G, L2⦄ ⊢ T1 ¡[h, g] → + ∀L1. G ⊢ L1 ¡⊑[h, g] L2 → ∀T2. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g] T2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] T & ⦃G, L1⦄ ⊢ T2 ➡* T. +#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2 lapply (lsubsv_cprs_trans … HL12 … HTT2) -HTT2 #HTT2 -elim (lsubsv_sstas_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0 +elim (lsubsv_sstas_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -G0 -L2 -L0 -T0 #T0 #HT10 #HT0 lapply (cpcs_cprs_strap1 … HT0 … HTT2) -T #HT02 elim (cpcs_inv_cprs … HT02) -HT02 /3 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma index 31d47c8c5..6d0e6d42d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma @@ -19,10 +19,10 @@ include "basic_2/dynamic/lsubsv.ma". (* Properties concerning basic local environment slicing ********************) (* Note: the constant 0 cannot be generalized *) -lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → +lemma lsubsv_ldrop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 → - ∃∃K2. h ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L2 ≡ K2. -#h #g #L1 #L2 #H elim H -L1 -L2 + ∃∃K2. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L2 ≡ K2. +#h #g #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3/ | #I #L1 #L2 #V #_ #IHL12 #K1 #e #H elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1 @@ -42,10 +42,10 @@ lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → qed-. (* Note: the constant 0 cannot be generalized *) -lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → +lemma lsubsv_ldrop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⊑[h, g] L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. h ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L1 ≡ K1. -#h #g #L1 #L2 #H elim H -L1 -L2 + ∃∃K1. G ⊢ K1 ¡⊑[h, g] K2 & ⇩[0, e] L1 ≡ K1. +#h #g #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3/ | #I #L1 #L2 #V #_ #IHL12 #K2 #e #H elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2 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 7d40d4081..27da78fca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma @@ -19,8 +19,8 @@ include "basic_2/dynamic/lsubsv.ma". (* Forward lemmas on lenv refinement for atomic arity assignment ************) -lemma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[h, g] L2 → L1 ⁝⊑ L2. -#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +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 #W1 #V2 #l #HV #HW #_ #_ #_ #IHL12 -W1 -V2 elim (snv_fwd_aaa … HV) -HV #A #HV elim (snv_fwd_aaa … HW) -HW #B #HW diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma index 67230d980..840e4a31a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma @@ -20,14 +20,14 @@ include "basic_2/dynamic/lsubsv_cpcs.ma". (* Properties concerning stratified native validity *************************) -fact snv_lsubsv_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → - ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_lsubsv h g L1 T1. -#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 * * [||||*] // -[ #i #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 +fact snv_lsubsv_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsubsv h g G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lsubsv h g G1 L1 T1. +#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L2 * * [||||*] // +[ #i #HG0 #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 elim (snv_inv_lref … H) -H #I2 #K2 #W2 #HLK2 #HW2 elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -HL12 #X #H #HLK1 elim (lsubsv_inv_pair2 … H) -H * #K1 @@ -35,11 +35,11 @@ fact snv_lsubsv_aux: ∀h,g,L0,T0. /5 width=8 by snv_lref, fsupp_ygt, fsupp_lref/ (**) (* auto too slow without trace *) | #V #W1 #V2 #l #HV #_ #_ #_ #_ #_ #H destruct /2 width=5/ ] -| #p #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 -IH1 +| #p #HG0 #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 -IH1 elim (snv_inv_gref … H) -| #a #I #V #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 +| #a #I #V #T #HG0 #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 elim (snv_inv_bind … H) -H /4 width=4/ -| #V #T #HL0 #HT0 #H #L1 #HL12 destruct +| #V #T #HG0 #HL0 #HT0 #H #L1 #HL12 destruct elim (snv_inv_appl … H) -H #a #W #W0 #U #l #HV #HT #HVW #HW0 #HTU lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0 elim (lsubsv_ssta_trans … HVW … HL12) -HVW #W1 #HVW1 #HW1 @@ -50,7 +50,7 @@ fact snv_lsubsv_aux: ∀h,g,L0,T0. elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0 lapply (cpds_cprs_trans … (ⓛ{a}W0.U2) HTU ?) [ /2 width=1/ ] -HTU -HW0 /4 width=8 by snv_appl, fsupp_ygt/ (**) (* auto too slow without trace *) -| #W #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 +| #W #T #HG0 #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 elim (snv_inv_cast … H) -H #U #l #HW #HT #HTU #HUW lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW elim (lsubsv_ssta_trans … HTU … HL12) -HTU #U0 #HTU0 #HU0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma index 15f2e14b7..dc922ff54 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma @@ -20,12 +20,12 @@ include "basic_2/dynamic/lsubsv_ldrop.ma". (* Properties on stratified static type assignment **************************) -lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[h, g] ⦃l, U2⦄ → - ∀L1. h ⊢ L1 ¡⊑[h, g] L2 → - ∃∃U1. ⦃h, L1⦄ ⊢ T •[h, g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2. -#h #g #L2 #T #U #l #H elim H -L2 -T -U -l +lemma lsubsv_ssta_trans: ∀h,g,G,L2,T,U2,l. ⦃G, L2⦄ ⊢ T •[h, g] ⦃l, U2⦄ → + ∀L1. G ⊢ L1 ¡⊑[h, g] L2 → + ∃∃U1. ⦃G, L1⦄ ⊢ T •[h, g] ⦃l, U1⦄ & ⦃G, L1⦄ ⊢ U1 ⬌* U2. +#h #g #G #L2 #T #U #l #H elim H -G -L2 -T -U -l [ /3 width=3/ -| #L2 #K2 #X #Y #U #i #l #HLK2 #_ #HYU #IHXY #L1 #HL12 +| #G #L2 #K2 #X #Y #U #i #l #HLK2 #_ #HYU #IHXY #L1 #HL12 elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HYU -IHXY -HLK1 ] [ #HK12 #H destruct @@ -34,7 +34,7 @@ lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[h, g] ⦃l, U2 elim (lift_total T 0 (i+1)) /3 width=11/ | #V #W1 #V2 #l0 #_ #_ #_ #_ #_ #H destruct ] -| #L2 #K2 #Y #X #U #i #l #HLK2 #HYX #HYU #IHYX #L1 #HL12 +| #G #L2 #K2 #Y #X #U #i #l #HLK2 #HYX #HYU #IHYX #L1 #HL12 elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 elim (lsubsv_inv_pair2 … H) -H * #K1 [ -HYX | -IHYX ] [ #HK12 #H destruct @@ -47,11 +47,11 @@ lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[h, g] ⦃l, U2 elim (lift_total W 0 (i+1)) /4 width=11 by cpcs_lift, ex2_intro, ssta_ldef, ssta_cast/ ] -| #a #I #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12 +| #a #I #G #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12 elim (IHTU2 (L1.ⓑ{I}V2) …) [2: /2 width=1/ ] -L2 /3 width=3/ -| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12 +| #G #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12 elim (IHTU2 … HL12) -L2 /3 width=5/ -| #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12 +| #G #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #HL12 elim (IHTU2 … HL12) -L2 /3 width=3/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma index 3f62cff77..a60c3cd7d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma @@ -12,118 +12,119 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/nativevalid_4.ma". +include "basic_2/notation/relations/nativevalid_5.ma". include "basic_2/computation/cpds.ma". include "basic_2/equivalence/cpcs.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) -inductive snv (h:sh) (g:sd h): lenv → predicate term ≝ -| snv_sort: ∀L,k. snv h g L (⋆k) -| snv_lref: ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g K V → snv h g L (#i) -| snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T) -| snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T → +(* activate genv *) +inductive snv (h:sh) (g:sd h): relation3 genv lenv term ≝ +| snv_sort: ∀G,L,k. snv h g G L (⋆k) +| snv_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g G K V → snv h g G L (#i) +| snv_bind: ∀a,I,G,L,V,T. snv h g G L V → snv h g G (L.ⓑ{I}V) T → snv h g G L (ⓑ{a,I}V.T) +| snv_appl: ∀a,G,L,V,W,W0,T,U,l. snv h g G L V → snv h g G L T → ⦃G, L⦄ ⊢ V •[h, g] ⦃l+1, W⦄ → ⦃G, L⦄ ⊢ W ➡* W0 → - ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g L (ⓐV.T) -| snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T → - ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ → ⦃G, L⦄ ⊢ U ⬌* W → snv h g L (ⓝW.T) + ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U → snv h g G L (ⓐV.T) +| snv_cast: ∀G,L,W,T,U,l. snv h g G L W → snv h g G L T → + ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ → ⦃G, L⦄ ⊢ U ⬌* W → snv h g G L (ⓝW.T) . interpretation "stratified native validity (term)" - 'NativeValid h g L T = (snv h g L T). + 'NativeValid h g G L T = (snv h g G L T). (* Basic inversion lemmas ***************************************************) -fact snv_inv_lref_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i → - ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ¡[h, g]. -#h #g #L #X * -L -X -[ #L #k #i #H destruct -| #I #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5/ -| #a #I #L #V #T #_ #_ #i #H destruct -| #a #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #i #H destruct -| #L #W #T #U #l #_ #_ #_ #_ #i #H destruct +fact snv_inv_lref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀i. X = #i → + ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. +#h #g #G #L #X * -G -L -X +[ #G #L #k #i #H destruct +| #I #G #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5/ +| #a #I #G #L #V #T #_ #_ #i #H destruct +| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #i #H destruct +| #G #L #W #T #U #l #_ #_ #_ #_ #i #H destruct ] -qed. - -lemma snv_inv_lref: ∀h,g,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] → - ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ¡[h, g]. -/2 width=3/ qed-. - -fact snv_inv_gref_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥. -#h #g #L #X * -L -X -[ #L #k #p #H destruct -| #I #L #K #V #i #_ #_ #p #H destruct -| #a #I #L #V #T #_ #_ #p #H destruct -| #a #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #p #H destruct -| #L #W #T #U #l #_ #_ #_ #_ #p #H destruct +qed-. + +lemma snv_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ #i ¡[h, g] → + ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ¡[h, g]. +/2 width=3 by snv_inv_lref_aux/ qed-. + +fact snv_inv_gref_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀p. X = §p → ⊥. +#h #g #G #L #X * -G -L -X +[ #G #L #k #p #H destruct +| #I #G #L #K #V #i #_ #_ #p #H destruct +| #a #I #G #L #V #T #_ #_ #p #H destruct +| #a #G #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #p #H destruct +| #G #L #W #T #U #l #_ #_ #_ #_ #p #H destruct ] -qed. - -lemma snv_inv_gref: ∀h,g,L,p. ⦃G, L⦄ ⊢ §p ¡[h, g] → ⊥. -/2 width=7/ qed-. - -fact snv_inv_bind_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → - ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. -#h #g #L #X * -L -X -[ #L #k #a #I #V #T #H destruct -| #I0 #L #K #V0 #i #_ #_ #a #I #V #T #H destruct -| #b #I0 #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1/ -| #b #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct -| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #a #I #V #T #H destruct +qed-. + +lemma snv_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ §p ¡[h, g] → ⊥. +/2 width=8 by snv_inv_gref_aux/ qed-. + +fact snv_inv_bind_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → + ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. +#h #g #G #L #X * -G -L -X +[ #G #L #k #a #I #V #T #H destruct +| #I0 #G #L #K #V0 #i #_ #_ #a #I #V #T #H destruct +| #b #I0 #G #L #V0 #T0 #HV0 #HT0 #a #I #V #T #H destruct /2 width=1/ +| #b #G #L #V0 #W0 #W00 #T0 #U0 #l #_ #_ #_ #_ #_ #a #I #V #T #H destruct +| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #a #I #V #T #H destruct ] -qed. +qed-. -lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, g] → - ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. -/2 width=4/ qed-. +lemma snv_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, g] → + ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. +/2 width=4 by snv_inv_bind_aux/ qed-. -fact snv_inv_appl_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T → +fact snv_inv_appl_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T → ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & ⦃G, L⦄ ⊢ V •[h, g] ⦃l+1, W⦄ & ⦃G, L⦄ ⊢ W ➡* W0 & ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. -#h #g #L #X * -L -X -[ #L #k #V #T #H destruct -| #I #L #K #V0 #i #_ #_ #V #T #H destruct -| #a #I #L #V0 #T0 #_ #_ #V #T #H destruct -| #a #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8/ -| #L #W0 #T0 #U0 #l #_ #_ #_ #_ #V #T #H destruct +#h #g #G #L #X * -L -X +[ #G #L #k #V #T #H destruct +| #I #G #L #K #V0 #i #_ #_ #V #T #H destruct +| #a #I #G #L #V0 #T0 #_ #_ #V #T #H destruct +| #a #G #L #V0 #W0 #W00 #T0 #U0 #l #HV0 #HT0 #HVW0 #HW00 #HTU0 #V #T #H destruct /2 width=8/ +| #G #L #W0 #T0 #U0 #l #_ #_ #_ #_ #V #T #H destruct ] -qed. +qed-. -lemma snv_inv_appl: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] → +lemma snv_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] → ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & ⦃G, L⦄ ⊢ V •[h, g] ⦃l+1, W⦄ & ⦃G, L⦄ ⊢ W ➡* W0 & ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. -/2 width=3/ qed-. +/2 width=3 by snv_inv_appl_aux/ qed-. -fact snv_inv_cast_aux: ∀h,g,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T → +fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T → ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ & ⦃G, L⦄ ⊢ U ⬌* W. -#h #g #L #X * -L -X -[ #L #k #W #T #H destruct -| #I #L #K #V #i #_ #_ #W #T #H destruct -| #a #I #L #V #T0 #_ #_ #W #T #H destruct -| #a #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #W #T #H destruct -| #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HUW0 #W #T #H destruct /2 width=4/ +#h #g #G #L #X * -G -L -X +[ #G #L #k #W #T #H destruct +| #I #G #L #K #V #i #_ #_ #W #T #H destruct +| #a #I #G #L #V #T0 #_ #_ #W #T #H destruct +| #a #G #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #W #T #H destruct +| #G #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HUW0 #W #T #H destruct /2 width=4/ ] -qed. +qed-. -lemma snv_inv_cast: ∀h,g,L,W,T. ⦃G, L⦄ ⊢ ⓝW.T ¡[h, g] → +lemma snv_inv_cast: ∀h,g,G,L,W,T. ⦃G, L⦄ ⊢ ⓝW.T ¡[h, g] → ∃∃U,l. ⦃G, L⦄ ⊢ W ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ & ⦃G, L⦄ ⊢ U ⬌* W. -/2 width=3/ qed-. +/2 width=3 by snv_inv_cast_aux/ qed-. (* Basic forward lemmas *****************************************************) -lemma snv_fwd_ssta: ∀h,g,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃∃l,U. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄. -#h #g #L #T #H elim H -L -T -[ #L #k elim (deg_total h g k) /3 width=3/ -| * #L #K #V #i #HLK #_ * #l0 #W #HVW +lemma snv_fwd_ssta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃∃l,U. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄. +#h #g #G #L #T #H elim H -G -L -T +[ #G #L #k elim (deg_total h g k) /3 width=3/ +| * #G #L #K #V #i #HLK #_ * #l0 #W #HVW [ elim (lift_total W 0 (i+1)) /3 width=8/ | elim (lift_total V 0 (i+1)) /3 width=8/ ] -| #a #I #L #V #T #_ #_ #_ * /3 width=3/ -| #a #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/ -| #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *) +| #a #I #G #L #V #T #_ #_ #_ * /3 width=3/ +| #a #G #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/ +| #G #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *) ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma index 3a161e1f9..6a823189a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma @@ -21,21 +21,21 @@ include "basic_2/dynamic/snv.ma". (* Forward lemmas on atomic arity assignment for terms **********************) -lemma snv_fwd_aaa: ∀h,g,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A. -#h #g #L #T #H elim H -L -T +lemma snv_fwd_aaa: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∃A. ⦃G, L⦄ ⊢ T ⁝ A. +#h #g #G #L #T #H elim H -G -L -T [ /2 width=2/ -| #I #L #K #V #i #HLK #_ * /3 width=6/ -| #a * #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/ -| #a #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT +| #I #G #L #K #V #i #HLK #_ * /3 width=6/ +| #a * #G #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/ +| #a #G #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT lapply (cpds_aaa h g … HV W0 ?) [ -HTU /3 width=4/ ] -W #HW0 (**) (* auto fail without -HTU *) lapply (cpds_aaa … HT … HTU) -HTU #H elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/ -| #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT +| #G #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT lapply (aaa_cpcs_mono … HUW A … HW) -HUW /2 width=7/ -HTU #H destruct /3 width=3/ ] qed-. -lemma snv_fwd_csn: ∀h,g,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -#h #g #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/ +lemma snv_fwd_csn: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +#h #g #G #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma index 8aaf788a2..d5d16cafa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -21,64 +21,64 @@ include "basic_2/dynamic/ygt.ma". (* Inductive premises for the preservation results **************************) -definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[h, g] → - ∀T2. L1 ⊢ T1 ➡ T2 → ∀L2. L1 ⊢ ➡ L2 → ⦃h, L2⦄ ⊢ T2 ¡[h, g]. - -definition IH_ssta_cpr_lpr: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[h, g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ → - ∀T2. L1 ⊢ T1 ➡ T2 → ∀L2. L1 ⊢ ➡ L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. - -definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → +definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. + +definition IH_ssta_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀U1,l. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ & ⦃G, L2⦄ ⊢ U1 ⬌* U2. + +definition IH_snv_ssta: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∀U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄ → ⦃G, L⦄ ⊢ U ¡[h, g]. -definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L2,T. ⦃h, L2⦄ ⊢ T ¡[h, g] → - ∀L1. h ⊢ L1 ¡⊑[h, g] L2 → ⦃h, L1⦄ ⊢ T ¡[h, g]. +definition IH_snv_lsubsv: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] → + ∀L1. G ⊢ L1 ¡⊑[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g]. (* Properties for the preservation results **********************************) -fact snv_cprs_lpr_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[h, g] → - ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → ⦃h, L2⦄ ⊢ T2 ¡[h, g]. -#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #T2 #H +fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. +#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H elim H -T2 [ /2 width=6/ ] -HT1 /4 width=6 by ygt_yprs_trans, cprs_yprs/ qed-. -fact ssta_cprs_lpr_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[h, g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ → - ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #T2 #H +fact ssta_cprs_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀U1,l. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #T2 #H elim H -T2 [ /2 width=7/ ] #T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 elim (IHT1 L1) // -IHT1 #U #HTU #HU1 elim (IH1 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 -[2: /3 width=9 by snv_cprs_lpr_aux/ +[2: /3 width=10 by snv_cprs_lpr_aux/ |3: /5 width=6 by ygt_yprs_trans, cprs_yprs/ -] -L0 -T0 -T1 -T #U2 #HTU2 #HU2 +] -G0 -L0 -T0 -T1 -T #U2 #HTU2 #HU2 lapply (lpr_cpcs_conf … HL12 … HU1) -L1 #HU1 lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/ qed-. -fact ssta_cpcs_lpr_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - ∀L1,T1,T2. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T2⦄ → - ⦃h, L1⦄ ⊢ T1 ¡[h, g] → ⦃h, L1⦄ ⊢ T2 ¡[h, g] → - ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l1, U1⦄ → - ∀U2,l2. ⦃h, L1⦄ ⊢ T2 •[h, g] ⦃l2, U2⦄ → - L1 ⊢ T1 ⬌* T2 → ∀L2. L1 ⊢ ➡ L2 → - l1 = l2 ∧ L2 ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #T2 #H01 #H02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H #L2 #HL12 +fact ssta_cpcs_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1,T2. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T2⦄ → + ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → + ∀U1,l1. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l1, U1⦄ → + ∀U2,l2. ⦃G, L1⦄ ⊢ T2 •[h, g] ⦃l2, U2⦄ → + ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + l1 = l2 ∧ ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #T2 #H01 #H02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H #L2 #HL12 elim (cpcs_inv_cprs … H) -H #T #H1 #H2 elim (ssta_cprs_lpr_aux … H01 HT1 … HTU1 … H1 … HL12) -T1 /2 width=1/ #W1 #H1 #HUW1 elim (ssta_cprs_lpr_aux … H02 HT2 … HTU2 … H2 … HL12) -T2 /2 width=1/ #W2 #H2 #HUW2 -L0 -T0 @@ -86,71 +86,71 @@ elim (ssta_mono … H1 … H2) -h -T #H1 #H2 destruct lapply (cpcs_canc_dx … HUW1 … HUW2) -W2 /2 width=1/ qed-. -fact snv_sstas_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - ∀L,T. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → +fact snv_sstas_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + ∀G,L,T. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → ∀U. ⦃G, L⦄ ⊢ T •*[h, g] U → ⦃G, L⦄ ⊢ U ¡[h, g]. -#h #g #L0 #T0 #IH #L #T #H01 #HT #U #H +#h #g #G0 #L0 #T0 #IH #G #L #T #H01 #HT #U #H @(sstas_ind … H) -U // -HT /4 width=5 by ygt_yprs_trans, sstas_yprs/ qed-. -fact snv_sstas_lpr_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - ∀L1,T. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T⦄ → ⦃h, L1⦄ ⊢ T ¡[h, g] → - ∀U. ⦃h, L1⦄ ⊢ T •*[h, g] U → ∀L2. L1 ⊢ ➡ L2 → ⦃h, L2⦄ ⊢ U ¡[h, g]. -/4 width=7 by snv_sstas_aux, ygt_yprs_trans, sstas_yprs/ +fact snv_sstas_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + ∀G,L1,T. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T⦄ → ⦃G, L1⦄ ⊢ T ¡[h, g] → + ∀U. ⦃G, L1⦄ ⊢ T •*[h, g] U → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U ¡[h, g]. +/4 width=8 by snv_sstas_aux, ygt_yprs_trans, sstas_yprs/ qed-. -fact sstas_cprs_lpr_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[h, g] → - ∀U1. ⦃h, L1⦄ ⊢ T1 •*[h, g] U1 → ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[h, g] U2 & L2 ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #H +fact sstas_cprs_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, g] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #H @(sstas_ind … H) -U1 [ /3 width=5 by lpr_cprs_conf, ex2_intro/ ] #U1 #W1 #l1 #HTU1 #HUW1 #IHTU1 #T2 #HT12 #L2 #HL12 elim (IHTU1 … HT12 … HL12) -IHTU1 #U2 #HTU2 #HU12 lapply (snv_cprs_lpr_aux … IH2 … HT1 … HT12 … HL12) // #HT2 elim (snv_sstas_fwd_correct … HTU2) // #W2 #l2 #HUW2 elim (IH1 … HUW1 U1 … HL12) -HUW1 // -[2: /3 width=7 by snv_sstas_aux/ -|3: /3 width=4 by ygt_yprs_trans, sstas_yprs/ +[2: /3 width=8 by snv_sstas_aux/ +|3: /3 width=5 by ygt_yprs_trans, sstas_yprs/ ] #W #HU1W #HW1 elim (ssta_cpcs_lpr_aux … IH2 IH1 … HU1W … HUW2 … HU12 L2) // -IH1 -HU1W -HU12 -[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, cprs_lpr_yprs/ -|3: /3 width=10 by snv_sstas_lpr_aux/ +[2: /4 width=9 by snv_sstas_aux, ygt_yprs_trans, cprs_lpr_yprs/ +|3: /3 width=11 by snv_sstas_lpr_aux/ |4,5: /4 width=5 by ygt_yprs_trans, cprs_lpr_yprs, sstas_yprs/ -] -L0 -T0 -L1 -T1 -HT2 #H #HW12 destruct +] -G0 -L0 -T0 -L1 -T1 -HT2 #H #HW12 destruct lapply (cpcs_trans … HW1 … HW12) -W /3 width=4/ qed-. -fact cpds_cprs_lpr_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[h, g] → - ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[h, g] U1 → - ∀T2. L1 ⊢ T1 ➡* T2 → ∀L2. L1 ⊢ ➡ L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[h, g] U2 & L2 ⊢ U1 ➡* U2. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 +fact cpds_cprs_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. +#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 elim (sstas_cprs_lpr_aux … IH3 IH2 IH1 … H01 … HTW1 … HT12 … HL12) // -L0 -T0 -T1 #W2 #HTW2 #HW12 lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H elim (cpcs_inv_cprs … H) -H /3 width=3/ qed-. -fact ssta_cpds_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - ∀L,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → +fact ssta_cpds_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → ∀l,U1. ⦃G, L⦄ ⊢ T1 •[h, g] ⦃l+1, U1⦄ → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → ∃∃U,U2. ⦃G, L⦄ ⊢ U1 •*[h, g] U & ⦃G, L⦄ ⊢ T2 •*[h, g] U2 & ⦃G, L⦄ ⊢ U ⬌* U2. -#h #g #L0 #T0 #IH2 #IH1 #L #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2 +#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2 elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ] -[ elim (ssta_cprs_lpr_aux … IH2 IH1 … HTU1 … HTT2 L) // -L0 -T0 -T /3 width=5/ +[ elim (ssta_cprs_lpr_aux … IH2 IH1 … HTU1 … HTT2 L) // -G0 -L0 -T0 -T /3 width=5/ | @(ex3_2_intro …T2 HU1T) // /2 width=1/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma index 9b9513f0a..34e6c2db9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma @@ -20,77 +20,77 @@ include "basic_2/dynamic/snv.ma". (* Relocation properties ****************************************************) -lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊢ T ¡[h, g] → ∀L,d,e. ⇩[d, e] L ≡ K → +lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,d,e. ⇩[d, e] L ≡ K → ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ U ¡[h, g]. -#h #g #K #T #H elim H -K -T -[ #K #k #L #d #e #_ #X #H +#h #g #G #K #T #H elim H -G -K -T +[ #G #K #k #L #d #e #_ #X #H >(lift_inv_sort1 … H) -X -K -d -e // -| #I #K #K0 #V #i #HK0 #_ #IHV #L #d #e #HLK #X #H +| #I #G #K #K0 #V #i #HK0 #_ #IHV #L #d #e #HLK #X #H elim (lift_inv_lref1 … H) * #Hid #H destruct [ elim (ldrop_trans_le … HLK … HK0) -K /2 width=2/ #X #HL0 #H elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #L0 #W #HLK0 #HVW #H destruct /3 width=8/ | lapply (ldrop_trans_ge … HLK … HK0 ?) -K // -Hid /3 width=8/ ] -| #a #I #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H +| #a #I #G #K #V #T #_ #_ #IHV #IHT #L #d #e #HLK #X #H elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=4/ -| #a #K #V #V0 #V1 #T #T1 #l #_ #_ #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H +| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #HV0 #HV01 #HT1 #IHV #IHT #L #d #e #HLK #X #H elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct elim (lift_total V0 d e) #W0 #HVW0 elim (lift_total V1 d e) #W1 #HVW1 elim (lift_total T1 (d+1) e) #U1 #HTU1 @(snv_appl … a … W0 … W1 … U1 l) [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ] - @(cpds_lift … HLK … HTU … HT1) /2 width=1/ -| #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H + @(cpds_lift … HT1 … HLK … HTU) /2 width=1/ +| #G #K #V0 #T #V #l #_ #_ #HTV #HV0 #IHV0 #IHT #L #d #e #HLK #X #H elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct elim (lift_total V d e) #W #HVW @(snv_cast … W l) [ /2 width=4/ | /2 width=4/ | /2 width=9/ | /2 width=9/ ] ] qed. -lemma snv_inv_lift: ∀h,g,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,d,e. ⇩[d, e] L ≡ K → - ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊢ T ¡[h, g]. -#h #g #L #U #H elim H -L -U -[ #L #k #K #d #e #_ #X #H +lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,d,e. ⇩[d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ T ¡[h, g]. +#h #g #G #L #U #H elim H -G -L -U +[ #G #L #k #K #d #e #_ #X #H >(lift_inv_sort2 … H) -X -L -d -e // -| #I #L #L0 #W #i #HL0 #_ #IHW #K #d #e #HLK #X #H +| #I #G #L #L0 #W #i #HL0 #_ #IHW #K #d #e #HLK #X #H elim (lift_inv_lref2 … H) * #Hid #H destruct [ elim (ldrop_conf_le … HLK … HL0) -L /2 width=2/ #X #HK0 #H elim (ldrop_inv_skip1 … H) -H /2 width=1/ -Hid #K0 #V #HLK0 #HVW #H destruct /3 width=8/ | lapply (ldrop_conf_ge … HLK … HL0 ?) -L // -Hid /3 width=8/ ] -| #a #I #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H +| #a #I #G #L #W #U #_ #_ #IHW #IHU #K #d #e #HLK #X #H elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=4/ -| #a #L #W #W0 #W1 #U #U1 #l #_ #_ #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H +| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #HW0 #HW01 #HU1 #IHW #IHU #K #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct elim (ssta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HV0 #HVW0 elim (cprs_inv_lift1 … HW01 … HLK … HVW0) -W0 #V1 #HVW1 #HV01 - elim (cpds_inv_lift1 … HLK … HTU … HU1) -HU1 #X #H #HTU + elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct lapply (lift_inj … HY … HVW1) -HY #H destruct /3 width=8/ -| #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H +| #G #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HTV #HVW - lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/ + lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W /3 width=4/ ] qed-. (* Advanced properties ******************************************************) -lemma snv_fsup_conf: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → - ⦃h, L1⦄ ⊢ T1 ¡[h, g] → ⦃h, L2⦄ ⊢ T2 ¡[h, g]. -#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 -[ #I1 #L1 #V1 #H +lemma snv_fsup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g]. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I1 #G1 #L1 #V1 #H elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2 lapply (ldrop_inv_O2 … H) -H #H destruct // |2: * |5,6: /3 width=7 by snv_inv_lift/ ] -[1,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // -|2,4: * #L1 #V1 #T1 #H +[1,3: #a #I #G1 #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H // +|2,4: * #G1 #L1 #V1 #T1 #H [1,3: elim (snv_inv_appl … H) -H // |2,4: elim (snv_inv_cast … H) -H // ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index 3007d7d67..8623b0f46 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -20,20 +20,20 @@ include "basic_2/dynamic/snv_cpcs.ma". (* Properties on context-free parallel reduction for local environments *****) -fact snv_cpr_lpr_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g L1 T1. -#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*] -[ #k #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1 +fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsubsv h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g G1 L1 T1. +#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [||||*] +[ #k #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1 >(cpr_inv_sort1 … H2) -X // -| #i #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 +| #i #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - lapply (fsupp_lref … HLK1) #HKL + lapply (fsupp_lref … G1 … HLK1) #HKL elim (cpr_inv_lref1 … H2) -H2 [ #H destruct -HLK1 lapply (IH1 … HV12 … HK12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HKL /2 width=5/ @@ -42,9 +42,9 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0. lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 lapply (IH1 … HVW0 … HK12) -IH1 -HVW0 -HK12 // -HV1 [ /2 width=1/ ] -HKL /3 width=7/ ] -| #p #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1 +| #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 +| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 elim (snv_inv_bind … H1) -H1 #HV1 #HT1 elim (cpr_inv_bind1 … H2) -H2 * [ #V2 #T2 #HV12 #HT12 #H destruct @@ -54,7 +54,7 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0. lapply (IH1 … HT1 … HT12 (L2.ⓓV1) ?) -IH1 [1,2: /2 width=1/ ] -L1 -T1 #HT2 lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/ ] -| #V1 #T1 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1 elim (cpr_inv_appl1 … H2) -H2 * [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 @@ -80,7 +80,7 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0. lapply (IH1 … HW202 … HL12) // [ /2 width=1/ ] -HW20 #HW2 lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) [1,2: /2 width=1/ ] -HT20 #HT2 lapply (IH2 … HV2W3) // - [ @(ygt_yprs_trans … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *) + [ @(ygt_yprs_trans … G1 G1 … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *) [ /2 width=1 by fsupp_ygt/ | /3 width=1 by cprs_lpr_yprs, cpr_cprs/ ] @@ -89,8 +89,8 @@ fact snv_cpr_lpr_aux: ∀h,g,L0,T0. elim (ssta_fwd_correct … HV2W3) [h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ssta h g L1 T1. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [||||*] -[ #k #HL0 #HT0 #_ #X #l #H2 destruct -IH3 -IH2 -IH1 +fact snv_ssta_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_ssta h g G1 L1 T1. +#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [||||*] +[ #k #HG0 #HL0 #HT0 #_ #X #l #H2 destruct -IH3 -IH2 -IH1 elim (ssta_inv_sort1 … H2) -H2 #_ #H destruct // -| #i #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 +| #i #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 elim (ssta_inv_lref1 … H2) -H2 * #K0 #V0 #W1 [| #l ] #H #HVW1 #HX [| #_ ] lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (fsupp_lref … HLK1) #H + lapply (fsupp_lref … G1 … HLK1) #H lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=7/ -| #p #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 -IH1 +| #p #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 +| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 elim (snv_inv_bind … H1) -H1 #HV1 #HT1 elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=5/ -| #V1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct elim (snv_inv_appl … H1) -H1 #a #W1 #W0 #T0 #l0 #HV1 #HT1 #HVW1 #HW10 #HT10 elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct lapply (IH1 … HT1 … HTU1) -IH1 /2 width=1/ #HU1 @@ -47,7 +47,7 @@ fact snv_ssta_aux: ∀h,g,L0,T0. elim (cpcs_inv_abst2 … HU0) -HU0 #W2 #U2 #HU2 #HU02 elim (cprs_inv_abst … HU02) -HU02 #HW02 #_ lapply (cprs_trans … HW10 … HW02) -W0 /3 width=10 by snv_appl, ex2_intro/ (**) (* auto is too slow without trace *) -| #W1 #T1 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 +| #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #HTU1 #HUW1 lapply (ssta_inv_cast1 … H2) -H2 /3 width=5/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma index bb07981b0..28f87d7c4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma @@ -20,21 +20,21 @@ include "basic_2/dynamic/lsubsv_ssta.ma". (* Properties on sn parallel reduction for local environments ***************) -fact ssta_cpr_lpr_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_snv_cpr_lpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[h, g] ⦃L1, T1⦄ → IH_ssta_cpr_lpr h g L1 T1) → - ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_cpr_lpr h g L1 T1. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *] -[ #k #_ #_ #_ #X2 #l #H2 #X3 #H3 #L2 #HL12 -IH3 -IH2 -IH1 +fact ssta_cpr_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_ssta h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, g] ⦃G1, L1, T1⦄ → IH_ssta_cpr_lpr h g G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_ssta_cpr_lpr h g G1 L1 T1. +#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| *] +[ #k #_ #_ #_ #_ #X2 #l #H2 #X3 #H3 #L2 #HL12 -IH3 -IH2 -IH1 elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct >(cpr_inv_sort1 … H3) -X3 /4 width=6/ -| #i #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 +| #i #HG0 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1 elim (ssta_inv_lref1 … H2) -H2 * #K1 #V1 #W1 [| #l0 ] #HLK1 #HVW1 #HWU1 [| #H destruct ] lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (fsupp_lref … HLK1) #HKV1 + lapply (fsupp_lref … G1 … HLK1) #HKV1 elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) #H2 @@ -55,9 +55,9 @@ fact ssta_cpr_lpr_aux: ∀h,g,L0,T0. lapply (ssta_lift … HVW2 … H2 … HW0 … HWU2) -HVW2 -HW0 lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/ ] -| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 +| #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 +| #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 elim (snv_inv_bind … H1) -H1 #_ #HT1 elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct elim (cpr_inv_bind1 … H3) -H3 * @@ -70,7 +70,7 @@ fact ssta_cpr_lpr_aux: ∀h,g,L0,T0. lapply (cpcs_bind1 true … V1 V1 … HU12) // -HU12 #HU12 lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 /2 width=3/ ] -| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct elim (cpr_inv_appl1 … H3) -H3 * @@ -87,7 +87,7 @@ fact ssta_cpr_lpr_aux: ∀h,g,L0,T0. lapply (IH3 … HVW1) -IH3 // [ /2 width=1/ ] #HW1 elim (ssta_cpcs_lpr_aux … IH2 IH1 … HWX1 … HWV22 … L1) -HWX1 // [2: /2 width=1/ - |3: /4 width=4 by ygt_yprs_trans, fsupp_ygt, sstas_yprs, ssta_sstas/ + |3: /4 width=5 by ygt_yprs_trans, fsupp_ygt, sstas_yprs, ssta_sstas/ ] #H #_ destruct -X1 lapply (IH2 … HV1 … HV12 … HL12) [ /2 width=1/ ] #HV2 lapply (IH2 … HW2 … HW20 … HL12) [ /2 width=1/ ] -IH2 #H2W20 @@ -117,7 +117,7 @@ fact ssta_cpr_lpr_aux: ∀h,g,L0,T0. lapply (cpcs_flat … HV10 … HU02 Appl) -HV10 -HU02 #HU02 lapply (cpcs_cpr_strap1 … HU02 (ⓓ{b}W2.ⓐV2.U2) ?) [ /2 width=3/ ] -V0 /4 width=3/ ] -| #U0 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 +| #U0 #T1 #HG0 #HL0 #HT0 #H1 #X2 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 elim (snv_inv_cast … H1) -H1 #T0 #l0 #_ #HT1 #HT10 #_ lapply (ssta_inv_cast1 … H2) -H2 #HTU1 elim (ssta_mono … HT10 … HTU1) -HT10 #H1 #H2 destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma index bc2d74497..da5a4c9cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma @@ -19,8 +19,8 @@ include "basic_2/dynamic/snv.ma". (* Forward_lemmas on iterated stratified static type assignment for terms ***) -lemma snv_sstas_fwd_correct: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ⦃G, L⦄ ⊢ T1 •* [h, g] T2 → +lemma snv_sstas_fwd_correct: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ⦃G, L⦄ ⊢ T1 •* [h, g] T2 → ∃∃U2,l. ⦃G, L⦄ ⊢ T2 •[h, g] ⦃l, U2⦄. -#h #g #L #T1 #T2 #HT1 #HT12 +#h #g #G #L #T1 #T2 #HT1 #HT12 elim (snv_fwd_ssta … HT1) -HT1 /2 width=5 by sstas_fwd_correct/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma index 7b50bfdcf..0e4ed9f64 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma @@ -12,67 +12,67 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btpredstarproper_6.ma". +include "basic_2/notation/relations/btpredstarproper_8.ma". include "basic_2/dynamic/ysc.ma". include "basic_2/dynamic/yprs.ma". (* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************) -inductive ygt (h) (g) (L1) (T1): relation2 lenv term ≝ -| ygt_inj : ∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≻[h, g] ⦃L2, T2⦄ → - ygt h g L1 T1 L2 T2 -| ygt_step: ∀L,L2,T. ygt h g L1 T1 L T → ⦃G, L⦄ ⊢ ➡ L2 → ygt h g L1 T1 L2 T +inductive ygt (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| ygt_inj : ∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + ygt h g G1 L1 T1 G2 L2 T2 +| ygt_step: ∀G,L,L2,T. ygt h g G1 L1 T1 G L T → ⦃G, L⦄ ⊢ ➡ L2 → ygt h g G1 L1 T1 G L2 T . interpretation "'big tree' proper parallel computation (closure)" - 'BTPRedStarProper h g L1 T1 L2 T2 = (ygt h g L1 T1 L2 T2). + 'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (ygt h g G1 L1 T1 G2 L2 T2). (* Basic forvard lemmas *****************************************************) -lemma ygt_fwd_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H elim H -L2 -T2 -/3 width=4 by yprs_strap1, ysc_ypr, ypr_lpr/ +lemma ygt_fwd_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 +/3 width=5 by yprs_strap1, ysc_ypr, ypr_lpr/ qed-. (* Basic properties *********************************************************) -lemma ysc_ygt: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[h, g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄. -/3 width=4/ qed. +lemma ysc_ygt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +/3 width=5/ qed. -lemma ygt_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ ≽[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄. -#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 +lemma ygt_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 lapply (ygt_fwd_yprs … H1) #H0 -elim (ypr_inv_ysc … H2) -H2 [| * #HL2 #H destruct ] /2 width=4/ +elim (ypr_inv_ysc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] /2 width=5/ qed-. -lemma ygt_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ >[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄. -#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -L2 -T2 -[ /3 width=4 by ygt_inj, yprs_strap2/ | /2 width=3/ ] +lemma ygt_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -G2 -L2 -T2 +[ /3 width=5 by ygt_inj, yprs_strap2/ | /2 width=3/ ] qed-. -lemma ygt_yprs_trans: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ ≥[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄. -#h #g #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -L2 -T2 // -/2 width=4 by ygt_strap1/ +lemma ygt_yprs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -G2 -L2 -T2 // +/2 width=5 by ygt_strap1/ qed-. -lemma yprs_ygt_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L, T⦄ → - ∀L2,T2. h ⊢ ⦃L, T⦄ >[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄. -#h #g #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -L -T // -/3 width=4 by ygt_strap2/ +lemma yprs_ygt_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → + ∀G2,L2,T2. ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -G -L -T // +/3 width=5 by ygt_strap2/ qed-. -lemma fsupp_ygt: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[h, g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/ +lemma fsupp_ygt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 /3 width=1/ /3 width=5/ qed. -lemma cprs_ygt: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → - h ⊢ ⦃L, T1⦄ >[h, g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 +lemma cprs_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → + ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. +#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 [ #H elim H // | #T #T2 #_ #HT2 #IHT1 #HT12 elim (term_eq_dec T1 T) #H destruct @@ -83,9 +83,9 @@ lemma cprs_ygt: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) ] qed. -lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → (T1 = T2 → ⊥) → - h ⊢ ⦃L, T1⦄ >[h, g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 +lemma sstas_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → (T1 = T2 → ⊥) → + ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. +#h #g #G #L #T1 #T2 #H @(sstas_ind … H) -T2 [ #H elim H // | #T #T2 #l #_ #HT2 #IHT1 #HT12 -HT12 elim (term_eq_dec T1 T) #H destruct @@ -96,6 +96,6 @@ lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → (T1 = T2 ] qed. -lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → - h ⊢ ⦃L1, T⦄ >[h, g] ⦃L2, T⦄. +lemma lsubsv_ygt: ∀h,g,G,L1,L2,T. G ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → + ⦃G, L1, T⦄ >[h, g] ⦃G, L2, T⦄. /4 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma index 99deeefb1..443dbcbf0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma @@ -18,5 +18,5 @@ include "basic_2/dynamic/ygt.ma". (* Main properties **********************************************************) -theorem ygt_trans: ∀h,g. bi_transitive … (ygt h g). -/3 width=4 by ygt_fwd_yprs, ygt_yprs_trans/ qed-. +theorem ygt_trans: ∀h,g. tri_transitive … (ygt h g). +/3 width=5 by ygt_fwd_yprs, ygt_yprs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma index 84879b10a..2c8c96d27 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma @@ -12,26 +12,26 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btpred_6.ma". +include "basic_2/notation/relations/btpred_8.ma". include "basic_2/relocation/fsup.ma". include "basic_2/reduction/lpr.ma". include "basic_2/dynamic/lsubsv.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) -inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝ -| ypr_fsup : ∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2 -| ypr_lpr : ∀L2. L1 ⊢ ➡ L2 → ypr h g L1 T1 L2 T1 -| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2 -| ypr_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l+1, T2⦄ → ypr h g L1 T1 L1 T2 -| ypr_lsubsv: ∀L2. h ⊢ L2 ¡⊑[h, g] L1 → ypr h g L1 T1 L2 T1 +inductive ypr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| ypr_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ypr h g G1 L1 T1 G2 L2 T2 +| ypr_lpr : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → ypr h g G1 L1 T1 G1 L2 T1 +| ypr_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → ypr h g G1 L1 T1 G1 L1 T2 +| ypr_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 •[h, g] ⦃l+1, T2⦄ → ypr h g G1 L1 T1 G1 L1 T2 +| ypr_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → ypr h g G1 L1 T1 G1 L2 T1 . interpretation "'big tree' parallel reduction (closure)" - 'BTPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2). + 'BTPRed h g G1 L1 T1 G2 L2 T2 = (ypr h g G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g). +lemma ypr_refl: ∀h,g. tri_reflexive … (ypr h g). /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma index a8be72e72..c055f6040 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma @@ -12,71 +12,71 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btpredstar_6.ma". +include "basic_2/notation/relations/btpredstar_8.ma". include "basic_2/substitution/fsupp.ma". include "basic_2/computation/lprs.ma". include "basic_2/dynamic/ypr.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) -definition yprs: ∀h. sd h → bi_relation lenv term ≝ - λh,g. bi_TC … (ypr h g). +definition yprs: ∀h. sd h → tri_relation genv lenv term ≝ + λh,g. tri_TC … (ypr h g). interpretation "'big tree' parallel computation (closure)" - 'BTPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2). + 'BTPRedStar h g G1 L1 T1 G2 L2 T2 = (yprs h g G1 L1 T1 G2 L2 T2). (* Basic eliminators ********************************************************) -lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 → - (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≽[h, g] ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄ → R L2 T2. -/3 width=7 by bi_TC_star_ind/ qed-. +lemma yprs_ind: ∀h,g,G1,L1,T1. ∀R:relation3 genv lenv term. R G1 L1 T1 → + (∀L,G2,G,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. +/3 width=8 by tri_TC_star_ind/ qed-. -lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 → - (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≥[h, g] ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄ → R L1 T1. -/3 width=7 by bi_TC_star_ind_dx/ qed-. +lemma yprs_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1. +/3 width=8 by tri_TC_star_ind_dx/ qed-. (* Basic properties *********************************************************) -lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g). +lemma yprs_refl: ∀h,g. tri_reflexive … (yprs h g). /2 width=1/ qed. -lemma ypr_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄. +lemma ypr_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. /2 width=1/ qed. -lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ ≽[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄. -/2 width=4/ qed-. +lemma yprs_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/2 width=5/ qed-. -lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ ≥[h, g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄. -/2 width=4/ qed-. +lemma yprs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/2 width=5/ qed-. (* Note: this is a general property of bi_TC *) -lemma fsupp_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/ +lemma fsupp_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 /3 width=1/ /3 width=5/ qed. -lemma cprs_yprs: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[h, g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4 by ypr_cpr, yprs_strap1/ +lemma cprs_yprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. +#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=5 by ypr_cpr, yprs_strap1/ qed. -lemma lprs_yprs: ∀h,g,L1,L2,T. L1 ⊢ ➡* L2 → h ⊢ ⦃L1, T⦄ ≥[h, g] ⦃L2, T⦄. -#h #g #L1 #L2 #T #H @(lprs_ind … H) -L2 // /3 width=4 by ypr_lpr, yprs_strap1/ +lemma lprs_yprs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. +#h #g #G #L1 #L2 #T #H @(lprs_ind … H) -L2 // /3 width=5 by ypr_lpr, yprs_strap1/ qed. -lemma sstas_yprs: ∀h,g,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → - h ⊢ ⦃L, T1⦄ ≥[h, g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=4 by ypr_ssta, yprs_strap1/ +lemma sstas_yprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, g] T2 → + ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. +#h #g #G #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=5 by ypr_ssta, yprs_strap1/ qed. -lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[h, g] L1 → h ⊢ ⦃L1, T⦄ ≥[h, g] ⦃L2, T⦄. +lemma lsubsv_yprs: ∀h,g,G,L1,L2,T. G ⊢ L2 ¡⊑[h, g] L1 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. /3 width=1/ qed. -lemma cprs_lpr_yprs: ∀h,g,L1,L2,T1,T2. L1 ⊢ T1 ➡* T2 → L1 ⊢ ➡ L2 → - h ⊢ ⦃L1, T1⦄ ≥[h, g] ⦃L2, T2⦄. -/3 width=4 by yprs_strap1, ypr_lpr, cprs_yprs/ +lemma cprs_lpr_yprs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄. +/3 width=5 by yprs_strap1, ypr_lpr, cprs_yprs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma index 96354706d..d05f23c7c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma @@ -16,5 +16,5 @@ include "basic_2/dynamic/yprs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) -theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g). -/2 width=4/ qed-. +theorem yprs_trans: ∀h,g. tri_transitive … (yprs h g). +/2 width=5/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma index 09785875c..2d4d80bc5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma @@ -12,34 +12,35 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btpredproper_6.ma". +include "basic_2/notation/relations/btpredproper_8.ma". include "basic_2/dynamic/ypr.ma". (* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) -inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝ -| ysc_fsup : ∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ysc h g L1 T1 L2 T2 -| ysc_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2 -| ysc_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l+1, T2⦄ → ysc h g L1 T1 L1 T2 -| ysc_lsubsv: ∀L2. h ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1 +inductive ysc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| ysc_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ysc h g G1 L1 T1 G2 L2 T2 +| ysc_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g G1 L1 T1 G1 L1 T2 +| ysc_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 •[h, g] ⦃l+1, T2⦄ → ysc h g G1 L1 T1 G1 L1 T2 +| ysc_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → ysc h g G1 L1 T1 G1 L2 T1 . interpretation "'big tree' proper parallel reduction (closure)" - 'BTPRedProper h g L1 T1 L2 T2 = (ysc h g L1 T1 L2 T2). + 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (ysc h g G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma ysc_ypr: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[h, g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /2 width=1/ /2 width=2/ +lemma ysc_ypr: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1/ /2 width=2/ qed. (* Inversion lemmas on "big tree" parallel reduction for closures ***********) -lemma ypr_inv_ysc: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[h, g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ ≻[h, g] ⦃L2, T2⦄ ∨ (L1 ⊢ ➡ L2 ∧ T1 = T2). -#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /3 width=1/ /3 width=2/ +lemma ypr_inv_ysc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨ + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡ L2 & T1 = T2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /3 width=1/ /3 width=2/ [ #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/ | #L2 #HL21 elim (lenv_eq_dec L1 L2) #H destruct /3 width=1/ /4 width=1/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_6.ma deleted file mode 100644 index cfc3ae926..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_6.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 T1 ⦄ ≽ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRed $h $g $L1 $T1 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma new file mode 100644 index 000000000..80e40a157 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.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( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTPRed $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_6.ma deleted file mode 100644 index eaf9a0a79..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_6.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 T1 ⦄ ≻ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRedProper $h $g $L1 $T1 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma new file mode 100644 index 000000000..bb6d3d1af --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.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( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTPRedProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_6.ma deleted file mode 100644 index 60cc3ef50..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_6.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 T1 ⦄ ≥ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRedStar $h $g $L1 $T1 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma new file mode 100644 index 000000000..3943a33fd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.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( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTPRedStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_6.ma deleted file mode 100644 index b76e2a5d3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_6.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 T1 ⦄ > break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRedStarProper $h $g $L1 $T1 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_8.ma new file mode 100644 index 000000000..66d7a34ba --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarproper_8.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( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ > break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTPRedStarProper $h $g $G1 $L1 $T1 $G2 $L2 $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 deleted file mode 100644 index 1124b8b8f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_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 @{ 'LRSubEqV $h $g $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma new file mode 100644 index 000000000..a617f7923 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.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( 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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_4.ma deleted file mode 100644 index 5704d8ef9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_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( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 g ] )" - non associative with precedence 45 - for @{ 'NativeValid $h $g $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma new file mode 100644 index 000000000..d6426f6c1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.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( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 h, break term 46 g ] )" + non associative with precedence 45 + for @{ 'NativeValid $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index af73af5fc..76c69725f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -33,7 +33,7 @@ Closure of context-sensitive extended computation for native validity. - + Passive support for global environments.