From c8ba3d001893666a52c393d9cf8a0929dacd007a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 11 Dec 2021 00:23:33 +0100 Subject: [PATCH] update in ground + basic support for subsets as predicates --- .../contribs/lambdadelta/ground/lib/subset.ma | 33 ++++++++++++++ .../ground/lib/subset_equivalence.ma | 44 +++++++++++++++++++ .../ground/lib/subset_inclusion.ma | 36 +++++++++++++++ .../ground/notation/functions/powerclass_1.ma | 19 ++++++++ .../ground/notation/relations/epsilon_3.ma | 29 ++++++++++++ .../notation/relations/white_harrow_2.ma} | 6 +-- matita/matita/predefined_virtuals.ml | 2 +- 7 files changed, 165 insertions(+), 4 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/lib/subset.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma rename matita/matita/contribs/lambdadelta/{delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma => ground/notation/relations/white_harrow_2.ma} (87%) diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma new file mode 100644 index 000000000..25863fe2b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma @@ -0,0 +1,33 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/notation/functions/powerclass_1.ma". +include "ground/notation/relations/epsilon_3.ma". +include "ground/lib/relations.ma". + +(* SUBSETS ******************************************************************) + +definition subset (A): Type[0] ≝ + predicate A. + +interpretation + "power class (subset)" + 'PowerClass A = (subset A). + +definition subset_in (A): 𝒫❨A❩ → 𝒫❨A❩ ≝ + λu.u. + +interpretation + "membership (subset)" + 'Epsilon A a u = (subset_in A u a). diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma new file mode 100644 index 000000000..bab6b26e1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_equivalence.ma @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/notation/relations/white_harrow_2.ma". +include "ground/lib/subset_inclusion.ma". + +(* EQUIVALENCE FOR SUBSETS **************************************************) + +definition subset_eq (A): relation2 𝒫❨A❩ 𝒫❨A❩ ≝ + λu1,u2. ∧∧ u1 ⊆ u2 & u2 ⊆ u1. + +interpretation + "equivalence (subset)" + 'WhiteHArrow u1 u2 = (subset_eq ? u1 u2). + +(* Basic constructions ******************************************************) + +lemma subset_eq_refl (A): + reflexive … (subset_eq A). +/2 width=1 by conj/ qed. + +lemma subset_eq_sym (A): + symmetric … (subset_eq A). +#A #u1 #u2 * /2 width=1 by conj/ +qed-. + +(* Main constructions *******************************************************) + +theorem subset_eq_trans (A): + Transitive … (subset_eq A). +#A #u1 #u2 * #H12 #H21 #u3 * #H23 #H32 +/3 width=5 by subset_le_trans, conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma new file mode 100644 index 000000000..6f2e5c9b7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_inclusion.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground/lib/subset.ma". + +(* INCLUSION FOR SUBSETS ****************************************************) + +definition subset_le (A): relation2 𝒫❨A❩ 𝒫❨A❩ ≝ + λu1,u2. ∀p. p ϵ u1 → p ϵ u2. + +interpretation + "inclusion (subset)" + 'subseteq u1 u2 = (subset_le ? u1 u2). + +(* Basic constructions ******************************************************) + +lemma subset_le_refl (A): + reflexive … (subset_le A). +// qed. + +(* Main constructions *******************************************************) + +theorem subset_le_trans (A): + Transitive … (subset_le A). +/3 width=1 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_1.ma new file mode 100644 index 000000000..8eab6e62f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/powerclass_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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation "hvbox( 𝒫 ❨ break term 46 S ❩ )" + non associative with precedence 75 + for @{ 'PowerClass $S }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma new file mode 100644 index 000000000..2f5287d6b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/epsilon_3.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ********************************************) + +(* GROUND NOTATION **********************************************************) + +notation < "hvbox( a ϵ break term 46 u )" + non associative with precedence 45 + for @{ 'Epsilon $S $a $u }. + +notation > "hvbox( a ϵ break term 46 u )" + non associative with precedence 45 + for @{ 'Epsilon ? $a $u }. + +notation > "hvbox( a ϵ{ break term 46 S } break term 46 u )" + non associative with precedence 45 + for @{ 'Epsilon $S $a $u }. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/white_harrow_2.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma rename to matita/matita/contribs/lambdadelta/ground/notation/relations/white_harrow_2.ma index ffef611a4..b7130dfcb 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/up_down_arrow_epsilon_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/white_harrow_2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -(* NOTATION FOR DELAYED UPDATING ********************************************) +(* GROUND NOTATION **********************************************************) -notation "hvbox( p ϵ⬦ break term 46 t )" +notation "hvbox( a1 ⇔ break term 46 a2 )" non associative with precedence 45 - for @{ 'UpDownArrowEpsilon $p $t }. + for @{ 'WhiteHArrow $a1 $a2 }. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index a816099a6..1271e2c52 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1565,7 +1565,7 @@ let predefined_classes = [ ["o"; "θ"; "ϑ"; "𝕠"; "∘"; "⊚"; "ø"; "○"; "●"; "𝐨"; "𝛉"; "ⓞ"; ] ; ["O"; "Θ"; "𝕆"; "𝐎"; "𝚯"; "𝚹"; "Ⓞ"; ] ; ["p"; "π"; "𝕡"; "𝐩"; "𝛑"; "ⓟ"; ] ; - ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; ] ; + ["P"; "Π"; "℘"; "ℙ"; "𝐏"; "𝚷"; "Ⓟ"; "𝒫"; ] ; ["q"; "𝕢"; "𝐪"; "ⓠ"; ] ; ["Q"; "ℚ"; "𝐐"; "Ⓠ"; ] ; ["r"; "ρ"; "ϱ"; "𝕣"; "𝐫"; "𝛒"; "𝛠"; "ⓡ"; ] ; -- 2.39.2