From ba575c0609015580c1419c17b350de19a158e8e3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 7 Nov 2012 17:48:14 +0000 Subject: [PATCH] - commit completed!! The static type of .T is now the static type of T. This allows to prove that each valid term has a static type as expected! --- .../lambda_delta/basic_2/computation/yprs.ma | 48 ------------- .../basic_2/computation/yprs_csups.ma | 25 ------- .../basic_2/computation/yprs_xprs.ma | 28 -------- .../basic_2/computation/yprs_yprs.ma | 20 ------ .../basic_2/computation/ysteps.ma | 43 ------------ .../basic_2/computation/ysteps_csups.ma | 28 -------- .../lambda_delta/basic_2/dynamic/snv_ssta.ma | 67 +++++++++++++++++++ .../basic_2/reducibility/ltpr_aaa.ma | 4 +- .../basic_2/reducibility/tpr_tpr.ma | 2 +- .../lambda_delta/basic_2/reducibility/ypr.ma | 37 ---------- 10 files changed, 70 insertions(+), 232 deletions(-) delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/yprs.ma delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/yprs_csups.ma delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/yprs_xprs.ma delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/yprs_yprs.ma delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/ysteps.ma delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/ysteps_csups.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma delete mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/ypr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/yprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/yprs.ma deleted file mode 100644 index 9ad7e53c4..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/yprs.ma +++ /dev/null @@ -1,48 +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/reducibility/ypr.ma". - -(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************) - -definition yprs: ∀h. sd h → bi_relation lenv term ≝ - λh,g. bi_TC … (ypr h g). - -interpretation "hyper parallel computation (closure)" - 'YPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 → - (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L2 T2. -/3 width=7 by bi_TC_star_ind/ qed-. - -lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 → - (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → R L1 T1. -/3 width=7 by bi_TC_star_ind_dx/ qed-. - -(* Basic properties *********************************************************) - -lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g). -/2 width=1/ qed. - -lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ •⥸[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄. -/2 width=4/ qed. - -lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ •⥸[g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ •⥸*[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄. -/2 width=4/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_csups.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_csups.ma deleted file mode 100644 index 08c939d8d..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_csups.ma +++ /dev/null @@ -1,25 +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/csups.ma". -include "basic_2/computation/yprs.ma". - -(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************) - -(* Properties on iterated supclosure ****************************************) - -lemma csups_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 /3 width=1/ /3 width=4/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_xprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_xprs.ma deleted file mode 100644 index 2feb88a2f..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_xprs.ma +++ /dev/null @@ -1,28 +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/xprs_cprs.ma". -include "basic_2/computation/yprs.ma". - -(* HYPER PARALLEL COMPUTATION ON CLOSURES ***********************************) - -(* Properties on extended parallel computation for terms ********************) - -lemma xprs_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 → - h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(xprs_ind … H) -T2 // /3 width=4/ -qed. - -lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ •⥸*[g] ⦃L, T2⦄. -/3 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_yprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_yprs.ma deleted file mode 100644 index d737dd817..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_yprs.ma +++ /dev/null @@ -1,20 +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/yprs.ma". - -(* HYPER PARALLEL COMPUTATION ON TERMS **************************************) - -theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g). -/2 width=4/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ysteps.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ysteps.ma deleted file mode 100644 index a6114c3b1..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/ysteps.ma +++ /dev/null @@ -1,43 +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/csup.ma". -include "basic_2/computation/yprs.ma". - -(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************) - -inductive ysteps (h) (g) (L1) (T1) (L2) (T2): Prop ≝ -| ysteps_intro: h ⊢ ⦃L1, T1⦄ •⥸*[g] ⦃L2, T2⦄ → (L1 = L2 → T1 = T2 → ⊥) → - ysteps h g L1 T1 L2 T2 -. - -interpretation "iterated step of hyper parallel computation (closure)" - 'YPRedStepStar h g L1 T1 L2 T2 = (ysteps h g L1 T1 L2 T2). - -(* Basic properties *********************************************************) - -lemma ssta_ysteps: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U → - h ⊢ ⦃L, T⦄ •⭃*[g] ⦃L, U⦄. -#h #g #L #T #U #l #HTU -@ysteps_intro /3 width=2/ #_ #H destruct -elim (ssta_inv_refl … HTU) -qed. - -lemma csup_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H -lapply (csup_fwd_cw … H) #H1 -@ysteps_intro /3 width=1/ -H #H2 #H3 destruct -elim (lt_refl_false … H1) -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ysteps_csups.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ysteps_csups.ma deleted file mode 100644 index 2e48f396d..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/ysteps_csups.ma +++ /dev/null @@ -1,28 +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/yprs_csups.ma". -include "basic_2/computation/ysteps.ma". - -(* ITERATED STEP OF HYPER PARALLEL COMPUTATION ON CLOSURES ******************) - -(* Properties on iterated supclosure ****************************************) - -lemma csups_ysteps: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ •⭃*[g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H -lapply (csups_fwd_cw … H) #H1 -@ysteps_intro /2 width=1/ -H #H2 #H3 destruct -elim (lt_refl_false … H1) -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma new file mode 100644 index 000000000..a934ca08e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma @@ -0,0 +1,67 @@ +(**************************************************************************) +(* ___ *) +(* ||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". +include "basic_2/dynamic/snv.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Properties on stratified static type assignment for terms ****************) + +lemma snv_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃U,l. ⦃h, L⦄ ⊢ T •[g, l] U. +#h #g #L #T #H elim H -L -T +[ #L #k elim (deg_total h g k) /3 width=3/ +| * #L #K #V #i #HLK #_ * #W #l0 #HVW + [ elim (lift_total W 0 (i+1)) /3 width=8/ + | elim (lift_total V 0 (i+1)) /3 width=8/ + ] +| #a #I #L #V #T #_ #_ #_ * /3 width=3/ +| #a #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/ +| #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *) +] +qed-. +(* +fact snv_ssta_conf_aux: ∀h,g,L,T. ( + ∀L0,T1,U1,l1. ⦃h, L0⦄ ⊢ T1 •[g, l1] U1 → + ∀T2,U2,l2. ⦃h, L0⦄ ⊢ T2 •[g, l2] U2 → + L0 ⊢ T1 ⬌* T2 → ⦃h, L0⦄ ⊩ T1 :[g] → ⦃h, L0⦄ ⊩ T2 :[g] → + #{L0, T1} < #{L ,T} → + l1 = l2 ∧ L0 ⊢ U1 ⬌* U2 + ) → ( + ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → + ∀U0. ⦃h, L0⦄ ⊢ T0 •➡*[g] U0 → + #{L0, T0} < #{L ,T} → + ⦃h, L0⦄ ⊩ U0 :[g] + ) → + ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → + ∀U0,l. ⦃h, L⦄ ⊢ T0 •[g, l + 1] U0 → + L0 = L → T0 = T → ⦃h, L0⦄ ⊩ U0 :[g]. +#h #g #L #T #IH2 #IH1 #L0 #T0 * -L0 -T0 +[ +| +| +| #a #L0 #V #W #W0 #T0 #V0 #l0 #HV #HT0 #HVW #HW0 #HTV0 #X #l #H #H1 #H2 destruct + elim (ssta_inv_appl1 … H) -H #U0 #HTU0 #H destruct + lapply (IH1 … HT0 U0 ? ?) // [ /3 width=2/ ] -HTU0 #HU0 + @(snv_appl … HV HU0 HVW HW0) -HV -HU0 -HVW -HW0 +| #L0 #W #T0 #W0 #l0 #HW #HT0 #HTW0 #HW0 #X #l #H #H1 #H2 destruct + elim (ssta_inv_cast1 … H) -H (tpr_inv_atom1 … H) -H // | #I #L1 #K1 #V1 #B #i #HLK1 #HK1 #H1 #H2 #L2 #HL12 #T2 #H destruct >(tpr_inv_atom1 … H) -T2 - lapply (ldrop_pair2_fwd_cw … HLK1 (#i)) #HKV1 + lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma index a50580b96..1522d00c0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma @@ -279,5 +279,5 @@ qed. (* Basic_1: was: pr0_confluence *) theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 → ∃∃T. T1 ➡ T & T2 ➡ T. -#T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/ +#T @(tw_ind … T) -T /3 width=6 by tpr_conf_aux/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ypr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ypr.ma deleted file mode 100644 index 72b22ece1..000000000 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ypr.ma +++ /dev/null @@ -1,37 +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/csup.ma". -include "basic_2/reducibility/xpr.ma". - -(* HYPER PARALLEL REDUCTION ON CLOSURES *************************************) - -inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝ -| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2 -| ypr_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2 -| ypr_csup: ∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2 -. - -interpretation - "hyper parallel reduction (closure)" - 'YPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2). - -(* Basic properties *********************************************************) - -lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g). -/2 width=1/ qed. - -lemma xpr_ypr: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •➡[g] T2 → h ⊢ ⦃L, T1⦄ •⥸[g] ⦃L, T2⦄. -#h #g #L #T1 #T2 * /2 width=1/ /2 width=2/ -qed. -- 2.39.2