From bef004f9c2ab68f9f0f9c95536918681a61849fc Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 28 Feb 2012 13:55:24 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter4.ma | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/weblib/tutorial/chapter4.ma b/weblib/tutorial/chapter4.ma index 2c98ad147..c159fa13d 100644 --- a/weblib/tutorial/chapter4.ma +++ b/weblib/tutorial/chapter4.ma @@ -278,7 +278,10 @@ example exhint1: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a #b #H @(\P H) qed. -(* pairs *) +(* The cartesian product of two DeqSets is still a DeqSet. To prove +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). @@ -292,7 +295,12 @@ qed. definition DeqProd ≝ λA,B:DeqSet. mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true 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, -- 2.39.2