(*
\ 5h1 class="section"\ 6Naif Set Theory\ 5/h1\ 6
*)
-In this Chapter we shall develop a naif theory of sets represented as
-characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type
-A→Prop. *)
-
include "basics/types.ma".
include "basics/bool.ma".
-
-(* For instance the empty set is defined by the always false function: *)
+(*
+In this Chapter we shall develop a naif theory of sets represented as
+characteristic predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type
+A→Prop.
+For instance the empty set is defined by the always false function: *)
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}.
#U #A #B #w normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-(* In several situation it is important to assume to have a decidable equality
+(*
+\ 5h2 class="section"\ 6Bool vs. Prop\ 5/h2\ 6
+In several situation it is important to assume to have a decidable equality
between elements of a set U, namely a boolean function eqb: U→U→bool such that
for any pair of elements a and b in U, (eqb x y) is true if and only if x=y.
A set equipped with such an equality is called a DeqSet: *)
notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
interpretation "eqb" 'eqb a b = (eqb ? a b).
-(* It is convenient to have a simple way to reflect a proof of the fact
+(*
+\ 5h2 class="section"\ 6Small Scale Reflection\ 5/h2\ 6
+It is convenient to have a simple way to reflect a proof of the fact
that (eqb a b) is true into a proof of the proposition (a = b); to this aim,
we introduce two operators "\P" and "\b". *)
[%1 @(\P H) | %2 @(\Pf H)]
qed.
-(* A simple example of a set with a decidable equality is bool. We first define
+(*
+\ 5h2 class="section"\ 6Unification Hints\ 5/h2\ 6
+A simple example of a set with a decidable equality is bool. We first define
the boolean equality beqb, that is just the xand function, then prove that
beqb b1 b2 is true if and only if b1=b2, and finally build the type DeqBool by
instantiating the DeqSet record with the previous information *)