From: Ferruccio Guidi Date: Thu, 22 Nov 2012 15:05:00 +0000 (+0000) Subject: - local environment refinement for the first recursive lemma on validity preservation X-Git-Tag: make_still_working~1452 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4bea40e6589ce21c15ecf99bdd5bd2a1c62f6809;p=helm.git - local environment refinement for the first recursive lemma on validity preservation - focalized equivalence - some corrections --- diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/fpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/fpc.ma new file mode 100644 index 000000000..f552d5818 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/fpc.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpr.ma". + +(* CONTEXT-FREE PARALLEL CONVERSION ON CLOSURES *****************************) + +definition fpc: bi_relation lenv term ≝ + λL1,T1,L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ ∨ ⦃L2, T2⦄ ➡ ⦃L1, T1⦄. + +interpretation + "context-free parallel conversion (closure)" + 'FocalizedPConv L1 T1 L2 T2 = (fpc L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma fpc_refl: bi_reflexive … fpc. +/2 width=1/ qed. + +lemma fpc_sym: bi_symmetric … fpc. +#L1 #L2 #T1 #T2 * /2 width=1/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma fpc_fwd_fpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌ ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ & ⦃L2, T2⦄ ➡ ⦃L, T⦄. +#L1 #L2 #T1 #T2 * /2 width=4/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/fpc_fpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/fpc_fpc.ma new file mode 100644 index 000000000..22fc16f37 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/fpc_fpc.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/conversion/fpc.ma". + +(* CONTEXT-FREE PARALLEL CONVERSION ON CLOSURES *****************************) + +(* Main properties **********************************************************) + +theorem fpc_conf: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ⬌ ⦃L1, T1⦄ → + ∀L2,T2. ⦃L0, T0⦄ ⬌ ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ⬌ ⦃L, T⦄ & ⦃L2, T2⦄ ⬌ ⦃L, T⦄. +/3 width=4/ 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 2a234c226..2be571525 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma @@ -26,7 +26,7 @@ inductive snv (h:sh) (g:sd h): lenv → predicate term ≝ ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 → ⦃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) + ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T) . interpretation "stratified native validity (term)" @@ -85,17 +85,17 @@ lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] → fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T → ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & - L ⊢ W ⬌* U & ⦃h, L⦄ ⊢ T •[g, l + 1] U. + ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W. #h #g #L #X * -L -X [ #L #k #W #T #H destruct | #I #L #K #V #i #_ #_ #W #T #H destruct | #a #I #L #V #T0 #_ #_ #W #T #H destruct | #a #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #W #T #H destruct -| #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HWU0 #W #T #H destruct /2 width=4/ +| #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HUW0 #W #T #H destruct /2 width=4/ ] qed. lemma snv_inv_cast: ∀h,g,L,W,T. ⦃h, L⦄ ⊩ ⓝW.T :[g] → - ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & - L ⊢ W ⬌* U & ⦃h, L⦄ ⊢ T •[g, l + 1] U. + ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & + ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W. /2 width=3/ qed-. 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 d7f9ec811..3d4761da8 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 @@ -32,11 +32,11 @@ lemma snv_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. 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/ -| #L #W #T #U #l #_ #_ #HTU #HWU * #B #HW * #A #HT - lapply (aaa_cpcs_mono … HWU … HW A ?) -HWU /2 width=7/ -HTU #H destruct /3 width=3/ +| #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT + lapply (aaa_cpcs_mono … HUW A … HW) -HUW /2 width=7/ -HTU #H destruct /3 width=3/ ] qed-. lemma snv_csn: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → L ⊢ ⬊* T. #h #g #L #T #H elim (snv_aaa … H) -H /2 width=2/ -qed. +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma index 67ab751c0..6d79ef571 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma @@ -74,6 +74,6 @@ lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L | #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HTV #HVW - lapply (cpcs_inv_lift … HLK … HVW0 … HVW ?) // -W /3 width=4/ + lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/ ] 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 index bd6b2121d..d96994e6c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_ssta.ma @@ -33,8 +33,8 @@ qed-. fact snv_ssta_conf_aux: ∀h,g,L,T. ( ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → - ∀U0. ⦃h, L0⦄ ⊢ T0 •➡*[g] U0 → - #{L0, T0} < #{L ,T} → ⦃h, L0⦄ ⊩ U0 :[g] + ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 → + #{L0, T0} < #{L, T} → ⦃h, L0⦄ ⊩ U0 :[g] ) → ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 → @@ -45,8 +45,7 @@ fact snv_ssta_conf_aux: ∀h,g,L,T. ( | | #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 + lapply (IH1 … HT0 … HTU0 ?) // #HU0 @(snv_appl … HV HU0 HVW HW0) -HV -HU0 -HVW -HW0 | #L0 #W #T0 #W0 #l0 #_ #HT0 #_ #_ #U0 #l #H #H1 #H2 destruct -W0 - lapply (ssta_inv_cast1 … H) -H #HTU0 - lapply (IH1 … HT0 U0 ? ?) -IH1 -HT0 // -W /3 width=2/ + lapply (ssta_inv_cast1 … H) -H /2 width=5/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma index cf0b9030c..ac9de9300 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma @@ -164,7 +164,6 @@ elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_div, cprs_lsubs_trans/ (**) (* /3 width=5/ is a bit slow *) qed. - (* Basic_1: was: pc3_lift *) lemma cpcs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs.ma new file mode 100644 index 000000000..c0e02359b --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs.ma @@ -0,0 +1,73 @@ +(**************************************************************************) +(* ___ *) +(* ||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/conversion/fpc.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +definition fpcs: bi_relation lenv term ≝ bi_TC … fpc. + +interpretation "context-free parallel equivalence (closure)" + 'FocalizedPConvStar L1 T1 L2 T2 = (fpcs L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma fpcs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 → + (∀L,L2,T,T2. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L, T⦄ ⬌ ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → R L2 T2. +/3 width=7 by bi_TC_star_ind/ qed-. + +lemma fpcs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 → + (∀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. +/3 width=7 by bi_TC_star_ind_dx/ qed-. + +(* Basic properties *********************************************************) + +lemma fpcs_refl: bi_reflexive … fpcs. +/2 width=1/ qed. + +lemma fpcs_sym: bi_symmetric … fpcs. +/3 width=1/ qed. + +lemma fpcs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L, T⦄ ⬌ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/2 width=4/ qed. + +lemma fpcs_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⬌ ⦃L, T⦄ → ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/2 width=4/ qed. + +lemma fpcs_fpr_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=1/ qed. + +lemma fpcs_fpr_sn: ∀L1,L2,T1,T2. ⦃L2, T2⦄ ➡ ⦃L1, T1⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=1/ qed. + +lemma fpcs_fpr_strap1: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → + ∀L2,T2. ⦃L, T⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed. + +lemma fpcs_fpr_strap2: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → + ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed. + +lemma fpcs_fpr_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → + ∀L2,T2. ⦃L2, T2⦄ ➡ ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed. + +lemma fpr_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡ ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed-. + +lemma fpcs_fpr_conf: ∀L1,L,T1,T. ⦃L, T⦄ ➡ ⦃L1, T1⦄ → + ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_aaa.ma new file mode 100644 index 000000000..9f4327bff --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_aaa.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fprs_aaa.ma". +include "basic_2/equivalence/fpcs_fpcs.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +(* Main properties about atomic arity assignment on terms *******************) + +theorem aaa_fpcs_mono: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → + ∀A1. L1 ⊢ T1 ⁝ A1 → ∀A2. L2 ⊢ T2 ⁝ A2 → + A1 = A2. +#L1 #L2 #T1 #T2 #H12 #A1 #HT1 #A2 #HT2 +elim (fpcs_inv_fprs … H12) -H12 #L #T #H1 #H2 +lapply (aaa_fprs_conf … HT1 … H1) -L1 -T1 #HT1 +lapply (aaa_fprs_conf … HT2 … H2) -L2 -T2 #HT2 +lapply (aaa_mono … HT1 … HT2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_cpcs.ma new file mode 100644 index 000000000..4b51a7084 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_cpcs.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fprs_cprs.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/equivalence/fpcs_fprs.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +(* Properties on context-sensitive parallel equivalence for terms ***********) + +lemma cpcs_fpcs: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → ⦃L, T1⦄ ⬌* ⦃L, T2⦄. +#L #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H /3 width=4 by fprs_div, cprs_fprs/ (**) (* too slow without trace *) +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fpcs.ma new file mode 100644 index 000000000..270e8dc40 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fpcs.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fprs_fprs.ma". +include "basic_2/conversion/fpc_fpc.ma". +include "basic_2/equivalence/fpcs_fprs.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +(* Advanced inversion lemmas ************************************************) + +lemma fpcs_inv_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ & ⦃L2, T2⦄ ➡* ⦃L, T⦄. +#L1 #L2 #T1 #T2 #H @(fpcs_ind … H) -L2 -T2 +[ /3 width=4/ +| #L #L2 #T #T2 #_ #HT2 * #L0 #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 + [ elim (fprs_strip … HT2 … HT0) -L -T #L #T #HT2 #HT0 + lapply (fprs_strap1 … HT10 … HT0) -L0 -T0 /2 width=4/ + | lapply (fprs_strap2 … HT2 … HT0) -L -T /2 width=4/ + ] +] +qed-. + +(* Advanced properties ******************************************************) + +lemma fpr_fprs_conf: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L #L1 #L2 #T #T1 #T2 #HT1 #HT2 +elim (fprs_strip … HT2 … HT1) /2 width=4 by fpr_fprs_div/ +qed-. + +lemma fprs_fpr_conf: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → ⦃L2, T2⦄ ⬌* ⦃L1, T1⦄. +#L #L1 #L2 #T #T1 #T2 #HT1 #HT2 +elim (fprs_strip … HT2 … HT1) /2 width=4 by fprs_fpr_div/ +qed-. + +lemma fprs_conf: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L #L1 #L2 #T #T1 #T2 #HT1 #HT2 +elim (fprs_conf … HT1 … HT2) /2 width=4/ +qed-. + +lemma fpcs_strip: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ⬌ ⦃L1, T1⦄ → + ∀L2,T2. ⦃L0, T0⦄ ⬌* ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ & ⦃L2, T2⦄ ⬌ ⦃L, T⦄. +/3 width=4/ qed. + +(* Main properties **********************************************************) + +theorem fpcs_trans: bi_transitive … fpcs. +/2 width=4/ qed. + +theorem fpcs_canc_sn: ∀L,L1,L2,T,T1,T2. ⦃L, T⦄ ⬌* ⦃L1, T1⦄ → ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4 by fpcs_trans, fpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) + +theorem fpcs_canc_dx: ∀L1,L2,L,T1,T2,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ⦃L2, T2⦄ ⬌* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4 by fpcs_trans, fpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fprs.ma new file mode 100644 index 000000000..1d3f71f9e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/fpcs_fprs.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/computation/fprs.ma". +include "basic_2/equivalence/fpcs.ma". + +(* CONTEXT-FREE PARALLEL EQUIVALENCE ON CLOSURES ****************************) + +(* Properties on context-free parallel computation for closures *************) + +(* Note: lemma 1000 *) +lemma fpcs_fprs_dx: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /width=1/ /3 width=4/ +qed. + +lemma fpcs_fprs_sn: ∀L1,L2,T1,T2. ⦃L2, T2⦄ ➡* ⦃L1, T1⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L2 #T1 #T2 #H @(fprs_ind_dx … H) -L2 -T2 /width=1/ /3 width=4/ +qed. + +lemma fpcs_fprs_strap1: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ∀L2,T2. ⦃L, T⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #HT1 #L2 #T2 #H @(fprs_ind … H) -L2 -T2 /width=1/ /2 width=4/ +qed. + +lemma fpcs_fprs_strap2: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #H #L2 #T2 #HT2 @(fprs_ind_dx … H) -L1 -T1 /width=1/ /2 width=4/ +qed. + +lemma fpcs_fprs_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ⬌* ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #HT1 #L2 #T2 #H @(fprs_ind_dx … H) -L2 -T2 /width=1/ /2 width=4/ +qed. + +lemma fpcs_fprs_conf: ∀L1,L,T1,T. ⦃L, T⦄ ➡* ⦃L1, T1⦄ → ∀L2,T2. ⦃L, T⦄ ⬌* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #H #T2 #HT2 @(fprs_ind … H) -L1 -T1 /width=1/ /3 width=4 by fpcs_fpr_conf/ (**) (* /2 width=4/ does not work *) +qed. + +lemma fprs_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +#L1 #L #T1 #T #HT1 #T2 #L2 #H @(fprs_ind_dx … H) -L2 -T2 /2 width=1/ /2 width=4/ +qed. + +lemma fprs_fpr_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡ ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=7 by bi_step, fprs_div/ qed-. + +lemma fpr_fprs_div: ∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ∀L2,T2. ⦃L2, T2⦄ ➡* ⦃L, T⦄ → ⦃L1, T1⦄ ⬌* ⦃L2, T2⦄. +/3 width=4 by bi_step, fprs_div/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse.ma new file mode 100644 index 000000000..6719c7afe --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse.ma @@ -0,0 +1,114 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cprs.ma". +include "basic_2/equivalence/cpcs.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR CONTEXT-SENSITIVE PARALLEL EQUIVALENCE **) + +(* Note: this is not transitive *) +inductive lsubse (h:sh) (g:sd h): relation lenv ≝ +| lsubse_atom: lsubse h g (⋆) (⋆) +| lsubse_pair: ∀I,L1,L2,V. lsubse h g L1 L2 → + lsubse h g (L1. ⓑ{I} V) (L2. ⓑ{I} V) +| lsubse_abbr: ∀L1,L2,V1,V2,W1,W2,l. L1 ⊢ W1 ⬌* W2 → + ⦃h, L1⦄ ⊢ V1 •[g, l + 1] W1 → ⦃h, L2⦄ ⊢ W2 •[g, l] V2 → + lsubse h g L1 L2 → lsubse h g (L1. ⓓV1) (L2. ⓛW2) +. + +interpretation + "local environment refinement (context-sensitive parallel equivalence)" + 'CrSubEqSE h g L1 L2 = (lsubse h g L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact lsubse_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → L1 = ⋆ → L2 = ⋆. +#h #g #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #H destruct +] +qed-. + +lemma lsubse_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ⊢•⊑[g] L2 → L2 = ⋆. +/2 width=5 by lsubse_inv_atom1_aux/ qed-. + +fact lsubse_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → + ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + (∃∃K2. h ⊢ K1 ⊢•⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ + ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + K1 ⊢ W1 ⬌* W2 & h ⊢ K1 ⊢•⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. +#h #g #L1 #L2 * -L1 -L2 +[ #J #K1 #U1 #H destruct +| #I #L1 #L2 #V #HL12 #J #K1 #U1 #H destruct /3 width=3/ +| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #HL12 #J #K1 #U1 #H destruct /3 width=10/ +] +qed-. + +lemma lsubse_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ⊢•⊑[g] L2 → + (∃∃K2. h ⊢ K1 ⊢•⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ + ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + K1 ⊢ W1 ⬌* W2 & h ⊢ K1 ⊢•⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. +/2 width=3 by lsubse_inv_pair1_aux/ qed-. + +fact lsubse_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → L2 = ⋆ → L1 = ⋆. +#h #g #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #H destruct +] +qed-. + +lemma lsubse_inv_atom2: ∀h,g,L1. h ⊢ L1 ⊢•⊑[g] ⋆ → L1 = ⋆. +/2 width=5 by lsubse_inv_atom2_aux/ qed-. + +fact lsubse_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → + ∀I,K2,W2. L2 = K2. ⓑ{I} W2 → + (∃∃K1. h ⊢ K1 ⊢•⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ + ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + K1 ⊢ W1 ⬌* W2 & h ⊢ K1 ⊢•⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. +#h #g #L1 #L2 * -L1 -L2 +[ #J #K2 #U2 #H destruct +| #I #L1 #L2 #V #HL12 #J #K2 #U2 #H destruct /3 width=3/ +| #L1 #L2 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #HL12 #J #K2 #U2 #H destruct /3 width=10/ +] +qed-. + +lemma lsubse_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ⊢•⊑[g] K2. ⓑ{I} W2 → + (∃∃K1. h ⊢ K1 ⊢•⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ + ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + K1 ⊢ W1 ⬌* W2 & h ⊢ K1 ⊢•⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. +/2 width=3 by lsubse_inv_pair2_aux/ qed-. + +(* Basic_forward lemmas *****************************************************) + +lemma lsubse_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → L1 ≼[0, |L1|] L2. +#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +qed-. + +lemma lsubse_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → L1 ≼[0, |L2|] L2. +#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +qed-. + +(* Basic properties *********************************************************) + +lemma lsubse_refl: ∀h,g,L. h ⊢ L ⊢•⊑[g] L. +#h #g #L elim L -L // /2 width=1/ +qed. + +lemma lsubse_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → + ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. +/3 width=5 by lsubse_fwd_lsubs2, cprs_lsubs_trans/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_cpcs.ma new file mode 100644 index 000000000..2cc3ce076 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_cpcs.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/equivalence/cpcs_cpcs.ma". +include "basic_2/equivalence/lsubse.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR CONTEXT-SENSITIVE PARALLEL EQUIVALENCE **) + +(* Properties on context-sensitive parallel equivalence for terms ***********) + +lemma lsubse_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → + ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2. +/3 width=5 by lsubse_fwd_lsubs2, cpcs_lsubs_trans/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ldrop.ma new file mode 100644 index 000000000..729f4b61f --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ldrop.ma @@ -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/equivalence/lsubse.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR CONTEXT-SENSITIVE PARALLEL EQUIVALENCE **) + +(* Properties concerning basic local environment slicing ********************) + +(* Note: the constant 0 cannot be generalized *) +lemma lsubse_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → + ∀K1,e. ⇩[0, e] L1 ≡ K1 → + ∃∃K2. h ⊢ K1 ⊢•⊑[g] K2 & ⇩[0, e] L2 ≡ K2. +#h #g #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 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #_ #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=6/ + | elim (IHL12 … HLK1) -L1 /3 width=3/ + ] +] +qed-. + +(* Note: the constant 0 cannot be generalized *) +lemma lsubse_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ⊢•⊑[g] L2 → + ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. h ⊢ K1 ⊢•⊑[g] K2 & ⇩[0, e] L1 ≡ K1. +#h #g #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 #V1 #V2 #W1 #W2 #l #HW12 #HVW1 #HWV2 #_ #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=6/ + | elim (IHL12 … HLK2) -L2 /3 width=3/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ssta.ma new file mode 100644 index 000000000..b5dc3f5ac --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lsubse_ssta.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lsubss.ma". +*) +include "basic_2/equivalence/lsubse.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR CONTEXT-SENSITIVE PARALLEL EQUIVALENCE **) + +(* Properties on stratified native type assignment **************************) + +axiom lsubse_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g,l] U2 → + ∀L1. h ⊢ L1 ⊢•⊑[g] L2 → + ∃∃U1. ⦃h, L1⦄ ⊢ T •[g,l] U1 & L1 ⊢ U1 ⬌* U2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv.etc new file mode 100644 index 000000000..25122262a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv.etc @@ -0,0 +1,112 @@ +(**************************************************************************) +(* ___ *) +(* ||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/snv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Note: this is not transitive *) +inductive lsubsv (h:sh) (g:sd h): relation lenv ≝ +| lsubsv_atom: lsubsv h g (⋆) (⋆) +| lsubsv_pair: ∀I,L1,L2,V. lsubsv h g L1 L2 → + lsubsv h g (L1. ⓑ{I} V) (L2. ⓑ{I} V) +| lsubsv_abbr: ∀L1,L2,V1,V2,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → L1 ⊢ W2 ⬌* W1 → + ⦃h, L1⦄ ⊢ V1 •[g, l + 1] W1 → ⦃h, L2⦄ ⊢ W2 •[g, l] V2 → + lsubsv h g L1 L2 → lsubsv h g (L1. ⓓV1) (L2. ⓛW2) +. + +interpretation + "local environment refinement (stratified native validity)" + 'CrSubEqV h g L1 L2 = (lsubsv h g L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 = ⋆ → L2 = ⋆. +#h #g #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct +] +qed-. + +lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ⊩:⊑[g] L2 → L2 = ⋆. +/2 width=5 by lsubsv_inv_atom1_aux/ qed-. + +fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → + ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ + ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. +#h #g #L1 #L2 * -L1 -L2 +[ #J #K1 #U1 #H destruct +| #I #L1 #L2 #V #HL12 #J #K1 #U1 #H destruct /3 width=3/ +| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HW21 #HVW1 #HWV2 #HL12 #J #K1 #U1 #H destruct /3 width=10/ +] +qed-. + +lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ⊩:⊑[g] L2 → + (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ + ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. +/2 width=3 by lsubsv_inv_pair1_aux/ qed-. + +fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L2 = ⋆ → L1 = ⋆. +#h #g #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct +] +qed-. + +lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ⊩:⊑[g] ⋆ → L1 = ⋆. +/2 width=5 by lsubsv_inv_atom2_aux/ qed-. + +fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → + ∀I,K2,W2. L2 = K2. ⓑ{I} W2 → + (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ + ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. +#h #g #L1 #L2 * -L1 -L2 +[ #J #K2 #U2 #H destruct +| #I #L1 #L2 #V #HL12 #J #K2 #U2 #H destruct /3 width=3/ +| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV #HW21 #HVW1 #HWV2 #HL12 #J #K2 #U2 #H destruct /3 width=11/ +] +qed-. + +lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ⊩:⊑[g] K2. ⓑ{I} W2 → + (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ + ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. +/2 width=3 by lsubsv_inv_pair2_aux/ qed-. + +(* Basic_forward lemmas *****************************************************) + +lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L1|] L2. +#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +qed-. + +lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L2|] L2. +#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +qed-. + +(* Basic properties *********************************************************) + +lemma lsubsv_refl: ∀h,g,L. h ⊢ L ⊩:⊑[g] L. +#h #g #L elim L -L // /2 width=1/ +qed. + +lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → + ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. +/3 width=5 by lsubsv_fwd_lsubs2, cprs_lsubs_trans/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_cpcs.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_cpcs.etc new file mode 100644 index 000000000..87a72e0fd --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_cpcs.etc @@ -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/equivalence/cpcs_cpcs.ma". +include "basic_2/dynamic/lsubsv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Properties on context-sensitive parallel equivalence for terms ***********) + +lemma lsubsv_cpcs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → + ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2. +/3 width=5 by lsubsv_fwd_lsubs2, cpcs_lsubs_trans/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ldrop.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ldrop.etc new file mode 100644 index 000000000..2c3381f86 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ldrop.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/lsubsv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Properties concerning basic local environment slicing ********************) + +(* Note: the constant 0 cannot be generalized *) +lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → + ∀K1,e. ⇩[0, e] L1 ≡ K1 → + ∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L2 ≡ K2. +#h #g #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 #V1 #V2 #W1 #W2 #l #HV1 #HW21 #HVW1 #HWV2 #_ #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=6/ + | elim (IHL12 … HLK1) -L1 /3 width=3/ + ] +] +qed. + +(* Note: the constant 0 cannot be generalized *) +lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → + ∀K2,e. ⇩[0, e] L2 ≡ K2 → + ∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & ⇩[0, e] L1 ≡ K1. +#h #g #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 #V1 #V2 #W1 #W2 #l #HV #HW21 #HVW1 #HWV2 #_ #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=6/ + | elim (IHL12 … HLK2) -L2 /3 width=3/ + ] +] +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_snv.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_snv.etc new file mode 100644 index 000000000..e5bd9951e --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_snv.etc @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lsubsv_ldrop.ma". +include "basic_2/dynamic/lsubsv_ssta.ma". +include "basic_2/dynamic/lsubsv_cpcs.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Properties concerning stratified native validity *************************) + +axiom lsubsv_xprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → + ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡*[g] T2. +(* +/3 width=3 by lsubsv_fwd_lsubss, lsubss_xprs_trans/ qed-. +*) +axiom lsubsv_snv_trans: ∀h,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] → + ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g]. +(* +#h #g #L2 #T #H elim H -L2 -T // +[ #I2 #L2 #K2 #V2 #i #HLK2 #_ #IHV2 #L1 #HL12 + elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 + elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -IHV2 ] + [ #HK12 #H destruct /3 width=5/ + | #V1 #l #HV1 #_ #_ #_ #H destruct /2 width=5/ + ] +| #a #I #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 /4 width=1/ +| #a #L2 #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU #IHV #IHT #L1 #HL12 + lapply (IHV … HL12) -IHV #HV + lapply (IHT … HL12) -IHT #HT + lapply (lsubsv_ssta_trans … HVW … HL12) -HVW #HVW + lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0 + lapply (lsubsv_xprs_trans … HL12 … HTU) -HL12 -HTU /2 width=8/ +| #L2 #W #T #U #l #_ #_ #HTU #HWU #IHW #IHT #L1 #HL12 + lapply (IHW … HL12) -IHW #HW + lapply (IHT … HL12) -IHT #HT + lapply (lsubsv_ssta_trans … HTU … HL12) -HTU #HTU + lapply (lsubsv_cpcs_trans … HL12 … HWU) -HL12 -HWU /2 width=4/ +] +qed-. +*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ssta.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ssta.etc new file mode 100644 index 000000000..1e5b5fddd --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/lsubsv/lsubsv_ssta.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lsubss.ma". +include "basic_2/dynamic/lsubsv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Properties on stratified native type assignment **************************) + +axiom lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g,l] U2 → + ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → + ∃∃U1. L1 ⊢ U2 ⬌* U1 & ⦃h, L1⦄ ⊢ T •[g,l] U1. diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index bba14af32..eb59a9d8f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -430,6 +430,10 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )" non associative with precedence 45 for @{ 'PConvStar $L $T1 $T2 }. +notation "hvbox( h ⊢ break term 46 L1 ⊢ • ⊑ [ g ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'CrSubEqSE $h $g $L1 $L2 }. + notation "hvbox( ⦃ L1 ⦄ ⬌ * break ⦃ L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConvStar $L1 $L2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma index 4b716c342..b45dbb99e 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_aaa.ma @@ -55,12 +55,12 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T elim (aaa_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct 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/ + lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 [2,4: // |3,5: skip ] /2 width=1/ -T0 -L1 -V1 /4 width=7/ | #a #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct elim (aaa_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 + lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 [2,4: // |3,5: skip ] /2 width=1/ -V1 -T0 -L1 -W0 #HT2 @(aaa_abbr … HW2) -HW2 @(aaa_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *) ] diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml index edf66e433..c6a00c160 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml @@ -33,9 +33,9 @@ 5 4 5 5 6 4 + 6 5 6 6 6 7 - 7 4 7 7 3 4 diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma index 9da161d42..ac4c8f9f7 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma @@ -168,6 +168,14 @@ inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Pro interpretation "multiple existental quantifier (6, 4)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5). +(* multiple existental quantifier (6, 5) *) + +inductive ex6_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex6_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → ex6_5 ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (6, 5)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5). + (* multiple existental quantifier (6, 6) *) inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ @@ -184,14 +192,6 @@ inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2 interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple existental quantifier (7, 4) *) - -inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝ - | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). - (* multiple existental quantifier (7, 7) *) inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma index 9e2f4d099..6f614f2e5 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma @@ -204,6 +204,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) }. +(* multiple existental quantifier (6, 5) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) }. + (* multiple existental quantifier (6, 6) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" @@ -224,16 +234,6 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. -(* multiple existental quantifier (7, 4) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }. - (* multiple existental quantifier (7, 7) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"