From 8a47ade5ffd1942f9d16474c547e5050caab3cc8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 16 Mar 2022 22:41:40 +0100 Subject: [PATCH] update in delayed_updating + some additions and corrections --- .../functions/black_downtriangle_2.ma | 19 +++++++++++ .../functions/black_downtriangle_4.ma | 27 +++++++++++++++ .../delayed_updating/syntax/bdd_term.ma | 4 +-- .../delayed_updating/syntax/path_balanced.ma | 2 +- .../syntax/path_structure_inner.ma | 34 +++++++++++++++++++ .../syntax/prototerm_constructors.ma | 2 +- 6 files changed, 84 insertions(+), 4 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_4.ma create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_2.ma new file mode 100644 index 000000000..73cccf605 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_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 DELAYED UPDATING ********************************************) + +notation "hvbox( ▼[ term 46 t1 ] break term 70 t2 )" + non associative with precedence 70 + for @{ 'BlackDownTriangle $t1 $t2 }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_4.ma new file mode 100644 index 000000000..9235b7e10 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_4.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 DELAYED UPDATING ********************************************) + +notation < "hvbox( ▼❨ term 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 70 + for @{ 'BlackDownTriangle $S $k $p $f }. + +notation > "hvbox( ▼❨ term 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 70 + for @{ 'BlackDownTriangle ? $k $p $f }. + +notation > "hvbox( ▼{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )" + non associative with precedence 70 + for @{ 'BlackDownTriangle $S $k $p $f }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma index 8d514e0d7..9cfe28ad9 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma @@ -35,7 +35,7 @@ interpretation "by-depth delayed (prototerm)" 'ClassDPhi = (bdd). -(* +(* COMMENT (* Basic inversions *********************************************************) @@ -213,4 +213,4 @@ lemma bbd_mono_in_root_d: ] ] qed-. -*) \ No newline at end of file +*) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma index 017cfc5ba..c279d2231 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_balanced.ma @@ -17,7 +17,7 @@ include "delayed_updating/notation/functions/class_b_0.ma". (* BALANCE CONDITION FOR PATH ***********************************************) -(* This condition applies to a structural path *) +(* Note: this condition applies to a structural path *) inductive pbc: predicate path ≝ | pbc_empty: pbc (𝐞) | pbc_redex: ∀b. pbc b → pbc (𝗔◗b◖𝗟) diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma new file mode 100644 index 000000000..5c0e5e6eb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure_inner.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/syntax/path_structure.ma". +include "delayed_updating/syntax/path_inner.ma". + +(* STRUCTURE FOR PATH *******************************************************) + +(* Constructions with pic ***************************************************) + +lemma structure_pic (p): + ⊗p ϵ 𝐈. +#p @(list_ind_rcons … p) -p +[