From 601adf4ee553a77be1c55bc29159ed0e209500a1 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 28 Feb 2012 13:59:14 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter4.ma | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) 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 -- 2.39.2