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,
+(* \ 5h2 class="section"\ 6Set Quality\ 5/h2\ 6
+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
+(*
+This notion of equality is different from the intensional equality of
functions; the fact it defines an equivalence relation must be explicitly
proved: *)
[%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 *)
definition DeqBool ≝ \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb.def(2)"\ 6beqb\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter4/beqb_true.def(4)"\ 6beqb_true\ 5/a\ 6.
-(*
-\ 5h2 class="section"\ 6Unification Hints\ 5/h2\ 6
-At this point, we would expect to be able to prove things like the
+(* At this point, we would expect to be able to prove things like the
following: for any boolean b, if b==false is true then b=false.
Unfortunately, this would not work, unless we declare b of type
DeqBool (change the type in the following statement and see what