-(**************************************************************************)
-(* ___ *)
-(* ||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 "arithmetics/nat.ma".
-include "basics/lists/list.ma".
-include "basics/sets.ma".
-
-definition word ≝ λS:DeqSet.list S.
-
-notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
-interpretation "epsilon" 'epsilon = (nil ?).
-
-(* concatenation *)
-definition cat : ∀S,l1,l2,w.Prop ≝
- λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
-notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
-interpretation "cat lang" 'middot a b = (cat ? a b).
-
-let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
-
-let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
-match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ].
-
-(* kleene's star *)
-definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.
-notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
-interpretation "star lang" 'star l = (star ? l).
-
-lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop.
- A =1 C → A · B =1 C · B.
-#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
-cases (H w1) /6/
+(**** For instance the empty set is defined by the always function predicate *)
+
+definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
+notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
+interpretation "empty set" 'empty_set = (empty_set ?).
+
+(* Similarly, a singleton set contaning containing an element a, is defined
+by by the characteristic function asserting equality with a *)
+
+definition singleton ≝ λA.λx,a:A.x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 6a.
+(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
+interpretation "singleton" 'singl x = (singleton ? x).
+
+(* The membership relation between an element of type A and a set S:A →Prop is
+simply the predicate resulting from the application of S to a.
+The operations of union, intersection, complement and substraction
+are easily defined in terms of the propositional connectives of dijunction,
+conjunction and negation *)
+
+definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 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 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym∧] (in [term])"\ 6\ 5/span\ 6 Q a.
+interpretation "intersection" 'intersects a b = (intersection ? a b).
+
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A w.
+interpretation "complement" 'not a = (complement ? a).
+
+definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 B w.
+interpretation "substraction" 'minus a b = (substraction ? a b).
+
+(* Finally, we use implication to define the inclusion relation between
+sets *)
+
+definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
+interpretation "subset" 'subseteq a b = (subset ? a b).
+
+(* Two sets are equals if and only if they have the same elements, that is,
+if the two characteristic functions are extensionally equivalent: *)
+
+definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym↔] (in [term])"\ 6\ 5/span\ 6 Q a.
+notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
+interpretation "extensional equality" 'eqP a b = (eqP ? a b).
+
+(* This notion of equality is different from the intensional equality of
+functions; the fact it defines an equivalence relation must be explicitly
+proved: *)
+
+lemma eqP_sym: ∀U.∀A,B:U →Prop.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
+#U #A #B #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @eqAB qed.
+
+lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C.
+#U #A #B #C #eqAB #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 // qed.
+
+(* For the same reason, we must also prove that all the operations behave well
+with respect to eqP: *)
+
+lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5span class="error" title="Parse error: NUMBER '1' or [term] expected after [sym=] (in [term])"\ 6\ 5/span\ 61 C → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B.
+#U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_or_r.def(2)"\ 6iff_or_r\ 5/a\ 6 @eqAB qed.
+
+lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
+ B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C.
+#U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_or_l.def(2)"\ 6iff_or_l\ 5/a\ 6 @eqBC qed.
+
+lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 B.
+#U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_and_r.def(2)"\ 6iff_and_r\ 5/a\ 6 @eqAB qed.
+
+lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
+ B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym∩] (in [term])"\ 6\ 5/span\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C.
+#U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 @eqBC qed.
+
+lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B.
+#U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_and_r.def(2)"\ 6iff_and_r\ 5/a\ 6 @eqAB qed.
+
+lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
+ B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C.
+#U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/iff_not.def(4)"\ 6iff_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+(* We can now prove several properties of the previous set-theoretic operations.
+In particular, union is commutative and associative, and the empty set is an
+identity element: *)
+
+lemma union_empty_r: ∀U.∀A:U→Prop.
+ A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6∅\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
+#U #A #w % [* // normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]