commit by user andrea

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index c159fa13db6b0dfe72246273c57a1db5ecab7236..be1b604770f4d3926c64f9bddf7477e22b37ef4e 100644 (file)
--- a/weblib/tutorial/chapter4.ma
+++ b/weblib/tutorial/chapter4.ma
@@ -283,36 +283,36 @@ this, we must as usual define the boolen equality function, and prove
 it correctly reflects propositional equality. *)
 
 definition eq_pairs ≝
-  λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
+  λA,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λp1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.(\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p1 \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 p2) \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p1 \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= \ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 p2).
 
-lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
-  eq_pairs A B p1 p2 = true ↔ p1 = p2.
+lemma eq_pairs_true: ∀A,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀p1,p2:A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B.
+  \ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B p1 p2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 p1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 p2.
 #A #B * #a1 #b1 * #a2 #b2 %
-  [#H cases (andb_true …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
-  |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
+  [#H cases (\ 5a href="cic:/matita/basics/bool/andb_true.def(5)"\ 6andb_true\ 5/a\ 6 …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
+  |#H destruct normalize >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … a2)) >(\b (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 … b2)) //
   ]
 qed.
 
-definition DeqProd ≝ λA,B:DeqSet.
-  mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
+definition DeqProd ≝ λA,B:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.
+  \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"\ 6mk_DeqSet\ 5/a\ 6 (A\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6B) (\ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 A B) (\ 5a href="cic:/matita/tutorial/chapter4/eq_pairs_true.def(6)"\ 6eq_pairs_true\ 5/a\ 6 A B).
 
 (* Having an unification problem of the kind T1×T2 = carr X, what kind 
 of hint can we give to the system? We expect T1 to be the carrier of a
 DeqSet C1, T2 to be the carrier of a DeqSet C2, and X to be DeqProd C1 C2.
 This is expressed by the following hint: *)
 
-unification hint  0 ≔ C1,C2; 
-    T1 ≟ carr C1,
-    T2 ≟ carr C2,
-    X ≟ DeqProd C1 C2
+unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"\ 6≔\ 5/a\ 6 C1,C2; 
+    T1 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C1,
+    T2 ≟ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 C2,
+    X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 C1 C2
 (* ---------------------------------------- *) ⊢ 
-    T1×T2 ≡ carr X.
+    T1\ 5a title="Product" href="cic:/fakeuri.def(1)"\ 6×\ 5/a\ 6T2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"\ 6carr\ 5/a\ 6 X.
 
-unification hint  0 ≔ T1,T2,p1,p2; 
-    X ≟ DeqProd T1 T2
+unification hint  0 \ 5a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"\ 6≔\ 5/a\ 6 T1,T2,p1,p2; 
+    X ≟ \ 5a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"\ 6DeqProd\ 5/a\ 6 T1 T2
 (* ---------------------------------------- *) ⊢ 
-    eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
+    \ 5a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"\ 6eq_pairs\ 5/a\ 6 T1 T2 p1 p2 ≡ \ 5a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"\ 6eqb\ 5/a\ 6 X p1 p2.
 
 example hint2: ∀b1,b2. 
-  〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
+  \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6b1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,b2〉\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6b1,\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6〉\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6,b2〉.
 #b1 #b2 #H @(\P H).
\ No newline at end of file