From f59274b53205d0ffc399e239de333de106b5c642 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Mon, 12 Dec 2011 13:53:54 +0000 Subject: [PATCH] commit by user andrea --- weblib/tutorial/chapter2.ma | 80 +++++++++++++++++++------------------ 1 file changed, 41 insertions(+), 39 deletions(-) diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma index 42b3d8e74..fffe5e1cc 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,31 +138,32 @@ 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 - +(* 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,10 +179,10 @@ 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〉. +(* 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 @@ -220,19 +221,20 @@ lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)" 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] ≝ -- 2.39.2