From: Ferruccio Guidi Date: Thu, 10 May 2012 15:57:36 +0000 (+0000) Subject: - predefined_virtuals: an addition X-Git-Tag: make_still_working~1757 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ba7ef901a6b72210692792f2396c08bc0cff52c;p=helm.git - predefined_virtuals: an addition - lambda_delta: some notation changes --- diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma index 788c39902..e25f2975f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma @@ -25,7 +25,7 @@ include "basic_2/computation/lsubc_ldrops.ma". (* Basic_1: was: sc3_arity_csubc *) theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L1,T,A. L1 ⊢ T ÷ A → ∀L0,des. ⇩*[des] L0 ≡ L1 → + ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 → ∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 → ⦃L2, T0⦄ [RP] ϵ 〚A〛. #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A @@ -90,11 +90,11 @@ qed. (* Basic_1: was: sc3_arity *) lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L,T,A. L ⊢ T ÷ A → ⦃L, T⦄ [RP] ϵ 〚A〛. + ∀L,T,A. L ⊢ T ⁝ A → ⦃L, T⦄ [RP] ϵ 〚A〛. /2 width=8/ qed. lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L,T,A. L ⊢ T ÷ A → RP L T. + ∀L,T,A. L ⊢ T ⁝ A → RP L T. #RR #RS #RP #H1RP #H2RP #L #T #A #HT lapply (aacr_acr … H1RP H2RP A) #HA @(s1 … HA) /2 width=4/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma index 67312a9ac..8b36e75ae 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma @@ -19,7 +19,7 @@ include "basic_2/computation/csn_tstc_vector.ma". (* Properties concerning atomic arity assignment ****************************) -lemma csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⬇* T. +lemma csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬇* T. #L #T #A #H @(acp_aaa … csn_acp csn_acr … H) qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma new file mode 100644 index 000000000..6b4b61ae6 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_alt.ma @@ -0,0 +1,99 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/cprs.ma". +include "basic_2/computation/csn.ma". + +(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) + +(* alternative definition of csn *) +definition csna: lenv → predicate term ≝ λL. SN … (cprs L) (eq …). + +interpretation + "context-sensitive strong normalization (term) alternative" + 'SNAlt L T = (csna L T). + +(* Basic eliminators ********************************************************) + +lemma csna_ind: ∀L. ∀R:predicate term. + (∀T1. L ⊢ ⬇⬇* T1 → + (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1 + ) → + ∀T. L ⊢ ⬇⬇* T → R T. +#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 +@H0 -H0 /3 width=1/ -IHT1 /4 width=1/ +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: sn3_intro *) +lemma csna_intro: ∀L,T1. + (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1. +#L #T1 #H +@(SN_intro … H) +qed. + +fact csna_intro_aux: ∀L,T1. + (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1. +/4 width=3/ qed-. + +(* Basic_1: was: sn3_pr3_trans (old version) *) +lemma csna_cprs_trans: ∀L,T1. L ⊢ ⬇⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇⬇* T2. +#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 +@csna_intro #T #HLT2 #HT2 +elim (term_eq_dec T1 T2) #HT12 +[ -IHT1 -HLT12 destruct /3 width=1/ +| -HT1 -HT2 /3 width=4/ +qed. + +(* Basic_1: was: sn3_pr2_intro (old version) *) +lemma csna_intro_cpr: ∀L,T1. + (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → + L ⊢ ⬇⬇* T1. +#L #T1 #H +@csna_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T +[ -H #H destruct #H + elim (H ?) // +| #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct + elim (term_eq_dec T0 T) #HT0 + [ -HLT1 -HLT2 -H /3 width=1/ + | -IHT -HT12 /4 width=3/ + ] +] +qed. + +(* Main properties **********************************************************) + +theorem csn_csna: ∀L,T. L ⊢ ⬇* T → L ⊢ ⬇⬇* T. +#L #T #H @(csn_ind … H) -T /4 width=1/ +qed. + +theorem csna_csn: ∀L,T. L ⊢ ⬇⬇* T → L ⊢ ⬇* T. +#L #T #H @(csna_ind … H) -T /4 width=1/ +qed. + +(* Basic_1: was: sn3_pr3_trans *) +lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇* T2. +/4 width=3/ qed. + +(* Main eliminators *********************************************************) + +lemma csn_ind_alt: ∀L. ∀R:predicate term. + (∀T1. L ⊢ ⬇* T1 → + (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1 + ) → + ∀T. L ⊢ ⬇* T → R T. +#L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1 +@H0 -H0 /2 width=1/ -HT1 /3 width=1/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma deleted file mode 100644 index c32947631..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma +++ /dev/null @@ -1,100 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/cprs.ma". -include "basic_2/computation/csn.ma". - -(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) - -(* Properties concerning context-sensitive computation on terms *************) - -definition csns: lenv → predicate term ≝ λL. SN … (cprs L) (eq …). - -interpretation - "context-sensitive strong normalization (term)" - 'SNStar L T = (csns L T). - -(* Basic eliminators ********************************************************) - -lemma csns_ind: ∀L. ∀R:predicate term. - (∀T1. L ⊢ ⬇** T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1 - ) → - ∀T. L ⊢ ⬇** T → R T. -#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1 -@H0 -H0 /3 width=1/ -IHT1 /4 width=1/ -qed-. - -(* Basic properties *********************************************************) - -(* Basic_1: was: sn3_intro *) -lemma csns_intro: ∀L,T1. - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → L ⊢ ⬇** T2) → L ⊢ ⬇** T1. -#L #T1 #H -@(SN_intro … H) -qed. - -fact csns_intro_aux: ∀L,T1. - (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → False) → L ⊢ ⬇** T2) → L ⊢ ⬇** T1. -/4 width=3/ qed-. - -(* Basic_1: was: sn3_pr3_trans (old version) *) -lemma csns_cprs_trans: ∀L,T1. L ⊢ ⬇** T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇** T2. -#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 -@csns_intro #T #HLT2 #HT2 -elim (term_eq_dec T1 T2) #HT12 -[ -IHT1 -HLT12 destruct /3 width=1/ -| -HT1 -HT2 /3 width=4/ -qed. - -(* Basic_1: was: sn3_pr2_intro (old version) *) -lemma csns_intro_cpr: ∀L,T1. - (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇** T2) → - L ⊢ ⬇** T1. -#L #T1 #H -@csns_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T -[ -H #H destruct #H - elim (H ?) // -| #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct - elim (term_eq_dec T0 T) #HT0 - [ -HLT1 -HLT2 -H /3 width=1/ - | -IHT -HT12 /4 width=3/ - ] -] -qed. - -(* Main properties **********************************************************) - -theorem csn_csns: ∀L,T. L ⊢ ⬇* T → L ⊢ ⬇** T. -#L #T #H @(csn_ind … H) -T /4 width=1/ -qed. - -theorem csns_csn: ∀L,T. L ⊢ ⬇** T → L ⊢ ⬇* T. -#L #T #H @(csns_ind … H) -T /4 width=1/ -qed. - -(* Basic_1: was: sn3_pr3_trans *) -lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇* T2. -/4 width=3/ qed. - -(* Main eliminators *********************************************************) - -lemma csn_ind_cprs: ∀L. ∀R:predicate term. - (∀T1. L ⊢ ⬇* T1 → - (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1 - ) → - ∀T. L ⊢ ⬇* T → R T. -#L #R #H0 #T1 #H @(csns_ind … (csn_csns … H)) -T1 #T1 #HT1 #IHT1 -@H0 -H0 /2 width=1/ -HT1 /3 width=1/ -qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma index 92d30c7fd..169073516 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma @@ -16,20 +16,20 @@ include "basic_2/grammar/tstc_tstc.ma". include "basic_2/computation/cprs_cprs.ma". include "basic_2/computation/csn_lift.ma". include "basic_2/computation/csn_cpr.ma". -include "basic_2/computation/csn_cprs.ma". +include "basic_2/computation/csn_alt.ma". (* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************) (* Advanced properties ******************************************************) lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬇* T → L2 ⊢ ⬇* T. -#L1 #L2 #HL12 #T #H @(csn_ind_cprs … H) -T #T #_ #IHT +#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT @csn_intro #T0 #HLT0 #HT0 @IHT /2 width=2/ -IHT -HT0 /2 width=3/ qed. lemma csn_abbr: ∀L,V. L ⊢ ⬇* V → ∀T. L. ⓓV ⊢ ⬇* T → L ⊢ ⬇* ⓓV. T. -#L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_cprs … HT) -T #T #HT #IHT +#L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 elim (cpr_inv_abbr1 … H1) -H1 * [ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct @@ -47,7 +47,7 @@ qed. fact csn_appl_beta_aux: ∀L,W. L ⊢ ⬇* W → ∀U. L ⊢ ⬇* U → ∀V,T. U = ⓓV. T → L ⊢ ⬇* ⓐV. ⓛW. T. -#L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_cprs … H) -X #X #HVT #IHVT #V #T #H destruct +#L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct lapply (csn_fwd_pair_sn … HVT) #HV lapply (csn_fwd_bind_dx … HVT) #HT -HVT @csn_intro #X #H #H2 @@ -76,7 +76,7 @@ lemma csn_appl_beta: ∀L,W. L ⊢ ⬇* W → ∀V,T. L ⊢ ⬇* ⓓV. T → fact csn_appl_theta_aux: ∀L,U. L ⊢ ⬇* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 → ∀V,T. U = ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T. -#L #X #H @(csn_ind_cprs … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct +#L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct lapply (csn_fwd_pair_sn … HVT) #HV lapply (csn_fwd_bind_dx … HVT) -HVT #HVT @csn_intro #X #HL #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma index 9be9b17e4..73a6261e3 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_aaa.ma @@ -20,16 +20,16 @@ include "basic_2/computation/lcprs.ma". (* Properties about atomic arity assignment on terms ************************) -lemma aaa_lcprs_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ÷ A. +lemma aaa_lcprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A. #L1 #T #A #HT #L2 #HL12 -@(TC_Conf3 … (λL,A. L ⊢ T ÷ A) … HT ? HL12) /2 width=3/ +@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/ qed. -lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ÷ A. +lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A. #L #T1 #A #HT1 #T2 #HT12 @(TC_Conf3 … HT1 ? HT12) /2 width=3/ qed. -lemma aaa_lcprs_cprs_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ⊢ ➡* L2 → - ∀T2. L2 ⊢ T1 ➡* T2 → L2 ⊢ T2 ÷ A. +lemma aaa_lcprs_cprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ⊢ ➡* L2 → + ∀T2. L2 ⊢ T1 ➡* T2 → L2 ⊢ T2 ⁝ A. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma index d7094600c..7c2ef6050 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma @@ -20,7 +20,7 @@ include "basic_2/computation/acp_cr.ma". inductive lsubc (RP:lenv→predicate term): relation lenv ≝ | lsubc_atom: lsubc RP (⋆) (⋆) | lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V) -| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → L2 ⊢ W ÷ A → +| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → L2 ⊢ W ⁝ A → lsubc RP L1 L2 → lsubc RP (L1. ⓓV) (L2. ⓛW) . @@ -44,7 +44,7 @@ lemma lsubc_inv_atom1: ∀RP,L2. ⋆ [RP] ⊑ L2 → L2 = ⋆. fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V → (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A & + ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A & K1 [RP] ⊑ K2 & L2 = K2. ⓛW & I = Abbr. #RP #L1 #L2 * -L1 -L2 @@ -57,7 +57,7 @@ qed. (* Basic_1: was: csubc_gen_head_r *) lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V [RP] ⊑ L2 → (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A & + ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A & K1 [RP] ⊑ K2 & L2 = K2. ⓛW & I = Abbr. /2 width=3/ qed-. @@ -76,7 +76,7 @@ lemma lsubc_inv_atom2: ∀RP,L1. L1 [RP] ⊑ ⋆ → L1 = ⋆. fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W → (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A & + ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A & K1 [RP] ⊑ K2 & L1 = K1. ⓓV & I = Abst. #RP #L1 #L2 * -L1 -L2 @@ -89,7 +89,7 @@ qed. (* Basic_1: was: csubc_gen_head_l *) lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 [RP] ⊑ K2. ⓑ{I} W → (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A & + ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A & K1 [RP] ⊑ K2 & L1 = K1. ⓓV & I = Abst. /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma index e50551086..e9dcbe5d2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma @@ -20,7 +20,7 @@ include "basic_2/computation/acp_aaa.ma". (* properties concerning lenv refinement for atomic arity assignment ********) lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) → - ∀L1,L2. L1 ÷⊑ L2 → L1 [RP] ⊑ L2. + ∀L1,L2. L1 ⁝⊑ L2 → L1 [RP] ⊑ L2. #RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /3 width=4/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma index 17c9fb939..aa2b8ef2a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lcpcs_aaa.ma @@ -21,7 +21,7 @@ include "basic_2/equivalence/lcpcs_lcpcs.ma". (* Main properties about atomic arity assignment on terms *******************) theorem aaa_lcpcs_mono: ∀L1,L2. L1 ⊢ ⬌* L2 → - ∀T,A1. L1 ⊢ T ÷ A1 → ∀A2. L2 ⊢ T ÷ A2 → + ∀T,A1. L1 ⊢ T ⁝ A1 → ∀A2. L2 ⊢ T ⁝ A2 → A1 = A2. #L1 #L2 #HL12 #T #A1 #HT1 #A2 #HT2 elim (lcpcs_inv_lcprs … HL12) -HL12 #L #HL1 #HL2 @@ -31,7 +31,7 @@ lapply (aaa_mono … HT1 … HT2) -L -T // qed-. theorem aaa_cpcs_mono: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → - ∀A1. L ⊢ T1 ÷ A1 → ∀A2. L ⊢ T2 ÷ A2 → + ∀A1. L ⊢ T1 ⁝ A1 → ∀A2. L ⊢ T2 ⁝ A2 → A1 = A2. #L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2 elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 1e1daa375..3051f1e11 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -202,14 +202,22 @@ notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡≡ break term (* Static typing ************************************************************) -notation "hvbox( L ⊢ break term 46 T ÷ break term 46 A )" +notation "hvbox( L ⊢ break term 46 T ⁝ break term 46 A )" non associative with precedence 45 for @{ 'AtomicArity $L $T $A }. -notation "hvbox( T1 ÷ ⊑ break term 46 T2 )" +notation "hvbox( T1 ⁝ ⊑ break term 46 T2 )" non associative with precedence 45 for @{ 'CrSubEqA $T1 $T2 }. +notation "hvbox( L ⊢ break term 46 T ÷ break term 46 A )" + non associative with precedence 45 + for @{ 'BinaryArity $L $T $A }. + +notation "hvbox( T1 ÷ ⊑ break term 46 T2 )" + non associative with precedence 45 + for @{ 'CrSubEqB $T1 $T2 }. + notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break term 46 T2 )" non associative with precedence 45 for @{ 'StaticType $h $L $T1 $T2 }. @@ -308,9 +316,9 @@ notation "hvbox( L ⊢ ⬇ * term 46 T )" non associative with precedence 45 for @{ 'SN $L $T }. -notation "hvbox( L ⊢ ⬇ * * term 46 T )" +notation "hvbox( L ⊢ ⬇ ⬇ * term 46 T )" non associative with precedence 45 - for @{ 'SNStar $L $T }. + for @{ 'SNAlt $L $T }. notation "hvbox( ⦃ L, break T ⦄ break [ R ] ϵ break 〚 A 〛 )" non associative with precedence 45 diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma index 61ed86b5b..c620b4eca 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_aaa.ma @@ -21,14 +21,14 @@ include "basic_2/reducibility/lcpr.ma". (* Properties about atomic arity assignment on terms ************************) -lemma aaa_lcpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ÷ A. +lemma aaa_lcpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A. #L1 #T #A #HT #L2 * /3 width=5/ qed. -lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ÷ A. +lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A. #L #T1 #A #HT1 #T2 * /3 width=5/ qed. -lemma aaa_lcpr_cpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ⊢ ➡ L2 → - ∀T2. L2 ⊢ T1 ➡ T2 → L2 ⊢ T2 ÷ A. +lemma aaa_lcpr_cpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ⊢ ➡ L2 → + ∀T2. L2 ⊢ T1 ➡ T2 → L2 ⊢ T2 ⁝ A. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma index 31370c5e0..91777310c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma @@ -20,8 +20,8 @@ include "basic_2/reducibility/ltpr_ldrop.ma". (* Properties about atomic arity assignment on terms ************************) -fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ÷ A → L = L1 → T = T1 → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ÷ A. +fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T1 → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A. #L #T @(cw_wf_ind … L T) -L -T #L #T #IH #L1 #T1 #A * -L1 -T1 -A [ -IH #L1 #k #H1 #H2 #L2 #_ #T2 #H destruct @@ -77,12 +77,12 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ÷ A → L = L1 → T = T1 ] qed. -lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ➡ L2 → - ∀T2. T1 ➡ T2 → L2 ⊢ T2 ÷ A. +lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ➡ L2 → + ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A. /2 width=9/ qed. -lemma aaa_ltpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ➡ L2 → L2 ⊢ T ÷ A. +lemma aaa_ltpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ➡ L2 → L2 ⊢ T ⁝ A. /2 width=5/ qed. -lemma aaa_tpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. T1 ➡ T2 → L ⊢ T2 ÷ A. +lemma aaa_tpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. T1 ➡ T2 → L ⊢ T2 ⁝ A. /2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma index 097d24d60..59e110db2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma @@ -33,7 +33,7 @@ interpretation "atomic arity assignment (term)" (* Basic inversion lemmas ***************************************************) -fact aaa_inv_sort_aux: ∀L,T,A. L ⊢ T ÷ A → ∀k. T = ⋆k → A = ⓪. +fact aaa_inv_sort_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀k. T = ⋆k → A = ⓪. #L #T #A * -L -T -A [ // | #I #L #K #V #B #i #_ #_ #k #H destruct @@ -44,11 +44,11 @@ fact aaa_inv_sort_aux: ∀L,T,A. L ⊢ T ÷ A → ∀k. T = ⋆k → A = ⓪. ] qed. -lemma aaa_inv_sort: ∀L,A,k. L ⊢ ⋆k ÷ A → A = ⓪. +lemma aaa_inv_sort: ∀L,A,k. L ⊢ ⋆k ⁝ A → A = ⓪. /2 width=5/ qed-. -fact aaa_inv_lref_aux: ∀L,T,A. L ⊢ T ÷ A → ∀i. T = #i → - ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ÷ A. +fact aaa_inv_lref_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀i. T = #i → + ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A. #L #T #A * -L -T -A [ #L #k #i #H destruct | #I #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5/ @@ -59,12 +59,12 @@ fact aaa_inv_lref_aux: ∀L,T,A. L ⊢ T ÷ A → ∀i. T = #i → ] qed. -lemma aaa_inv_lref: ∀L,A,i. L ⊢ #i ÷ A → - ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ÷ A. +lemma aaa_inv_lref: ∀L,A,i. L ⊢ #i ⁝ A → + ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A. /2 width=3/ qed-. -fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓓW. U → - ∃∃B. L ⊢ W ÷ B & L. ⓓW ⊢ U ÷ A. +fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀W,U. T = ⓓW. U → + ∃∃B. L ⊢ W ⁝ B & L. ⓓW ⊢ U ⁝ A. #L #T #A * -L -T -A [ #L #k #W #U #H destruct | #I #L #K #V #B #i #_ #_ #W #U #H destruct @@ -75,12 +75,12 @@ fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓓW. U → ] qed. -lemma aaa_inv_abbr: ∀L,V,T,A. L ⊢ ⓓV. T ÷ A → - ∃∃B. L ⊢ V ÷ B & L. ⓓV ⊢ T ÷ A. +lemma aaa_inv_abbr: ∀L,V,T,A. L ⊢ ⓓV. T ⁝ A → + ∃∃B. L ⊢ V ⁝ B & L. ⓓV ⊢ T ⁝ A. /2 width=3/ qed-. -fact aaa_inv_abst_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓛW. U → - ∃∃B1,B2. L ⊢ W ÷ B1 & L. ⓛW ⊢ U ÷ B2 & A = ②B1. B2. +fact aaa_inv_abst_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀W,U. T = ⓛW. U → + ∃∃B1,B2. L ⊢ W ⁝ B1 & L. ⓛW ⊢ U ⁝ B2 & A = ②B1. B2. #L #T #A * -L -T -A [ #L #k #W #U #H destruct | #I #L #K #V #B #i #_ #_ #W #U #H destruct @@ -91,12 +91,12 @@ fact aaa_inv_abst_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓛW. U → ] qed. -lemma aaa_inv_abst: ∀L,W,T,A. L ⊢ ⓛW. T ÷ A → - ∃∃B1,B2. L ⊢ W ÷ B1 & L. ⓛW ⊢ T ÷ B2 & A = ②B1. B2. +lemma aaa_inv_abst: ∀L,W,T,A. L ⊢ ⓛW. T ⁝ A → + ∃∃B1,B2. L ⊢ W ⁝ B1 & L. ⓛW ⊢ T ⁝ B2 & A = ②B1. B2. /2 width=3/ qed-. -fact aaa_inv_appl_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓐW. U → - ∃∃B. L ⊢ W ÷ B & L ⊢ U ÷ ②B. A. +fact aaa_inv_appl_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀W,U. T = ⓐW. U → + ∃∃B. L ⊢ W ⁝ B & L ⊢ U ⁝ ②B. A. #L #T #A * -L -T -A [ #L #k #W #U #H destruct | #I #L #K #V #B #i #_ #_ #W #U #H destruct @@ -107,12 +107,12 @@ fact aaa_inv_appl_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓐW. U → ] qed. -lemma aaa_inv_appl: ∀L,V,T,A. L ⊢ ⓐV. T ÷ A → - ∃∃B. L ⊢ V ÷ B & L ⊢ T ÷ ②B. A. +lemma aaa_inv_appl: ∀L,V,T,A. L ⊢ ⓐV. T ⁝ A → + ∃∃B. L ⊢ V ⁝ B & L ⊢ T ⁝ ②B. A. /2 width=3/ qed-. -fact aaa_inv_cast_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓣW. U → - L ⊢ W ÷ A ∧ L ⊢ U ÷ A. +fact aaa_inv_cast_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀W,U. T = ⓣW. U → + L ⊢ W ⁝ A ∧ L ⊢ U ⁝ A. #L #T #A * -L -T -A [ #L #k #W #U #H destruct | #I #L #K #V #B #i #_ #_ #W #U #H destruct @@ -123,6 +123,6 @@ fact aaa_inv_cast_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓣW. U → ] qed. -lemma aaa_inv_cast: ∀L,W,T,A. L ⊢ ⓣW. T ÷ A → - L ⊢ W ÷ A ∧ L ⊢ T ÷ A. +lemma aaa_inv_cast: ∀L,W,T,A. L ⊢ ⓣW. T ⁝ A → + L ⊢ W ⁝ A ∧ L ⊢ T ⁝ A. /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma index ef00bfeeb..05fccc9e2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma @@ -19,7 +19,7 @@ include "basic_2/static/aaa.ma". (* Main properties **********************************************************) -theorem aaa_mono: ∀L,T,A1. L ⊢ T ÷ A1 → ∀A2. L ⊢ T ÷ A2 → A1 = A2. +theorem aaa_mono: ∀L,T,A1. L ⊢ T ⁝ A1 → ∀A2. L ⊢ T ⁝ A2 → A1 = A2. #L #T #A1 #H elim H -L -T -A1 [ #L #k #A2 #H >(aaa_inv_sort … H) -H // diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma index b243338ee..a2ab874e0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma @@ -19,8 +19,8 @@ include "basic_2/static/aaa.ma". (* Properties concerning basic relocation ***********************************) -lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → - ∀T2. ⇧[d, e] T1 ≡ T2 → L2 ⊢ T2 ÷ A. +lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → + ∀T2. ⇧[d, e] T1 ≡ T2 → L2 ⊢ T2 ⁝ A. #L1 #T1 #A #H elim H -L1 -T1 -A [ #L1 #k #L2 #d #e #_ #T2 #H >(lift_inv_sort1 … H) -H // @@ -46,8 +46,8 @@ lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 ] qed. -lemma aaa_inv_lift: ∀L2,T2,A. L2 ⊢ T2 ÷ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → - ∀T1. ⇧[d, e] T1 ≡ T2 → L1 ⊢ T1 ÷ A. +lemma aaa_inv_lift: ∀L2,T2,A. L2 ⊢ T2 ⁝ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → + ∀T1. ⇧[d, e] T1 ≡ T2 → L1 ⊢ T1 ⁝ A. #L2 #T2 #A #H elim H -L2 -T2 -A [ #L2 #k #L1 #d #e #_ #T1 #H >(lift_inv_sort2 … H) -H // diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma index cc1803672..7514f6dc5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma @@ -20,7 +20,7 @@ include "basic_2/static/aaa_lift.ma". (* Properties concerning generic relocation *********************************) lemma aaa_lifts: ∀L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 → - L1 ⊢ T1 ÷ A → L2 ⊢ T2 ÷ A. + L1 ⊢ T1 ⁝ A → L2 ⊢ T2 ⁝ A. #L1 #L2 #T2 #A #des #H elim H -L1 -L2 -des [ #L #T1 #H #HT1 <(lifts_inv_nil … H) -H // diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma index 9de6b6541..ed624a9df 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_ltpss.ma @@ -21,8 +21,8 @@ include "basic_2/static/aaa_lift.ma". (* Properties about parallel unfold *****************************************) (* Note: lemma 500 *) -lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A. +lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 [d, e] ▶* L2 → + ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ⁝ A. #L1 #T1 #A #H elim H -L1 -T1 -A [ #L1 #k #L2 #d #e #_ #T2 #H >(tpss_inv_sort1 … H) -H // @@ -59,18 +59,18 @@ lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ] qed. -lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 → - ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A. +lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 [d, e] ▶* L2 → + ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ⁝ A. /3 width=7/ qed. -lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ÷ A → - ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ÷ A. +lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → + ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ⁝ A. /2 width=7/ qed. -lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ÷ A → - ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ÷ A. +lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → + ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ⁝ A. /2 width=7/ qed. -lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ÷ A → - ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ÷ A. +lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → + ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ⁝ A. /2 width=7/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma index b3ca5d41b..1f253774a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma @@ -19,7 +19,7 @@ include "basic_2/static/aaa.ma". inductive lsuba: relation lenv ≝ | lsuba_atom: lsuba (⋆) (⋆) | lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. ⓑ{I} V) (L2. ⓑ{I} V) -| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ÷ A → L2 ⊢ W ÷ A → +| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ⁝ A → L2 ⊢ W ⁝ A → lsuba L1 L2 → lsuba (L1. ⓓV) (L2. ⓛW) . @@ -29,7 +29,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ÷⊑ L2 → L1 = ⋆ → L2 = ⋆. +fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ⁝⊑ L2 → L1 = ⋆ → L2 = ⋆. #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -37,12 +37,12 @@ fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ÷⊑ L2 → L1 = ⋆ → L2 = ⋆. ] qed. -lemma lsuba_inv_atom1: ∀L2. ⋆ ÷⊑ L2 → L2 = ⋆. +lemma lsuba_inv_atom1: ∀L2. ⋆ ⁝⊑ L2 → L2 = ⋆. /2 width=3/ qed-. -fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V → - (∃∃K2. K1 ÷⊑ K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 & +fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V → + (∃∃K2. K1 ⁝⊑ K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 & L2 = K2. ⓛW & I = Abbr. #L1 #L2 * -L1 -L2 [ #I #K1 #V #H destruct @@ -51,13 +51,13 @@ fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V ] qed. -lemma lsuba_inv_pair1: ∀I,K1,L2,V. K1. ⓑ{I} V ÷⊑ L2 → - (∃∃K2. K1 ÷⊑ K2 & L2 = K2. ⓑ{I} V) ∨ - ∃∃K2,W,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 & +lemma lsuba_inv_pair1: ∀I,K1,L2,V. K1. ⓑ{I} V ⁝⊑ L2 → + (∃∃K2. K1 ⁝⊑ K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 & L2 = K2. ⓛW & I = Abbr. /2 width=3/ qed-. -fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ÷⊑ L2 → L2 = ⋆ → L1 = ⋆. +fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ⁝⊑ L2 → L2 = ⋆ → L1 = ⋆. #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -65,12 +65,12 @@ fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ÷⊑ L2 → L2 = ⋆ → L1 = ⋆. ] qed. -lemma lsubc_inv_atom2: ∀L1. L1 ÷⊑ ⋆ → L1 = ⋆. +lemma lsubc_inv_atom2: ∀L1. L1 ⁝⊑ ⋆ → L1 = ⋆. /2 width=3/ qed-. -fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W → - (∃∃K1. K1 ÷⊑ K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 & +fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W → + (∃∃K1. K1 ⁝⊑ K2 & L1 = K1. ⓑ{I} W) ∨ + ∃∃K1,V,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 & L1 = K1. ⓓV & I = Abst. #L1 #L2 * -L1 -L2 [ #I #K2 #W #H destruct @@ -79,14 +79,14 @@ fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W ] qed. -lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ÷⊑ K2. ⓑ{I} W → - (∃∃K1. K1 ÷⊑ K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 & +lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ⁝⊑ K2. ⓑ{I} W → + (∃∃K1. K1 ⁝⊑ K2 & L1 = K1. ⓑ{I} W) ∨ + ∃∃K1,V,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 & L1 = K1. ⓓV & I = Abst. /2 width=3/ qed-. (* Basic properties *********************************************************) -lemma lsuba_refl: ∀L. L ÷⊑ L. +lemma lsuba_refl: ∀L. L ⁝⊑ L. #L elim L -L // /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma index 4f45ce712..66e802aae 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma @@ -19,7 +19,7 @@ include "basic_2/static/lsuba_ldrop.ma". (* Properties concerning atomic arity assignment ****************************) -lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ÷ A → ∀L2. L1 ÷⊑ L2 → L2 ⊢ V ÷ A. +lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ⁝ A → ∀L2. L1 ⁝⊑ L2 → L2 ⊢ V ⁝ A. #L1 #V #A #H elim H -L1 -V -A [ // | #I #L1 #K1 #V1 #B #i #HLK1 #HV1B #IHV1 #L2 #HL12 @@ -36,7 +36,7 @@ lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ÷ A → ∀L2. L1 ÷⊑ L2 → L2 ⊢ ] qed. -lemma lsuba_aaa_trans: ∀L2,V,A. L2 ⊢ V ÷ A → ∀L1. L1 ÷⊑ L2 → L1 ⊢ V ÷ A. +lemma lsuba_aaa_trans: ∀L2,V,A. L2 ⊢ V ⁝ A → ∀L1. L1 ⁝⊑ L2 → L1 ⊢ V ⁝ A. #L2 #V #A #H elim H -L2 -V -A [ // | #I #L2 #K2 #V2 #B #i #HLK2 #HV2B #IHV2 #L1 #HL12 diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma index f055c01f5..1094133f0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma @@ -20,8 +20,8 @@ include "basic_2/static/lsuba.ma". (* Note: the constant 0 cannot be generalized *) -lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ÷⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 → - ∃∃K2. K1 ÷⊑ K2 & ⇩[0, e] L2 ≡ K2. +lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 → + ∃∃K2. K1 ⁝⊑ K2 & ⇩[0, e] L2 ≡ K2. #L1 #L2 #H elim H -L1 -L2 [ /2 width=3/ | #I #L1 #L2 #V #_ #IHL12 #K1 #e #H @@ -41,8 +41,8 @@ lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ÷⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K ] qed-. -lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ÷⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → - ∃∃K1. K1 ÷⊑ K2 & ⇩[0, e] L1 ≡ K1. +lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1. #L1 #L2 #H elim H -L1 -L2 [ /2 width=3/ | #I #L1 #L2 #V #_ #IHL12 #K2 #e #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma index 9fae68633..5d64516a5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma @@ -18,7 +18,7 @@ include "basic_2/static/lsuba_aaa.ma". (* Main properties **********************************************************) -theorem lsuba_trans: ∀L1,L. L1 ÷⊑ L → ∀L2. L ÷⊑ L2 → L1 ÷⊑ L2. +theorem lsuba_trans: ∀L1,L. L1 ⁝⊑ L → ∀L2. L ⁝⊑ L2 → L1 ⁝⊑ L2. #L1 #L #H elim H -L1 -L [ #X #H >(lsuba_inv_atom1 … H) -H // | #I #L1 #L #V #HL1 #IHL1 #X #H diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index cbdafb2e0..965ae8f2d 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1503,6 +1503,7 @@ let load_predefined_virtuals () = ;; let predefined_classes = [ + [":"; "⁝"; ]; ["."; "•"; "◦"; ]; ["#"; "⌘"; ]; ["-"; "÷"; "⊢"; ];