X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=weblib%2Ftutorial%2Fchapter2.ma;fp=weblib%2Ftutorial%2Fchapter2.ma;h=d564b7220c03dd5e7348860bf227eb9dffb9595e;hb=ae7b573a31d8843d03977c5eeb3ec14576fb4985;hp=ad0896d708ce9792ef00ed8cfb19c1bae68b7fe0;hpb=a01d31298e5e699fa198135655018bf73fe6e3f0;p=helm.git diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index ad0896d70..d564b7220 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -77,6 +77,19 @@ For Matita, the task is trivial and we can simply close the goal with // *) // qed. +(* COERCIONS *) + +inductive bool : Type[0] ≝ +| tt : bool +| ff : bool. + +definition nat_of_bool ≝ λb. match b with +[ tt ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a +| ff ⇒ a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a +]. + +(* coercion nat_of_bool. ?? *) + (* Let us now define the following function: *) definition twice ≝ λn.a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"add/a n n. @@ -138,29 +151,30 @@ qed. (* Instead of proving the existence of a number corresponding to the half of n, we could be interested in computing it. The best way to do it is to define this division operation -together with the remainder, that is 0 if the input term is even, and 1 if the input term -is odd. Since we must return a pair, we could use a suitably defined record type, or simply -a product type N × N, defined in the basic library. The product type is just a sort of -general purpose record, with standard fields fst and snd, called projections. A pair of -values n and m is written (pair … m n) or \langle n,m \rangle - visually rendered as 〈n,m〉 +together with the remainder, that in our case is just a boolean value: tt if the input term +is even, and ff if the input term is odd. Since we must return a pair, we could use a +suitably defined record type, or simply a product type nat × bool, defined in the basic library. +The product type is just a sort of general purpose record, with standard fields fst and snd, +called projections. A pair of values n and m is written (pair … m n) or \langle n,m \rangle - +visually rendered as 〈n,m〉 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/nat.con(0,1,0)"O/a〉 +[ 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〉 | 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 - [ O ⇒ 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/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉 - | S b ⇒ 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/nat.con(0,1,0)"O/a〉 + [ 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〉 ] ]. -(* The function is computed by recursion over the input n. If n is 0, then both quotient -and remainder are 0. If n = S a, we start computing the half of a, say 〈q,r〉. Then we -have two cases according to the possible values of b: if b is 0, then we must return - 〈q,1〉, while if b = 1 (no other case is possible), then we must return 〈S q,0〉. +(* The function is computed by recursion over the input n. If n is 0, then the quotient +is 0 and the remainder is tt. If n = S a, we start computing the half of a, say 〈q,b〉. +Then we have two cases according to the possible values of b: if b is tt, then we must return + 〈q,ff〉, while if b = ff then we must return 〈S q,tt〉. It is important to point out the deep, substantial analogy between the algorithm for computing div2 and the the proof of ex_half. In particular ex_half returns a @@ -169,7 +183,7 @@ n and a boolean indicating which one between the two conditions A(n) and B(n) is This is precisely the quotient-remainder pair returned by div2. In both cases we proceed by recurrence (respectively, induction or recursion) over the input argument n. In case n = 0, we conclude the proof in ex_half by providing the -witness O and a proof of A(O); this corresponds to returning the pair 〈O,O〉 in div2. +witness O and a proof of A(O); this corresponds to returning the pair 〈O,tt〉 in div2. Similarly, in the inductive case n = S a, we must exploit the inductive hypothesis for a (i.e. the result of the recursive call), distinguishing two subcases according to the the two possibilites A(a) or B(a) (i.e. the two possibile values of the remainder @@ -181,22 +195,21 @@ 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〉. #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/nat.con(0,1,0)"O/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/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉. +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/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/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/nat.con(0,1,0)"O/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)"=/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〉. #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〉 → - r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a span style="text-decoration: underline;"/spana title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q a title="logical or" href="cic:/fakeuri.def(1)"∨/a - r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q). +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 %1 /2/ - |#a #Hind #q #r cases (Hind … (a href="cic:/matita/tutorial/chapter2/surjective_pairing.def(3)"surjective_pairing/a …)) * #eqr #eqa - [>(a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"div2SO/a a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))) // #H %2 destruct (a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"div2S1/a a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))) // #H %1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a (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 <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) ] - ] qed. (* There is still another possibility, however, namely to mix the program and its @@ -219,27 +232,31 @@ record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝ {witness: A; proof: P witness}. - definition div2Spec ≝ λn.λp.∀q,r. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,r〉 → - r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a span style="text-decoration: underline;"/spana title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q a title="logical or" href="cic:/fakeuri.def(1)"∨/a - r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q). - -(* We can now construct a function from n to {p|div2Spec n p} by composing the objects +definition qr_spec ≝ λn.λp.∀q,r. p 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). + +(* 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)"×/aa href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/a) (a href="cic:/matita/tutorial/chapter2/div2Spec.def(3)"div2Spec/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 *) -definition div2Pbis : ∀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)"×/aa href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"nat/a) (a href="cic:/matita/tutorial/chapter2/div2Spec.def(3)"div2Spec/a n). +definition div2Pagain : ∀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;"/spana href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"bool/a) (a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"qr_spec/a n). #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/nat.con(0,1,0)"O/a〉) normalize #q #r #H %1 destruct /2/ - |#a * #p #spec cases (spec … (a href="cic:/matita/tutorial/chapter2/surjective_pairing.def(3)"surjective_pairing/a …)) * #eqr #eqa - [@(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/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉) #q #r #H %2 destruct /2/ - |@(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/nat.con(0,1,0)"O/a〉) #q #r #H %1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a /2/ - ] + [@(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 <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) ] +qed. +example quotient7: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"witness/a … (a href="cic:/matita/tutorial/chapter2/div2P.def(5)"div2P/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/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/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a(a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a)),a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"tt/a〉. +// qed. -lemma foo: True. -pre /pre \ No newline at end of file +example quotient8: a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"witness/a … (a href="cic:/matita/tutorial/chapter2/div2P.def(5)"div2P/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/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/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a 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〉. +// qed. +prepre /pre/pre \ No newline at end of file