X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter4.ma;h=1be877197f9cff9659a5e5573d508e9af1e2ef2d;hb=f848433620419e71cd19ec0b4f58c717ac50f85e;hp=8457aa48473c75affa2f64983ceca88b1f2d8318;hpb=01d39f9b4feb6eba25f951c6fda8037840db88b4;p=helm.git

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index 8457aa484..1be877197 100644
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -1,5 +1,5 @@
 (* In this Chapter we shall develop a naif theory of sets represented as characteristic
-predicates over some universe codeA/code, that is as objects of type A→Prop *)
+predicates over some universe codeA/code, that is as objects of type A→Prop. *)
 
 include "basics/logic.ma".
 
@@ -16,7 +16,9 @@ definition singleton ≝ λA.λx,a:A.xa title="leibnitz's equality" href="cic:/
 (* 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 *)
 
@@ -46,88 +48,102 @@ 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
-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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B → B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A.
-#U #A #B #eqAB #a @iff_sym @eqAB qed.
+#U #A #B #eqAB #a @a href="cic:/matita/basics/logic/iff_sym.def(2)"iff_sym/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B → B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C → A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C.
+#U #A #B #C #eqAB #eqBC #a @a href="cic:/matita/basics/logic/iff_trans.def(2)"iff_trans/a // 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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="union" href="cic:/fakeuri.def(1)"∪/a B.
+#U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_or_r.def(2)"iff_or_r/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="union" href="cic:/fakeuri.def(1)"∪/a C.
+#U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_or_l.def(2)"iff_or_l/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="intersection" href="cic:/fakeuri.def(1)"∩/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="intersection" href="cic:/fakeuri.def(1)"∩/a B.
+#U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_and_r.def(2)"iff_and_r/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="intersection" href="cic:/fakeuri.def(1)"∩/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="intersection" href="cic:/fakeuri.def(1)"∩/a C.
+#U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_and_l.def(2)"iff_and_l/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="substraction" href="cic:/fakeuri.def(1)"-/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C a title="substraction" href="cic:/fakeuri.def(1)"-/a B.
+#U #A #B #C #eqAB #a @a href="cic:/matita/basics/logic/iff_and_r.def(2)"iff_and_r/a @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 a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 C  → A a title="substraction" href="cic:/fakeuri.def(1)"-/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="substraction" href="cic:/fakeuri.def(1)"-/a C.
+#U #A #B #C #eqBC #a @a href="cic:/matita/basics/logic/iff_and_l.def(2)"iff_and_l/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/iff_not.def(4)"iff_not/a/span/span/ 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 a title="union" href="cic:/fakeuri.def(1)"∪/a a title="empty set" href="cic:/fakeuri.def(1)"∅/a a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A.
+#U #A #w % [* // normalize #abs @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace /span/span/ | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/]
 qed.
 
 lemma union_comm : ∀U.∀A,B:U →Prop. 
-  A ∪ B =1 B ∪ A.
-#U #A #B #a % * /2/ qed. 
+  A a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B a title="union" href="cic:/fakeuri.def(1)"∪/a A.
+#U #A #B #a % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ 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 a title="union" href="cic:/fakeuri.def(1)"∪/a B a title="union" href="cic:/fakeuri.def(1)"∪/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="union" href="cic:/fakeuri.def(1)"∪/a (B a title="union" href="cic:/fakeuri.def(1)"∪/a C).
+#S #A #B #C #w % [* [* /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/] | * [/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ | * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/]
 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 a title="intersection" href="cic:/fakeuri.def(1)"∩/a B a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 B a title="intersection" href="cic:/fakeuri.def(1)"∩/a A.
+#U #A #B #a % * /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed. 
+
+lemma cap_assoc: ∀U.∀A,B,C:U→Prop.
+  A a title="intersection" href="cic:/fakeuri.def(1)"∩/a (B a title="intersection" href="cic:/fakeuri.def(1)"∩/a C) a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (A a title="intersection" href="cic:/fakeuri.def(1)"∩/a B) a title="intersection" href="cic:/fakeuri.def(1)"∩/a C.
+#U #A #B #C #w % [ * #Aw * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ span class="autotactic"span class="autotrace"/span/span| * * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ ]
+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  a title="union" href="cic:/fakeuri.def(1)"∪/a A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A.
+#U #A #a % [* // | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/] qed. 
 
 lemma cap_idemp: ∀U.∀A:U →Prop. 
-  A ∩ A =1 A.
-#U #A #a % [* // | /2/] qed. 
+  A a title="intersection" href="cic:/fakeuri.def(1)"∩/a A a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A.
+#U #A #a % [* // | /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/] 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 a title="union" href="cic:/fakeuri.def(1)"∪/a B) a title="intersection" href="cic:/fakeuri.def(1)"∩/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (A a title="intersection" href="cic:/fakeuri.def(1)"∩/a C) a title="union" href="cic:/fakeuri.def(1)"∪/a (B a title="intersection" href="cic:/fakeuri.def(1)"∩/a C).
+#U #A #B #C #w % [* * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ | * * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/] 
 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 a title="union" href="cic:/fakeuri.def(1)"∪/a B) a title="substraction" href="cic:/fakeuri.def(1)"-/a C a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 (A a title="substraction" href="cic:/fakeuri.def(1)"-/a C) a title="union" href="cic:/fakeuri.def(1)"∪/a (B a title="substraction" href="cic:/fakeuri.def(1)"-/a C).
+#U #A #B #C #w % [* * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ | * * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a, a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/] 
 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. Aa title="substraction" href="cic:/fakeuri.def(1)"-/aB a title="extensional equality" href="cic:/fakeuri.def(1)"=/a1 A a title="intersection" href="cic:/fakeuri.def(1)"∩/a a title="complement" href="cic:/fakeuri.def(1)"¬/aB.
+#U #A #B #w normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/
 qed.
 
-include "basics/types.ma".
-include "basics/bool.ma".
-
 (****** DeqSet: a set with a decidbale equality ******)
 
 record DeqSet : Type[1] ≝ { carr :> Type[0];
@@ -168,7 +184,7 @@ definition beqb ≝ λb1,b2.
 
 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 /span class="autotactic"2span class="autotrace" trace conj/span/span/
 qed. 
 
 definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
@@ -194,7 +210,7 @@ definition eq_pairs ≝
 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.