From cb38da6095e3af84131a3ebf47a9f252f34a804c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 1 Jun 2012 12:34:16 +0000 Subject: [PATCH] - predefined_virtuals: some additions - lambda_delta: first results on lenv. ref. for native typing some notational changes --- .../apps_2/functional/rtm_step.ma | 2 +- .../lambda_delta/apps_2/functional/subst.ma | 4 +- .../contribs/lambda_delta/basic_2/basic_1.txt | 12 +-- .../basic_2/computation/acp_cr.ma | 2 +- .../lambda_delta/basic_2/computation/cprs.ma | 4 +- .../basic_2/computation/cprs_delift.ma | 4 +- .../basic_2/computation/cprs_tstc.ma | 4 +- .../basic_2/computation/cprs_tstc_vector.ma | 4 +- .../lambda_delta/basic_2/computation/csn.ma | 2 +- .../basic_2/computation/csn_tstc_vector.ma | 2 +- .../lambda_delta/basic_2/dynamic/lsubn.ma | 100 ++++++++++++++++++ .../basic_2/dynamic/lsubn_ldrop.ma | 64 +++++++++++ .../lambda_delta/basic_2/dynamic/lsubn_nta.ma | 47 ++++++++ .../lambda_delta/basic_2/dynamic/nta.ma | 6 +- .../lambda_delta/basic_2/dynamic/nta_alt.ma | 4 +- .../lambda_delta/basic_2/dynamic/nta_lift.ma | 4 +- .../lambda_delta/basic_2/dynamic/nta_nta.ma | 2 +- .../lambda_delta/basic_2/dynamic/nta_thin.ma | 6 +- .../basic_2/equivalence/cpcs_delift.ma | 4 +- .../basic_2/etc/lsubn/lsubn_lsubn.etc | 36 +++++++ .../contribs/lambda_delta/basic_2/names.txt | 2 +- .../contribs/lambda_delta/basic_2/notation.ma | 10 +- .../lambda_delta/basic_2/reducibility/cpr.ma | 6 +- .../basic_2/reducibility/cpr_delift.ma | 4 +- .../lambda_delta/basic_2/reducibility/tif.ma | 2 +- .../lambda_delta/basic_2/reducibility/tnf.ma | 2 +- .../lambda_delta/basic_2/reducibility/tpr.ma | 10 +- .../basic_2/reducibility/tpr_delift.ma | 4 +- .../basic_2/reducibility/tpr_tpr.ma | 2 +- .../lambda_delta/basic_2/reducibility/trf.ma | 2 +- .../lambda_delta/basic_2/static/aaa.ma | 6 +- .../lambda_delta/basic_2/static/sta.ma | 6 +- .../lambda_delta/basic_2/unfold/delift.ma | 42 ++++---- .../lambda_delta/basic_2/unfold/delift_alt.ma | 20 ++-- .../basic_2/unfold/delift_delift.ma | 2 +- .../basic_2/unfold/delift_lift.ma | 32 +++--- .../basic_2/unfold/delift_ltpss.ma | 6 +- .../basic_2/unfold/delift_tpss.ma | 32 +++--- .../basic_2/unfold/ltpss_ltpss.ma | 4 +- .../lambda_delta/basic_2/unfold/thin.ma | 6 +- .../basic_2/unfold/thin_delift.ma | 46 ++++---- .../lambda_delta/basic_2/unfold/thin_ldrop.ma | 16 +-- matita/matita/predefined_virtuals.ml | 9 +- 43 files changed, 410 insertions(+), 174 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_ldrop.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/etc/lsubn/lsubn_lsubn.etc diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma index 9a04c8070..bf04f72c9 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma @@ -37,7 +37,7 @@ inductive rtm_step: relation rtm ≝ rtm_step (mk_rtm (G. ⓛV) u E S (§p)) (mk_rtm G u E S V) | rtm_tau : ∀G,u,E,S,W,T. - rtm_step (mk_rtm G u E S (ⓣW. T)) + rtm_step (mk_rtm G u E S (ⓝW. T)) (mk_rtm G u E S T) | rtm_appl : ∀G,u,E,S,V,T. rtm_step (mk_rtm G u E S (ⓐV. T)) diff --git a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma index e8ba1c2f2..78f319a06 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma @@ -34,7 +34,7 @@ interpretation "functional core substitution" 'Subst V d T = (fsubst V d T). (* Main properties **********************************************************) theorem fsubst_delift: ∀K,V,T,L,d. - ⇩[0, d] L ≡ K. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T. + ⇩[0, d] L ≡ K. ⓓV → L ⊢ T ▼*[d, 1] ≡ [d ← V] T. #K #V #T elim T -T [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/ elim (lt_or_eq_or_gt i d) #Hid @@ -49,7 +49,7 @@ qed. (* Main inversion properties ************************************************) theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV → - L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2. + L ⊢ T1 ▼*[d, 1] ≡ T2 → [d ← V] T1 = T2. #K #V #T1 elim T1 -T1 [ * #i #L #T2 #d #HLK #H [ -HLK >(delift_inv_sort1 … H) -H // diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt index 87bf34936..9e3ecb792 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -78,22 +78,12 @@ csubc/arity csubc_arity_trans csubc/drop1 drop1_csubc_trans csubc/drop drop_csubc_trans -csubt/clear csubt_clear_conf csubt/csuba csubt_csuba -csubt/drop csubt_drop_flat -csubt/drop csubt_drop_abbr -csubt/drop csubt_drop_abst csubt/fwd csubt_gen_abbr csubt/fwd csubt_gen_abst -csubt/fwd csubt_gen_flat -csubt/fwd csubt_gen_bind -csubt/getl csubt_getl_abbr -csubt/getl csubt_getl_abst csubt/pc3 csubt_pr2 csubt/pc3 csubt_pc3 -csubt/props csubt_refl -csubt/ty3 csubt_ty3 -csubt/ty3 csubt_ty3_ld + csubv/clear csubv_clear_conf csubv/clear csubv_clear_conf_void csubv/drop csubv_drop_conf diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma index 1805953b9..5b8a2c1ea 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma @@ -42,7 +42,7 @@ definition S5 ≝ λRP,C:lenv→predicate term. ∀V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓV. T). definition S6 ≝ λRP,C:lenv→predicate term. - ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓣW. T). + ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓝW. T). definition S7 ≝ λC:lenv→predicate term. ∀L2,L1,T1,d,e. C L1 T1 → ∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma index a25a36a3e..dbd23a0a4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma @@ -78,8 +78,8 @@ lemma cprs_inv_sort1: ∀L,U2,k. L ⊢ ⋆k ➡* U2 → U2 = ⋆k. qed-. (* Basic_1: was: pr3_gen_cast *) -lemma cprs_inv_cast1: ∀L,W1,T1,U2. L ⊢ ⓣW1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨ - ∃∃W2,T2. L ⊢ W1 ➡* W2 & L ⊢ T1 ➡* T2 & U2 = ⓣW2.T2. +lemma cprs_inv_cast1: ∀L,W1,T1,U2. L ⊢ ⓝW1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨ + ∃∃W2,T2. L ⊢ W1 ➡* W2 & L ⊢ T1 ➡* T2 & U2 = ⓝW2.T2. #L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ #U2 #U #_ #HU2 * /3 width=3/ * #W #T #HW1 #HT1 #H destruct diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma index 65488a734..14b516624 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_delift.ma @@ -21,8 +21,8 @@ include "basic_2/computation/cprs.ma". (* Basic_1: was only: pr3_gen_cabbr *) lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 → - ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 → - ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ U2 [d, e] ≡ T2. + ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 → + ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ U2 ▼*[d, e] ≡ T2. #L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/ #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1 elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma index 59668d4d1..eb59c5f84 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma @@ -84,8 +84,8 @@ elim (cprs_inv_appl1 … H) -H * ] qed-. -lemma cprs_fwd_tau: ∀L,W,T,U. L ⊢ ⓣW. T ➡* U → - ⓣW. T ≃ U ∨ L ⊢ T ➡* U. +lemma cprs_fwd_tau: ∀L,W,T,U. L ⊢ ⓝW. T ➡* U → + ⓝW. T ≃ U ∨ L ⊢ T ➡* U. #L #W #T #U #H elim (cprs_inv_cast1 … H) -H /2 width=1/ * #W0 #T0 #_ #_ #H destruct /2 width=1/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma index a7f9b33cd..5a4c2bc34 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma @@ -134,8 +134,8 @@ elim (cprs_inv_appl1 … H) -H * qed-. (* Basic_1: was: pr3_iso_appls_cast *) -lemma cprs_fwd_tau_vector: ∀L,Vs,W,T,U. L ⊢ ⒶVs. ⓣW. T ➡* U → - ⒶVs. ⓣW. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U. +lemma cprs_fwd_tau_vector: ∀L,Vs,W,T,U. L ⊢ ⒶVs. ⓝW. T ➡* U → + ⒶVs. ⓝW. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U. #L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_tau/ #V #Vs #IHVs #W #T #U #H elim (cprs_inv_appl1 … H) -H * diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma index 481683f2a..c9b39fce3 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma @@ -55,7 +55,7 @@ elim (term_eq_dec T1 T2) #HT12 qed. (* Basic_1: was: sn3_cast *) -lemma csn_cast: ∀L,W. L ⊢ ⬇* W → ∀T. L ⊢ ⬇* T → L ⊢ ⬇* ⓣW. T. +lemma csn_cast: ∀L,W. L ⊢ ⬇* W → ∀T. L ⊢ ⬇* T → L ⊢ ⬇* ⓝW. T. #L #W #HW elim HW -W #W #_ #IHW #T #HT @(csn_ind … HT) -T #T #HT #IHT @csn_intro #X #H1 #H2 elim (cpr_inv_cast1 … H1) -H1 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma index 566084615..205642fac 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma @@ -90,7 +90,7 @@ qed. (* Basic_1: was: sn3_appls_cast *) lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W → ∀Vs,T. L ⊢ ⬇* ⒶVs. T → - L ⊢ ⬇* ⒶVs. ⓣW. T. + L ⊢ ⬇* ⒶVs. ⓝW. T. #L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW #V #Vs #IHV #T #H1T lapply (csn_fwd_pair_sn … H1T) #HV diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma new file mode 100644 index 000000000..9a4eaac88 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma @@ -0,0 +1,100 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/nta.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************) + +(* Note: may not be transitive *) +inductive lsubn (h:sh): relation lenv ≝ +| lsubn_atom: lsubn h (⋆) (⋆) +| lsubn_pair: ∀I,L1,L2,W. lsubn h L1 L2 → lsubn h (L1. ⓑ{I} W) (L2. ⓑ{I} W) +| lsubn_abbr: ∀L1,L2,V,W. ⦃h, L1⦄ ⊢ V : W → ⦃h, L2⦄ ⊢ V : W → + lsubn h L1 L2 → lsubn h (L1. ⓓV) (L2. ⓛW) +. + +interpretation + "local environment refinement (native type assigment)" + 'CrSubEqN h L1 L2 = (lsubn h L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact lsubn_inv_atom1_aux: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L1 = ⋆ → L2 = ⋆. +#h #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V #W #_ #_ #_ #H destruct +] +qed. + +lemma lsubn_inv_atom1: ∀h,L2. h ⊢ ⋆ :⊑ L2 → L2 = ⋆. +/2 width=4/ qed-. + +fact lsubn_inv_pair1_aux: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V → + (∃∃K2. h ⊢ K1 :⊑ K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W. ⦃h, K1⦄ ⊢ V : W & ⦃h, K2⦄ ⊢ V : W & + h ⊢ K1 :⊑ K2 & L2 = K2. ⓛW & I = Abbr. +#h #L1 #L2 * -L1 -L2 +[ #I #K1 #V #H destruct +| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/ +| #L1 #L2 #V #W #H1VW #H2VW #HL12 #I #K1 #V1 #H destruct /3 width=7/ +] +qed. + +lemma lsubn_inv_pair1: ∀h,I,K1,L2,V. h ⊢ K1. ⓑ{I} V :⊑ L2 → + (∃∃K2. h ⊢ K1 :⊑ K2 & L2 = K2. ⓑ{I} V) ∨ + ∃∃K2,W. ⦃h, K1⦄ ⊢ V : W & ⦃h, K2⦄ ⊢ V : W & + h ⊢ K1 :⊑ K2 & L2 = K2. ⓛW & I = Abbr. +/2 width=3/ qed-. + +fact lsubn_inv_atom2_aux: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L2 = ⋆ → L1 = ⋆. +#h #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V #W #_ #_ #_ #H destruct +] +qed. + +lemma lsubc_inv_atom2: ∀h,L1. h ⊢ L1 :⊑ ⋆ → L1 = ⋆. +/2 width=4/ qed-. + +fact lsubn_inv_pair2_aux: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W → + (∃∃K1. h ⊢ K1 :⊑ K2 & L1 = K1. ⓑ{I} W) ∨ + ∃∃K1,V. ⦃h, K1⦄ ⊢ V : W & ⦃h, K2⦄ ⊢ V : W & + h ⊢ K1 :⊑ K2 & L1 = K1. ⓓV & I = Abst. +#h #L1 #L2 * -L1 -L2 +[ #I #K2 #W #H destruct +| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/ +| #L1 #L2 #V #W #H1VW #H2VW #HL12 #I #K2 #W2 #H destruct /3 width=7/ +] +qed. + +(* Basic_1: was: csubt_gen_bind *) +lemma lsubn_inv_pair2: ∀h,I,L1,K2,W. h ⊢ L1 :⊑ K2. ⓑ{I} W → + (∃∃K1. h ⊢ K1 :⊑ K2 & L1 = K1. ⓑ{I} W) ∨ + ∃∃K1,V. ⦃h, K1⦄ ⊢ V : W & ⦃h, K2⦄ ⊢ V : W & + h ⊢ K1 :⊑ K2 & L1 = K1. ⓓV & I = Abst. +/2 width=3/ qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: csubt_refl *) +lemma lsubn_refl: ∀h,L. h ⊢ L :⊑ L. +#h #L elim L -L // /2 width=1/ +qed. + +(* Basic_1: removed theorems 6: + csubt_gen_flat csubt_drop_flat csubt_clear_conf + csubt_getl_abbr csubt_getl_abst csubt_ty3_ld +*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_ldrop.ma new file mode 100644 index 000000000..a16fff618 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_ldrop.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/lsubn.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************) + +(* Properties concerning basic local environment slicing ********************) + +(* Note: the constant 0 cannot be generalized *) +lemma lsubn_ldrop_O1_conf: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 → + ∃∃K2. h ⊢ K1 :⊑ K2 & ⇩[0, e] L2 ≡ K2. +#h #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3/ +| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK1 + [ destruct + elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK1) -L1 /3 width=3/ + ] +| #L1 #L2 #V #W #H1VW #H2VW #_ #IHL12 #K1 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK1 + [ destruct + elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK1) -L1 /3 width=3/ + ] +] +qed. + +(* Note: the constant 0 cannot be generalized *) +(* Basic_1: was only: csubt_drop_abbr csubt_drop_abst *) +lemma lsubn_ldrop_O1_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. h ⊢ K1 :⊑ K2 & ⇩[0, e] L1 ≡ K1. +#h #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3/ +| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK2 + [ destruct + elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK2) -L2 /3 width=3/ + ] +| #L1 #L2 #V #W #H1VW #H2VW #_ #IHL12 #K2 #e #H + elim (ldrop_inv_O1 … H) -H * #He #HLK2 + [ destruct + elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H + <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ + | elim (IHL12 … HLK2) -L2 /3 width=3/ + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma new file mode 100644 index 000000000..6f91a1c52 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/nta_nta.ma". +include "basic_2/dynamic/lsubn_ldrop.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************) + +(* Properties concerning atomic arity assignment ****************************) + +(* Note: the corresponding confluence property does not hold *) +(* Basic_1: was: csubt_ty3 *) +axiom lsubn_nta_trans: ∀h,L2,T,U. ⦃h, L2⦄ ⊢ T : U → ∀L1. h ⊢ L1 :⊑ L2 → + ⦃h, L1⦄ ⊢ T : U. +(* +#h #L2 #T #U #H elim H -L2 -T -U +[ // +| #L2 #K2 #V2 #W2 #U2 #i #HLK2 #_ #WU2 #IHVW2 #L1 #HL12 + elim (lsubn_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubn_inv_pair2 … H) -H * #K1 + [ #HK12 #H destruct /3 width=6/ + | #V1 #_ #_ #_ #_ #H destruct + ] +| #L2 #K2 #W2 #V2 #U2 #i #HLK2 #_ #HWU2 #IHWV2 #L1 #HL12 + elim (lsubn_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubn_inv_pair2 … H) -H * #K1 [ | -IHWV2 ] + [ #HK12 #H destruct /3 width=6/ + | #V1 #H1V1W2 #_ #_ #H #_ destruct /2 width=6/ + ] +| /4 width=2/ +| /3 width=1/ +| /3 width=2/ +| /3 width=1/ +] +qed. +*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma index 7a24249f2..fa4a8ed8f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma @@ -29,7 +29,7 @@ inductive nta (h:sh): lenv → relation term ≝ nta h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U) | nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W → nta h L (ⓐV.T) (ⓐV.U) -| nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓣU. T) U +| nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓝU. T) U | nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 → nta h L T U2 . @@ -41,11 +41,11 @@ interpretation "native type assignment (term)" (* Basic_1: was: ty3_cast *) lemma nta_cast_old: ∀h,L,W,T,U. - ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → ⦃h, L⦄ ⊢ ⓣU.T : ⓣW.U. + ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → ⦃h, L⦄ ⊢ ⓝU.T : ⓝW.U. /4 width=3/ qed. (* Basic_1: was: ty3_typecheck *) -lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓣU.T : T0. +lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓝU.T : T0. /3 width=2/ qed. (* Basic_1: removed theorems 4: diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma index 9c1567460..8cbd59518 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma @@ -30,7 +30,7 @@ inductive ntaa (h:sh): lenv → relation term ≝ ntaa h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U) | ntaa_pure: ∀L,V,W,T,U. ntaa h L T U → ntaa h L (ⓐV.U) W → ntaa h L (ⓐV.T) (ⓐV.U) -| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓣU. T) U +| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U | ntaa_conv: ∀L,T,U1,U2,V2. ntaa h L T U1 → L ⊢ U1 ⬌* U2 → ntaa h L U2 V2 → ntaa h L T U2 . @@ -177,7 +177,7 @@ lemma nta_ind_alt: ∀h. ∀R:lenv→relation term. ) → (∀L,T,U,W. ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → - R L T U → R L U W → R L (ⓣU.T) U + R L T U → R L U W → R L (ⓝU.T) U ) → (∀L,T,U1,U2,V2. ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma index 294c1710e..0631ca4f2 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma @@ -77,7 +77,7 @@ lemma nta_inv_bind1: ∀h,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{I}Y.X : U → elim (ntaa_inv_bind1 … (nta_ntaa … H)) -H /3 width=3 by ntaa_nta, ex3_2_intro/ qed-. -fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X → +fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓝY.X → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U. #h #L #T #U #H elim H -L -T -U [ #L #k #X #Y #H destruct @@ -94,7 +94,7 @@ fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X qed. (* Basic_1: was: ty3_gen_cast *) -lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U. +lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓝY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U. /2 width=3/ qed-. (* Advanced forvard lemmas **************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma index f0bf7119e..b36725d92 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma @@ -52,7 +52,7 @@ qed-. (* Advanced properties ******************************************************) lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T : W → ⦃h, L⦄ ⊢ T : U → - ⦃h, L⦄ ⊢ ⓣW.T : U. + ⦃h, L⦄ ⊢ ⓝW.T : U. #h #L #T #W #U #HTW #HTU lapply (nta_mono … HTW … HTU) #HWU elim (nta_fwd_correct … HTU) -HTU /3 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma index 1c0b1f053..c3f94f9eb 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma @@ -25,9 +25,9 @@ include "basic_2/dynamic/nta_lift.ma". (* Note: this is known as the substitution lemma *) (* Basic_1: was only: ty3_gen_cabbr *) lemma nta_thin_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → - ∀L2,d,e. ≼ [d, e] L1 → L1 [d, e] ≡ L2 → + ∀L2,d,e. ≼ [d, e] L1 → L1 ▼*[d, e] ≡ L2 → ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 & - L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2. + L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2. #h #L1 #T1 #U1 #H elim H -L1 -T1 -U1 [ /2 width=5/ | #L1 #K1 #V1 #W1 #U1 #i #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL1 #HL12 @@ -114,5 +114,5 @@ qed. lemma nta_ldrop_conf: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ≼ [d, e] L1 → ⇩[d, e] L1 ≡ L2 → ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : U2 & - L1 ⊢ T1 [d, e] ≡ T2 & L1 ⊢ U1 [d, e] ≡ U2. + L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2. /3 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma index 58697b9c1..e57f9f32b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma @@ -22,8 +22,8 @@ include "basic_2/equivalence/cpcs_cpcs.ma". (* Basic_1: was only: pc3_gen_cabbr *) lemma thin_cpcs_delift_mono: ∀L,U1,U2. L ⊢ U1 ⬌* U2 → - ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 → - ∀T2. L ⊢ U2 [d, e] ≡ T2 → K ⊢ T1 ⬌* T2. + ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 → + ∀T2. L ⊢ U2 ▼*[d, e] ≡ T2 → K ⊢ T1 ⬌* T2. #L #U1 #U2 #H #K #d #e #HLK #T1 #HTU1 #T2 #HTU2 elim (cpcs_inv_cprs … H) -H #U #HU1 #HU2 elim (thin_cprs_delift_conf … HU1 … HLK … HTU1) -U1 #T #HT1 #HUT diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubn/lsubn_lsubn.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubn/lsubn_lsubn.etc new file mode 100644 index 000000000..9ef3dda88 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubn/lsubn_lsubn.etc @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/lsubn_nta.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************) + +(* Main properties **********************************************************) + +(* Note: new property *) +theorem lsubn_trans: ∀h,L1,L. h ⊢ L1 :⊑ L → ∀L2. h ⊢ L :⊑ L2 → h ⊢ L1 :⊑ L2. +#h #L1 #L #H elim H -L1 -L +[ #X #H >(lsubn_inv_atom1 … H) -H // +| #I #L1 #L #V #HL1 #H1W #IHL1 #X #H + elim (lsubn_inv_pair1 … H) -H * #L2 + [ #HL2 #H #H2W destruct /4 width=1/ + | #W #H1VW #H2VW #HL2 #H1 #H2 destruct /3 width=3/ + ] +| #L1 #L #V1 #W1 #H1VW1 #H2VW1 #HL1 #IHL1 #X #H + elim (lsubn_inv_pair1 … H) -H * #L2 + [ #HL2 #H #HW destruct /3 width=1/ + | #V #_ #_ #_ #_ #H destruct + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/names.txt b/matita/matita/contribs/lambda_delta/basic_2/names.txt index dfa83ebdd..31ae26c39 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/names.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/names.txt @@ -37,4 +37,4 @@ b: binder d: abbreviation f: flat l: abstraction -t: native type annotation +n: native type annotation diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index ba7e981ca..eb3d61cac 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -68,7 +68,7 @@ notation "hvbox( ⓐ term 55 T1 . break term 55 T2 )" non associative with precedence 55 for @{ 'SnAppl $T1 $T2 }. -notation "hvbox( ⓣ term 55 T1 . break term 55 T2 )" +notation "hvbox( ⓝ term 55 T1 . break term 55 T2 )" non associative with precedence 55 for @{ 'SnCast $T1 $T2 }. @@ -188,19 +188,19 @@ notation "hvbox( L ⊢ break term 46 T1 break ▶▶* [ d , break e ] break term non associative with precedence 45 for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }. -notation "hvbox( T1 break [ d , break e ] ≡ break term 46 T2 )" +notation "hvbox( T1 break ▼* [ d , break e ] ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubst $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡ break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▼* [ d , break e ] ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubst $L $T1 $d $e $T2 }. -notation "hvbox( T1 break [ d , break e ] ≡ ≡ break term 46 T2 )" +notation "hvbox( T1 break ▼▼* [ d , break e ] ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $T1 $d $e $T2 }. -notation "hvbox( L ⊢ break term 46 T1 break [ d , break e ] ≡ ≡ break term 46 T2 )" +notation "hvbox( L ⊢ break term 46 T1 break ▼▼* [ d , break e ] ≡ break term 46 T2 )" non associative with precedence 45 for @{ 'TSubstAlt $L $T1 $d $e $T2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma index caa36dfd5..18ad47c3e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma @@ -49,7 +49,7 @@ lemma cpr_flat: ∀I,L,V1,V2,T1,T2. qed. lemma cpr_cast: ∀L,V,T1,T2. - L ⊢ T1 ➡ T2 → L ⊢ ⓣV. T1 ➡ T2. + L ⊢ T1 ➡ T2 → L ⊢ ⓝV. T1 ➡ T2. #L #V #T1 #T2 * /3 width=3/ qed. @@ -97,9 +97,9 @@ elim (tpr_inv_abbr1 … H1) -H1 * qed-. (* Basic_1: was: pr2_gen_cast *) -lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓣV1. T1 ➡ U2 → ( +lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓝV1. T1 ➡ U2 → ( ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 & - U2 = ⓣV2. T2 + U2 = ⓝV2. T2 ) ∨ L ⊢ T1 ➡ U2. #L #V1 #T1 #U2 * #X #H #HU2 elim (tpr_inv_cast1 … H) -H /3 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma index 7437e6ac8..40c9074bd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_delift.ma @@ -22,8 +22,8 @@ include "basic_2/reducibility/cpr.ma". (* Basic_1: was only: pr2_gen_cabbr *) lemma thin_cpr_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡ U2 → - ∀K,d,e. L [d, e] ≡ K → ∀T1. L ⊢ U1 [d, e] ≡ T1 → - ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ U2 [d, e] ≡ T2. + ∀K,d,e. L ▼*[d, e] ≡ K → ∀T1. L ⊢ U1 ▼*[d, e] ≡ T1 → + ∃∃T2. K ⊢ T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2. #L #U1 #U2 * #U #HU1 #HU2 #K #d #e #HLK #T1 #HTU1 elim (tpr_delift_conf … HU1 … HTU1) -U1 #T #HT1 #HUT elim (le_or_ge (|L|) d) #Hd diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma index a745dd844..26e2d137b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma @@ -35,7 +35,7 @@ generalize in match HVT; -HVT elim T -T // * // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/ qed-. -lemma tif_inv_cast: ∀V,T. 𝐈⦃ⓣV.T⦄ → ⊥. +lemma tif_inv_cast: ∀V,T. 𝐈⦃ⓝV.T⦄ → ⊥. /2 width=1/ qed-. (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma index 294546af9..2e357a292 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma @@ -53,7 +53,7 @@ lemma tnf_inv_abbr: ∀V,T. 𝐍⦃ⓓV.T⦄ → ⊥. ] qed. -lemma tnf_inv_cast: ∀V,T. 𝐍⦃ⓣV.T⦄ → ⊥. +lemma tnf_inv_cast: ∀V,T. 𝐍⦃ⓝV.T⦄ → ⊥. #V #T #H lapply (H T ?) -H /2 width=1/ #H @discr_tpair_xy_y // qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma index 8cb87ef2c..79d8df114 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma @@ -30,7 +30,7 @@ inductive tpr: relation term ≝ tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 → tpr (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2) | tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2 -| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (ⓣV. T1) T2 +| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (ⓝV. T1) T2 . interpretation @@ -169,8 +169,8 @@ elim (tpr_inv_appl1 … H) -H * qed-. (* Basic_1: was: pr0_gen_cast *) -lemma tpr_inv_cast1: ∀V1,T1,U2. ⓣV1. T1 ➡ U2 → - (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓣV2. T2) +lemma tpr_inv_cast1: ∀V1,T1,U2. ⓝV1. T1 ➡ U2 → + (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓝV2. T2) ∨ T1 ➡ U2. #V1 #T1 #U2 #H elim (tpr_inv_flat1 … H) -H * /3 width=5/ @@ -183,7 +183,7 @@ fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i → ∨∨ T1 = #i | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i & T1 = ⓓV. T - | ∃∃V,T. T ➡ #i & T1 = ⓣV. T. + | ∃∃V,T. T ➡ #i & T1 = ⓝV. T. #T1 #T2 * -T1 -T2 [ #I #i #H destruct /2 width=1/ | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct @@ -199,7 +199,7 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i → ∨∨ T1 = #i | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i & T1 = ⓓV. T - | ∃∃V,T. T ➡ #i & T1 = ⓣV. T. + | ∃∃V,T. T ➡ #i & T1 = ⓝV. T. /2 width=3/ qed-. (* Basic_1: removed theorems 3: diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma index 3cbff71ce..762640521 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_delift.ma @@ -19,8 +19,8 @@ include "basic_2/reducibility/tpr_tpss.ma". (* Properties on inverse basic term relocation ******************************) -lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 [d, e] ≡ T1 → - ∃∃T2. T1 ➡ T2 & L ⊢ U2 [d, e] ≡ T2. +lemma tpr_delift_conf: ∀U1,U2. U1 ➡ U2 → ∀L,T1,d,e. L ⊢ U1 ▼*[d, e] ≡ T1 → + ∃∃T2. T1 ➡ T2 & L ⊢ U2 ▼*[d, e] ≡ T2. #U1 #U2 #HU12 #L #T1 #d #e * #W1 #HUW1 #HTW1 elim (tpr_tpss_conf … HU12 … HUW1) -U1 #U1 #HWU1 #HU21 elim (tpr_inv_lift … HWU1 … HTW1) -W1 /3 width=5/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma index 2082ab368..fcb2350e9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma @@ -97,7 +97,7 @@ fact tpr_conf_flat_cast: ∃∃X. X1 ➡ X & X2 ➡ X ) → V0 ➡ V1 → T0 ➡ T1 → T0 ➡ X2 → - ∃∃X. ⓣV1. T1 ➡ X & X2 ➡ X. + ∃∃X. ⓝV1. T1 ➡ X & X2 ➡ X. #X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02 elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma index eb3576d84..6d6993de3 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma @@ -23,7 +23,7 @@ inductive trf: predicate term ≝ | trf_appl_sn: ∀V,T. trf V → trf (ⓐV. T) | trf_appl_dx: ∀V,T. trf T → trf (ⓐV. T) | trf_abbr : ∀V,T. trf (ⓓV. T) -| trf_cast : ∀V,T. trf (ⓣV. T) +| trf_cast : ∀V,T. trf (ⓝV. T) | trf_beta : ∀V,W,T. trf (ⓐV. ⓛW. T) . 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 59e110db2..fa6649769 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma @@ -25,7 +25,7 @@ inductive aaa: lenv → term → predicate aarity ≝ | aaa_abst: ∀L,V,T,B,A. aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛV. T) (②B. A) | aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (②B. A) → aaa L (ⓐV. T) A -| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (ⓣV. T) A +| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (ⓝV. T) A . interpretation "atomic arity assignment (term)" @@ -111,7 +111,7 @@ 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 → +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 @@ -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 → +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/sta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma index 4c38a083b..20302c623 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma @@ -27,7 +27,7 @@ inductive sta (h:sh): lenv → relation term ≝ sta h L (ⓑ{I}V.T) (ⓑ{I}V.U) | sta_appl: ∀L,V,T,U. sta h L T U → sta h L (ⓐV.T) (ⓐV.U) -| sta_cast: ∀L,W,T,U. sta h L T U → sta h L (ⓣW. T) U +| sta_cast: ∀L,W,T,U. sta h L T U → sta h L (ⓝW. T) U . interpretation "static type assignment (term)" @@ -111,7 +111,7 @@ lemma sta_inv_appl1: ∀h,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X • U → ∃∃Z. ⦃h, L⦄ ⊢ X • Z & U = ⓐY.Z. /2 width=3/ qed-. -fact sta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓣY.X → +fact sta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓝY.X → ⦃h, L⦄ ⊢ X • U. #h #L #T #U * -L -T -U [ #L #k #X #Y #H destruct @@ -124,5 +124,5 @@ fact sta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓣY. qed. (* Basic_1: was: sty0_gen_cast *) -lemma sta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X • U → ⦃h, L⦄ ⊢ X • U. +lemma sta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓝY.X • U → ⦃h, L⦄ ⊢ X • U. /2 width=4/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma index f0935a041..82cd0c87f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma @@ -25,59 +25,59 @@ interpretation "inverse basic relocation (term)" (* Basic properties *********************************************************) lemma lift_delift: ∀T1,T2,d,e. ⇧[d, e] T1 ≡ T2 → - ∀L. L ⊢ T2 [d, e] ≡ T1. + ∀L. L ⊢ T2 ▼*[d, e] ≡ T1. /2 width=3/ qed. -lemma delift_refl_O2: ∀L,T,d. L ⊢ T [d, 0] ≡ T. +lemma delift_refl_O2: ∀L,T,d. L ⊢ T ▼*[d, 0] ≡ T. /2 width=3/ qed. -lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 → - ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡ T2. +lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼*[d, e] ≡ T2 → + ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▼*[d, e] ≡ T2. #L1 #T1 #T2 #d #e * /3 width=3/ qed. -lemma delift_sort: ∀L,d,e,k. L ⊢ ⋆k [d, e] ≡ ⋆k. +lemma delift_sort: ∀L,d,e,k. L ⊢ ⋆k ▼*[d, e] ≡ ⋆k. /2 width=3/ qed. -lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ #i [d, e] ≡ #i. +lemma delift_lref_lt: ∀L,d,e,i. i < d → L ⊢ #i ▼*[d, e] ≡ #i. /3 width=3/ qed. -lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ #i [d, e] ≡ #(i - e). +lemma delift_lref_ge: ∀L,d,e,i. d + e ≤ i → L ⊢ #i ▼*[d, e] ≡ #(i - e). /3 width=3/ qed. -lemma delift_gref: ∀L,d,e,p. L ⊢ §p [d, e] ≡ §p. +lemma delift_gref: ∀L,d,e,p. L ⊢ §p ▼*[d, e] ≡ §p. /2 width=3/ qed. lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e. - L ⊢ V1 [d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 → - L ⊢ ⓑ{I} V1. T1 [d, e] ≡ ⓑ{I} V2. T2. + L ⊢ V1 ▼*[d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 → + L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡ ⓑ{I} V2. T2. #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2 lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/ qed. lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e. - L ⊢ V1 [d, e] ≡ V2 → L ⊢ T1 [d, e] ≡ T2 → - L ⊢ ⓕ{I} V1. T1 [d, e] ≡ ⓕ{I} V2. T2. + L ⊢ V1 ▼*[d, e] ≡ V2 → L ⊢ T1 ▼*[d, e] ≡ T2 → + L ⊢ ⓕ{I} V1. T1 ▼*[d, e] ≡ ⓕ{I} V2. T2. #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/ qed. (* Basic inversion lemmas ***************************************************) -lemma delift_inv_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k [d, e] ≡ U2 → U2 = ⋆k. +lemma delift_inv_sort1: ∀L,U2,d,e,k. L ⊢ ⋆k ▼*[d, e] ≡ U2 → U2 = ⋆k. #L #U2 #d #e #k * #U #HU >(tpss_inv_sort1 … HU) -HU #HU2 >(lift_inv_sort2 … HU2) -HU2 // qed-. -lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ §p [d, e] ≡ U2 → U2 = §p. +lemma delift_inv_gref1: ∀L,U2,d,e,p. L ⊢ §p ▼*[d, e] ≡ U2 → U2 = §p. #L #U #d #e #p * #U #HU >(tpss_inv_gref1 … HU) -HU #HU2 >(lift_inv_gref2 … HU2) -HU2 // qed-. -lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 [d, e] ≡ U2 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 & - L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 & +lemma delift_inv_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 ▼*[d, e] ≡ U2 → + ∃∃V2,T2. L ⊢ V1 ▼*[d, e] ≡ V2 & + L. ⓑ{I} V2 ⊢ T1 ▼*[d+1, e] ≡ T2 & U2 = ⓑ{I} V2. T2. #I #L #V1 #T1 #U2 #d #e * #U #HU #HU2 elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct @@ -85,16 +85,16 @@ elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2 lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/ qed-. -lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 [d, e] ≡ U2 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 & - L ⊢ T1 [d, e] ≡ T2 & +lemma delift_inv_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 ▼*[d, e] ≡ U2 → + ∃∃V2,T2. L ⊢ V1 ▼*[d, e] ≡ V2 & + L ⊢ T1 ▼*[d, e] ≡ T2 & U2 = ⓕ{I} V2. T2. #I #L #V1 #T1 #U2 #d #e * #U #HU #HU2 elim (tpss_inv_flat1 … HU) -HU #V #T #HV1 #HT1 #X destruct elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/ qed-. -lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≡ T2 → T1 = T2. +lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▼*[d, 0] ≡ T2 → T1 = T2. #L #T1 #T2 #d * #T #HT1 >(tpss_inv_refl_O2 … HT1) -HT1 #HT2 >(lift_inv_refl_O2 … HT2) -HT2 // diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma index 34b2d2c20..0cc9f55b5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_alt.ma @@ -38,8 +38,8 @@ interpretation "inverse basic relocation (term) alternative" (* Basic properties *********************************************************) -lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡≡ T2 → - ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 [d, e] ≡≡ T2. +lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▼▼*[d, e] ≡ T2 → + ∀L2. L1 ≼ [d, e] L2 → L2 ⊢ T1 ▼▼*[d, e] ≡ T2. #L1 #T1 #T2 #d #e #H elim H -L1 -T1 -T2 -d -e // /2 width=1/ [ #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 elim (ldrop_lsubs_ldrop1_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // /3 width=6/ @@ -48,7 +48,7 @@ lemma delifta_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡≡ T2 → ] qed. -lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡≡ T2. +lemma delift_delifta: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → L ⊢ T1 ▼▼*[d, e] ≡ T2. #L #T1 @(cw_wf_ind … L T1) -L -T1 #L #T1 elim T1 -T1 [ * #i #IH #T2 #d #e #H [ >(delift_inv_sort1 … H) -H // @@ -73,7 +73,7 @@ qed. (* Basic inversion lemmas ***************************************************) -lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡≡ T2 → L ⊢ T1 [d, e] ≡ T2. +lemma delifta_delift: ∀L,T1,T2,d,e. L ⊢ T1 ▼▼*[d, e] ≡ T2 → L ⊢ T1 ▼*[d, e] ≡ T2. #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e // /2 width=1/ /2 width=6/ qed-. @@ -81,20 +81,20 @@ lemma delift_ind_alt: ∀R:ℕ→ℕ→lenv→relation term. (∀L,d,e,k. R d e L (⋆k) (⋆k)) → (∀L,d,e,i. i < d → R d e L (#i) (#i)) → (∀L,K,V1,V2,W2,i,d,e. d ≤ i → i < d + e → - ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 [O, d + e - i - 1] ≡ V2 → + ⇩[O, i] L ≡ K.ⓓV1 → K ⊢ V1 ▼*[O, d + e - i - 1] ≡ V2 → ⇧[O, d] V2 ≡ W2 → R O (d+e-i-1) K V1 V2 → R d e L #i W2 ) → (∀L,d,e,i. d + e ≤ i → R d e L (#i) (#(i - e))) → (∀L,d,e,p. R d e L (§p) (§p)) → - (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 → - L.ⓑ{I}V2 ⊢ T1 [d + 1, e] ≡ T2 → R d e L V1 V2 → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▼*[d, e] ≡ V2 → + L.ⓑ{I}V2 ⊢ T1 ▼*[d + 1, e] ≡ T2 → R d e L V1 V2 → R (d+1) e (L.ⓑ{I}V2) T1 T2 → R d e L (ⓑ{I}V1.T1) (ⓑ{I}V2.T2) ) → - (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 [d, e] ≡ V2 → - L⊢ T1 [d, e] ≡ T2 → R d e L V1 V2 → + (∀L,I,V1,V2,T1,T2,d,e. L ⊢ V1 ▼*[d, e] ≡ V2 → + L⊢ T1 ▼*[d, e] ≡ T2 → R d e L V1 V2 → R d e L T1 T2 → R d e L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) ) → - ∀d,e,L,T1,T2. L ⊢ T1 [d, e] ≡ T2 → R d e L T1 T2. + ∀d,e,L,T1,T2. L ⊢ T1 ▼*[d, e] ≡ T2 → R d e L T1 T2. #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #e #L #T1 #T2 #H elim (delift_delifta … H) -L -T1 -T2 -d -e // /2 width=1 by delifta_delift/ /3 width=1 by delifta_delift/ /3 width=7 by delifta_delift/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma index 30fa27193..a4c94fedc 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_delift.ma @@ -21,7 +21,7 @@ include "basic_2/unfold/delift.ma". (* Main properties **********************************************************) theorem delift_mono: ∀L,T,T1,T2,d,e. - L ⊢ T [d, e] ≡ T1 → L ⊢ T [d, e] ≡ T2 → T1 = T2. + L ⊢ T ▼*[d, e] ≡ T1 → L ⊢ T ▼*[d, e] ≡ T2 → T1 = T2. #L #T #T1 #T2 #d #e * #U1 #H1TU1 #H2TU1 * #U2 #H1TU2 #H2TU2 elim (tpss_conf_eq … H1TU1 … H1TU2) -T #U #HU1 #HU2 lapply (tpss_inv_lift1_eq … HU1 … H2TU1) -HU1 #H destruct diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma index 490c6ac5b..d8c746697 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma @@ -20,8 +20,8 @@ include "basic_2/unfold/delift.ma". (* Advanced properties ******************************************************) lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e → - ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, d + e - i - 1] ≡ V2 → - ⇧[0, d] V2 ≡ U2 → L ⊢ #i [d, e] ≡ U2. + ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 → + ⇧[0, d] V2 ≡ U2 → L ⊢ #i ▼*[d, e] ≡ U2. #L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2 elim (lift_total V 0 (i+1)) #U #HVU lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus (lift_inv_lref2_lt … HU2) // @@ -41,10 +41,10 @@ elim (tpss_inv_lref1 … HU) -HU ] qed-. -lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 → +lemma delift_inv_lref1_be: ∀L,U2,d,e,i. L ⊢ #i ▼*[d, e] ≡ U2 → d ≤ i → i < d + e → ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 & - K ⊢ V1 [0, d + e - i - 1] ≡ V2 & + K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 & ⇧[0, d] V2 ≡ U2. #L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide elim (tpss_inv_lref1 … HU) -HU @@ -54,7 +54,7 @@ elim (tpss_inv_lref1 … HU) -HU ] qed-. -lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → +lemma delift_inv_lref1_ge: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 → d + e ≤ i → U2 = #(i - e). #L #U2 #i #d #e * #U #HU #HU2 #Hdei elim (tpss_inv_lref1 … HU) -HU @@ -65,11 +65,11 @@ elim (tpss_inv_lref1 … HU) -HU ] qed-. -lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i [d, e] ≡ U2 → +lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 → ∨∨ (i < d ∧ U2 = #i) | (∃∃K,V1,V2. d ≤ i & i < d + e & ⇩[0, i] L ≡ K. ⓓV1 & - K ⊢ V1 [0, d + e - i - 1] ≡ V2 & + K ⊢ V1 ▼*[0, d + e - i - 1] ≡ V2 & ⇧[0, d] V2 ≡ U2 ) | (d + e ≤ i ∧ U2 = #(i - e)). @@ -85,10 +85,10 @@ qed-. (* Properties on basic term relocation **************************************) -lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 → +lemma delift_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 → ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d - et, e] T2 ≡ U2 → - L ⊢ U1 [dt, et] ≡ U2. + L ⊢ U1 ▼*[dt, et] ≡ U2. #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdetd #HLK #HTU1 #U2 #HTU2 elim (lift_total T d e) #U #HTU lapply (tpss_lift_le … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1 @@ -96,20 +96,20 @@ elim (lift_trans_ge … HT2 … HTU ?) -T // -Hdetd #T #HT2 #HTU >(lift_mono … HTU2 … HT2) -T2 /2 width=3/ qed. -lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 → +lemma delift_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 → ∀L,U1,d,e. dt ≤ d → d ≤ dt + et → ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → - L ⊢ U1 [dt, et + e] ≡ T2. + L ⊢ U1 ▼*[dt, et + e] ≡ T2. #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 elim (lift_total T d e) #U #HTU lapply (tpss_lift_be … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1 lapply (lift_trans_be … HT2 … HTU ? ?) -T // -Hdtd -Hddet /2 width=3/ qed. -lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≡ T2 → +lemma delift_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▼*[dt, et] ≡ T2 → ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 → - L ⊢ U1 [dt + e, et] ≡ U2. + L ⊢ U1 ▼*[dt + e, et] ≡ U2. #K #T1 #T2 #dt #et * #T #HT1 #HT2 #L #U1 #d #e #Hddt #HLK #HTU1 #U2 #HTU2 elim (lift_total T d e) #U #HTU lapply (tpss_lift_ge … HT1 … HLK HTU1 … HTU) -T1 -HLK // #HU1 @@ -117,9 +117,9 @@ elim (lift_trans_le … HT2 … HTU ?) -T // -Hddt #T #HT2 #HTU >(lift_mono … HTU2 … HT2) -T2 /2 width=3/ qed. -lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 [i, d + e - i] ≡ T → +lemma delift_lift_div_be: ∀L,T1,T,d,e,i. L ⊢ T1 ▼*[i, d + e - i] ≡ T → ∀T2. ⇧[d, i - d] T2 ≡ T → d ≤ i → i ≤ d + e → - L ⊢ T1 [d, e] ≡ T2. + L ⊢ T1 ▼*[d, e] ≡ T2. #L #T1 #T #d #e #i * #T0 #HT10 #HT0 #T2 #HT2 #Hdi #Hide lapply (tpss_weak … HT10 d e ? ?) -HT10 // [ >commutative_plus /2 width=1/ ] #HT10 lapply (lift_trans_be … HT2 … HT0 ? ?) -T // diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma index 02efff1fa..ee3aec8be 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_ltpss.ma @@ -19,15 +19,15 @@ include "basic_2/unfold/delift.ma". (* Properties on partial unfold on local environments ***********************) -lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≡ T2 → - ∀K. L ▶* [d, e] K → K ⊢ T1 [d, e] ≡ T2. +lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → + ∀K. L ▶* [d, e] K → K ⊢ T1 ▼*[d, e] ≡ T2. #L #T1 #T2 #d #e * #T #HT1 #HT2 #K #HLK elim (ltpss_tpss_conf … HT1 … HLK) -L #T0 #HT10 #HT0 lapply (tpss_inv_lift1_eq … HT0 … HT2) -HT0 #H destruct /2 width=3/ qed. lemma ltpss_delift_trans_eq: ∀L,K,d,e. L ▶* [d, e] K → - ∀T1,T2. K ⊢ T1 [d, e] ≡ T2 → L ⊢ T1 [d, e] ≡ T2. + ∀T1,T2. K ⊢ T1 ▼*[d, e] ≡ T2 → L ⊢ T1 ▼*[d, e] ≡ T2. #L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2 lapply (ltpss_tpss_trans_eq … HT1 … HLK) -K /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma index c706163a9..aabd723ac 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_tpss.ma @@ -20,73 +20,73 @@ include "basic_2/unfold/delift.ma". (* Properties on partial unfold on terms ************************************) lemma delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd → - ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2. + ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 ▼*[dd, ee] ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 elim (tpss_inv_lift1_le … HXU1 … HLK … HTX1 ?) -X1 -HLK // -H1 /3 width=5/ qed. lemma delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d + e ≤ dd → - ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 [dd, ee] ≡ T2. + ∃∃T2. K ⊢ T1 ▶* [d, e] T2 & L ⊢ U2 ▼*[dd, ee] ≡ T2. /3 width=3/ qed. lemma delift_tpss_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee → ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 & - L ⊢ U2 [dd, ee] ≡ T2. + L ⊢ U2 ▼*[dd, ee] ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 #H3 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 elim (tpss_inv_lift1_le_up … HXU1 … HLK … HTX1 ? ? ?) -X1 -HLK // -H1 -H2 -H3 /3 width=5/ qed. lemma delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee → ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 & - L ⊢ U2 [dd, ee] ≡ T2. + L ⊢ U2 ▼*[dd, ee] ≡ T2. /3 width=6/ qed. lemma delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e → ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 & - L ⊢ U2 [dd, ee] ≡ T2. + L ⊢ U2 ▼*[dd, ee] ≡ T2. #L #U1 #U2 #d #e #HU12 #T1 #dd #ee * #X1 #HUX1 #HTX1 #K #HLK #H1 #H2 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 elim (tpss_inv_lift1_be … HXU1 … HLK … HTX1 ? ?) -X1 -HLK // -H1 -H2 /3 width=5/ qed. lemma delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T1,dd,ee. L ⊢ U1 [dd, ee] ≡ T1 → + ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → ∀K. ⇩[dd, ee] L ≡ K → d ≤ dd → dd + ee ≤ d + e → ∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 & - L ⊢ U2 [dd, ee] ≡ T2. + L ⊢ U2 ▼*[dd, ee] ≡ T2. /3 width=3/ qed. lemma delift_tpss_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T. + ∀T. L ⊢ U1 ▼*[d, e] ≡ T → L ⊢ U2 ▼*[d, e] ≡ T. #L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1 elim (tpss_conf_eq … HU12 … HUX1) -U1 #U1 #HU21 #HXU1 lapply (tpss_inv_lift1_eq … HXU1 … HTX1) -HXU1 #H destruct /2 width=3/ qed. lemma delift_tps_conf_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T. L ⊢ U1 [d, e] ≡ T → L ⊢ U2 [d, e] ≡ T. + ∀T. L ⊢ U1 ▼*[d, e] ≡ T → L ⊢ U2 ▼*[d, e] ≡ T. /3 width=3/ qed. lemma tpss_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → - ∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T. + ∀T. L ⊢ U2 ▼*[d, e] ≡ T → L ⊢ U1 ▼*[d, e] ≡ T. #L #U1 #U2 #d #e #HU12 #T * #X1 #HUX1 #HTX1 lapply (tpss_trans_eq … HU12 … HUX1) -U2 /2 width=3/ qed. lemma tps_delift_trans_eq: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → - ∀T. L ⊢ U2 [d, e] ≡ T → L ⊢ U1 [d, e] ≡ T. + ∀T. L ⊢ U2 ▼*[d, e] ≡ T → L ⊢ U1 ▼*[d, e] ≡ T. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma index cb8b981c6..ac4d17815 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma @@ -49,9 +49,9 @@ fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e. #Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH #L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e [ // -| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL10 #H1 #H2 destruct +| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1; - elim (ltpss_ldrop_trans_be … HL10 … HLK1 ? ?) -HL10 -HLK1 // /2 width=2/ #X #H #HLK0 + elim (ltpss_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0 elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct lapply (tpss_fwd_tw … HV01) #H2 lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma index aaead6136..c86d9b160 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin.ma @@ -24,13 +24,13 @@ interpretation "basic thinning (local environment)" (* Basic properties *********************************************************) -lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → L1 [d, e] ≡ L2. +lemma ldrop_thin: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → L1 ▼*[d, e] ≡ L2. /2 width=3/ qed. (* Basic inversion lemmas ***************************************************) -lemma thin_inv_thin1: ∀I,K1,V1,L2,e. K1. ⓑ{I} V1 [0, e] ≡ L2 → 0 < e → - K1 [0, e - 1] ≡ L2. +lemma thin_inv_thin1: ∀I,K1,V1,L2,e. K1. ⓑ{I} V1 ▼*[0, e] ≡ L2 → 0 < e → + K1 ▼*[0, e - 1] ≡ L2. #I #K1 #V1 #L2 #e * #X #HK1 #HL2 #e elim (ltpss_inv_tpss21 … HK1 ?) -HK1 // #K #V #HK1 #_ #H destruct lapply (ldrop_inv_ldrop1 … HL2 ?) -HL2 // /2 width=3/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma index 606c77022..7166fa221 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/thin_delift.ma @@ -20,9 +20,9 @@ include "basic_2/unfold/thin.ma". (* Inversion lemmas on inverse basic term relocation ************************) -lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. K1. ⓑ{I} V1 [d, e] ≡ L2 → 0 < d → - ∃∃K2,V2. K1 [d - 1, e] ≡ K2 & - K1 ⊢ V1 [d - 1, e] ≡ V2 & +lemma thin_inv_delift1: ∀I,K1,V1,L2,d,e. K1. ⓑ{I} V1 ▼*[d, e] ≡ L2 → 0 < d → + ∃∃K2,V2. K1 ▼*[d - 1, e] ≡ K2 & + K1 ⊢ V1 ▼*[d - 1, e] ≡ V2 & L2 = K2. ⓑ{I} V2. #I #K1 #V1 #L2 #d #e * #X #HK1 #HL2 #e elim (ltpss_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct @@ -32,8 +32,8 @@ qed-. (* Properties on inverse basic term relocation ******************************) -lemma thin_delift1: ∀L1,L2,d,e. L1 [d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 [d, e] ≡ V2 → - ∀I. L1.ⓑ{I}V1 [d + 1, e] ≡ L2.ⓑ{I}V2. +lemma thin_delift1: ∀L1,L2,d,e. L1 ▼*[d, e] ≡ L2 → ∀V1,V2. L1 ⊢ V1 ▼*[d, e] ≡ V2 → + ∀I. L1.ⓑ{I}V1 ▼*[d + 1, e] ≡ L2.ⓑ{I}V2. #L1 #L2 #d #e * #L #HL1 #HL2 #V1 #V2 * #V #HV1 #HV2 #I elim (ltpss_tpss_conf … HV1 … HL1) -HV1 #V0 #HV10 #HV0 elim (tpss_inv_lift1_be … HV0 … HL2 … HV2 ? ?) -HV0 // "; "〉"; "»"; "❭"; "❯"; "❱"; ] ; + [">"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ; ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ; @@ -1565,10 +1564,10 @@ let predefined_classes = [ ["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; "ⓢ"; ] ; ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; ] ; ["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; "ⓣ"; ] ; - ["T"; "𝕋"; "𝐓"; "Ⓣ"; ] ; + ["T"; "𝕋"; "𝐓"; "Ⓣ"; "⊥"; ] ; ["u"; "𝕦"; "𝐮"; "ⓤ"; ] ; ["U"; "𝕌"; "𝐔"; "Ⓤ"; ] ; - ["v"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; "ⓥ"; ] ; + ["v"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; "ⓥ"; "▼"; ] ; ["V"; "𝕍"; "𝐕"; "Ⓥ"; ] ; ["w"; "ω"; "𝕨"; "𝐰"; "𝛚"; "ⓦ"; ] ; ["W"; "Ω"; "𝕎"; "𝐖"; "𝛀"; "Ⓦ"; ] ; -- 2.39.2