From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 28 Feb 2012 13:59:14 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1929
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=601adf4ee553a77be1c55bc29159ed0e209500a1

commit by user andrea
---

diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma
index c159fa13d..be1b60477 100644
--- 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:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.λp1,p2:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB.(a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p1 a title="eqb" href="cic:/fakeuri.def(1)"=/a= a title="pair pi1" href="cic:/fakeuri.def(1)"\fst/a p2) a title="boolean and" href="cic:/fakeuri.def(1)"∧/a (a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a p1 a title="eqb" href="cic:/fakeuri.def(1)"=/a= a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a 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:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.∀p1,p2:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB.
+  a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"eq_pairs/a A B p1 p2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="iff" href="cic:/fakeuri.def(1)"↔/a p1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a 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 (a href="cic:/matita/basics/bool/andb_true.def(5)"andb_true/a …H) normalize #eqa #eqb >(\P eqa) >(\P eqb) //
+  |#H destruct normalize >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … a2)) >(\b (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a … b2)) //
   ]
 qed.
 
-definition DeqProd ≝ λA,B:DeqSet.
-  mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
+definition DeqProd ≝ λA,B:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"DeqSet/a.
+  a href="cic:/matita/tutorial/chapter4/DeqSet.con(0,1,0)"mk_DeqSet/a (Aa title="Product" href="cic:/fakeuri.def(1)"×/aB) (a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"eq_pairs/a A B) (a href="cic:/matita/tutorial/chapter4/eq_pairs_true.def(6)"eq_pairs_true/a 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 a href="cic:/fakeuri.def(1)" title="hint_decl_Type1"≔/a C1,C2; 
+    T1 ≟ a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"carr/a C1,
+    T2 ≟ a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"carr/a C2,
+    X ≟ a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"DeqProd/a C1 C2
 (* ---------------------------------------- *) ⊢ 
-    T1×T2 ≡ carr X.
+    T1a title="Product" href="cic:/fakeuri.def(1)"×/aT2 ≡ a href="cic:/matita/tutorial/chapter4/carr.fix(0,0,2)"carr/a X.
 
-unification hint  0 ≔ T1,T2,p1,p2; 
-    X ≟ DeqProd T1 T2
+unification hint  0 a href="cic:/fakeuri.def(1)" title="hint_decl_Type0"≔/a T1,T2,p1,p2; 
+    X ≟ a href="cic:/matita/tutorial/chapter4/DeqProd.def(7)"DeqProd/a T1 T2
 (* ---------------------------------------- *) ⊢ 
-    eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
+    a href="cic:/matita/tutorial/chapter4/eq_pairs.def(4)"eq_pairs/a T1 T2 p1 p2 ≡ a href="cic:/matita/tutorial/chapter4/eqb.fix(0,0,3)"eqb/a X p1 p2.
 
 example hint2: ∀b1,b2. 
-  〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
+  a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ab1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉a title="eqb" href="cic:/fakeuri.def(1)"=/a=a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,b2〉a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → a title="Pair construction" href="cic:/fakeuri.def(1)"〈/ab1,a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a〉a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aa title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a,b2〉.
 #b1 #b2 #H @(\P H).
\ No newline at end of file