X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftutorial%2Fchapter2.ma;h=ab758c124f52fafb842e8e3bd4246b61346c2aa6;hb=fc43587e06d59afb5b1c65904372843d928fdfe5;hp=42b3d8e74043eed56c8c5625cfad6cfab1143b38;hpb=634dd58a077d3380f90e47a5f6a40a648ad9f17b;p=helm.git diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index 42b3d8e74..ab758c124 100644 --- a/weblib/tutorial/chapter2.ma +++ b/weblib/tutorial/chapter2.ma @@ -124,13 +124,13 @@ also automatically close G1. inductive hypothesis IH: ∃m. x = add m m ∨ x = S (add m m) At this point we should assume the existence of m enjoying the inductive -hypothesis. To eliminate the existential from the context we can just use the case -tactic. This situation where we introduce something into the context and immediately -eliminate it by case analysis is so frequent that Matita provides a convenient -shorthand: you can just type a single "*". -The star symbol should be reminiscent of an explosion: the idea is that you have a -structured hypothesis, and you ask to explode it into its constituents. In the case -of the existential, it allows to pass from a goal of the shape +hypothesis. To eliminate the existential from the context we can just use the +case tactic. This situation where we introduce something into the context and +immediately eliminate it by case analysis is so frequent that Matita provides a +convenient shorthand: you can just type a single "*". +The star symbol should be reminiscent of an explosion: the idea is that you have +a structured hypothesis, and you ask to explode it into its constituents. In the +case of the existential, it allows to pass from a goal of the shape (∃x.P x) → Q to a goal of the shape ∀x.P x → Q @@ -138,32 +138,34 @@ to a goal of the shape |#x * (* At this point we are left with a new goal with the following shape G3: ∀m. x = add m m ∨ x = S (add m m) → .... -We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and then -reason by cases on this hypothesis. It is the same situation as before: we explode the -disjunctive hypothesis into its possible consituents. In the case of a disjunction, the -* tactic allows to pass from a goal of the form +We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and +then reason by cases on this hypothesis. It is the same situation as before: +we explode the disjunctive hypothesis into its possible consituents. In the case +of a disjunction, the * tactic allows to pass from a goal of the form A∨B → Q to two subgoals of the form A → Q and B → Q *) #m * #eqx -(* In the first subgoal, we are under the assumption that x = add m m. The half of (S x) -is hence m, and we have to prove the right branch of the disjunction. -In the second subgoal, we are under the assumption that x = S (add m m). The halh of (S x) -is hence (S m), and have to follow the left branch of the disjunction. +(* In the first subgoal, we are under the assumption that x = add m m. The half +of (S x) is hence m, and we have to prove the right branch of the disjunction. +In the second subgoal, we are under the assumption that x = S (add m m). The halh +of (S x) is hence (S m), and have to follow the left branch of the disjunction. *) [@(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … m) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ | @(a href="cic:/matita/basics/logic/ex.con(0,1,2)"ex_intro/a … (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a m)) normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a/span/span/ ] 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 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〉 +(* 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 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.*) @@ -178,23 +180,24 @@ match n with ] ]. -(* 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 -proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the witness -n and a boolean indicating which one between the two conditions A(n) and B(n) is met. -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,ff〉 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 -for a). The reader is strongly invited to check all remaining details. +(* 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 +proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the +witness n and a boolean indicating which one between the two conditions A(n) and +B(n) is met. 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,ff〉 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 for a). The reader is strongly invited to check all remaining details. Let us now prove that our div2 function has the expected behaviour. *) @@ -214,25 +217,26 @@ lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)" |#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)) - [#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 <a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a @(Hind … H) + [#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) ] qed. (* There is still another possibility, however, namely to mix the program and its -specification into a single entity. The idea is to refine the output type of the div2 -function: it should not be just a generic pair 〈q,r〉 of natural numbers but a specific -pair satisfying the specification of the function. In other words, we need the -possibility to define, for a type A and a property P over A, the subset type -{a:A|P(a)} of all elements a of type A that satisfy the property P. Subset types are -just a particular case of the so called dependent types, that is types that can -depend over arguments (such as arrays of a specified length, taken as a parameter). -These kind of types are quite unusual in traditional programming languages, and their -study is one of the new frontiers of the current research on type systems. - -There is nothing special in a subset type {a:A|P(a)}: it is just a record composed by -an element of a of type A and a proof of P(a). The crucial point is to have a language -reach enough to comprise proofs among its expressions. +specification into a single entity. The idea is to refine the output type of the +div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a +specific pair satisfying the specification of the function. In other words, we need +the possibility to define, for a type A and a property P over A, the subset type +{a:A|P(a)} of all elements a of type A that satisfy the property P. Subset types +are just a particular case of the so called dependent types, that is types that +can depend over arguments (such as arrays of a specified length, taken as a +parameter).These kind of types are quite unusual in traditional programming +languages, and their study is one of the new frontiers of the current research on +type systems. + +There is nothing special in a subset type {a:A|P(a)}: it is just a record composed +by an element of a of type A and a proof of P(a). The crucial point is to have a +language reach enough to comprise proofs among its expressions. *) record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝ @@ -255,7 +259,8 @@ definition div2Pagain : ∀n.a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0, |#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/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 + 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) ] qed.