From 57296e7036707343c4d8a8e990a48e5f1518eee4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 10 Sep 2017 14:23:34 +0000 Subject: [PATCH] xoa notation refactoring and minor additions --- .../ground_2/notation/xoa/and_2.ma | 19 +++++++++++++++++++ .../{xoa_notation.ma => xoa/notation.ma} | 0 .../lambdadelta/ground_2/notation/xoa/or_2.ma | 19 +++++++++++++++++++ .../ground_2/relocation/rtmap_coafter.ma | 8 ++++++++ .../lambdadelta/ground_2/xoa.conf.xml | 2 +- .../contribs/lambdadelta/ground_2/xoa/xoa.ma | 2 +- .../lambdadelta/ground_2/xoa/xoa_props.ma | 2 ++ .../lambdadelta/ground_2/xoa2.conf.xml | 2 +- 8 files changed, 51 insertions(+), 3 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/and_2.ma rename matita/matita/contribs/lambdadelta/ground_2/notation/{xoa_notation.ma => xoa/notation.ma} (100%) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/or_2.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/and_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/and_2.ma new file mode 100644 index 000000000..854eb7b8c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/and_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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation > "hvbox(∧∧ term 34 P0 break & term 34 P1)" + non associative with precedence 35 + for @{ 'and $P0 $P1 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/or_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/or_2.ma new file mode 100644 index 000000000..c5da136f2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/or_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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation > "hvbox(∨∨ term 29 P0 break | term 29 P1)" + non associative with precedence 30 + for @{ 'or $P0 $P1 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma index c6e4b3a96..4864c9bae 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma @@ -151,6 +151,14 @@ lemma coafter_inv_xxn: ∀g1,g2,g. g1 ~⊚ g2 ≡ g → ∀f. ⫯f = g → ] qed-. +lemma coafter_inv_xnn: ∀g1,g2,g. g1 ~⊚ g2 ≡ g → + ∀f2,f. ⫯f2 = g2 → ⫯f = g → + ∃∃f1. f1 ~⊚ f2 ≡ f & ↑f1 = g1. +#g1 #g2 #g #Hg #f2 #f #H2 destruct #H +elim (coafter_inv_xxn … Hg … H) -g +#z1 #z2 #Hf #H1 #H2 destruct /2 width=3 by ex2_intro/ +qed-. + lemma coafter_inv_xxp: ∀g1,g2,g. g1 ~⊚ g2 ≡ g → ∀f. ↑f = g → (∃∃f1,f2. f1 ~⊚ f2 ≡ f & ↑f1 = g1 & ↑f2 = g2) ∨ ∃∃f1. f1 ~⊚ g2 ≡ f & ⫯f1 = g1. diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index 9ddee120d..eaa102c4e 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -3,7 +3,7 @@
contribs/lambdadelta/ ground_2/xoa/xoa - ground_2/notation/xoa_notation + ground_2/notation/xoa/notation basics/pts.ma 1 2 1 3 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma index 1566811d2..4954c0cc4 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma @@ -16,7 +16,7 @@ include "basics/pts.ma". -include "ground_2/notation/xoa_notation.ma". +include "ground_2/notation/xoa/notation.ma". (* multiple existental quantifier (1, 2) *) diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma index e917bacd2..408e1933d 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma @@ -15,6 +15,8 @@ include "basics/logic.ma". include "ground_2/notation/xoa/false_0.ma". include "ground_2/notation/xoa/true_0.ma". +include "ground_2/notation/xoa/or_2.ma". +include "ground_2/notation/xoa/and_2.ma". include "ground_2/xoa/xoa.ma". interpretation "logical false" 'false = False. diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml index ede212e41..593d91873 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml @@ -3,7 +3,7 @@
contribs/lambdadelta/ ground_2/xoa/xoa2 - ground_2/notation/xoa2_notation + ground_2/notation/xoa/notation2 basics/pts.ma
-- 2.39.2