(* 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 *)
+predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type A→Prop. *)
include "basics/logic.ma".
(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
interpretation "singleton" 'singl x = (singleton ? x).
-(* The operations of union, intersection, complement and substraction
+(* 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 *)
interpretation "extensional equality" 'eqP a b = (eqP ? a b).
(* This notion of equality is different from the intensional equality of
-fucntions, hence we have to prove the usual properties: *)
+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 @iff_sym @eqAB qed.
+#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 =1 B → B =1 C → A =1 C.
-#U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
+ 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 we have
- 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.
+(* 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\ 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 =1 C → A ∪ B =1 A ∪ C.
-#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
+ 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 =1 C → A ∩ B =1 C ∩ B.
-#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+ 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 =1 C → A ∩ B =1 A ∩ C.
-#U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
+ 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 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 =1 C → A - B =1 C - B.
-#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+ 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 =1 C → A - B =1 A - C.
-#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+ 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: *)
-(* set equalities *)
lemma union_empty_r: ∀U.∀A:U→Prop.
- A ∪ ∅ =1 A.
-#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
+ 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/]
qed.
lemma union_comm : ∀U.∀A,B:U →Prop.
- A ∪ B =1 B ∪ A.
-#U #A #B #a % * /2/ qed.
+ 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 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 A.
+#U #A #B #a % * /\ 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, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ 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/]
+ A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C \ 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 (B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 C).
+#S #A #B #C #w % [* [* /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] | * [/\ 5span class="autotactic"\ 63\ 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/ | * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
qed.
+(* In the same way we prove commutativity and associativity for set
+interesection *)
+
lemma cap_comm : ∀U.∀A,B:U →Prop.
- A ∩ B =1 B ∩ A.
-#U #A #B #a % * /2/ qed.
+ 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 B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 A.
+#U #A #B #a % * /\ 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.
+
+lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
+ A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 (B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C) \ 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 B) \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C.
+#U #A #B #C #w % [ * #Aw * /\ 5span class="autotactic"\ 63\ 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/ \ 5span class="autotactic"\ 6\ 5span class="autotrace"\ 6\ 5/span\ 6\ 5/span\ 6| * * /\ 5span class="autotactic"\ 63\ 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.
+
+(* We can also easily prove idempotency for union and intersection *)
lemma union_idemp: ∀U.∀A:U →Prop.
- A ∪ A =1 A.
-#U #A #a % [* // | /2/] qed.
+ A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
+#U #A #a % [* // | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] qed.
lemma cap_idemp: ∀U.∀A:U →Prop.
- A ∩ A =1 A.
-#U #A #a % [* // | /2/] qed.
+ A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A.
+#U #A #a % [* // | /\ 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.
-(*distributivities *)
+(* We conclude our examples with a couple of distributivity theorems,
+and a characterization of substraction in terms of interesection and
+complementation. *)
lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
- (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
-#U #A #B #C #w % [* * /3/ | * * /3/]
+ (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B) \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C \ 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) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6∩\ 5/a\ 6 C).
+#U #A #B #C #w % [* * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
qed.
lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
- (A ∪ B) - C =1 (A - C) ∪ (B - C).
-#U #A #B #C #w % [* * /3/ | * * /3/]
+ (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 B) \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C \ 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) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6∪\ 5/a\ 6 (B \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C).
+#U #A #B #C #w % [* * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
qed.
-(* substraction *)
-lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
-#U #A #B #w normalize /2/
+lemma substract_def:∀U.∀A,B:U→Prop. A\ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6B \ 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 \ 5a title="complement" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6B.
+#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.
-include "basics/types.ma".
-include "basics/bool.ma".
-
(****** DeqSet: a set with a decidbale equality ******)
record DeqSet : Type[1] ≝ { carr :> Type[0];
notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
-#b1 #b2 cases b1 cases b2 normalize /2/
+#b1 #b2 cases b1 cases b2 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace conj\ 5/span\ 6\ 5/span\ 6/
qed.
definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
eq_pairs A B p1 p2 = true ↔ p1 = p2.
#A #B * #a1 #b1 * #a2 #b2 %
- [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
+ [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
|#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
]
qed.
projects / helm.git / blobdiff