From: Ferruccio Guidi Date: Fri, 13 Jul 2012 16:28:23 +0000 (+0000) Subject: - dynamic type assignment dismissed for now X-Git-Tag: make_still_working~1610 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b074ebf6441993694c6e39e4eaeeb58a3186f479;p=helm.git - dynamic type assignment dismissed for now - stratified static type assignment and unwind defined --- 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 78f319a06..4c164f018 100644 --- a/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma +++ b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma @@ -39,7 +39,7 @@ theorem fsubst_delift: ∀K,V,T,L,d. [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/ elim (lt_or_eq_or_gt i d) #Hid [ -HLK >(tri_lt ?????? Hid) /3 width=3/ - | destruct >tri_eq /4 width=4 by tpss_strap, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *) + | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_1_intro/ (**) (* too slow without trace *) | -HLK >(tri_gt ?????? Hid) /3 width=3/ ] | * /3 width=1/ /4 width=1/ 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 c5fe6def0..70d162599 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -184,13 +184,6 @@ pr3/pr1 pr3_pr1 pr3/props pr3_eta sn3/props sns3_lifts sty1/cnt sty1_cnt -sty1/props sty1_trans -sty1/props sty1_bind -sty1/props sty1_appl -sty1/props sty1_lift -sty1/props sty1_correct -sty1/props sty1_abbr -sty1/props sty1_cast2 subst/fwd subst_sort subst/fwd subst_lref_lt subst/fwd subst_lref_eq diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma index 11ce81ff8..c3cabda9e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma @@ -47,6 +47,12 @@ lemma cprs_inv_abst1: ∀I,W,L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡* U2 → elim (cpr_inv_abst1 … HU2 I W) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ qed-. +lemma cprs_inv_abst: ∀L,V1,V2,T1,T2. L ⊢ ⓛV1. T1 ➡* ⓛV2. T2 → ∀I,W. + L ⊢ V1 ➡* V2 ∧ L. ⓑ{I} W ⊢ T1 ➡* T2. +#L #V1 #V2 #T1 #T2 #H #I #W +elim (cprs_inv_abst1 I W … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/ +qed-. + (* Relocation properties ****************************************************) (* Basic_1: was: pr3_lift *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma deleted file mode 100644 index cedff815a..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn.ma +++ /dev/null @@ -1,110 +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/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_forward lemmas *****************************************************) - -lemma lsubn_fwd_lsubs1: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L1 ≼[0, |L1|] L2. -#h #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ -qed-. - -lemma lsubn_fwd_lsubs2: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → L1 ≼[0, |L2|] L2. -#h #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ -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_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_cpcs.ma deleted file mode 100644 index 5f610bc96..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_cpcs.ma +++ /dev/null @@ -1,34 +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/equivalence/cpcs_cpcs.ma". -include "basic_2/dynamic/lsubn.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE TYPE ASSIGNMENT ******************) - -(* Properties on context-sensitive parallel equivalence for terms ***********) - -(* Basic_1: was: csubt_pr2 *) -lemma cpr_lsubn_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → - ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2. -/3 width=4 by lsubn_fwd_lsubs2, cpr_lsubs_trans/ qed. - -lemma cprs_lsubn_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → - ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -/3 width=4 by lsubn_fwd_lsubs2, cprs_lsubs_trans/ qed. - -(* Basic_1: was: csubt_pc3 *) -lemma cpcs_lsubn_trans: ∀h,L1,L2. h ⊢ L1 :⊑ L2 → - ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2. -/3 width=4 by lsubn_fwd_lsubs2, cpcs_lsubs_trans/ qed. 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 deleted file mode 100644 index a16fff618..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_ldrop.ma +++ /dev/null @@ -1,64 +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/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 deleted file mode 100644 index 5832b00b6..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/lsubn_nta.ma +++ /dev/null @@ -1,47 +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/dynamic/nta_nta.ma". -include "basic_2/dynamic/lsubn_ldrop.ma". -include "basic_2/dynamic/lsubn_cpcs.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 *) -lemma 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/ -| /4 width=6/ -] -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 deleted file mode 100644 index fa4a8ed8f..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma +++ /dev/null @@ -1,53 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/sh.ma". -include "basic_2/equivalence/cpcs.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -inductive nta (h:sh): lenv → relation term ≝ -| nta_sort: ∀L,k. nta h L (⋆k) (⋆(next h k)) -| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W → - ⇧[0, i + 1] W ≡ U → nta h L (#i) U -| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V → - ⇧[0, i + 1] W ≡ U → nta h L (#i) U -| nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U → - nta h L (ⓑ{I}V.T) (ⓑ{I}V.U) -| nta_appl: ∀L,V,W,T,U. nta h L V W → nta h L (ⓛW.T) (ⓛW.U) → - 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_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 → - nta h L T U2 -. - -interpretation "native type assignment (term)" - 'NativeType h L T U = (nta h L T U). - -(* Basic properties *********************************************************) - -(* 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. -/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. -/3 width=2/ qed. - -(* Basic_1: removed theorems 4: - ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0 -*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma deleted file mode 100644 index 962856983..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma +++ /dev/null @@ -1,49 +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/csn_aaa.ma". -include "basic_2/equivalence/lcpcs_aaa.ma". -include "basic_2/dynamic/nta.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -(* Forward lemmas on atomic arity assignment for terms **********************) - -lemma nta_fwd_aaa: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃∃A. L ⊢ T ⁝ A & L ⊢ U ⁝ A. -#h #L #T #U #H elim H -L -T -U -[ /2 width=3/ -| #L #K #V #W #U #i #HLK #_ #HWU * #B #HV #HW - lapply (ldrop_fwd_ldrop2 … HLK) /3 width=9/ -| #L #K #W #V #U #i #HLK #_ #HWU * #B #HW #_ -V - lapply (ldrop_fwd_ldrop2 … HLK) /3 width=9/ -| * #L #V #W #T #U #_ #_ * #B #HV #HW * #A #HT #HU - [ /3 width=3/ | /3 width=5/ ] -| #L #V #W #T #U #_ #_ * #B #HV #HW * #X #H1 #H2 - elim (aaa_inv_abst … H1) -H1 #B1 #A1 #HW1 #HT #H destruct - elim (aaa_inv_abst … H2) -H2 #B2 #A #_ #HU #H destruct - lapply (aaa_mono … HW1 … HW) -HW1 #H destruct /4 width=5/ -| #L #V #W #T #U #_ #_ * #X #HT #HUX * #A #H #_ -W - elim (aaa_inv_appl … H) -H #B #HV #HUA - lapply (aaa_mono … HUA … HUX) -HUX #H destruct /3 width=5/ -| #L #T #U #_ * #A #HT #HU /3 width=3/ -| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #X #HT #HU1 * #A #HU2 #_ - lapply (aaa_cpcs_mono … HU12 … HU1 … HU2) -U1 #H destruct /2 width=3/ -] -qed-. - -(* Note: this is the stong normalization property *) -(* Basic_1: was only: ty3_sn3 *) -theorem nta_fwd_csn: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → L ⊢ ⬇* T ∧ L ⊢ ⬇* U. -#h #L #T #U #H elim (nta_fwd_aaa … H) -H /3 width=2/ -qed-. 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 deleted file mode 100644 index 8cbd59518..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_alt.ma +++ /dev/null @@ -1,190 +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/equivalence/cpcs_cpcs.ma". -include "basic_2/dynamic/nta.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -(* alternative definition of nta *) -inductive ntaa (h:sh): lenv → relation term ≝ -| ntaa_sort: ∀L,k. ntaa h L (⋆k) (⋆(next h k)) -| ntaa_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → ntaa h K V W → - ⇧[0, i + 1] W ≡ U → ntaa h L (#i) U -| ntaa_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → ntaa h K W V → - ⇧[0, i + 1] W ≡ U → ntaa h L (#i) U -| ntaa_bind: ∀I,L,V,W,T,U. ntaa h L V W → ntaa h (L. ⓑ{I} V) T U → - ntaa h L (ⓑ{I}V.T) (ⓑ{I}V.U) -| ntaa_appl: ∀L,V,W,T,U. ntaa h L V W → ntaa h L (ⓛW.T) (ⓛW.U) → - 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_conv: ∀L,T,U1,U2,V2. ntaa h L T U1 → L ⊢ U1 ⬌* U2 → ntaa h L U2 V2 → - ntaa h L T U2 -. - -interpretation "native type assignment (term) alternative" - 'NativeTypeAlt h L T U = (ntaa h L T U). - -(* Advanced inversion lemmas ************************************************) - -fact ntaa_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ∀J,X,Y. T = ⓑ{J}Y.X → - ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y :: Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :: Z2 & - L ⊢ ⓑ{J}Y.Z2 ⬌* U. -#h #L #T #U #H elim H -L -T -U -[ #L #k #J #X #Y #H destruct -| #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct -| #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct -| #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/ -| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct -| #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct -| #L #T #U #W #_ #_ #_ #_ #J #X #Y #H destruct -| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct - elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1 - lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/ -] -qed. - -lemma ntaa_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X :: U → - ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y :: Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :: Z2 & - L ⊢ ⓑ{J}Y.Z2 ⬌* U. -/2 width=3/ qed-. - -lemma ntaa_nta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T :: U → ⦃h, L⦄ ⊢ T : U. -#h #L #T #U #H elim H -L -T -U -// /2 width=1/ /2 width=2/ /2 width=3/ /2 width=6/ -qed-. - -(* Properties on relocation *************************************************) - -lemma ntaa_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 :: U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → - ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 :: U2. -#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1 -[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2 - >(lift_inv_sort1 … H1) -X1 - >(lift_inv_sort1 … H2) -X2 // -| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2 - elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H - elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct - /3 width=8/ - | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 - lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ - ] -| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // (cprs_inv_sort1 … H) -H // -| -| -| -| -| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #T2 #H - elim (cprs_inv_appl1 … H) -H * - [ #V2 #T0 #HV12 #HT10 #H destruct - elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U - @(nta_conv … (ⓐV2.U1)) (* /2 width=1/*) [ /4 width=2/] (**) (* explicit constructor, /5 width=5/ is too slow *) - | #V2 #W2 #T0 #HV12 #HT10 #HT02 - lapply (IHTU1 … HL12 (ⓛW2.T0) ?) -IHTU1 /2 width=1/ -HT10 #H - elim (nta_inv_bind1 … H) -H #W #U0 #HW2 #HTU0 #HU01 - elim (cpcs_inv_abst1 … HU01) -HU01 #W #U #HU1 #HU0 - lapply (IHUW1 … HL12 (ⓐV2.ⓛW.U) ?) -IHUW1 -HL12 /2 width=1/ -HV12 #H - - - - elim (nta_fwd_pure1 … H) -H #W0 #U2 #HVU2 #H #HW01 - elim (nta_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H - elim (cpcs_inv_abst1 … H) -H #W4 #U4 -*) -(* -axiom nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 → - ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. -#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U -[ #L1 #k #L2 #_ #T2 #H - >(tpr_inv_atom1 … H) -H // -| #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H - >(tpr_inv_atom1 … H) -T2 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/ -| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H - >(tpr_inv_atom1 … H) -T2 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H - elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) #HLK - elim (lift_total V1 0 (i+1)) #W #HW - lapply (nta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12 - @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *) -| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H - elim (tpr_inv_bind1 … H) -H * - [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct - lapply (IHVW1 … HL12 … HV12) #HV2W1 - lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1 - lapply (IHTU1 (L2.ⓑ{I}V2) … HT10) -HT10 /2 width=1/ #HT0U1 - lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H - lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 - lapply (nta_tps_conf … HT0U1 … HT02) -T0 #HT2U1 - elim (nta_fwd_correct … H) -H #U2 #HU12 - @(nta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *) - | #T #HT1 #HTX #H destruct - lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1 - elim (lift_total X 0 1) #Y #HXY - lapply (tpr_lift … HTX … HT1 … HXY) -T #H - lapply (IHTU1 (L2.ⓓV1) … H) -T1 /2 width=1/ -L1 #H - elim (nta_fwd_correct … H) #T1 #HUT1 - elim (nta_thin_conf … H L2 0 (0+1) ? ?) -H /2 width=1/ /3 width=1/ #T #U #HTU #H - normalize in ⊢ (??%??? → ?); #HU1 - lapply (delift_inv_lift1_eq … H L2 … HXY) -Y /2 width=1/ #H destruct - @(nta_conv … U) // /2 width=2/ - ] -| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H - elim (tpr_inv_appl1 … H) -H * - [ #V2 #Y #HV12 #HY #H destruct - elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct - lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H - elim (nta_fwd_correct … H) -H #X #H - elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_ - @(nta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *) - | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct - lapply (IHVW1 … HL12 … HV12) #HVW2 - lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2 - lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1 - elim (nta_fwd_correct … H1) #T #H2 - elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H - elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21 - elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0 - lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2 - @(nta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *) - | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct - ] -| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #X #H - elim (tpr_inv_appl1 … H) -H * - [ #V2 #T2 #HV12 #HT12 #H destruct - elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U - @(nta_conv … (ⓐV2.U1)) /2 width=1/ /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *) - | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct - lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 /2 width=1/ -T0 #H - elim (nta_inv_bind1 … H) -H #W #U2 #HW2 #HTU2 #HU21 - lapply (IHUW1 … HL12 (ⓐV2.U1) ?) -IHUW1 -HL12 /2 width=1/ #H - elim (nta_inv_pure1 … H) -H #V0 #U0 #U #HV20 #HU10 #HU0W1 #HU0 - @(nta_conv … (ⓓV2.U2)) - [2: @nta_bind // - @(lsubn_nta_trans … HTU2) @lsubn_abbr // -(* - lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB - lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0 - lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/ -*) -*) -(* -axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y → - ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W. - -*) -(* SEGMENT 2 -| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H - elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct - lapply (cpr_tpss … HU12) /4 width=4/ -| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12 - @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *) -] -qed. -*) - -(* SEGMENT 3 -fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. - - - | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct - elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0 - lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2 - lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0 - lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2 - @(nta_abbr … HW2) -HW2 - @(nta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *) - ] -| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct - elim (tpr_inv_cast1 … H) -H - [ * #V2 #T2 #HV12 #HT12 #H destruct - lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2 - lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/ - | -HV1 #HT1X - lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/ - ] -] -qed. - -/2 width=9/ qed. - -axiom nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A. -/2 width=5/ qed. - -axiom nta_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/dynamic/nta_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpss.ma deleted file mode 100644 index 828fd82e0..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpss.ma +++ /dev/null @@ -1,121 +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/equivalence/cpcs_ltpss.ma". -include "basic_2/dynamic/nta_nta.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -(* Properties about parallel unfold *****************************************) - -lemma nta_ltpss_tpss_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → ⦃h, L2⦄ ⊢ T2 : U. -#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U -[ #L1 #k #L2 #d #e #_ #T2 #H - >(tpss_inv_sort1 … H) -H // -| #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #d #e #HL12 #T2 #H - elim (tpss_inv_lref1 … H) -H - [ #H destruct - elim (lt_or_ge i d) #Hdi - [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 - elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct - /3 width=7/ - | elim (lt_or_ge i (d + e)) #Hide [ | -Hdi ] - [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 - elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct - /3 width=7/ - | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=7/ - ] - ] - | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2 - elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 - elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct - lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 - lapply (tpss_trans_eq … HV12 HVW2) -V2 /3 width=9/ - ] -| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL12 #T2 #H - elim (tpss_inv_lref1 … H) -H [ | -HWV1 -HWU1 -IHWV1 ] - [ #H destruct - elim (lift_total V1 0 (i+1)) #W #HW - elim (lt_or_ge i d) #Hdi [ -HWV1 ] - [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 - elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #W2 #HK12 #HW12 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) #HLK - lapply (nta_lift h … HLK … HWU1 … HW) /2 width=4/ -HW - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12 - lapply (cpr_tpss … HU12) -HU12 #HU12 - @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *) - | elim (lt_or_ge i (d + e)) #Hide [ -HWV1 | -IHWV1 -HW -Hdi ] - [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 - elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #W2 #HK12 #HW12 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) #HLK - lapply (nta_lift h … HLK … HWU1 … HW) /2 width=4/ -HW - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12 - lapply (cpr_tpss … HU12) -HU12 #HU12 - @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *) - | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /2 width=6/ - ] - ] - | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #_ #_ - elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 - elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #_ #_ #H destruct - lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 -HLK2 #H destruct - ] -| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H - elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - lapply (cpr_tpss … HV12) #HV - lapply (IHTU1 (L2.ⓑ{I}V1) (d+1) e ? T1 ?) // /2 width=1/ #H - elim (nta_fwd_correct … H) -H #U2 #HU12 - @(nta_conv … (ⓑ{I}V2.U1)) /3 width=2/ /3 width=4/ /4 width=4/ (**) (* explicit constructor, /5 width=6/ is too slow *) -| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H - elim (tpss_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct - elim (tpss_inv_bind1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct - lapply (cpr_tpss … HV12) #HV - lapply (IHTU1 L2 d e ? (ⓛW1.T1) ?) // #H - elim (nta_fwd_correct … H) -H #X #H - elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_ - @(nta_conv … (ⓐV2.ⓛW1.U1)) /3 width=2/ /3 width=4/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *) -| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H - elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - lapply (cpr_tpss … HV12) #HV - elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=4/ ] #U #HU - @(nta_conv … (ⓐV2.U1)) // /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *) -| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H - elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct - lapply (cpr_tpss … HU12) /4 width=4/ -| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12 - @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *) -] -qed. - -lemma nta_ltpss_tps_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → - ∀L2,d,e. L1 ▶* [d, e] L2 → - ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → ⦃h, L2⦄ ⊢ T2 : U. -/3 width=7/ qed. - -lemma nta_ltpss_conf: ∀h,L1,T,U. ⦃h, L1⦄ ⊢ T : U → - ∀L2,d,e. L1 ▶* [d, e] L2 → ⦃h, L2⦄ ⊢ T : U. -/2 width=7/ qed. - -lemma nta_tpss_conf: ∀h,L,T1,U. ⦃h, L⦄ ⊢ T1 : U → - ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ⦃h, L⦄ ⊢ T2 : U. -/2 width=7/ qed. - -lemma nta_tps_conf: ∀h,L,T1,U. ⦃h, L⦄ ⊢ T1 : U → - ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ⦃h, L⦄ ⊢ T2 : U. -/2 width=7/ qed. 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 deleted file mode 100644 index 05eb6c55d..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma +++ /dev/null @@ -1,59 +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/dynamic/nta_lift.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -(* Main properties **********************************************************) - -(* Basic_1: was: ty3_unique *) -theorem nta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T : U1 → ∀U2. ⦃h, L⦄ ⊢ T : U2 → - L ⊢ U1 ⬌* U2. -#h #L #T #U1 #H elim H -L -T -U1 -[ #L #k #X #H - lapply (nta_inv_sort1 … H) -H // -| #L #K #V #W11 #W12 #i #HLK #_ #HW112 #IHVW11 #X #H - elim (nta_inv_lref1 … H) -H * #K0 #V0 #W21 #W22 #HLK0 #HVW21 #HW212 #HX - lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct - lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK - @(cpcs_trans … HX) -X /3 width=9 by cpcs_lift/ (**) (* to slow without trace *) -| #L #K #W #V1 #V #i #HLK #_ #HWV #_ #X #H - elim (nta_inv_lref1 … H) -H * #K0 #W0 #V2 #V0 #HLK0 #_ #HWV0 #HX - lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H destruct - lapply (lift_mono … HWV0 … HWV) -HWV0 -HWV #H destruct // -| #I #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H - elim (nta_inv_bind1 … H) -H #W2 #U2 #_ #HTU2 #H - @(cpcs_trans … H) -X /3 width=1/ -| #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H - elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H - @(cpcs_trans … H) -X /3 width=1/ -| #L #V #W1 #T #U1 #_ #_ #IHTU1 #_ #X #H - elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H - @(cpcs_trans … H) -X /3 width=1/ -| #L #T #U1 #_ #_ #X #H - elim (nta_inv_cast1 … H) -H // -| #L #T #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #_ #U2 #HTU2 - @(cpcs_canc_sn … HU112) -U12 /2 width=1/ -] -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 #T #W #U #HTW #HTU -lapply (nta_mono … HTW … HTU) #HWU -elim (nta_fwd_correct … HTU) -HTU /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma deleted file mode 100644 index 6268b98b1..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_sta.ma +++ /dev/null @@ -1,42 +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/static/sta.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/dynamic/nta.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -(* Properties on static type assignment *************************************) - -lemma nta_fwd_sta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → - ∃∃U0. ⦃h, L⦄ ⊢ T • U0 & L ⊢ U0 ⬌* U. -#h #L #T #U #H elim H -L -T -U -[ /2 width=3/ -| #L #K #V #W1 #V1 #i #HLK #_ #HWV1 * #W0 #HVW0 #HW01 - elim (lift_total W0 0 (i+1)) #V0 #HWV0 - lapply (ldrop_fwd_ldrop2 … HLK) #HLK0 - lapply (cpcs_lift … HLK0 … HWV0 … HWV1 HW01) -HLK0 -HWV1 -HW01 /3 width=6/ -| #L #K #W #V1 #W1 #i #HLK #HWV1 #HW1 * /3 width=6/ -| #I #L #V #W #T #U #_ #_ * #W0 #_ #_ * /3 width=3/ -| #L #V #W #T #U #_ #_ * #W0 #_ #HW0 * #X #H #HX - elim (sta_inv_bind1 … H) -H #U0 #HTU0 #H destruct - @(ex2_1_intro … (ⓐV.ⓛW.U0)) /2 width=1/ /3 width=1/ -| #L #V #W #T #U #_ #_ * #U0 #HTU0 #HU0 #_ -W - @(ex2_1_intro … (ⓐV.U0)) /2 width=1/ -| #L #T #U #HTU * #U0 #HTU0 #HU0 /3 width=3/ -| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #U0 #HTU0 #HU01 #_ - lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=3/ -] -qed-. 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 deleted file mode 100644 index f927f841a..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma +++ /dev/null @@ -1,116 +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/unfold/thin_ldrop.ma". -include "basic_2/equivalence/cpcs_delift.ma". -include "basic_2/dynamic/nta_lift.ma". - -(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) - -(* Properties on basic local environment thinning ***************************) - -(* 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 → - ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : 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 - elim (lt_or_ge i d) #Hdi [ -HVW1 ] - [ lapply (sfr_ldrop_trans_ge … HLK1 … HL1 ?) -HL1 /2 width=2/ #H - lapply (sfr_inv_skip … H ?) -H /2 width=1/ #HK1 - elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2 - elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct - elim (IHVW1 … HK1 HK12) -IHVW1 -HK1 -HK12 #X2 #W2 #HVW2 #H #HW12 - lapply (delift_mono … H … HV12) -H -HV12 #H destruct - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #HLK1 - lapply (delift_lift_ge … HW12 … HLK1 HWU1 … HWU2) -HW12 -HLK1 -HWU1 // - >minus_plus minus_plus #HU1 - lapply (lift_conf_be … HWU2 … HW2U ?) -W2 /2 width=1/ #HU2 - lapply (delift_lift_div_be … HU1 … HU2 ? ?) -U // /2 width=1/ /3 width=8/ - | lapply (transitive_le … (i+1) Hide ?) /2 width=1/ #Hdei - lapply (thin_ldrop_conf_ge … HL12 … HLK1 ?) -HL12 -HLK1 // #HL2K1 - elim (lift_split … HWU1 d (i+1-e) ? ? ?) -HWU1 // /2 width=1/ #W - commutative_plus minus_plus commutative_plus (lift_inv_sort1 … H1) -X1 + >(lift_inv_sort1 … H2) -X2 // +| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2 + elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H + elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct + /3 width=8/ + | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 + lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ + ] +| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // (cprs_inv_sort1 … H) -H // +| +| +| +| +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #T2 #H + elim (cprs_inv_appl1 … H) -H * + [ #V2 #T0 #HV12 #HT10 #H destruct + elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U + @(nta_conv … (ⓐV2.U1)) (* /2 width=1/*) [ /4 width=2/] (**) (* explicit constructor, /5 width=5/ is too slow *) + | #V2 #W2 #T0 #HV12 #HT10 #HT02 + lapply (IHTU1 … HL12 (ⓛW2.T0) ?) -IHTU1 /2 width=1/ -HT10 #H + elim (nta_inv_bind1 … H) -H #W #U0 #HW2 #HTU0 #HU01 + elim (cpcs_inv_abst1 … HU01) -HU01 #W #U #HU1 #HU0 + lapply (IHUW1 … HL12 (ⓐV2.ⓛW.U) ?) -IHUW1 -HL12 /2 width=1/ -HV12 #H + + + + elim (nta_fwd_pure1 … H) -H #W0 #U2 #HVU2 #H #HW01 + elim (nta_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H + elim (cpcs_inv_abst1 … H) -H #W4 #U4 +*) +(* +axiom nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 → + ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. +#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U +[ #L1 #k #L2 #_ #T2 #H + >(tpr_inv_atom1 … H) -H // +| #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H + >(tpr_inv_atom1 … H) -T2 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/ +| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H + >(tpr_inv_atom1 … H) -T2 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #HLK + elim (lift_total V1 0 (i+1)) #W #HW + lapply (nta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12 + @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *) +| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H + elim (tpr_inv_bind1 … H) -H * + [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct + lapply (IHVW1 … HL12 … HV12) #HV2W1 + lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1 + lapply (IHTU1 (L2.ⓑ{I}V2) … HT10) -HT10 /2 width=1/ #HT0U1 + lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H + lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 + lapply (nta_tps_conf … HT0U1 … HT02) -T0 #HT2U1 + elim (nta_fwd_correct … H) -H #U2 #HU12 + @(nta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *) + | #T #HT1 #HTX #H destruct + lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1 + elim (lift_total X 0 1) #Y #HXY + lapply (tpr_lift … HTX … HT1 … HXY) -T #H + lapply (IHTU1 (L2.ⓓV1) … H) -T1 /2 width=1/ -L1 #H + elim (nta_fwd_correct … H) #T1 #HUT1 + elim (nta_thin_conf … H L2 0 (0+1) ? ?) -H /2 width=1/ /3 width=1/ #T #U #HTU #H + normalize in ⊢ (??%??? → ?); #HU1 + lapply (delift_inv_lift1_eq … H L2 … HXY) -Y /2 width=1/ #H destruct + @(nta_conv … U) // /2 width=2/ + ] +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H + elim (tpr_inv_appl1 … H) -H * + [ #V2 #Y #HV12 #HY #H destruct + elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct + lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H + elim (nta_fwd_correct … H) -H #X #H + elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_ + @(nta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *) + | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct + lapply (IHVW1 … HL12 … HV12) #HVW2 + lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2 + lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1 + elim (nta_fwd_correct … H1) #T #H2 + elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H + elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21 + elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0 + lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2 + @(nta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *) + | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct + ] +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #X #H + elim (tpr_inv_appl1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct + elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U + @(nta_conv … (ⓐV2.U1)) /2 width=1/ /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *) + | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct + lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 /2 width=1/ -T0 #H + elim (nta_inv_bind1 … H) -H #W #U2 #HW2 #HTU2 #HU21 + lapply (IHUW1 … HL12 (ⓐV2.U1) ?) -IHUW1 -HL12 /2 width=1/ #H + elim (nta_inv_pure1 … H) -H #V0 #U0 #U #HV20 #HU10 #HU0W1 #HU0 + @(nta_conv … (ⓓV2.U2)) + [2: @nta_bind // + @(lsubn_nta_trans … HTU2) @lsubn_abbr // +(* + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB + lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0 + lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/ +*) +*) +(* +axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y → + ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W. + +*) +(* SEGMENT 2 +| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct + lapply (cpr_tpss … HU12) /4 width=4/ +| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12 + @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *) +] +qed. +*) + +(* SEGMENT 3 +fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. + + + | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct + elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0 + lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2 + lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0 + lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2 + @(nta_abbr … HW2) -HW2 + @(nta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *) + ] +| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct + elim (tpr_inv_cast1 … H) -H + [ * #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2 + lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/ + | -HV1 #HT1X + lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/ + ] +] +qed. + +/2 width=9/ qed. + +axiom nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A. +/2 width=5/ qed. + +axiom nta_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/etc/nta/nta_ltpss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpss.etc new file mode 100644 index 000000000..828fd82e0 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_ltpss.etc @@ -0,0 +1,121 @@ +(**************************************************************************) +(* ___ *) +(* ||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/equivalence/cpcs_ltpss.ma". +include "basic_2/dynamic/nta_nta.ma". + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +(* Properties about parallel unfold *****************************************) + +lemma nta_ltpss_tpss_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → ⦃h, L2⦄ ⊢ T2 : U. +#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U +[ #L1 #k #L2 #d #e #_ #T2 #H + >(tpss_inv_sort1 … H) -H // +| #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #d #e #HL12 #T2 #H + elim (tpss_inv_lref1 … H) -H + [ #H destruct + elim (lt_or_ge i d) #Hdi + [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct + /3 width=7/ + | elim (lt_or_ge i (d + e)) #Hide [ | -Hdi ] + [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct + /3 width=7/ + | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=7/ + ] + ] + | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2 + elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct + lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 + lapply (tpss_trans_eq … HV12 HVW2) -V2 /3 width=9/ + ] +| #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL12 #T2 #H + elim (tpss_inv_lref1 … H) -H [ | -HWV1 -HWU1 -IHWV1 ] + [ #H destruct + elim (lift_total V1 0 (i+1)) #W #HW + elim (lt_or_ge i d) #Hdi [ -HWV1 ] + [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #HLK + lapply (nta_lift h … HLK … HWU1 … HW) /2 width=4/ -HW + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12 + lapply (cpr_tpss … HU12) -HU12 #HU12 + @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *) + | elim (lt_or_ge i (d + e)) #Hide [ -HWV1 | -IHWV1 -HW -Hdi ] + [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #HLK + lapply (nta_lift h … HLK … HWU1 … HW) /2 width=4/ -HW + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12 + lapply (cpr_tpss … HU12) -HU12 #HU12 + @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *) + | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /2 width=6/ + ] + ] + | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #_ #_ + elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #_ #_ #H destruct + lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 -HLK2 #H destruct + ] +| #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HV + lapply (IHTU1 (L2.ⓑ{I}V1) (d+1) e ? T1 ?) // /2 width=1/ #H + elim (nta_fwd_correct … H) -H #U2 #HU12 + @(nta_conv … (ⓑ{I}V2.U1)) /3 width=2/ /3 width=4/ /4 width=4/ (**) (* explicit constructor, /5 width=6/ is too slow *) +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct + elim (tpss_inv_bind1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HV + lapply (IHTU1 L2 d e ? (ⓛW1.T1) ?) // #H + elim (nta_fwd_correct … H) -H #X #H + elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_ + @(nta_conv … (ⓐV2.ⓛW1.U1)) /3 width=2/ /3 width=4/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *) +| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HV + elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=4/ ] #U #HU + @(nta_conv … (ⓐV2.U1)) // /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *) +| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct + lapply (cpr_tpss … HU12) /4 width=4/ +| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12 + @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *) +] +qed. + +lemma nta_ltpss_tps_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → ⦃h, L2⦄ ⊢ T2 : U. +/3 width=7/ qed. + +lemma nta_ltpss_conf: ∀h,L1,T,U. ⦃h, L1⦄ ⊢ T : U → + ∀L2,d,e. L1 ▶* [d, e] L2 → ⦃h, L2⦄ ⊢ T : U. +/2 width=7/ qed. + +lemma nta_tpss_conf: ∀h,L,T1,U. ⦃h, L⦄ ⊢ T1 : U → + ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ⦃h, L⦄ ⊢ T2 : U. +/2 width=7/ qed. + +lemma nta_tps_conf: ∀h,L,T1,U. ⦃h, L⦄ ⊢ T1 : U → + ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ⦃h, L⦄ ⊢ T2 : U. +/2 width=7/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_nta.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_nta.etc new file mode 100644 index 000000000..05eb6c55d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_nta.etc @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lift.ma". + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: ty3_unique *) +theorem nta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T : U1 → ∀U2. ⦃h, L⦄ ⊢ T : U2 → + L ⊢ U1 ⬌* U2. +#h #L #T #U1 #H elim H -L -T -U1 +[ #L #k #X #H + lapply (nta_inv_sort1 … H) -H // +| #L #K #V #W11 #W12 #i #HLK #_ #HW112 #IHVW11 #X #H + elim (nta_inv_lref1 … H) -H * #K0 #V0 #W21 #W22 #HLK0 #HVW21 #HW212 #HX + lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK + @(cpcs_trans … HX) -X /3 width=9 by cpcs_lift/ (**) (* to slow without trace *) +| #L #K #W #V1 #V #i #HLK #_ #HWV #_ #X #H + elim (nta_inv_lref1 … H) -H * #K0 #W0 #V2 #V0 #HLK0 #_ #HWV0 #HX + lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H destruct + lapply (lift_mono … HWV0 … HWV) -HWV0 -HWV #H destruct // +| #I #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H + elim (nta_inv_bind1 … H) -H #W2 #U2 #_ #HTU2 #H + @(cpcs_trans … H) -X /3 width=1/ +| #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H + elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H + @(cpcs_trans … H) -X /3 width=1/ +| #L #V #W1 #T #U1 #_ #_ #IHTU1 #_ #X #H + elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H + @(cpcs_trans … H) -X /3 width=1/ +| #L #T #U1 #_ #_ #X #H + elim (nta_inv_cast1 … H) -H // +| #L #T #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #_ #U2 #HTU2 + @(cpcs_canc_sn … HU112) -U12 /2 width=1/ +] +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 #T #W #U #HTW #HTU +lapply (nta_mono … HTW … HTU) #HWU +elim (nta_fwd_correct … HTU) -HTU /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_sta.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_sta.etc new file mode 100644 index 000000000..6268b98b1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_sta.etc @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/sta.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/dynamic/nta.ma". + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +(* Properties on static type assignment *************************************) + +lemma nta_fwd_sta: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → + ∃∃U0. ⦃h, L⦄ ⊢ T • U0 & L ⊢ U0 ⬌* U. +#h #L #T #U #H elim H -L -T -U +[ /2 width=3/ +| #L #K #V #W1 #V1 #i #HLK #_ #HWV1 * #W0 #HVW0 #HW01 + elim (lift_total W0 0 (i+1)) #V0 #HWV0 + lapply (ldrop_fwd_ldrop2 … HLK) #HLK0 + lapply (cpcs_lift … HLK0 … HWV0 … HWV1 HW01) -HLK0 -HWV1 -HW01 /3 width=6/ +| #L #K #W #V1 #W1 #i #HLK #HWV1 #HW1 * /3 width=6/ +| #I #L #V #W #T #U #_ #_ * #W0 #_ #_ * /3 width=3/ +| #L #V #W #T #U #_ #_ * #W0 #_ #HW0 * #X #H #HX + elim (sta_inv_bind1 … H) -H #U0 #HTU0 #H destruct + @(ex2_1_intro … (ⓐV.ⓛW.U0)) /2 width=1/ /3 width=1/ +| #L #V #W #T #U #_ #_ * #U0 #HTU0 #HU0 #_ -W + @(ex2_1_intro … (ⓐV.U0)) /2 width=1/ +| #L #T #U #HTU * #U0 #HTU0 #HU0 /3 width=3/ +| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #U0 #HTU0 #HU01 #_ + lapply (cpcs_trans … HU01 … HU12) -U1 /2 width=3/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_thin.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_thin.etc new file mode 100644 index 000000000..f927f841a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/nta/nta_thin.etc @@ -0,0 +1,116 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/thin_ldrop.ma". +include "basic_2/equivalence/cpcs_delift.ma". +include "basic_2/dynamic/nta_lift.ma". + +(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************) + +(* Properties on basic local environment thinning ***************************) + +(* 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 → + ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 : 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 + elim (lt_or_ge i d) #Hdi [ -HVW1 ] + [ lapply (sfr_ldrop_trans_ge … HLK1 … HL1 ?) -HL1 /2 width=2/ #H + lapply (sfr_inv_skip … H ?) -H /2 width=1/ #HK1 + elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2 + elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct + elim (IHVW1 … HK1 HK12) -IHVW1 -HK1 -HK12 #X2 #W2 #HVW2 #H #HW12 + lapply (delift_mono … H … HV12) -H -HV12 #H destruct + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #HLK1 + lapply (delift_lift_ge … HW12 … HLK1 HWU1 … HWU2) -HW12 -HLK1 -HWU1 // + >minus_plus minus_plus #HU1 + lapply (lift_conf_be … HWU2 … HW2U ?) -W2 /2 width=1/ #HU2 + lapply (delift_lift_div_be … HU1 … HU2 ? ?) -U // /2 width=1/ /3 width=8/ + | lapply (transitive_le … (i+1) Hide ?) /2 width=1/ #Hdei + lapply (thin_ldrop_conf_ge … HL12 … HLK1 ?) -HL12 -HLK1 // #HL2K1 + elim (lift_split … HWU1 d (i+1-e) ? ? ?) -HWU1 // /2 width=1/ #W + commutative_plus minus_plus commutative_plus 0 & L ⊢ U0 ⬌* U + ). +#h #L #T #U #l #H elim H -L -T -U -l +[ #L #k #j #H destruct +| #L #K #V #W #U #i #l #HLK #HVW #HWU #_ #j #H destruct /3 width=8/ +| #L #K #W #V #U #i #l #HLK #HWV #HWU #_ #j #H destruct /3 width=8/ +| #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #j #H destruct +| #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #j #H destruct +| #L #V #T #U #W #l #_ #_ #_ #_ #j #H destruct +| #L #T #U #W #l1 #l2 #_ #_ #_ #_ #j #H destruct +| #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #j #H destruct + elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 [2: #H ] #HU01 + lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/ +] +qed. + +lemma snta_inv_lref1: ∀h,L,U,i,l. ⦃h, L⦄ ⊢ #i :[l] U → + (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V :[l] W & + ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U + ) ∨ + (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W :[l-1] V & + ⇧[0, i + 1] W ≡ U0 & l > 0 & L ⊢ U0 ⬌* U + ). +/2 width=3/ qed-. + +fact snta_inv_bind1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀J,X,Y. T = ⓑ{J}Y.X → + ∃∃Z1,Z2,l0. ⦃h, L⦄ ⊢ Y :[l0] Z1 & + ⦃h, L.ⓑ{J}Y⦄ ⊢ X :[l] Z2 & + L ⊢ ⓑ{J}Y.Z2 ⬌* U. +#h #L #T #U #l #H elim H -L -T -U -l +[ #L #k #J #X #Y #H destruct +| #L #K #V #W #U #i #l #_ #_ #_ #_ #J #X #Y #H destruct +| #L #K #W #V #U #i #l #_ #_ #_ #_ #J #X #Y #H destruct +| #I #L #V #W #T #U #l1 #l2 #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/ +| #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #J #X #Y #H destruct +| #L #V #T #U #W #l #_ #_ #_ #_ #J #X #Y #H destruct +| #L #T #U #W #l1 #l2 #_ #_ #_ #_ #J #X #Y #H destruct +| #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct + elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #l0 #HZ1 #HZ2 #HU1 + lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/ +] +qed. + +lemma snta_inv_bind1: ∀h,J,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓑ{J}Y.X :[l] U → + ∃∃Z1,Z2,l0. ⦃h, L⦄ ⊢ Y :[l0] Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :[l] Z2 & + L ⊢ ⓑ{J}Y.Z2 ⬌* U. +/2 width=3/ qed-. + +fact snta_inv_cast1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀X,Y. T = ⓝY.X → + ⦃h, L⦄ ⊢ X :[l] Y ∧ L ⊢ Y ⬌* U. +#h #L #T #U #l #H elim H -L -T -U -l +[ #L #k #X #Y #H destruct +| #L #K #V #W #U #i #l #_ #_ #_ #_ #X #Y #H destruct +| #L #K #W #V #U #i #l #_ #_ #_ #_ #X #Y #H destruct +| #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct +| #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct +| #L #V #T #U #W #l #_ #_ #_ #_ #X #Y #H destruct +| #L #T #U #W #l1 #l2 #HTU #_ #_ #_ #X #Y #H destruct /2 width=1/ +| #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct + elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1 + lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/ +] +qed. + +lemma snta_inv_cast1: ∀h,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X :[l] U → + ⦃h, L⦄ ⊢ X :[l] Y ∧ L ⊢ Y ⬌* U. +/2 width=3/ qed-. + +(* Properties on relocation *************************************************) + +lemma snta_lift: ∀h,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 :[l] U1 → + ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → + ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → + ⦃h, L2⦄ ⊢ T2 :[l] U2. +#h #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l +[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2 + >(lift_inv_sort1 … H1) -X1 + >(lift_inv_sort1 … H2) -X2 // +| #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2 + elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H + elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct + /3 width=8/ + | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 + lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ + ] +| #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // (tpr_inv_atom1 … H) -H // +| #L1 #K1 #V1 #W #U #i1 #l #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H #Hl -IH + >(tpr_inv_atom1 … H) -T2 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/ +| #L1 #K1 #W1 #V1 #U1 #i1 #l #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H #Hl -IH +(* + >(tpr_inv_atom1 … H) -T2 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H + elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #HLK + elim (lift_total V1 0 (i+1)) #W #HW + lapply (snta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12 + @(snta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *) +*) +| #I #L1 #V1 #W1 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H #Hl -IH +(* + elim (tpr_inv_bind1 … H) -H * + [ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct + lapply (IHVW1 … HL12 … HV12) #HV2W1 + lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1 + lapply (IHTU1 (L2.ⓑ{I}V2) … HT1) -HT1 /2 width=1/ #HTU1 + lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H + lapply (tps_lsubs_trans … HT2 (L2.ⓑ{I}V2) ?) -HT2 /2 width=1/ #HT2 + lapply (snta_tps_conf … HTU1 … HT2) -T #HT2U1 + elim (snta_fwd_correct … H) -H #U2 #HU12 + @(snta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *) + | #T #HT1 #HTX #H destruct + lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1 + lapply (IHTU1 (L2.ⓓV1) … HT1) -T1 /2 width=1/ -L1 #H + elim (snta_fwd_correct … H) #T1 #HUT1 + elim (snta_ldrop_conf … H L2 0 1 ? ?) -H // /2 width=1/ #T0 #U0 #HTU0 #H #HU10 + lapply (delift_inv_lift1_eq … H L2 … HTX) -H -HTX /2 width=1/ #H destruct + @(snta_conv … HTU0) /2 width=2/ + ] +*) +| #L1 #V1 #W11 #W2 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H #Hl -IH +(* + elim (tpr_inv_appl1 … H) -H * + [ #V2 #Y #HV12 #HY #H destruct + elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct + lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H + elim (snta_fwd_correct … H) -H #X #H + elim (snta_inv_bind1 … H) -H #W #U #HW #HU #_ + @(snta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *) + | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct + lapply (IHVW1 … HL12 … HV12) #HVW2 + lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2 + lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1 + elim (snta_fwd_correct … H1) #T #H2 + elim (snta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H + elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21 + elim (snta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0 + lapply (lsubsn_snta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2 + @(snta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *) + | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct + ] +*) +| #L1 #V1 #T1 #U1 #W1 #l #_ #HUW1 #IHTU1 #_ #L2 #HL12 #X #H #Hl + elim (tpr_inv_appl1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct + lapply (cpr_tpr … HV12 L2) #HV + elim (snta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) (l+1) ?) [2: /3 width=6/ ] #U + @(snta_conv … (ⓐV2.U1)) /2 width=1/ -HV12 /4 width=8 by snta_pure, cprs_flat_dx/ (**) (* explicit constructor, /4 width=8/ is too slow without trace *) + | #V2 #W0 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct + lapply (IHTU1 … HL12 (ⓛW0.T2) ? ?) -IHTU1 // /2 width=1/ -T0 #H1 + lapply (IH … (ⓐV2.U1) … HUW1 HL12 ?) // /3 width=1/ #H2 + lapply (snta_pure … H1 H2) -H2 #H + elim (snta_inv_bind1 … H1) -H1 #V0 #U2 #l1 #HWV0 #HTU2 #HU21 + @(snta_conv … (ⓓV2.U2)) (**) (* explicit constructor *) + [2: +(* + @snta_bind /3 width=2/ /3 width=6/ (**) (* /4 width=6/ is a bit slow *) +*) + |3: @(cpcs_cpr_conf … (ⓐV1.ⓛW0.U2)) /2 width=1/ + |4: /2 width=5/ + | skip + ] +(* + elim (snta_fwd_pure1 … H) -H #T1 #W2 #HVW2 #HUT1 #HTW1 + + elim (cpcs_inv_abst1 … HU21) #W3 #U3 #HU13 #H + elim (cprs_inv_abst … H Abst W0) -H #HW03 #_ + elim (pippo … IH … HUW1 ? V2 W3 U3 HL12 ? ?) -IH -HUW1 -HL12 // /3 width=1/ -HU13 #l2 #HV2W3 + lapply (snta_conv h L2 V2 W3 W0 V0 (l1+1) ? ? ?) /2 width=1/ -HV2W3 -HW03 -HWV0 #HV2W0 +*) +(* SEGMENT 1.5 + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB + lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0 + lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/ + +axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y → + ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W. + +*) +(* SEGMENT 2 +| #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct + lapply (cpr_tpss … HU12) /4 width=4/ +| #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12 + @(snta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *) +] +qed. +*) + +(* SEGMENT 3 +fact snta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 → + ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. + + + | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct + elim (snta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0 + lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2 + lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0 + lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2 + @(snta_abbr … HW2) -HW2 + @(snta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *) + ] +| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct + elim (tpr_inv_cast1 … H) -H + [ * #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2 + lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/ + | -HV1 #HT1X + lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/ + ] +] +qed. + +lemma snta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 → + ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U. + +/2 width=9/ qed. + +axiom snta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A. +/2 width=5/ qed. + +axiom snta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A. +/2 width=5/ qed. +*) +*)*) \ No newline at end of file diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc new file mode 100644 index 000000000..0e5f3930e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_ltpss.etc @@ -0,0 +1,123 @@ +(**************************************************************************) +(* ___ *) +(* ||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/equivalence/cpcs_ltpss.ma". +include "basic_2/dynamic/snta_snta.ma". + +(* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************) + +(* Properties about parallel unfold *****************************************) + +lemma snta_ltpss_tpss_conf: ∀h,L1,T1,U,l. ⦃h, L1⦄ ⊢ T1 :[l] U → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → ⦃h, L2⦄ ⊢ T2 :[l] U. +#h #L1 #T1 #U #l #H elim H -L1 -T1 -U -l +[ #L1 #k #L2 #d #e #_ #T2 #H + >(tpss_inv_sort1 … H) -H // +| #L1 #K1 #V1 #W #U #i #l #HLK1 #_ #HWU #IHV1 #L2 #d #e #HL12 #T2 #H + elim (tpss_inv_lref1 … H) -H + [ #H destruct + elim (lt_or_ge i d) #Hdi + [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #V2 #HK12 #HV12 #H destruct + /3 width=7/ + | elim (lt_or_ge i (d + e)) #Hide [ | -Hdi ] + [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #V2 #HK12 #HV12 #H destruct + /3 width=7/ + | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /3 width=7/ + ] + ] + | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #HVW2 #HWT2 + elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #HK12 #HV12 #H destruct + lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 + lapply (tpss_trans_eq … HV12 HVW2) -V2 /3 width=9/ + ] +| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #d #e #HL12 #T2 #H + elim (tpss_inv_lref1 … H) -H [ | -HWV1 -HWU1 -IHWV1 ] + [ #H destruct + elim (lift_total V1 0 (i+1)) #W #HW + elim (lt_or_ge i d) #Hdi [ -HWV1 ] + [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ -Hdi #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #HLK + lapply (snta_lift h … HLK … HWU1 … HW) [ /2 width=4/ | skip ] -HW #H + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12 + lapply (cpr_tpss … HU12) -HU12 #HU12 + @(snta_conv … U2) // /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *) + | elim (lt_or_ge i (d + e)) #Hide [ -HWV1 | -IHWV1 -HW -Hdi ] + [ elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K2 #W2 #HK12 #HW12 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2) #HLK + lapply (snta_lift h … HLK … HWU1 … HW) [ /2 width=4/ | skip ] -HW #H + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpss_lift_ge … HW12 … HLK … HWU1 … HWU2) -HLK -HWU1 // #HU12 + lapply (cpr_tpss … HU12) -HU12 #HU12 + @(snta_conv … U2) // /2 width=1/ /3 width=6/ (**) (* explicit constructor, /4 width=6/ is too slow *) + | lapply (ltpss_ldrop_conf_ge … HL12 … HLK1 ?) -L1 // -Hide /2 width=6/ + ] + ] + | * #K2 #V2 #W2 #Hdi #Hide #HLK2 #_ #_ + elim (ltpss_ldrop_conf_be … HL12 … HLK1 ? ?) -L1 // /2 width=2/ #X #H #HL2K0 + elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ -Hdi -Hide #K0 #V0 #_ #_ #H destruct + lapply (ldrop_mono … HL2K0 … HLK2) -HL2K0 -HLK2 #H destruct + ] +| #I #L1 #V1 #W1 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HV + lapply (IHTU1 (L2.ⓑ{I}V1) (d+1) e ? T1 ?) // /2 width=1/ #H + elim (snta_fwd_correct … H) -H #U2 #HU12 + @(snta_conv … (ⓑ{I}V2.U1)) /3 width=2/ /3 width=4/ /4 width=4/ (**) (* explicit constructor, /5 width=6/ is too slow *) +| #L1 #V1 #W11 #W12 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct + elim (tpss_inv_bind1 … HY) -HY #W21 #T2 #HW121 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HVV12 + lapply (IHTU1 L2 d e ? (ⓛW21.T2) ?) -IHTU1 // /2 width=1/ -HW121 -HT12 #H0 + elim (snta_fwd_correct … H0) #X #H + elim (snta_inv_bind1 … H) -H #W #U #l0 #HW #HU #_ + @(snta_conv … (ⓐV2.ⓛW12.U1)) /3 width=2/ /3 width=4/ /3 width=5/ (**) (* explicit constructor, /4 width=5/ is too slow *) +| #L1 #V1 #T1 #U1 #W1 #l #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + lapply (cpr_tpss … HV12) #HV + elim (snta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) (l+1) ?) [2: /3 width=4/ ] #U + @(snta_conv … (ⓐV2.U1)) /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *) +| #L1 #T1 #U1 #W1 #l1 #l2 #HTU1 #HUW1 #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H + elim (snta_fwd_correct … HTU1) -HTU1 #U #H + elim (snta_mono … HUW1 … H) -HUW1 -H #H #_ -U destruct + elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct + lapply (cpr_tpss … HU12) #HU /4 width=4/ +| #L1 #T1 #U11 #U12 #U #l #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12 + @(snta_conv … U11) /2 width=5/ (**) (* explicit constructor, /3 width=7/ is too slow *) +] +qed. + +lemma snta_ltpss_tps_conf: ∀h,L1,T1,U,l. ⦃h, L1⦄ ⊢ T1 :[l] U → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → ⦃h, L2⦄ ⊢ T2 :[l] U. +/3 width=7/ qed. + +lemma snta_ltpss_conf: ∀h,L1,T,U,l. ⦃h, L1⦄ ⊢ T :[l] U → + ∀L2,d,e. L1 ▶* [d, e] L2 → ⦃h, L2⦄ ⊢ T :[l] U. +/2 width=7/ qed. + +lemma snta_tpss_conf: ∀h,L,T1,U,l. ⦃h, L⦄ ⊢ T1 :[l] U → + ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ⦃h, L⦄ ⊢ T2 :[l] U. +/2 width=7/ qed. + +lemma snta_tps_conf: ∀h,L,T1,U,l. ⦃h, L⦄ ⊢ T1 :[l] U → + ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → ⦃h, L⦄ ⊢ T2 :[l] U. +/2 width=7/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc new file mode 100644 index 000000000..db71e1192 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_snta.etc @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||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/snta_lift.ma". + +(* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************) + +(* Main properties **********************************************************) + +theorem snta_mono: ∀h,L,T,U1,l1. ⦃h, L⦄ ⊢ T :[l1] U1 → + ∀U2,l2. ⦃h, L⦄ ⊢ T :[l2] U2 → l1 = l2 ∧ L ⊢ U1 ⬌* U2. +#h #L #T #U1 #l1 #H elim H -L -T -U1 -l1 +[ #L #k #X #l2 #H + lapply (snta_inv_sort1 … H) -H * /2 width=1/ +| #L #K #V #W11 #W12 #i #l1 #HLK #_ #HW112 #IHVW11 #X #l2 #H + elim (snta_inv_lref1 … H) -H * #K0 #V0 #W21 #W22 #HLK0 #HVW21 #HW212 #HX + lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct + lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK + elim (IHVW11 … HVW21) -IHVW11 -HVW21 #Hl12 #HW121 + lapply (cpcs_lift … HLK … HW112 … HW212 ?) // -K -W11 -W21 /3 width=3/ +| #L #K #W #V1 #V #i #l1 #HLK #_ #HWV #IHWV1 #X #l2 #H + elim (snta_inv_lref1 … H) -H * #K0 #W0 #V2 #V0 #HLK0 #HW0V2 #HWV0 [2: #HL2 ] #HX + lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H destruct + lapply (lift_mono … HWV0 … HWV) -HWV0 -HWV #H destruct + elim (IHWV1 … HW0V2) -IHWV1 -HW0V2 /3 width=1/ +| #I #L #V #W1 #T #U1 #l10 #l1 #_ #_ #_ #IHTU1 #X #l2 #H + elim (snta_inv_bind1 … H) -H #W2 #U2 #l20 #_ #HTU2 #H + elim (IHTU1 … HTU2) -IHTU1 -HTU2 #Hl12 #HU12 + lapply (cpcs_trans … (ⓑ{I}V.U1) … H) -H /2 width=1/ +| #L #V #W #W1 #T #U1 #l10 #l1 #_ #_ #_ #IHTU1 #X #l2 #H + elim (snta_fwd_pure1 … H) -H #U2 #W2 #l20 #_ #HTU2 #H + elim (IHTU1 … HTU2) -IHTU1 -HTU2 #Hl12 #HU12 + lapply (cpcs_trans … (ⓐV.ⓛW1.U1) … H) -H /2 width=1/ +| #L #V #T #U1 #W1 #l1 #_ #_ #IHTU1 #_ #X #l2 #H + elim (snta_fwd_pure1 … H) -H #U2 #W2 #l20 #_ #HTU2 #H + elim (IHTU1 … HTU2) -IHTU1 -HTU2 #Hl12 #HU12 + lapply (cpcs_trans … (ⓐV.U1) … H) -H /2 width=1/ +| #L #T #U1 #W1 #l10 #l1 #_ #_ #IHTU1 #_ #X #l2 #H + elim (snta_inv_cast1 … H) -H #HTU1 + elim (IHTU1 … HTU1) -IHTU1 -HTU1 /2 width=1/ +| #L #T #U11 #U12 #V12 #l1 #_ #HU112 #_ #IHTU11 #_ #U2 #l2 #HTU2 + elim (IHTU11 … HTU2) -IHTU11 -HTU2 #Hl12 #H + lapply (cpcs_canc_sn … HU112 … H) -U11 /2 width=1/ +] +qed-. + +(* Advanced properties ******************************************************) + +lemma snta_cast_alt: ∀h,L,T,W,U,l. ⦃h, L⦄ ⊢ T :[l] W → ⦃h, L⦄ ⊢ T :[l] U → + ⦃h, L⦄ ⊢ ⓝW.T :[l] U. +#h #L #T #W #U #l #HTW #HTU +elim (snta_mono … HTW … HTU) #_ #HWU +elim (snta_fwd_correct … HTU) -HTU /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc new file mode 100644 index 000000000..ceb5375bf --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/snta/snta_thin.etc @@ -0,0 +1,116 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/thin_ldrop.ma". +include "basic_2/equivalence/cpcs_delift.ma". +include "basic_2/dynamic/snta_lift.ma". + +(* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************) + +(* Properties on basic local environment thinning ***************************) + +(* Note: this is known as the substitution lemma *) +lemma snta_thin_conf: ∀h,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 :[l] U1 → + ∀L2,d,e. ≽ [d, e] L1 → L1 ▼*[d, e] ≡ L2 → + ∃∃T2,U2. ⦃h, L2⦄ ⊢ T2 :[l] U2 & + L1 ⊢ T1 ▼*[d, e] ≡ T2 & L1 ⊢ U1 ▼*[d, e] ≡ U2. +#h #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l +[ /2 width=5/ +| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL1 #HL12 + elim (lt_or_ge i d) #Hdi [ -HVW1 ] + [ lapply (sfr_ldrop_trans_ge … HLK1 … HL1 ?) -HL1 /2 width=2/ #H + lapply (sfr_inv_skip … H ?) -H /2 width=1/ #HK1 + elim (thin_ldrop_conf_le … HL12 … HLK1 ?) -HL12 /2 width=2/ #X #H #HLK2 + elim (thin_inv_delift1 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct + elim (IHVW1 … HK1 HK12) -IHVW1 -HK1 -HK12 #X2 #W2 #HVW2 #H #HW12 + lapply (delift_mono … H … HV12) -H -HV12 #H destruct + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #HLK1 + lapply (delift_lift_ge … HW12 … HLK1 HWU1 … HWU2) -HW12 -HLK1 -HWU1 // + >minus_plus minus_plus #HU1 + lapply (lift_conf_be … HWU2 … HW2U ?) -W2 /2 width=1/ #HU2 + lapply (delift_lift_div_be … HU1 … HU2 ? ?) -U // /2 width=1/ /3 width=8/ + | lapply (transitive_le … (i+1) Hide ?) /2 width=1/ #Hdei + lapply (thin_ldrop_conf_ge … HL12 … HLK1 ?) -HL12 -HLK1 // #HL2K1 + elim (lift_split … HWU1 d (i+1-e) ? ? ?) -HWU1 // /2 width=1/ #W + commutative_plus minus_plus commutative_plus (lift_inv_sort1 … H1) -X1 + >(lift_inv_sort1 … H2) -X2 // +| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2 + elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H + elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct + /3 width=8/ + | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 + lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ + ] +| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // (lift_inv_sort2 … H) -X /2 width=3/ +| #L2 #K2 #V2 #W2 #W #i #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H + elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ] + [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #V1 #HLK1 #HK21 #HV12 + elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HVW1 #HW12 + elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus minus_minus_m_m /2 width=1/ /3 width=6/ + | minus_plus minus_minus_m_m /2 width=1/ /3 width=6/ + | (tpss_inv_sort1 … H) -H /2 width=3/ +| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL12 #T2 #H + elim (tpss_inv_lref1 … H) -H [ | -HVW1 ] + [ #H destruct + elim (lt_or_ge i d) #Hdi [ -HVW1 | ] + [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct + elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12 + lapply (ldrop_fwd_ldrop2 … HLK2) #H + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1 + >minus_plus minus_plus #H + lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus minus_plus #H + lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus minus_plus minus_plus #H + lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus (sta_inv_sort1 … H) -X // +| #L #K #V #W #U1 #i #HLK #_ #HWU1 #IHVW #U2 #H + elim (sta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HW0U2 + lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct + lapply (IHVW … HVW0) -IHVW -HVW0 #H destruct + >(lift_mono … HWU1 … HW0U2) -W0 -U1 // +| #L #K #W #V #U1 #i #HLK #_ #HWU1 #IHWV #U2 #H + elim (sta_inv_lref1 … H) -H * #K0 #W0 #V0 #HLK0 #HWV0 #HV0U2 + lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct + lapply (IHWV … HWV0) -IHWV -HWV0 #H destruct + >(lift_mono … HWU1 … HV0U2) -W -U1 // +| #I #L #V #T #U1 #_ #IHTU1 #X #H + elim (sta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ +| #L #V #T #U1 #_ #IHTU1 #X #H + elim (sta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ +| #L #W #T #U1 #_ #IHTU1 #U2 #H + lapply (sta_inv_cast1 … H) -H /2 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma index 4c02d521d..83aff07c4 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma @@ -39,3 +39,8 @@ lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J. * /2 width=2/ #I #V #T #H elim (simple_inv_bind … H) qed-. + +(* +lemma mt: ∀R1,R2:Prop. (R1 → R2) → (R2 → ⊥) → R1 → ⊥. +/3 width=1/ qed-. +*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma b/matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma deleted file mode 100644 index c090997e6..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma +++ /dev/null @@ -1,53 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/dynamic/nta.ma". - -(* HIGHER ORDER NATIVE TYPE ASSIGNMENT ON TERMS *****************************) - -definition ntas: sh → lenv → relation term ≝ - λh,L. star … (nta h L). - -interpretation "higher order native type assignment (term)" - 'NativeTypeStar h L T U = (ntas h L T U). - -(* Basic eliminators ********************************************************) -(* -lemma cprs_ind: ∀L,T1. ∀R:predicate term. R T1 → - (∀T,T2. L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → R T → R T2) → - ∀T2. L ⊢ T1 ➡* T2 → R T2. -#L #T1 #R #HT1 #IHT1 #T2 #HT12 -@(TC_star_ind … HT1 IHT1 … HT12) // -qed-. -*) -axiom ntas_ind_dx: ∀h,L,T2. ∀R:predicate term. R T2 → - (∀T1,T. ⦃h, L⦄ ⊢ T1 : T → ⦃h, L⦄ ⊢ T :* T2 → R T → R T1) → - ∀T1. ⦃h, L⦄ ⊢ T1 :* T2 → R T1. -(* -#h #L #T2 #R #HT2 #IHT2 #T1 #HT12 -@(star_ind_dx … HT2 IHT2 … HT12) // -qed-. -*) -(* Basic properties *********************************************************) - -lemma ntas_refl: ∀h,L,T. ⦃h, L⦄ ⊢ T :* T. -// qed. - -lemma ntas_strap1: ∀h,L,T1,T,T2. - ⦃h, L⦄ ⊢ T1 :* T → ⦃h, L⦄ ⊢ T : T2 → ⦃h, L⦄ ⊢ T1 :* T2. -/2 width=3/ qed. - -lemma ntas_strap2: ∀h,L,T1,T,T2. - ⦃h, L⦄ ⊢ T1 : T → ⦃h, L⦄ ⊢ T :* T2 → ⦃h, L⦄ ⊢ T1 :* T2. -/2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma deleted file mode 100644 index 1adced79d..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma +++ /dev/null @@ -1,71 +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/dynamic/nta_lift.ma". -include "basic_2/hod/ntas.ma". - -(* HIGHER ORDER NATIVE TYPE ASSIGNMENT ON TERMS *****************************) - -(* Advanced properties on native type assignment for terms ******************) - -lemma nta_pure_ntas: ∀h,L,U,W,Y. ⦃h, L⦄ ⊢ U :* ⓛW.Y → ∀T. ⦃h, L⦄ ⊢ T : U → - ∀V. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.U. -#h #L #U #W #Y #H @(ntas_ind_dx … H) -U /2 width=1/ /3 width=2/ -qed. - -axiom pippo: ∀h,L,T,W,Y. ⦃h, L⦄ ⊢ T :* ⓛW.Y → ∀U. ⦃h, L⦄ ⊢ T : U → - ∃Z. ⦃h, L⦄ ⊢ U :* ⓛW.Z. -(* REQUIRES SUBJECT CONVERSION -#h #L #T #W #Y #H @(ntas_ind_dx … H) -T -[ #U #HYU - elim (nta_fwd_correct … HYU) #U0 #HU0 - elim (nta_inv_bind1 … HYU) #W0 #Y0 #HW0 #HY0 #HY0U -*) - -(* Advanced inversion lemmas on native type assignment for terms ************) - -fact nta_inv_pure1_aux: ∀h,L,Z,U. ⦃h, L⦄ ⊢ Z : U → ∀X,Y. Z = ⓐY.X → - ∃∃W,V,T. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & - L ⊢ ⓐY.V ⬌* U & ⦃h, L⦄ ⊢ V :* ⓛW.T. -#h #L #Z #U #H elim H -L -Z -U -[ #L #k #X #Y #H destruct -| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct -| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct -| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct -| #L #V #W #Z #U #HVW #HZU #_ #_ #X #Y #H destruct /2 width=7/ -| #L #V #W #Z #U #HZU #_ #_ #IHUW #X #Y #H destruct - elim (IHUW U Y ?) -IHUW // /3 width=9/ -| #L #Z #U #_ #_ #X #Y #H destruct -| #L #Z #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct - elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #W #V #T #HYW #HXV #HU1 #HVT - lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=7/ -] -qed. - -(* Basic_1: was only: ty3_gen_appl *) -lemma nta_inv_pure1: ∀h,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X : U → - ∃∃W,V,T. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & - L ⊢ ⓐY.V ⬌* U & ⦃h, L⦄ ⊢ V :* ⓛW.T. -/2 width=3/ qed-. - -axiom nta_inv_appl1: ∀h,L,Z,Y,X,U. ⦃h, L⦄ ⊢ ⓐZ.ⓛY.X : U → - ∃∃W. ⦃h, L⦄ ⊢ Z : Y & ⦃h, L⦄ ⊢ ⓛY.X : ⓛY.W & - L ⊢ ⓐZ.ⓛY.W ⬌* U. -(* REQUIRES SUBJECT REDUCTION -#h #L #Z #Y #X #U #H -elim (nta_inv_pure1 … H) -H #W #V #T #HZW #HXV #HVU #HVT -elim (nta_inv_bind1 … HXV) -HXV #Y0 #X0 #HY0 #HX0 #HX0V -lapply (cpcs_trans … (ⓐZ.ⓛY.X0) … HVU) -HVU /2 width=1/ -HX0V #HX0U -@(ex3_1_intro … HX0U) /2 width=2/ -*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/names.txt b/matita/matita/contribs/lambda_delta/basic_2/names.txt index 31ae26c39..1a4b33044 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/names.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/names.txt @@ -10,19 +10,28 @@ I,J : item K,L : local environment M,N : reserved: future use O : -P,Q : reserved: future use +P,Q : reserved: future use (lambda_delta 4) R : generic predicate (relation) S : RTM stack T,U,V,W: term X,Y,Z : reserved: transient objet denoted by a capital letter +a,b : reserved: future use (lambda_delta 4) +c : reserved: future use (lambda_delta 3) d : relocation depth e : relocation height +f : +g : sort degree parameter h : sort hierarchy parameter i,j : local reference position index (de Bruijn's) k : sort index +l : term degree +m,n : reserved: future use +o : p,q : global reference position +r,s : t,u : local reference position level (de Bruijn's) +v,w : x,y,z : reserved: transient objet denoted by a small letter NAMING CONVENTIONS FOR CONSTRUCTORS diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 31126679f..6bbde1839 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -222,15 +222,15 @@ 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 )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break [ g , break l ] break term 46 T2 )" non associative with precedence 45 - for @{ 'StaticType $h $L $T1 $T2 }. + for @{ 'StaticType $h $g $l $L $T1 $T2 }. (* Unwind *******************************************************************) -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break term 46 T2 )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 •* break [ g ] break term 46 T2 )" non associative with precedence 45 - for @{ 'StaticTypeStar $h $L $T1 $T2 }. + for @{ 'StaticTypeStar $h $g $L $T1 $T2 }. (* Reducibility *************************************************************) @@ -294,6 +294,10 @@ notation "hvbox( L1 ⊢ ➡ break term 46 L2 )" non associative with precedence 45 for @{ 'CPRed $L1 $L2 }. +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'XRed $h $g $L $T1 $T2 }. + (* Computation **************************************************************) notation "hvbox( T1 ➡* break term 46 T2 )" @@ -316,11 +320,11 @@ notation "hvbox( ⬇ * term 46 T )" non associative with precedence 45 for @{ 'SN $T }. -notation "hvbox( L ⊢ break ⬇ * term 46 T )" +notation "hvbox( L ⊢ ⬇ * break term 46 T )" non associative with precedence 45 for @{ 'SN $L $T }. -notation "hvbox( L ⊢ break ⬇ ⬇ * term 46 T )" +notation "hvbox( L ⊢ ⬇ ⬇ * break term 46 T )" non associative with precedence 45 for @{ 'SNAlt $L $T }. @@ -332,6 +336,14 @@ notation "hvbox( T1 ⊑ break [ R ] break term 46 T2 )" non associative with precedence 45 for @{ 'CrSubEq $T1 $R $T2 }. +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ * break [ g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'XRedStar $h $g $L $T1 $T2 }. + +notation "hvbox( ⦃ h , break L ⦄ ⊢ ➷ * break [ g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'XSN $h $g $L $T }. + (* Conversion ***************************************************************) notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" @@ -354,20 +366,20 @@ notation "hvbox( T1 ⊢ ⬌* break term 46 T2 )" (* Dynamic typing ***********************************************************) +notation "hvbox( ⦃ h , break L ⦄ ⊩ break term 46 T : break [ g ] )" + non associative with precedence 45 + for @{ 'NativeValid $h $g $L $T }. + notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : break term 46 T2 )" non associative with precedence 45 for @{ 'NativeType $h $L $T1 $T2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 :: break term 46 T2 )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )" non associative with precedence 45 for @{ 'NativeTypeAlt $h $L $T1 $T2 }. -notation "hvbox( h ⊢ break term 46 L1 : ⊑ break term 46 L2 )" - non associative with precedence 45 - for @{ 'CrSubEqN $h $L1 $L2 }. - (* Higher order dynamic typing **********************************************) -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 :* break term 46 T2 )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )" non associative with precedence 45 for @{ 'NativeTypeStar $h $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma index 068a5f751..b3dbcf40c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma @@ -78,7 +78,7 @@ elim (tpr_inv_abbr1 … H1) -H1 * lapply (tps_weak_all … HT0) -HT0 #HT0 lapply (tpss_lsubs_trans … HT02 (L. ⓓV) ?) -HT02 /2 width=1/ #HT02 lapply (tpss_weak_all … HT02) -HT02 #HT02 - lapply (tpss_strap … HT0 HT02) -T0 /4 width=7/ + lapply (tpss_strap2 … HT0 HT02) -T0 /4 width=7/ | #T2 #HT12 #HXT2 elim (lift_total Y 0 1) #Z #HYZ lapply (tpss_lift_ge … H2 (L.ⓓV1) … HXT2 … HYZ) -X // /2 width=1/ #H diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma new file mode 100644 index 000000000..04adbae95 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/static/sd.ma @@ -0,0 +1,105 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/sh.ma". + +(* SORT DEGREE **************************************************************) + +(* sort degree specification *) +record sd (h:sh): Type[0] ≝ { + deg : relation nat; (* degree of the sort *) + deg_total: ∀k. ∃l. deg k l; (* functional relation axioms *) + deg_mono : ∀k,l1,l2. deg k l1 → deg k l2 → l1 = l2; + deg_next : ∀k,l. deg k l → deg (next h k) (l - 1); (* compatibility condition *) + deg_prev : ∀k,l. deg (next h k) (l + 1) → deg k (l + 2) +}. + +(* Notable specifications ***************************************************) + +definition deg_O: relation nat ≝ λk,l. l = 0. + +definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O …. +// /2 width=1/ /2 width=2/ qed. + +inductive deg_SO (h:sh) (k:nat) (k0:nat): predicate nat ≝ +| deg_SO_pos : ∀l0. (next h)^l0 k0 = k → deg_SO h k k0 (l0 + 1) +| deg_SO_zero: ((∃l0. (next h)^l0 k0 = k) → ⊥) → deg_SO h k k0 0 +. + +fact deg_SO_inv_pos_aux: ∀h,k,k0,l0. deg_SO h k k0 l0 → ∀l. l0 = l + 1 → + (next h)^l k0 = k. +#h #k #k0 #l0 * -l0 +[ #l0 #Hl0 #l #H + lapply (injective_plus_l … H) -H #H destruct // +| #_ #l0 H -H #H + lapply (transitive_lt … H HK12) -k1 #H1 + lapply (nexts_le h k2 l) #H2 + lapply (le_to_lt_to_lt … H2 H1) -h -l #H + elim (lt_refl_false … H) +qed. + +definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) …. +[ #k0 + lapply (nexts_dec h k0 k) * [ * /3 width=2/ | /4 width=2/ ] +| #K0 #l1 #l2 * [ #l01 ] #H1 * [1,3: #l02 ] #H2 // + [ < H2 in H1; -H2 #H + lapply (nexts_inj … H) -H #H destruct // + | elim (H1 ?) /2 width=2/ + | elim (H2 ?) /2 width=2/ + ] +| #k0 #l0 * + [ #l #H destruct elim l -l normalize /2 width=1/ + | #H1 @deg_SO_zero * #l #H2 destruct + @H1 -H1 @(ex_intro … (S l)) /2 width=1/ (**) (* explicit constructor *) + ] +| #K0 #l0 #H + <(deg_SO_inv_pos … H) -H >plus_n_2 + @deg_SO_pos >iter_SO /2 width=1/ (**) (* explicit constructor: iter_SO is needed *) +] +qed. + +let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝ + match l with + [ O ⇒ sd_O h + | S l ⇒ match l with + [ O ⇒ sd_SO h k + | _ ⇒ sd_l h (next h k) l + ] + ]. + +(* Basic properties *********************************************************) + +lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1). +#h #k #l (lift_inv_sort1 … H1) -X1 + >(lift_inv_sort1 … H2) -X2 /2 width=1/ +| #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2 + elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H + elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct + /3 width=8/ + | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 + lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ + ] +| #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 + elim (lift_inv_lref1 … H) * #Hid #H destruct + [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // (lift_inv_sort2 … H) -X /3 width=3/ +| #L2 #K2 #V2 #W2 #W #i #l #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H + elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ] + [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #V1 #HLK1 #HK21 #HV12 + elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HVW1 #HW12 + elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus minus_minus_m_m /2 width=1/ /3 width=6/ + | minus_plus minus_minus_m_m /2 width=1/ /3 width=6/ + | (tpss_inv_sort1 … H) -H /3 width=3/ +| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL12 #T2 #H + elim (tpss_inv_lref1 … H) -H [ | -HVW1 ] + [ #H destruct + elim (lt_or_ge i d) #Hdi [ -HVW1 | ] + [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 + elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct + elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12 + lapply (ldrop_fwd_ldrop2 … HLK2) #H + elim (lift_total W2 0 (i+1)) #U2 #HWU2 + lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1 + >minus_plus minus_plus #H + lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus minus_plus #H + lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus minus_plus minus_plus #H + lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus (deg_mono … Hkl2 … Hkl) -g -L -l2 /2 width=1/ +| #L #K #V #W #U1 #i #l1 #HLK #_ #HWU1 #IHVW #U2 #l2 #H + elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 [2: #l0] #HLK0 #HVW0 #HW0U2 + lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct + lapply (IHVW … HVW0) -IHVW -HVW0 * #H1 #H2 destruct + >(lift_mono … HWU1 … HW0U2) -W0 -U1 /2 width=1/ +| #L #K #W #V #U1 #i #l1 #HLK #_ #HWU1 #IHWV #U2 #l2 #H + elim (ssta_inv_lref1 … H) -H * #K0 #W0 #V0 [2: #l0 ] #HLK0 #HWV0 #HV0U2 + lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct + lapply (IHWV … HWV0) -IHWV -HWV0 * #H1 #H2 destruct + >(lift_mono … HWU1 … HV0U2) -W -U1 /2 width=1/ +| #I #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H + elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct + elim (IHTU1 … HTU2) -T /3 width=1/ +| #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H + elim (ssta_inv_appl1 … H) -H #U2 #HTU2 #H destruct + elim (IHTU1 … HTU2) -T /3 width=1/ +| #L #V #W1 #T #U1 #l1 #_ #_ #IHVW1 #IHTU1 #U2 #l2 #H + elim (ssta_inv_cast1 … H) -H #W2 #T2 #HVW2 #HTU2 #H destruct + elim (IHVW1 … HVW2) -V + elim (IHTU1 … HTU2) -T /2 width=1/ +] +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 deleted file mode 100644 index 20302c623..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma +++ /dev/null @@ -1,128 +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/substitution/ldrop.ma". -include "basic_2/static/sh.ma". - -(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************) - -inductive sta (h:sh): lenv → relation term ≝ -| sta_sort: ∀L,k. sta h L (⋆k) (⋆(next h k)) -| sta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → sta h K V W → - ⇧[0, i + 1] W ≡ U → sta h L (#i) U -| sta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → sta h K W V → - ⇧[0, i + 1] W ≡ U → sta h L (#i) U -| sta_bind: ∀I,L,V,T,U. sta h (L. ⓑ{I} V) T U → - 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 -. - -interpretation "static type assignment (term)" - 'StaticType h L T U = (sta h L T U). - -(* Basic inversion lemmas ************************************************) - -fact sta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀k0. T = ⋆k0 → - U = ⋆(next h k0). -#h #L #T #U * -L -T -U -[ #L #k #k0 #H destruct // -| #L #K #V #W #U #i #_ #_ #_ #k0 #H destruct -| #L #K #W #V #U #i #_ #_ #_ #k0 #H destruct -| #I #L #V #T #U #_ #k0 #H destruct -| #L #V #T #U #_ #k0 #H destruct -| #L #W #T #U #_ #k0 #H destruct -qed. - -(* Basic_1: was: sty0_gen_sort *) -lemma sta_inv_sort1: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k • U → U = ⋆(next h k). -/2 width=4/ qed-. - -fact sta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀j. T = #j → - (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V • W & - ⇧[0, j + 1] W ≡ U - ) ∨ - (∃∃K,W,V. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W • V & - ⇧[0, j + 1] W ≡ U - ). -#h #L #T #U * -L -T -U -[ #L #k #j #H destruct -| #L #K #V #W #U #i #HLK #HVW #HWU #j #H destruct /3 width=6/ -| #L #K #W #V #U #i #HLK #HWV #HWU #j #H destruct /3 width=6/ -| #I #L #V #T #U #_ #j #H destruct -| #L #V #T #U #_ #j #H destruct -| #L #W #T #U #_ #j #H destruct -] -qed. - -(* Basic_1: was sty0_gen_lref *) -lemma sta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i • U → - (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V • W & - ⇧[0, i + 1] W ≡ U - ) ∨ - (∃∃K,W,V. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W • V & - ⇧[0, i + 1] W ≡ U - ). -/2 width=3/ qed-. - -fact sta_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀J,X,Y. T = ⓑ{J}Y.X → - ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X • Z & U = ⓑ{J}Y.Z. -#h #L #T #U * -L -T -U -[ #L #k #J #X #Y #H destruct -| #L #K #V #W #U #i #_ #_ #_ #J #X #Y #H destruct -| #L #K #W #V #U #i #_ #_ #_ #J #X #Y #H destruct -| #I #L #V #T #U #HTU #J #X #Y #H destruct /2 width=3/ -| #L #V #T #U #_ #J #X #Y #H destruct -| #L #W #T #U #_ #J #X #Y #H destruct -] -qed. - -(* Basic_1: was: sty0_gen_bind *) -lemma sta_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X • U → - ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X • Z & U = ⓑ{J}Y.Z. -/2 width=3/ qed-. - -fact sta_inv_appl1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓐY.X → - ∃∃Z. ⦃h, L⦄ ⊢ X • Z & U = ⓐY.Z. -#h #L #T #U * -L -T -U -[ #L #k #X #Y #H destruct -| #L #K #V #W #U #i #_ #_ #_ #X #Y #H destruct -| #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct -| #I #L #V #T #U #_ #X #Y #H destruct -| #L #V #T #U #HTU #X #Y #H destruct /2 width=3/ -| #L #W #T #U #_ #X #Y #H destruct -] -qed. - -(* Basic_1: was: sty0_gen_appl *) -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 → - ⦃h, L⦄ ⊢ X • U. -#h #L #T #U * -L -T -U -[ #L #k #X #Y #H destruct -| #L #K #V #W #U #i #_ #_ #_ #X #Y #H destruct -| #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct -| #I #L #V #T #U #_ #X #Y #H destruct -| #L #V #T #U #_ #X #Y #H destruct -| #L #W #T #U #HTU #X #Y #H destruct // -] -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. -/2 width=4/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma deleted file mode 100644 index c9fbda014..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma +++ /dev/null @@ -1,120 +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/substitution/ldrop_ldrop.ma". -include "basic_2/static/sta.ma". - -(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************) - -(* Properties on relocation *************************************************) - -(* Basic_1: was: sty0_lift *) -lemma sta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 • U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → - ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 • U2. -#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1 -[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2 - >(lift_inv_sort1 … H1) -X1 - >(lift_inv_sort1 … H2) -X2 // -| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2 - elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H - elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct - /3 width=8/ - | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2 - lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/ - ] -| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hid #H destruct - [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // (lift_inv_sort2 … H) -X /2 width=3/ -| #L2 #K2 #V2 #W2 #W #i #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H - elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ] - [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #V1 #HLK1 #HK21 #HV12 - elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HVW1 #HW12 - elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus minus_minus_m_m /2 width=1/ /3 width=6/ - | minus_plus minus_minus_m_m /2 width=1/ /3 width=6/ - | (tpss_inv_sort1 … H) -H /2 width=3/ -| #L1 #K1 #V1 #W1 #U1 #i #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #d #e #HL12 #T2 #H - elim (tpss_inv_lref1 … H) -H [ | -HVW1 ] - [ #H destruct - elim (lt_or_ge i d) #Hdi [ -HVW1 | ] - [ elim (ltpss_ldrop_conf_le … HL12 … HLK1 ?) -L1 /2 width=2/ #X #H #HLK2 - elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K2 #V2 #HK12 #HV12 #H destruct - elim (IHVW1 … HK12 … HV12) -IHVW1 -HK12 -HV12 #W2 #HVW2 #HW12 - lapply (ldrop_fwd_ldrop2 … HLK2) #H - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (tpss_lift_ge … HW12 … H … HWU1 … HWU2) // -HW12 -H -HWU1 - >minus_plus minus_plus #H - lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus minus_plus #H - lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus minus_plus minus_plus #H - lapply (tpss_weak … H d e ? ?) [1,2: normalize [ >commutative_plus (sta_inv_sort1 … H) -X // -| #L #K #V #W #U1 #i #HLK #_ #HWU1 #IHVW #U2 #H - elim (sta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HW0U2 - lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct - lapply (IHVW … HVW0) -IHVW -HVW0 #H destruct - >(lift_mono … HWU1 … HW0U2) -W0 -U1 // -| #L #K #W #V #U1 #i #HLK #_ #HWU1 #IHWV #U2 #H - elim (sta_inv_lref1 … H) -H * #K0 #W0 #V0 #HLK0 #HWV0 #HV0U2 - lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct - lapply (IHWV … HWV0) -IHWV -HWV0 #H destruct - >(lift_mono … HWU1 … HV0U2) -W -U1 // -| #I #L #V #T #U1 #_ #IHTU1 #X #H - elim (sta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ -| #L #V #T #U1 #_ #IHTU1 #X #H - elim (sta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1/ -| #L #W #T #U1 #_ #IHTU1 #U2 #H - lapply (sta_inv_cast1 … H) -H /2 width=1/ -] -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 2608f02ce..bb5b3ac4e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma @@ -99,3 +99,10 @@ lemma delift_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 ▼*[d, 0] ≡ T2 → T1 = T2. >(tpss_inv_refl_O2 … HT1) -HT1 #HT2 >(lift_inv_refl_O2 … HT2) -HT2 // qed-. + +(* Basic forward lemmas *****************************************************) + +lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▼*[d, e] ≡ T2 → #[T1] ≤ #[T2]. +#L #T1 #T2 #d #e * #T #HT1 #HT2 +>(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw / +qed-. 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 7166fa221..97f4e1fde 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 @@ -81,7 +81,7 @@ lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 → d ≤ dd → dd ≤ d + e → d + e ≤ dd + ee → ∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 & L ⊢ U2 ▼*[dd, ee] ≡ T2. -/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap/ qed. (**) (* too slow without trace *) +/3 width=6 by thin_delift_tpss_conf_le_up, tpss_strap2/ qed. (**) (* too slow without trace *) lemma thin_delift_tpss_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 → ∀T1,dd,ee. L ⊢ U1 ▼*[dd, ee] ≡ T1 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma index 0e98ece73..b44570c2f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma @@ -40,8 +40,8 @@ qed-. (* Basic properties *********************************************************) -lemma tpss_strap: ∀L,T1,T,T2,d,e. - L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2. +lemma tpss_strap2: ∀L,T1,T,T2,d,e. + L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2. /2 width=3/ qed. lemma tpss_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma new file mode 100644 index 000000000..9152b44ae --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas.ma @@ -0,0 +1,106 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta.ma". + +(* STRATIFIED UNWIND ON TERMS ***********************************************) + +inductive sstas (h:sh) (g:sd h) (L:lenv): relation term ≝ +| sstas_refl: ∀T,U. ⦃h, L⦄ ⊢ T •[g, 0] U → sstas h g L T T +| sstas_step: ∀T,U1,U2,l. ⦃h, L⦄ ⊢ T •[g, l+1] U1 → sstas h g L U1 U2 → + sstas h g L T U2. + +interpretation "stratified unwind (term)" + 'StaticTypeStar h g L T U = (sstas h g L T U). + +(* Basic eliminators ********************************************************) + +fact sstas_ind_alt_aux: ∀h,g,L,U2. ∀R:predicate term. + (∀T. ⦃h, L⦄ ⊢ U2 •[g , 0] T → R U2) → + (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → + ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T + ) → + ∀T,U. ⦃h, L⦄ ⊢ T •*[g] U → U = U2 → R T. +#h #g #L #U2 #R #H1 #H2 #T #U #H elim H -H -T -U /2 width=2/ /3 width=5/ +qed-. + +lemma sstas_ind_alt: ∀h,g,L,U2. ∀R:predicate term. + (∀T. ⦃h, L⦄ ⊢ U2 •[g , 0] T → R U2) → + (∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → + ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T + ) → + ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T. +/3 width=9 by sstas_ind_alt_aux/ qed-. + +(* Basic inversion lemmas ***************************************************) + +fact sstas_inv_sort1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀k. T = ⋆k → + ∀l. deg h g k l → U = ⋆((next h)^l k). +#h #g #L #T #U #H @(sstas_ind_alt … H) -T +[ #U0 #HU0 #k #H #l #Hkl destruct + elim (ssta_inv_sort1 … HU0) -L #HkO #_ -U0 + >(deg_mono … Hkl HkO) -g -l // +| #T0 #U0 #l0 #HTU0 #_ #IHU0 #k #H #l #Hkl destruct + elim (ssta_inv_sort1 … HTU0) -L #HkS #H destruct + lapply (deg_mono … Hkl HkS) -Hkl #H destruct + >(IHU0 (next h k) ? l0) -IHU0 // /2 width=1/ >iter_SO >iter_n_Sm // +] +qed. + +lemma sstas_inv_sort1: ∀h,g,L,U,k. ⦃h, L⦄ ⊢ ⋆k •*[g] U → ∀l. deg h g k l → + U = ⋆((next h)^l k). +/2 width=6/ qed-. + +fact sstas_inv_bind1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → + ∀J,X,Y. T = ⓑ{J}Y.X → + ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{J}Y.Z. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T +[ #U0 #HU0 #J #X #Y #H destruct + elim (ssta_inv_bind1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/ +| #T0 #U0 #l #HTU0 #_ #IHU0 #J #X #Y #H destruct + elim (ssta_inv_bind1 … HTU0) -HTU0 #X0 #HX0 #H destruct + elim (IHU0 J X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/ +] +qed. + +lemma sstas_inv_bind1: ∀h,g,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X •*[g] U → + ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X •*[g] Z & U = ⓑ{J}Y.Z. +/2 width=3/ qed-. + +fact sstas_inv_appl1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀X,Y. T = ⓐY.X → + ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T +[ #U0 #HU0 #X #Y #H destruct + elim (ssta_inv_appl1 … HU0) -HU0 #X0 #HX0 #H destruct /3 width=3/ +| #T0 #U0 #l #HTU0 #_ #IHU0 #X #Y #H destruct + elim (ssta_inv_appl1 … HTU0) -HTU0 #X0 #HX0 #H destruct + elim (IHU0 X0 Y ?) -IHU0 // #X1 #HX01 #H destruct /3 width=4/ +] +qed. + +lemma sstas_inv_appl1: ∀h,g,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X •*[g] U → + ∃∃Z. ⦃h, L⦄ ⊢ X •*[g] Z & U = ⓐY.Z. +/2 width=3/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma sstas_fwd_correct: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → + ∃∃W. ⦃h, L⦄ ⊢ U •[g, 0] W & ⦃h, L⦄ ⊢ U •*[g] U. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T /2 width=1/ /3 width=2/ +qed-. + +(* Basic_1: removed theorems 7: + sty1_bind sty1_abbr sty1_appl sty1_cast2 + sty1_lift sty1_correct sty1_trans +*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma new file mode 100644 index 000000000..28302d71b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_lift.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta_lift.ma". +include "basic_2/unwind/sstas.ma". + +(* STRATIFIED UNWIND ON TERMS ***********************************************) + +(* Advanced properties ******************************************************) + +lemma sstas_total_S: ∀h,g,L,l,T,U. ⦃h, L⦄ ⊢ T•[g, l + 1]U → + ∃∃W. ⦃h, L⦄ ⊢ T •*[g] W & ⦃h, L⦄ ⊢ U •*[g] W. +#h #g #L #l @(nat_ind_plus … l) -l +[ #T #U #HTU + elim (ssta_fwd_correct … HTU) /4 width=4/ +| #l #IHl #T #U #HTU + elim (ssta_fwd_correct … HTU) (lift_mono … HX … HU12) -X + elim (lift_total T1 d e) /3 width=10/ +| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL21 #T2 #HT02 #U2 #HU12 + elim (lift_total U0 d e) /3 width=10/ +] +qed. + +lemma sstas_inv_lift1: ∀h,g,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 → + ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 → + ∃∃U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 & ⇧[d, e] U1 ≡ U2. +#h #g #L2 #T2 #U2 #H @(sstas_ind_alt … H) -T2 +[ #T2 #HUT2 #L1 #d #e #HL21 #U1 #HU12 + elim (ssta_inv_lift1 … HUT2 … HL21 … HU12) -HUT2 -HL21 /3 width=3/ +| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L1 #d #e #HL21 #U1 #HU12 + elim (ssta_inv_lift1 … HTU0 … HL21 … HU12) -HTU0 -HU12 #U #HU1 #HU0 + elim (IHU01 … HL21 … HU0) -IHU01 -HL21 -U0 /3 width=4/ +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_ltpss.ma new file mode 100644 index 000000000..0ef8f47e7 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_ltpss.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta_ltpss.ma". +include "basic_2/unwind/sstas.ma". + +(* STRATIFIED UNWIND ON TERMS ***********************************************) + +(* Properties about parallel unfold *****************************************) + +lemma sstas_ltpss_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & + L2 ⊢ U1 ▶* [d, e] U2. +#h #g #L1 #T1 #U1 #H @(sstas_ind_alt … H) -T1 +[ #T1 #HUT1 #L2 #d #e #HL12 #U2 #HU12 + elim (ssta_ltpss_tpss_conf … HUT1 … HL12 … HU12) -HUT1 -HL12 /3 width=3/ +| #T0 #U0 #l0 #HTU0 #_ #IHU01 #L2 #d #e #HL12 #T #HT0 + elim (ssta_ltpss_tpss_conf … HTU0 … HL12 … HT0) -HTU0 -HT0 #U #HTU #HU0 + elim (IHU01 … HL12 … HU0) -IHU01 -HL12 -U0 /3 width=4/ +] +qed. + +lemma sstas_ltpss_tps_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. +/3 width=5/ qed. + +lemma sstas_ltpss_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*[g] U1 → + ∀L2,d,e. L1 ▶* [d, e] L2 → + ∃∃U2. ⦃h, L2⦄ ⊢ T •*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2. +/2 width=5/ qed. + +lemma sstas_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 → + ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2. +/2 width=5/ qed. + +lemma sstas_tps_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*[g] U1 → + ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → + ∃∃U2. ⦃h, L⦄ ⊢ T2 •*[g] U2 & L ⊢ U1 ▶* [d, e] U2. +/2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma new file mode 100644 index 000000000..9df5b0b47 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unwind/sstas_sstas.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/delift_lift.ma". +include "basic_2/static/ssta_ssta.ma". +include "basic_2/unwind/sstas_lift.ma". + +(* STRATIFIED UNWIND ON TERMS ***********************************************) + +(* Advanced inversion lemmas ************************************************) + +lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → + ∀T0. ⦃h, L⦄ ⊢ T •[g , 0] T0 → U = T. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T // +#T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01 +elim (ssta_mono … HTU0 … HT01) (sstas_inv_O … HU12 … HUT1) -h -L -T1 -U2 // +| #T0 #U0 #l0 #HTU0 #_ #IHU01 #U2 #HU12 + lapply (sstas_inv_S … HU12 … HTU0) -T0 -l0 /2 width=1/ +] +qed-. + +(* More advancd inversion lemmas ********************************************) + +fact sstas_inv_lref1_aux: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → ∀j. T = #j → + ∃∃I,K,V,W. ⇩[0, j] L ≡ K. ⓑ{I}V & ⦃h, K⦄ ⊢ V •*[g] W & + L ⊢ U ▼*[0, j + 1] ≡ W. +#h #g #L #T #U #H @(sstas_ind_alt … H) -T +[ #T #HUT #j #H destruct + elim (ssta_inv_lref1 … HUT) -HUT * #K #V #W [2: #l] #HLK #HVW #HVT + [ (sstas_mono … HWX … HWT) -X -W /3 width=7/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma index c65a47bcc..c51873baa 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/arith.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/arith.ma @@ -19,6 +19,9 @@ include "ground_2/star.ma". (* Equations ****************************************************************) +lemma plus_n_2: ∀n. n + 2 = n + 1 + 1. +// qed. + lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p). /2 by plus_minus/ qed. @@ -66,11 +69,21 @@ lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x. #Hxy elim (H Hxy) qed-. -(* -lemma pippo: ∀x,y,z. x < z → y < z - x → x + y < z. -/3 width=2/ +(* iterators ****************************************************************) -lemma le_or_ge: ∀m,n. m ≤ n ∨ n ≤ m. -#m #n elim (lt_or_ge m n) /2 width=1/ /3 width=2/ -qed-. -*) +(* Note: see also: lib/arithemetcs/bigops.ma *) +let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝ + match n with + [ O ⇒ nil + | S k ⇒ op (iter k B op nil) + ]. + +interpretation "iterated function" 'exp op n = (iter n ? op). + +lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b). +#B #f #b #l >commutative_plus // +qed. + +lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b). +#B #f #b #l elim l -l normalize // +qed.