From: Andrea Asperti Date: Tue, 6 Dec 2011 07:16:20 +0000 (+0000) Subject: naive sets (A-> Prop) X-Git-Tag: make_still_working~2053 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=24fc5e5485245fe879e17d46176530b688930b3b;p=helm.git naive sets (A-> Prop) --- diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index 59aad912d..a1bae198b 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -77,8 +77,9 @@ injective A B f → injective B C g → injective A C (λx.g (f x)). (* extensional equality *) +(* moved inside sets.ma definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ -λA.λP,Q.∀a.iff (P a) (Q a). +λA.λP,Q.∀a.iff (P a) (Q a). *) definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝ λA,B.λR,S.∀a.∀b.iff (R a b) (S a b). @@ -86,11 +87,12 @@ definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝ definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝ λA,B.λf,g.∀a.f a = g a. +(* notation " x \eqP y " non associative with precedence 45 for @{'eqP A $x $y}. interpretation "functional extentional equality" -'eqP A x y = (exteqP A x y). +'eqP A x y = (exteqP A x y). *) notation "x \eqR y" non associative with precedence 45 for @{'eqR ? ? x y}. diff --git a/matita/matita/lib/basics/sets.ma b/matita/matita/lib/basics/sets.ma new file mode 100644 index 000000000..622025d79 --- /dev/null +++ b/matita/matita/lib/basics/sets.ma @@ -0,0 +1,76 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "basics/logic.ma". + +(**** a subset of A is just an object of type A→Prop ****) + +definition empty_set ≝ λA:Type[0].λa:A.False. +notation "\emptyv" non associative with precedence 90 for @{'empty_set}. +interpretation "empty set" 'empty_set = (empty_set ?). + +definition singleton ≝ λA.λx,a:A.x=a. +(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *) +interpretation "singleton" 'singl x = (singleton ? x). + +definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a. +interpretation "union" 'union a b = (union ? a b). + +definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a. +interpretation "intersection" 'intersects a b = (intersection ? a b). + +definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a). +interpretation "subset" 'subseteq a b = (intersection ? a b). + +(* extensional equality *) +definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a. +notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}. +interpretation "extensional equality" 'eqP a b = (eqP ? a b). + +lemma eqP_sym: ∀U.∀A,B:U →Prop. + A =1 B → B =1 A. +#U #A #B #eqAB #a @iff_sym @eqAB qed. + +lemma eqP_trans: ∀U.∀A,B,C:U →Prop. + A =1 B → B =1 C → A =1 C. +#U #A #B #C #eqAB #eqBC #a @iff_trans // qed. + +lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. + A =1 C → A ∪ B =1 C ∪ B. +#U #A #B #C #eqAB #a @iff_or_r @eqAB qed. + +lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. + B =1 C → A ∪ B =1 A ∪ C. +#U #A #B #C #eqBC #a @iff_or_l @eqBC qed. + +(* set equalities *) +lemma union_comm : ∀U.∀A,B:U →Prop. + A ∪ B =1 B ∪ A. +#U #A #B #a % * /2/ qed. + +lemma union_assoc: ∀U.∀A,B,C:U → Prop. + A ∪ B ∪ C =1 A ∪ (B ∪ C). +#S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/] +qed. + +lemma cap_comm : ∀U.∀A,B:U →Prop. + A ∩ B =1 B ∩ A. +#U #A #B #a % * /2/ qed. + +lemma union_idemp: ∀U.∀A:U →Prop. + A ∪ A =1 A. +#U #A #a % [* // | /2/] qed. + +lemma cap_idemp: ∀U.∀A:U →Prop. + A ∩ A =1 A. +#U #A #a % [* // | /2/] qed. + +