From ab63ef8e3b4029307eea9646b099c04a1d499653 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 18 Jan 2022 16:52:11 +0100 Subject: [PATCH] update in ground + WIP on subsets --- .../contribs/lambdadelta/ground/lib/logic.ma | 3 ++ .../contribs/lambdadelta/ground/lib/subset.ma | 7 +++- .../lambdadelta/ground/lib/subset_ext.ma | 35 +++++++++++++++++++ .../ground/lib/subset_ext_equivalence.ma | 26 ++++++++++++++ .../ground/lib/subset_ext_inclusion.ma | 32 +++++++++++++++++ .../notation/relations/not_epsilon_3.ma | 27 ++++++++++++++ matita/matita/predefined_virtuals.ml | 1 + 7 files changed, 130 insertions(+), 1 deletion(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/lib/subset_ext.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/lib/subset_ext_equivalence.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/lib/subset_ext_inclusion.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/relations/not_epsilon_3.ma diff --git a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma index 4cf0e0096..8786e77ae 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/logic.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/logic.ma @@ -28,6 +28,9 @@ interpretation (* LOGIC ********************************************************************) +definition negation (A:Prop): Prop ≝ + A → ⊥. + (* Constructions with land **************************************************) lemma commutative_and (A) (B): diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma index 25863fe2b..8f0154d81 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/subset.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma @@ -12,9 +12,10 @@ (* *) (**************************************************************************) +include "ground/lib/relations.ma". include "ground/notation/functions/powerclass_1.ma". include "ground/notation/relations/epsilon_3.ma". -include "ground/lib/relations.ma". +include "ground/notation/relations/not_epsilon_3.ma". (* SUBSETS ******************************************************************) @@ -31,3 +32,7 @@ definition subset_in (A): 𝒫❨A❩ → 𝒫❨A❩ ≝ interpretation "membership (subset)" 'Epsilon A a u = (subset_in A u a). + +interpretation + "negated membership (subset)" + 'NotEpsilon A a u = (negation (subset_in A u a)). diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_ext.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext.ma new file mode 100644 index 000000000..5d623ad16 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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". + +(* EXTENSIONS FOR SUBSETS ***************************************************) + +definition subset_ext_f1 (A1) (A0) (f:A1→A0): 𝒫❨A1❩ → 𝒫❨A0❩ ≝ + λu1,a0. ∃∃a1. a1 ϵ u1 & f a1 = a0. + +definition subset_ext_p1 (A1) (Q:predicate A1): predicate (𝒫❨A1❩) ≝ + λu1. ∀a1. a1 ϵ u1 → Q a1. + +(* Basic constructions ******************************************************) + +lemma subset_in_ext_f1_dx (A1) (A0) (f) (u1) (a1): + a1 ϵ u1 → f a1 ϵ subset_ext_f1 A1 A0 f u1. +/2 width=3 by ex2_intro/ qed. + +(* Basic inversions *********************************************************) + +lemma subset_in_inv_ext_p1_dx (A1) (Q) (u1) (a1): + a1 ϵ u1 → subset_ext_p1 A1 Q u1 → Q a1. +/2 width=1 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_equivalence.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_equivalence.ma new file mode 100644 index 000000000..f20aca24f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_equivalence.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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_ext_inclusion.ma". +include "ground/lib/subset_equivalence.ma". + +(* EXTENSIONS FOR SUBSETS ***************************************************) + +(* Constructions with subset_equivalence ************************************) + +lemma subset_equivalence_ext_f1_bi (A1) (A0) (f) (u1) (v1): + u1 ⇔ v1 → subset_ext_f1 A1 A0 f u1 ⇔ subset_ext_f1 A1 A0 f v1. +#A1 #A0 #f #u1 #v1 * #Huv1 #Hvu1 +/3 width=3 by subset_inclusion_ext_f1_bi, conj/ +qed. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_inclusion.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_inclusion.ma new file mode 100644 index 000000000..7fd5fd418 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/lib/subset_ext_inclusion.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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_inclusion.ma". +include "ground/lib/subset_ext.ma". + +(* EXTENSIONS FOR SUBSETS ***************************************************) + +(* Constructions with subset_inclusion **************************************) + +lemma subset_inclusion_ext_f1_bi (A1) (A0) (f) (u1) (v1): + u1 ⊆ v1 → subset_ext_f1 A1 A0 f u1 ⊆ subset_ext_f1 A1 A0 f v1. +#A1 #A0 #f #u1 #v1 #Huv1 #a0 * #a1 #Hau1 #H destruct +/3 width=3 by subset_in_ext_f1_dx/ +qed. + +lemma subset_inclusion_ext_p1_trans (A1) (Q) (u1) (v1): + u1 ⊆ v1 → subset_ext_p1 A1 Q v1 → subset_ext_p1 A1 Q u1. +#A1 #Q #u1 #v1 #Huv1 #Hv1 +/3 width=1 by/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/not_epsilon_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/not_epsilon_3.ma new file mode 100644 index 000000000..2bf35dc4d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/not_epsilon_3.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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation < "hvbox( a ⧸ϵ break term 46 u )" + non associative with precedence 45 + for @{ 'NotEpsilon $S $a $u }. + +notation > "hvbox( a ⧸ϵ break term 46 u )" + non associative with precedence 45 + for @{ 'NotEpsilon ? $a $u }. + +notation > "hvbox( a ⧸ϵ{ break term 46 S } break term 46 u )" + non associative with precedence 45 + for @{ 'NotEpsilon $S $a $u }. diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index cc2953e4d..7656dc68c 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1503,6 +1503,7 @@ let load_predefined_virtuals () = ;; let predefined_classes = [ + ["/"; "⧸"; ]; ["&"; "⅋"; ]; ["|"; "❘"; "∥"; ]; ["!"; "¡"; "⫯"; "⫰"; "⟟"; "⫱"; ]; -- 2.39.2