From: Ferruccio Guidi Date: Sun, 17 Mar 2013 15:28:18 +0000 (+0000) Subject: notational change for snv and lsubsv: inverted "!" used for now X-Git-Tag: make_still_working~1212 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cdfd45ca5a2b52601b7bde732a7811de55a52fed;p=helm.git notational change for snv and lsubsv: inverted "!" used for now --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index 7958de918..089dbed26 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -22,8 +22,8 @@ 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,V1,V2,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → ⦃h, L1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ → - L1 ⊢ W1 ⬌* W2 → ⦃h, L2⦄ ⊩ W2 :[g] → ⦃h, L2⦄ ⊢ W2 •[g] ⦃l, V2⦄ → +| lsubsv_abbr: ∀L1,L2,V1,V2,W1,W2,l. ⦃h, L1⦄ ⊢ V1 ¡[g] → ⦃h, L1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ → + L1 ⊢ W1 ⬌* W2 → ⦃h, L2⦄ ⊢ W2 ¡[g] → ⦃h, L2⦄ ⊢ W2 •[g] ⦃l, V2⦄ → lsubsv h g L1 L2 → lsubsv h g (L1. ⓓV1) (L2. ⓛW2) . @@ -33,7 +33,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 = ⋆ → L2 = ⋆. +fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 = ⋆ → L2 = ⋆. #h #g #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -41,15 +41,15 @@ fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 = ⋆ → ] qed-. -lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ⊩:⊑[g] L2 → L2 = ⋆. +lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ¡⊑[g] L2 → L2 = ⋆. /2 width=5 by lsubsv_inv_atom1_aux/ qed-. -fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → +fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ - ∃∃K2,V2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & - K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & - h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. + (∃∃K2. h ⊢ K1 ¡⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ + ∃∃K2,V2,W1,W2,l. ⦃h, K1⦄ ⊢ V1 ¡[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & + K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊢ W2 ¡[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & + h ⊢ K1 ¡⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. #h #g #L1 #L2 * -L1 -L2 [ #J #K1 #U1 #H destruct | #I #L1 #L2 #V #HL12 #J #K1 #U1 #H destruct /3 width=3/ @@ -57,14 +57,14 @@ fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → ] qed-. -lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ⊩:⊑[g] L2 → - (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ - ∃∃K2,V2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & - K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & - h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. +lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ¡⊑[g] L2 → + (∃∃K2. h ⊢ K1 ¡⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ + ∃∃K2,V2,W1,W2,l. ⦃h, K1⦄ ⊢ V1 ¡[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & + K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊢ W2 ¡[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & + h ⊢ K1 ¡⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. /2 width=3 by lsubsv_inv_pair1_aux/ qed-. -fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L2 = ⋆ → L1 = ⋆. +fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L2 = ⋆ → L1 = ⋆. #h #g #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -72,15 +72,15 @@ fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L2 = ⋆ → ] qed-. -lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ⊩:⊑[g] ⋆ → L1 = ⋆. +lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ¡⊑[g] ⋆ → L1 = ⋆. /2 width=5 by lsubsv_inv_atom2_aux/ qed-. -fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → +fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → ∀I,K2,W2. L2 = K2. ⓑ{I} W2 → - (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ - ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & - K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & - h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. + (∃∃K1. h ⊢ K1 ¡⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ + ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊢ V1 ¡[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & + K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊢ W2 ¡[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & + h ⊢ K1 ¡⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. #h #g #L1 #L2 * -L1 -L2 [ #J #K2 #U2 #H destruct | #I #L1 #L2 #V #HL12 #J #K2 #U2 #H destruct /3 width=3/ @@ -88,34 +88,34 @@ fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → ] qed-. -lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ⊩:⊑[g] K2. ⓑ{I} W2 → - (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ - ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & - K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & - h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. +lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ¡⊑[g] K2. ⓑ{I} W2 → + (∃∃K1. h ⊢ K1 ¡⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ + ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊢ V1 ¡[g] & ⦃h, K1⦄ ⊢ V1 •[g] ⦃l+1, W1⦄ & + K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊢ W2 ¡[g] & ⦃h, K2⦄ ⊢ W2 •[g] ⦃l, V2⦄ & + h ⊢ K1 ¡⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. /2 width=3 by lsubsv_inv_pair2_aux/ qed-. (* Basic_forward lemmas *****************************************************) -lemma lsubsv_fwd_lsubss: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → h ⊢ L1 •⊑[g] L2. +lemma lsubsv_fwd_lsubss: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → h ⊢ L1 •⊑[g] L2. #h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/ qed-. -lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L1|] L2. +lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L1|] L2. /3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs1/ qed-. -lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L2|] L2. +lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → L1 ≼[0, |L2|] L2. /3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs2/ qed-. (* Basic properties *********************************************************) -lemma lsubsv_refl: ∀h,g,L. h ⊢ L ⊩:⊑[g] L. +lemma lsubsv_refl: ∀h,g,L. h ⊢ L ¡⊑[g] L. #h #g #L elim L -L // /2 width=1/ qed. -lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → +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_lsubss, lsubss_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 87a72e0fd..15acdc943 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 ⊩:⊑[g] L2 → +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_lsubs2, cpcs_lsubs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma index f77bc41eb..9666bffdd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma @@ -24,8 +24,8 @@ fact sstas_lsubsv_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → - ∀L2,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T⦄ → ⦃h, L2⦄ ⊩ T :[g] → - ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ∀U2. ⦃h, L2⦄ ⊢ T •*[g] U2 → + ∀L2,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T⦄ → ⦃h, L2⦄ ⊢ T ¡[g] → + ∀L1. h ⊢ L1 ¡⊑[g] L2 → ∀U2. ⦃h, L2⦄ ⊢ T •*[g] U2 → ∃∃U1. ⦃h, L1⦄ ⊢ T •*[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/ ] #U2 #W #l #HTU2 #HU2W * #U1 #HTU1 #HU12 @@ -45,8 +45,8 @@ fact dxprs_lsubsv_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → - ∀L2,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T1⦄ → ⦃h, L2⦄ ⊩ T1 :[g] → - ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → + ∀L2,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T1⦄ → ⦃h, L2⦄ ⊢ T1 ¡[g] → + ∀L1. h ⊢ L1 ¡⊑[g] L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ∃∃T. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T & L1 ⊢ T2 ➡* T. #h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2 lapply (lsubsv_cprs_trans … HL12 … HTT2) -HTT2 #HTT2 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 bf109cdc0..686095062 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma @@ -19,9 +19,9 @@ 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 ⊩:⊑[g] L2 → +lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 → - ∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L2 ≡ K2. + ∃∃K2. h ⊢ K1 ¡⊑[g] K2 & ⇩[0, e] L2 ≡ K2. #h #g #L1 #L2 #H elim H -L1 -L2 [ /2 width=3/ | #I #L1 #L2 #V #_ #IHL12 #K1 #e #H @@ -42,9 +42,9 @@ lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → qed. (* Note: the constant 0 cannot be generalized *) -lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → +lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ¡⊑[g] L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L1 ≡ K1. + ∃∃K1. h ⊢ K1 ¡⊑[g] K2 & ⇩[0, e] L1 ≡ K1. #h #g #L1 #L2 #H elim H -L1 -L2 [ /2 width=3/ | #I #L1 #L2 #V #_ #IHL12 #K2 #e #H 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 7928373cf..d19d320e4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma @@ -19,7 +19,7 @@ include "basic_2/dynamic/lsubsv.ma". (* Properties on local environment refinement for atomic arity assignment ***) -lemma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ⁝⊑ L2. +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 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 b85b4a8fa..594c72662 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma @@ -20,7 +20,7 @@ include "basic_2/dynamic/lsubsv.ma". (* Properties on stratified static type assignment **************************) lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ → - ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → + ∀L1. h ⊢ L1 ¡⊑[g] L2 → ∃∃U1. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2. /3 width=3 by lsubsv_fwd_lsubss, lsubss_ssta_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma index 4eb644013..69906c437 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma @@ -33,8 +33,8 @@ interpretation "stratified native validity (term)" (* Basic inversion lemmas ***************************************************) -fact snv_inv_lref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀i. X = #i → - ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g]. +fact snv_inv_lref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊢ X ¡[g] → ∀i. X = #i → + ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ¡[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/ @@ -44,11 +44,11 @@ fact snv_inv_lref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀i. X = #i → ] qed. -lemma snv_inv_lref: ∀h,g,L,i. ⦃h, L⦄ ⊩ #i :[g] → - ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g]. +lemma snv_inv_lref: ∀h,g,L,i. ⦃h, L⦄ ⊢ #i ¡[g] → + ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ¡[g]. /2 width=3/ qed-. -fact snv_inv_gref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀p. X = §p → ⊥. +fact snv_inv_gref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊢ X ¡[g] → ∀p. X = §p → ⊥. #h #g #L #X * -L -X [ #L #k #p #H destruct | #I #L #K #V #i #_ #_ #p #H destruct @@ -58,11 +58,11 @@ fact snv_inv_gref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀p. X = §p → ] qed. -lemma snv_inv_gref: ∀h,g,L,p. ⦃h, L⦄ ⊩ §p :[g] → ⊥. +lemma snv_inv_gref: ∀h,g,L,p. ⦃h, L⦄ ⊢ §p ¡[g] → ⊥. /2 width=7/ qed-. -fact snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → - ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. +fact snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊢ X ¡[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → + ⦃h, L⦄ ⊢ V ¡[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ T ¡[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 @@ -72,12 +72,12 @@ fact snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ ] qed. -lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{a,I}V.T :[g] → - ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. +lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊢ ⓑ{a,I}V.T ¡[g] → + ⦃h, L⦄ ⊢ V ¡[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ T ¡[g]. /2 width=4/ qed-. -fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T → - ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & +fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊢ X ¡[g] → ∀V,T. X = ⓐV.T → + ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊢ V ¡[g] & ⦃h, L⦄ ⊢ T ¡[g] & ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ & L ⊢ W ➡* W0 & ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U. #h #g #L #X * -L -X @@ -89,14 +89,14 @@ fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T ] qed. -lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] → - ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & +lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ ⓐV.T ¡[g] → + ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊢ V ¡[g] & ⦃h, L⦄ ⊢ T ¡[g] & ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ & L ⊢ W ➡* W0 & ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U. /2 width=3/ qed-. -fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T → - ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & +fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊢ X ¡[g] → ∀W,T. X = ⓝW.T → + ∃∃U,l. ⦃h, L⦄ ⊢ W ¡[g] & ⦃h, L⦄ ⊢ T ¡[g] & ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ & L ⊢ U ⬌* W. #h #g #L #X * -L -X [ #L #k #W #T #H destruct @@ -107,14 +107,14 @@ fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T ] qed. -lemma snv_inv_cast: ∀h,g,L,W,T. ⦃h, L⦄ ⊩ ⓝW.T :[g] → - ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & +lemma snv_inv_cast: ∀h,g,L,W,T. ⦃h, L⦄ ⊢ ⓝW.T ¡[g] → + ∃∃U,l. ⦃h, L⦄ ⊢ W ¡[g] & ⦃h, L⦄ ⊢ T ¡[g] & ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ & L ⊢ U ⬌* W. /2 width=3/ qed-. (* Basic forward lemmas *****************************************************) -lemma snv_fwd_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃l,U. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄. +lemma snv_fwd_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → ∃∃l,U. ⦃h, L⦄ ⊢ T •[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 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 f492c019b..b5835bef9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma @@ -21,7 +21,7 @@ include "basic_2/dynamic/snv.ma". (* Forward lemmas on atomic arity assignment for terms **********************) -lemma snv_fwd_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. +lemma snv_fwd_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → ∃A. L ⊢ T ⁝ A. #h #g #L #T #H elim H -L -T [ /2 width=2/ | #I #L #K #V #i #HLK #_ * /3 width=6/ @@ -36,6 +36,6 @@ lemma snv_fwd_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. ] qed-. -lemma snv_fwd_csn: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → L ⊢ ⬊* T. +lemma snv_fwd_csn: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ¡[g] → L ⊢ ⬊* T. #h #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 c80e11c79..9451e34d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -23,35 +23,35 @@ include "basic_2/dynamic/ygt.ma". (* Inductive premises for the preservation results **************************) definition IH_snv_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊩ T2 :[g]. + λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 ¡[g]. definition IH_ssta_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → + λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] → ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L1⦄ ⊩ U1 :[g]. + λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L1⦄ ⊢ U1 ¡[g]. definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] → - ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g]. + λh,g,L2,T. ⦃h, L2⦄ ⊢ T ¡[g] → + ∀L1. h ⊢ L1 ¡⊑[g] L2 → ⦃h, L1⦄ ⊢ T ¡[g]. (* Properties for the preservation results **********************************) fact snv_ltpr_cpr_aux: ∀h,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 → - ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L2⦄ ⊩ T2 :[g]. + ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 ¡[g]. #h #g #L1 #T1 #IH #HT1 #L2 #HL12 #T2 * #T #HT1T #HTT2 lapply (IH … HL12 … HT1T) -HL12 // -T1 #HT0 lapply (snv_tpss_conf … HT0 … HTT2) -T // qed-. fact ssta_ltpr_cpr_aux: ∀h,g,L1,T1. IH_ssta_ltpr_tpr h g L1 T1 → - ⦃h, L1⦄ ⊩ T1 :[g] → + ⦃h, L1⦄ ⊢ T1 ¡[g] → ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. @@ -63,8 +63,8 @@ qed-. fact snv_ltpr_cprs_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊩ T2 :[g]. + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 ¡[g]. #h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #L2 #HL12 #T2 #H @(cprs_ind … H) -T2 [ /2 width=6 by snv_ltpr_cpr_aux/ ] -HT1 /5 width=6 by snv_ltpr_cpr_aux, ygt_yprs_trans, ltpr_cprs_yprs/ @@ -73,7 +73,7 @@ qed-. fact ssta_ltpr_cprs_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. @@ -91,7 +91,7 @@ fact ssta_ltpr_cpcs_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → ∀L1,L2,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T2⦄ → - ⦃h, L1⦄ ⊩ T1 :[g] → ⦃h, L2⦄ ⊩ T2 :[g] → + ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L2⦄ ⊢ T2 ¡[g] → ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ → ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l2, U2⦄ → L1 ➡ L2 → L2 ⊢ T1 ⬌* T2 → @@ -106,8 +106,8 @@ qed-. fact snv_sstas_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ⦃h, L1⦄ ⊩ U1 :[g]. + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → + ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ⦃h, L1⦄ ⊢ U1 ¡[g]. #h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H @(sstas_ind … H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/ qed-. @@ -116,7 +116,7 @@ fact sstas_ltpr_cprs_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ⬌* U2. #h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H @@ -136,7 +136,7 @@ fact dxprs_ltpr_cprs_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 → ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2. @@ -150,7 +150,7 @@ qed-. fact ssta_dxprs_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 → ∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2. #h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2 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 ec9be23a4..854fff7f3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma @@ -20,8 +20,8 @@ include "basic_2/dynamic/snv.ma". (* Relocation properties ****************************************************) -lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡ K → - ∀U. ⇧[d, e] T ≡ U → ⦃h, L⦄ ⊩ U :[g]. +lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊢ T ¡[g] → ∀L,d,e. ⇩[d, e] L ≡ K → + ∀U. ⇧[d, e] T ≡ U → ⦃h, L⦄ ⊢ U ¡[g]. #h #g #K #T #H elim H -K -T [ #K #k #L #d #e #_ #X #H >(lift_inv_sort1 … H) -X -K -d -e // @@ -50,8 +50,8 @@ lemma snv_lift: ∀h,g,K,T. ⦃h, K⦄ ⊩ T :[g] → ∀L,d,e. ⇩[d, e] L ≡ ] qed. -lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L ≡ K → - ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊩ T :[g]. +lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊢ U ¡[g] → ∀K,d,e. ⇩[d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊢ T ¡[g]. #h #g #L #U #H elim H -L -U [ #L #k #K #d #e #_ #X #H >(lift_inv_sort2 … H) -X -L -d -e // diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_dx.ma index 7a31a714d..ca55239f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_dx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_dx.ma @@ -20,9 +20,9 @@ include "basic_2/dynamic/snv_lift.ma". (* Properties about dx parallel unfold **************************************) -lemma snv_ltpss_dx_tpss_conf: ∀h,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → +lemma snv_ltpss_dx_tpss_conf: ∀h,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] → ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → ⦃h, L2⦄ ⊩ T2 :[g]. + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → ⦃h, L2⦄ ⊢ T2 ¡[g]. #h #g #L1 #T1 #H elim H -L1 -T1 [ #L1 #k #L2 #d #e #_ #X #H >(tpss_inv_sort1 … H) -X // @@ -68,20 +68,20 @@ lemma snv_ltpss_dx_tpss_conf: ∀h,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → ] qed-. -lemma snv_ltpss_dx_conf: ∀h,g,L1,T. ⦃h, L1⦄ ⊩ T :[g] → - ∀L2,d,e. L1 ▶* [d, e] L2 → ⦃h, L2⦄ ⊩ T :[g]. +lemma snv_ltpss_dx_conf: ∀h,g,L1,T. ⦃h, L1⦄ ⊢ T ¡[g] → + ∀L2,d,e. L1 ▶* [d, e] L2 → ⦃h, L2⦄ ⊢ T ¡[g]. #h #g #L1 #T #HT #L2 #d #e #HL12 @(snv_ltpss_dx_tpss_conf … HT … HL12) // qed-. -lemma snv_tpss_conf: ∀h,g,L,T1. ⦃h, L⦄ ⊩ T1 :[g] → - ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ⦃h, L⦄ ⊩ T2 :[g]. +lemma snv_tpss_conf: ∀h,g,L,T1. ⦃h, L⦄ ⊢ T1 ¡[g] → + ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ⦃h, L⦄ ⊢ T2 ¡[g]. #h #g #L #T1 #HT1 #T2 #d #e #HT12 @(snv_ltpss_dx_tpss_conf … HT1 … HT12) // qed-. -lemma snv_tps_conf: ∀h,g,L,T1. ⦃h, L⦄ ⊩ T1 :[g] → - ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ⦃h, L⦄ ⊩ T2 :[g]. +lemma snv_tps_conf: ∀h,g,L,T1. ⦃h, L⦄ ⊢ T1 ¡[g] → + ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ⦃h, L⦄ ⊢ T2 ¡[g]. #h #g #L #T1 #HT1 #T2 #d #e #HT12 @(snv_tpss_conf … HT1 T2) /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_sn.ma index 8c4c81c34..3c8070249 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpss_sn.ma @@ -19,7 +19,7 @@ include "basic_2/dynamic/snv_ltpss_dx.ma". (* Properties about sn parallel unfold **************************************) lemma snv_ltpss_sn_conf: ∀h,g,L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → - ∀T. ⦃h, L1⦄ ⊩ T :[g] → ⦃h, L2⦄ ⊩ T :[g]. + ∀T. ⦃h, L1⦄ ⊢ T ¡[g] → ⦃h, L2⦄ ⊢ T ¡[g]. #h #g #L1 #L2 #d #e #H lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 // #L #L2 #_ #HL2 #IHL1 #T1 #HT1 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 d0da185ca..0bdfd7496 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma @@ -19,7 +19,7 @@ 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. ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊢ T1 •* [g] T2 → +lemma snv_sstas_fwd_correct: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ¡[g] → ⦃h, L⦄ ⊢ T1 •* [g] T2 → ∃∃U2,l. ⦃h, L⦄ ⊢ T2 •[g] ⦃l, U2⦄. #h #g #L #T1 #T2 #HT1 #HT12 elim (snv_fwd_ssta … HT1) -HT1 /2 width=5 by sstas_fwd_correct/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma index 85419d1ea..3b55fca99 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma @@ -94,6 +94,6 @@ lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → (T1 = T2 → ] qed. -lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) → +lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → (L1 = L2 → ⊥) → h ⊢ ⦃L1, T⦄ >[g] ⦃L2, T⦄. /4 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma index 065e8c83e..9135495f8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma @@ -22,7 +22,7 @@ inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝ | ypr_ltpr : ∀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 •[g] ⦃l+1, T2⦄ → ypr h g L1 T1 L1 T2 -| ypr_lsubsv: ∀L2. h ⊢ L2 ⊩:⊑[g] L1 → ypr h g L1 T1 L2 T1 +| ypr_lsubsv: ∀L2. h ⊢ L2 ¡⊑[g] L1 → ypr h g L1 T1 L2 T1 . interpretation diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma index 30c90c43e..0c7231075 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma @@ -69,7 +69,7 @@ lemma sstas_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → #h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=4 by ypr_ssta, yprs_strap1/ qed. -lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄. +lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ¡⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄. /3 width=1/ qed. lemma ltpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma index a1e54168d..203cf3ebd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma @@ -20,7 +20,7 @@ inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝ | ysc_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → 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 •[g] ⦃l+1, T2⦄ → ysc h g L1 T1 L1 T2 -| ysc_lsubsv: ∀L2. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1 +| ysc_lsubsv: ∀L2. h ⊢ L2 ¡⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1 . interpretation diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma index 7489da188..1c4dcdd04 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma @@ -13,8 +13,7 @@ (**************************************************************************) (* THE FORMAL SYSTEM λδ: MATITA SOURCE FILES - * Suggested invocation to start formal specifications with: - * - Patience on me to gain peace and perfection! - + * Initial invocation: - Patience on me to gain peace and perfection! - *) include "ground_2/star.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 54b47600c..8745932e9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -448,11 +448,11 @@ notation "hvbox( ⦃ term 46 L1 , break term 46 T1 ⦄ ⬌ ⬌ * break ⦃ term (* Dynamic typing ***********************************************************) -notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊩ break term 46 T : break [ term 46 g ] )" +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 }. -notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ break [ term 46 g ] break term 46 L2 )" +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/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index c4c962070..00db0e50b 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 @@ -48,11 +48,11 @@ table { } ] [ { "local env. ref. for stratified native validity" * } { - [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ] + [ "lsubsv ( ? ⊢ ? ¡⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ] } ] [ { "stratified native validity" * } { - [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_ltpss_dx" + "snv_ltpss_sn" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_ltpr" + "snv_ltpr" + "snv_cpcs" * ] + [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?] )" "snv_lift" + "snv_ltpss_dx" + "snv_ltpss_sn" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_ltpr" + "snv_ltpr" + "snv_cpcs" * ] } ] }