From f7386d0b74f935f07ede4be46d0489a233d68b85 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 29 Oct 2012 18:28:47 +0000 Subject: [PATCH] - we set up the support for the "bt-reduction" of Automath literature - we now use the STIX GENERAL fonts for a better rendering of U+2B43 --- .../lambda_delta/basic_2/computation/xprs.ma | 18 +++--- .../basic_2/computation/xprs_aaa.ma | 2 +- .../basic_2/computation/xprs_cprs.ma | 5 +- .../basic_2/computation/xprs_lift.ma | 16 +++--- .../basic_2/computation/xprs_xprs.ma | 20 +++++++ .../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.ma | 6 +- .../lambda_delta/basic_2/dynamic/snv_aaa.ma | 3 +- .../contribs/lambda_delta/basic_2/notation.ma | 26 ++++++++- .../lambda_delta/basic_2/reducibility/xpr.ma | 14 ++--- .../basic_2/reducibility/xpr_aaa.ma | 4 +- .../basic_2/reducibility/xpr_lift.ma | 16 +++--- .../lambda_delta/basic_2/reducibility/ypr.ma | 37 ++++++++++++ .../lambda_delta/basic_2/static/ssta.ma | 20 +++++++ .../lambda_delta/basic_2/substitution/csup.ma | 35 ++++++++++++ .../lambda_delta/basic_2/unfold/csups.ma | 57 +++++++++++++++++++ .../basic_2/unfold/csups_csups.ma | 22 +++++++ 22 files changed, 444 insertions(+), 49 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/xprs_xprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/yprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/yprs_csups.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/yprs_xprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/yprs_yprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/ysteps.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/ysteps_csups.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/ypr.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/substitution/csup.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/csups.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/unfold/csups_csups.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma index c07de4dfd..34e93db9d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs.ma @@ -27,31 +27,31 @@ interpretation "extended parallel computation (term)" (* Basic eliminators ********************************************************) lemma xprs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 → - (∀T,T2. ⦃h, L⦄ ⊢ T1 ➸*[g] T → ⦃h, L⦄ ⊢ T ➸[g] T2 → R T → R T2) → - ∀T2. ⦃h, L⦄ ⊢ T1 ➸*[g] T2 → R T2. + (∀T,T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T → ⦃h, L⦄ ⊢ T •➡[g] T2 → R T → R T2) → + ∀T2. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 → R T2. #h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) // qed-. lemma xprs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 → - (∀T1,T. ⦃h, L⦄ ⊢ T1 ➸[g] T → ⦃h, L⦄ ⊢ T ➸*[g] T2 → R T → R T1) → - ∀T1. ⦃h, L⦄ ⊢ T1 ➸*[g] T2 → R T1. + (∀T1,T. ⦃h, L⦄ ⊢ T1 •➡[g] T → ⦃h, L⦄ ⊢ T •➡*[g] T2 → R T → R T1) → + ∀T1. ⦃h, L⦄ ⊢ T1 •➡*[g] T2 → R T1. #h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12 @(TC_star_ind_dx … HT2 IHT2 … HT12) // qed-. (* Basic properties *********************************************************) -lemma xprs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸*[g] T. +lemma xprs_refl: ∀h,g,L. reflexive … (xprs h g L). /2 width=1/ qed. lemma xprs_strap1: ∀h,g,L,T1,T,T2. - ⦃h, L⦄ ⊢ T1 ➸*[g] T → ⦃h, L⦄ ⊢ T ➸[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2. -/2 width=3 by step/ qed. (**) (* NTypeChecker failure without trace *) + ⦃h, L⦄ ⊢ T1 •➡*[g] T → ⦃h, L⦄ ⊢ T •➡[g] T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2. +/2 width=3/ qed. lemma xprs_strap2: ∀h,g,L,T1,T,T2. - ⦃h, L⦄ ⊢ T1 ➸[g] T → ⦃h, L⦄ ⊢ T ➸*[g] T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2. -/2 width=3 by TC_strap/ qed. (**) (* NTypeChecker failure without trace *) + ⦃h, L⦄ ⊢ T1 •➡[g] T → ⦃h, L⦄ ⊢ T •➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2. +/2 width=3/ qed. (* Basic inversion lemmas ***************************************************) (* diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma index 2de7cbcd8..5beb8fe19 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_aaa.ma @@ -19,6 +19,6 @@ include "basic_2/computation/xprs.ma". (* Properties on atomic arity assignment for terms **************************) -lemma xprs_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T ➸*[g] U → L ⊢ U ⁝ A. +lemma xprs_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •➡*[g] U → L ⊢ U ⁝ A. #h #g #L #T #A #HT #U #H @(xprs_ind … H) -U // /2 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma index 0d2e22c58..13a4f8889 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_cprs.ma @@ -19,7 +19,6 @@ include "basic_2/computation/xprs.ma". (* properties on context sensitive parallel computation for terms ***********) -lemma cprs_xprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➸*[g] T2. -#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // -/3 width=3 by xprs_strap1, cpr_xpr/ (**) (* NTypeChecker failure without trace *) +lemma cprs_xprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 •➡*[g] T2. +#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma index 54bdc487a..cb151a194 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_lift.ma @@ -20,7 +20,7 @@ include "basic_2/computation/xprs.ma". (* Advanced forward lemmas **************************************************) -lemma xprs_fwd_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 ➸*[g] U2 → +lemma xprs_fwd_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 •➡*[g] U2 → ∃∃V2,T2. L ⊢ V1 ➡* V2 & U2 = ⓛ{a}V2. T2. #h #g #a #L #V1 #T1 #U2 #H @(xprs_ind … H) -U2 /2 width=4/ #U #U2 #_ #HU2 * #V #T #HV1 #H destruct @@ -30,23 +30,21 @@ qed-. (* Relocation properties ****************************************************) lemma xprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → - ∀h,g,T2. ⦃h, K⦄ ⊢ T1 ➸*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 → - ⦃h, L⦄ ⊢ U1 ➸*[g] U2. + ∀h,g,T2. ⦃h, K⦄ ⊢ T1 •➡*[g] T2 → ∀U2. ⇧[d, e] T2 ≡ U2 → + ⦃h, L⦄ ⊢ U1 •➡*[g] U2. #L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #T2 #HT12 @(xprs_ind … HT12) -T2 [ -HLK #T2 #HT12 <(lift_mono … HTU1 … HT12) -T1 // | -HTU1 #T #T2 #_ #HT2 #IHT2 #U2 #HTU2 elim (lift_total T d e) #U #HTU - lapply (xpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK (* /3 width=3/ *) - #H @(step …H) /2 width=1/ (**) (* NTypeChecker failure *) + lapply (xpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK /3 width=3/ ] qed. lemma xprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → - ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 ➸*[g] U2 → - ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 ➸*[g] T2. + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 •➡*[g] U2 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •➡*[g] T2. #L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 #HU12 @(xprs_ind … HU12) -U2 /2 width=3/ -HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1 -elim (xpr_inv_lift1 … HLK … HTU … HU2) -U -HLK (* /3 width=5/ *) -#U #HU2 #HTU @(ex2_1_intro … HU2) @(step … HT1 HTU) (**) (* NTypeChecker failure *) +elim (xpr_inv_lift1 … HLK … HTU … HU2) -U -HLK /3 width=5/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_xprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_xprs.ma new file mode 100644 index 000000000..9593f0550 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/xprs_xprs.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". + +(* EXTENDED PARALLEL COMPUTATION ON TERMS ***********************************) + +theorem xprs_trans: ∀h,g,L. transitive … (xprs h g L). +/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/yprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/yprs.ma new file mode 100644 index 000000000..9ad7e53c4 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/yprs.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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 new file mode 100644 index 000000000..08c939d8d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_csups.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 new file mode 100644 index 000000000..2feb88a2f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_xprs.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 new file mode 100644 index 000000000..d737dd817 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/yprs_yprs.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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 new file mode 100644 index 000000000..a6114c3b1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ysteps.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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 new file mode 100644 index 000000000..2e48f396d --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ysteps_csups.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma index 223dba7ee..2a234c226 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma @@ -24,7 +24,7 @@ inductive snv (h:sh) (g:sd h): lenv → predicate term ≝ | snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T) | snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T → ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 → - ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T) + ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T) | snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T → ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ W ⬌* U → snv h g L (ⓝW.T) . @@ -67,7 +67,7 @@ lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{a,I}V.T :[g] → fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T → ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & - ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U. + ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U. #h #g #L #X * -L -X [ #L #k #V #T #H destruct | #I #L #K #V0 #i #_ #_ #V #T #H destruct @@ -80,7 +80,7 @@ qed. lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] → ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & - ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U. + ⦃h, L⦄ ⊢ T •➡*[g] ⓛ{a}W0.U. /2 width=3/ qed-. fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T → diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma index fdef6d003..d7f9ec811 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma @@ -28,8 +28,7 @@ lemma snv_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. | #I #L #K #V #i #HLK #_ * /3 width=6/ | #a * #L #V #T #_ #_ * #B #HV * #A #HA /3 width=2/ | #a #L #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU * #B #HV * #X #HT - lapply (xprs_aaa h g … HV W0 ?) - [ /3 width=3 by xprs_strap2, ssta_xpr, cprs_xprs/ ] -W #HW0 (**) (* NTypeChecker failure without trace *) + lapply (xprs_aaa h g … HV W0 ?) [ /3 width=3/ ] -W #HW0 lapply (xprs_aaa … HT … HTU) -HTU #H elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 78838bc9d..f53dcf867 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -162,6 +162,10 @@ notation "hvbox( ⇩ [ d , break e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDrop $d $e $L1 $L2 }. +notation "hvbox( ⦃ L1, break T1 ⦄ > break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'SupTerm $L1 $T1 $L2 $T2 }. + notation "hvbox( L ⊢ break ⌘ ⦃ T ⦄ ≡ break term 46 k )" non associative with precedence 45 for @{ 'ICM $L $T $k }. @@ -188,6 +192,10 @@ notation "hvbox( ⇩ * [ e ] break term 46 L1 ≡ break term 46 L2 )" non associative with precedence 45 for @{ 'RDropStar $e $L1 $L2 }. +notation "hvbox( ⦃ L1, break T1 ⦄ > * break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'SupTermStar $L1 $T1 $L2 $T2 }. + notation "hvbox( T1 break ▶ * [ d , break e ] break term 46 T2 )" non associative with precedence 45 for @{ 'PSubstStar $T1 $d $e $T2 }. @@ -328,10 +336,14 @@ notation "hvbox( ⦃ L1 ⦄ ➡ ➡ break ⦃ L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedAlt $L1 $L2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 ➸ break [ g ] 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 @{ 'XPRed $h $g $L $T1 $T2 }. +notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ break [ g ] break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'YPRed $h $g $L1 $T1 $L2 $T2 }. + (* Computation **************************************************************) notation "hvbox( T1 ➡ * break term 46 T2 )" @@ -386,14 +398,22 @@ 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 )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • ➡ * break [ g ] break term 46 T2 )" non associative with precedence 45 for @{ 'XPRedStar $h $g $L $T1 $T2 }. -notation "hvbox( ⦃ h , break L ⦄ ⊢ ➷ * break [ g ] break term 46 T2 )" +notation "hvbox( ⦃ h , break L ⦄ ⊢ • ⬊ * break [ g ] break term 46 T2 )" non associative with precedence 45 for @{ 'XSN $h $g $L $T }. +notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⥸ * break [ g ] break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'YPRedStar $h $g $L1 $T1 $L2 $T2 }. + +notation "hvbox( h ⊢ break ⦃ L1, break T1 ⦄ • ⭃ * break [ g ] break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'YPRedStepStar $h $g $L1 $T1 $L2 $T2 }. + (* Conversion ***************************************************************) notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma index 78dd4502a..7375349ef 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr.ma @@ -17,8 +17,10 @@ include "basic_2/reducibility/cpr.ma". (* EXTENDED PARALLEL REDUCTION ON TERMS *************************************) -definition xpr: ∀h. sd h → lenv → relation term ≝ - λh,g,L,T1,T2. L ⊢ T1 ➡ T2 ∨ ∃l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2. +inductive xpr (h) (g) (L) (T1) (T2): Prop ≝ +| xpr_cpr : L ⊢ T1 ➡ T2 → xpr h g L T1 T2 +| xpr_ssta: ∀l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → xpr h g L T1 T2 +. interpretation "extended parallel reduction (term)" @@ -26,11 +28,5 @@ interpretation (* Basic properties *********************************************************) -lemma cpr_xpr: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2. -/2 width=1/ qed. - -lemma ssta_xpr: ∀h,g,L,T1,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l + 1] T2 → ⦃h, L⦄ ⊢ T1 ➸[g] T2. -/3 width=2/ qed. - -lemma xpr_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➸[g] T. +lemma xpr_refl: ∀h,g,L. reflexive … (xpr h g L). /2 width=1/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma index bce096e3b..98fe01347 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_aaa.ma @@ -20,6 +20,6 @@ include "basic_2/reducibility/xpr.ma". (* Properties on atomic arity assignment for terms **************************) -lemma xpr_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T ➸[g] U → L ⊢ U ⁝ A. -#h #g #L #T #A #HT #U * [2: * ] /2 width=3/ /2 width=6/ +lemma xpr_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •➡[g] U → L ⊢ U ⁝ A. +#h #g #L #T #A #HT #U * /2 width=3/ /2 width=6/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma index 1f2bdb130..8f5deca51 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/xpr_lift.ma @@ -20,12 +20,12 @@ include "basic_2/reducibility/xpr.ma". (* Advanced inversion lemmas ************************************************) -lemma xpr_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 ➸[g] U2 → - ∃∃V2,T2. L ⊢ V1 ➡ V2 & ⦃h, L. ⓛV1⦄ ⊢ T1 ➸[g] T2 & +lemma xpr_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 •➡[g] U2 → + ∃∃V2,T2. L ⊢ V1 ➡ V2 & ⦃h, L. ⓛV1⦄ ⊢ T1 •➡[g] T2 & U2 = ⓛ{a}V2. T2. #h #g #a #L #V1 #T1 #U2 * [ #H elim (cpr_inv_abst1 … H Abst V1) /3 width=5/ -| * #l #H elim (ssta_inv_bind1 … H) /3 width=5/ +| #l #H elim (ssta_inv_bind1 … H) /3 width=5/ ] qed-. @@ -33,15 +33,15 @@ qed-. lemma xpr_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → - ∀h,g. ⦃h, K⦄ ⊢ T1 ➸[g] T2 → ⦃h, L⦄ ⊢ U1 ➸[g] U2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #h #g * [2: * ] + ∀h,g. ⦃h, K⦄ ⊢ T1 •➡[g] T2 → ⦃h, L⦄ ⊢ U1 •➡[g] U2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #h #g * /3 width=9/ /3 width=10/ qed. lemma xpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → - ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 ➸[g] U2 → - ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 ➸[g] T2. -#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * [ #HU12 | * #l #HU12 ] + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀h,g,U2. ⦃h, L⦄ ⊢ U1 •➡[g] U2 → + ∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •➡[g] T2. +#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * [ #HU12 | #l #HU12 ] [ elim (cpr_inv_lift1 … HLK … HTU1 … HU12) -L -U1 /3 width=3/ | elim (ssta_inv_lift1 … HU12 … HLK … HTU1) -L -U1 /3 width=4/ ] diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ypr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ypr.ma new file mode 100644 index 000000000..72b22ece1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ypr.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma index 80147fad3..ec990f13b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/ssta.ma @@ -132,3 +132,23 @@ lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X •[g, l] U → ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y •[g, l-1] Z1 & ⦃h, L⦄ ⊢ X •[g, l] Z2 & U = ⓝZ1.Z2. /2 width=4/ qed-. + +(* Advanced inversion lemmas ************************************************) + +fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → T = U → ⊥. +#h #g #L #T #U #l #H elim H -L -T -U -l +[ #L #k #l #_ #H + lapply (next_lt h k) destruct -H -e0 (**) (* these premises are not erased *) + ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}. +#L1 #L2 #T1 #T2 * -L1 -L2 -T1 -T2 /width=1/ /2 width=4 by ldrop_pair2_fwd_cw/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/csups.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/csups.ma new file mode 100644 index 000000000..56cfa9ee8 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/csups.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/substitution/csup.ma". + +(* ITERATED SUPCLOSURE ******************************************************) + +definition csups: bi_relation lenv term ≝ bi_TC … csup. + +interpretation "iterated structural predecessor (closure)" + 'SupTermStar L1 T1 L2 T2 = (csups L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma csups_ind: ∀L1,T1. ∀R:relation2 lenv term. + (∀L2,T2. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L2 T2) → + (∀L,T,L2,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → R L2 T2. +#L1 #T1 #R #IH1 #IH2 #L2 #T2 #H +@(bi_TC_ind … IH1 IH2 ? ? H) +qed-. + +lemma csups_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. + (∀L1,T1. ⦃L1, T1⦄ > ⦃L2, T2⦄ → R L1 T1) → + (∀L1,L,T1,T. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → R L1 T1. +#L2 #T2 #R #IH1 #IH2 #L1 #T1 #H +@(bi_TC_ind_dx … IH1 IH2 ? ? H) +qed-. + +(* Basic properties *********************************************************) + +lemma csups_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ >* ⦃L, T⦄ → ⦃L, T⦄ > ⦃L2, T2⦄ → + ⦃L1, T1⦄ >* ⦃L2, T2⦄. +/2 width=4/ qed. + +lemma csups_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ > ⦃L, T⦄ → ⦃L, T⦄ >* ⦃L2, T2⦄ → + ⦃L1, T1⦄ >* ⦃L2, T2⦄. +/2 width=4/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma csups_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ >* ⦃L2, T2⦄ → #{L2, T2} < #{L1, T1}. +#L1 #L2 #T1 #T2 #H @(csups_ind … H) -L2 -T2 +/3 width=3 by csup_fwd_cw, transitive_lt/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/csups_csups.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/csups_csups.ma new file mode 100644 index 000000000..1446246c3 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/csups_csups.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +(* ITERATED SUPCLOSURE ******************************************************) + +(* Main propertis ***********************************************************) + +theorem csups_trans: bi_transitive … csups. +/2 width=4/ qed. -- 2.39.2