From dc9c7181b2dc66c8d297f708324dcdeea98bc4d8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 30 Nov 2017 13:16:15 +0000 Subject: [PATCH] the previous commit was incomplete :( --- .../basic_2/notation/functions/voidstar_2.ma | 19 ++++++++ .../lambdadelta/basic_2/syntax/voids.ma | 48 +++++++++++++++++++ .../basic_2/syntax/voids_length.ma | 43 +++++++++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 1 + 4 files changed, 111 insertions(+) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/functions/voidstar_2.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/syntax/voids_length.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/voidstar_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/voidstar_2.ma new file mode 100644 index 000000000..4c95b4170 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/voidstar_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 n ] term 46 L )" + non associative with precedence 46 + for @{ 'VoidStar $n $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.ma new file mode 100644 index 000000000..766eefd5c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/voids.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/notation/functions/voidstar_2.ma". +include "basic_2/syntax/lenv.ma". + +(* EXTENSION OF A LOCAL ENVIRONMENT WITH EXCLUSION BINDERS ******************) + +rec definition voids (L:lenv) (n:nat) on n: lenv ≝ match n with +[ O ⇒ L | S m ⇒ (voids L m).ⓧ ]. + +interpretation "extension with exclusion binders (local environment)" + 'VoidStar n L = (voids L n). + +(* Basic properties *********************************************************) + +lemma voids_zero: ∀L. L = ⓧ*[0]L. +// qed. + +lemma voids_succ: ∀L,n. (ⓧ*[n]L).ⓧ = ⓧ*[⫯n]L. +// qed. + +(* Advanced properties ******************************************************) + +lemma voids_next: ∀n,L. ⓧ*[n](L.ⓧ) = ⓧ*[⫯n]L. +#n elim n -n // +qed. + +(* Main inversion properties ************************************************) + +theorem voids_inj: ∀n. injective … (λL. ⓧ*[n]L). +#n elim n -n // +#n #IH #L1 #L2 +length_bind