X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter2.ma;h=11eb476e0f9cfa119e7b196f07f591497979aadf;hb=7956b9a84e0556d2d24fffedbbbabcd9e248d702;hp=ab758c124f52fafb842e8e3bd4246b61346c2aa6;hpb=fc43587e06d59afb5b1c65904372843d928fdfe5;p=helm.git

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index ab758c124..11eb476e0 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -171,12 +171,12 @@ We first write down the function, and then discuss it.*)
 
 let rec div2 n ≝ 
 match n with
-[ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉
+[ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/aspan class="error" title="Parse error: [sym,] expected after [term level 19] (in [term])"/span,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉
 | S a ⇒ span style="text-decoration: underline;"/span
    let p ≝ (div2 a) in
-   match (a href="cic:/matita/basics/types/snd.def(1)"snd/a … p) with
-   [ tt ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉 
-   | ff ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p, a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉
+   match (a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/aspan class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"/span … p) with
+   [ tt ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉 
+   | ff ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p, a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉
    ]
 ]. 
 
@@ -202,21 +202,21 @@ the remainder for a). The reader is strongly invited to check all remaining deta
 Let us now prove that our div2 function has the expected behaviour.
 *)
 
-lemma surjective_pairing: ∀A,B.∀p:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a … p〉.
+lemma surjective_pairing: ∀A,B.∀p:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/aspan class="error" title="Parse error: [sym〉] or [sym,] expected after [term level 19] (in [term])"/span … p〉.
 #A #B * // qed.
 
 lemma div2SO: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aspan style="text-decoration: underline;"/spanq,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉.
 #n #q #H normalize >H normalize // qed.
 
-lemma div2S1: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a q,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉.
+lemma div2S1: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aspan class="error" title="Parse error: [term] expected after [sym=] (in [term])"/span a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a q,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉.
 #n #q #H normalize >H normalize // qed.
 
 lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,r〉 → n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q) (a href="cic:/matita/tutorial/chapter2/nat_of_bool.def(1)"nat_of_bool/a r).
 #n elim n
   [#q #r normalize #H destruct //
   |#a #Hind #q #r 
-   cut (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a), a href="cic:/matita/basics/types/snd.def(1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a)〉) [//] 
-   cases (a href="cic:/matita/basics/types/snd.def(1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))
+   cut (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a), a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a)〉) [//] 
+   cases (a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))
     [#H >(a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"div2S1/a … H) #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a whd in ⊢ (???%); <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(Hind … H) 
     |#H >(a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"div2SO/a … H) #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(Hind … H) 
     ]
@@ -248,7 +248,7 @@ definition qr_spec ≝ λn.λp.∀q,r. p a title="leibnitz's equality" href="ci
 (* We can now construct a function from n to {p|qr_spec n p} by composing the objects
 we already have *)
 
-definition div2P: ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)" Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aspan style="text-decoration: underline;"a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"bool/a/span) (a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"qr_spec/a n) ≝ λn.
+definition div2P: ∀n. a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"Sub/a (a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/aa title="Product" href="cic:/fakeuri.def(1)"×/aspan style="text-decoration: underline;"a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"bool/a/span) (a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"qr_spec/a n) ≝ λn.
  a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a ?? (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n) (a href="cic:/matita/tutorial/chapter2/div2_ok.def(4)"div2_ok/a n).
 
 (* But we can also try do directly build such an object *)
@@ -257,11 +257,11 @@ definition div2Pagain : ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,
 #n elim n
   [@(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) normalize #q #r #H destruct //
   |#a * #p #qrspec 
-   cut (p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p, a href="cic:/matita/basics/types/snd.def(1)"snd/a … p〉) [//] 
-   cases (a href="cic:/matita/basics/types/snd.def(1)"snd/a … p)
-    [#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) whd #q #r #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a
+   cut (p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p, a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/a … p〉) [//] 
+   cases (a href="cic:/matita/basics/types/snd.fix(0,2,1)"snd/a … p)
+    [#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"ff/a〉) whd #q #r #H1 destruct @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a span style="text-decoration: underline;">/spana href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a
      whd in ⊢ (???%); <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(qrspec … H)
-    |#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉) whd #q #r #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(qrspec … H) 
+    |#H @(a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"mk_Sub/a … a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.fix(0,2,1)"fst/a … p,a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉) whd #q #r #H1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @a href="cic:/matita/basics/logic/eq_f.def(3)"eq_f/a @(qrspec … H) 
   ]
 qed.