From: Ferruccio Guidi Date: Thu, 20 Apr 2017 15:19:53 +0000 (+0000) Subject: - notation for the exclusion binder in local envirinments X-Git-Tag: make_still_working~455 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7632da8aa4f6751e351546be3d90fb23f634108c - notation for the exclusion binder in local envirinments - advances on lfsx --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/notation/dxpair2_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/notation/dxpair2_3.etc new file mode 100644 index 000000000..77e894dd6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/notation/dxpair2_3.etc @@ -0,0 +1,3 @@ +notation > "hvbox( L . break ②{ term 46 I } break term 47 T1 )" + non associative with precedence 46 + for @{ 'DxBind2 $L $I $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index a1cb0e0d1..fbf3612a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -44,11 +44,13 @@ F: boolean false T: boolean true a: application -b: binder +b: generic binder with one argument d: abbreviation -f: flat -l: abstraction +f: generic flat with one argument +l: typed abstraction n: native type annotation +u: generic binder with zero argument +x: exclusion NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma index 80ba76465..5f6319bd2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma @@ -15,5 +15,5 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) notation "hvbox( L . break ⓓ T1 )" - left associative with precedence 48 + left associative with precedence 49 for @{ 'DxAbbr $L $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma index 5455e678e..b3d909641 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma @@ -15,5 +15,5 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) notation "hvbox( L . break ⓛ T1 )" - left associative with precedence 49 + left associative with precedence 50 for @{ 'DxAbst $L $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma new file mode 100644 index 000000000..e4f48e77c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L . break ⓤ { term 46 I } )" + non associative with precedence 46 + for @{ 'DxBind1 $L $I }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma index b276334f1..fc371c285 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma @@ -14,10 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation > "hvbox( L . break ②{ term 46 I } break term 47 T1 )" - non associative with precedence 46 - for @{ 'DxBind2 $L $I $T1 }. - notation "hvbox( L . break ⓑ { term 46 I } break term 48 T1 )" non associative with precedence 47 for @{ 'DxBind2 $L $I $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma new file mode 100644 index 000000000..34ad27e9f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L . ⓧ )" + non associative with precedence 48 + for @{ 'DxVoid $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind1_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind1_2.ma new file mode 100644 index 000000000..aaaf81391 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snbind1_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⓤ { term 46 I } . break term 55 L )" + non associative with precedence 55 + for @{ 'SnBind1 $I $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snvoid_1.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snvoid_1.ma new file mode 100644 index 000000000..36522d22b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snvoid_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⓧ . term 55 L )" + non associative with precedence 55 + for @{ 'SnVoid $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma index 9664ec0a3..3d547a49c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma @@ -44,7 +44,7 @@ lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ②{I}V.T] 𝐒⦃L #h #o #I #G #L #V #T #H @(lfsx_ind … H) -L #L1 #_ #IHL1 @lfsx_intro #L2 #H #HnL12 elim (lfpx_pair_sn_split … o I … T H) -H -/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/ +/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/ qed-. (* Basic_2A1: uses: lsx_fwd_flat_dx *) @@ -53,7 +53,7 @@ lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L #h #o #I #G #L #V #T #H @(lfsx_ind … H) -L #L1 #_ #IHL1 @lfsx_intro #L2 #H #HnL12 elim (lfpx_flat_dx_split … o I … V … H) -H -/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_flat_dx/ +/6 width=3 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_flat_dx/ qed-. (* Advanced inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index ea1e66bad..ec9343106 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -30,6 +30,10 @@ lemma lfpx_flat_dx_split: ∀h,o,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L & L ≡[h, o, T] L2. /3 width=5 by lfpx_frees_conf, lfxs_flat_dx_split/ qed-. +lemma lfpx_bind_dx_split: ∀h,o,p,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 → + ∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≡[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V. +/3 width=5 by lfpx_frees_conf, lfxs_bind_dx_split/ qed-. + lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o). #h #o #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/ [ #G #L0 #s0 #X0 #H0 #L1 #HL01 #L2 #HL02 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index 78b1c526b..4cf5505cc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -70,6 +70,25 @@ elim (HR … Hf … H) -HR -Hf -H /4 width=7 by sle_lexs_trans, ex2_intro/ qed-. +lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → + lexs_frees_confluent … R1 cfull → + ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⦻*[R1, T] L2 → ∀p. + ∃∃L,V. L1 ⦻*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⦻*[R2, T] L2 & R1 L1 V1 V. +#R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p +elim (frees_total L1 (ⓑ{p,I}V1.T)) #g #Hg +elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy +lapply(frees_mono … H … Hf) -H #H2 +lapply (tl_eq_repl … H2) -H2 #H2 +lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy +lapply (sor_inv_sle_dx … Hy) -y1 #Hfg +lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg +elim (lexs_sle_split … HR1 HR2 … HL12 … Hfg) -HL12 #Y #H #HL2 +lapply (sle_lexs_trans … H … Hfg) // #H0 +elim (lexs_inv_next1 … H) -H #L #V #HL1 #HV0 #H destruct +elim (HR … Hf … H0) -HR -Hf -H0 +/4 width=7 by sle_lexs_trans, ex3_2_intro, ex2_intro/ +qed-. + (* Main properties **********************************************************) (* Basic_2A1: uses: llpx_sn_bind llpx_sn_bind_O *)