1 (******************************** Induction ***********************************)
3 include "basics/types.ma".
5 (* Most of the types we have seen so far are enumerated types, composed by a
6 finite set of alternatives, and records, composed by tuples of heteregoneous
7 elements. A more interesting case of type definition is when some of the rules
8 defining its elements are recursive, i.e. they allow the formation of more
9 elements of the type in terms of the already defined ones. The most typical case
10 is provided by the natural numbers, that can be defined as the smallest set
11 generated by a constant 0 and a successor function from natural numbers to
14 inductive nat : Type[0] ≝
18 (* The two terms O and S are called constructors: they define the signature of
19 the type, whose objects are the elements freely generated by means of them. So,
20 examples of natural numbers are O, S O, S (S O), S (S (S O)) and so on.
22 The language of Matita allows the definition of well founded recursive functions
23 over inductive types; in order to guarantee termination of recursion you are
24 only allowed to make recursive calls on structurally smaller arguments than the
25 ones you received in input. Most mathematical functions can be naturally defined
26 in this way. For instance, the sum of two natural numbers can be defined as
29 let rec add n (m:nat) ≝
37 (* Observe that the definition of a recursive function requires the keyword
38 "let rec" instead of "definition". The specification of formal parameters is
39 different too. In this case, they come before the body, and do not require a λ.
40 If you need to specify the type of some argument, you need to enclose it in
41 brackets, as follows: (n:nat).
43 By convention, recursion is supposed to operate over the first argument (that
44 means that this is the only argument that is supposed to decrease in the
45 recursive calls). In case you need to work on a different argument, say foo, you
46 can specify it by explicitly mention "on foo" just after the declaration of all
49 (******************************* Elimination **********************************)
51 (* It is worth to observe that the previous algorithm works by recursion over
52 the first argument. This means that, for instance, (add O x) will reduce to x,
53 as expected, but (add x O) is stuck.
54 How can we prove that, for a generic x, (add x O) = x? The mathematical tool to
55 do it is called induction. The induction principle states that, given a property
56 P(n) over natural numbers, if we prove P(0) and prove that, for any m, P(m)
57 implies P(S m), than we can conclude P(n) for any n.
59 The elim tactic, allow you to apply induction in a very simple way. If your goal
60 is P(n), the invocation of elim n will break down your task to prove the two
61 subgoals P(0) and ∀m.P(m) → P(S m).
63 Let us apply it to our case *)
65 lemma add_0: ∀a. add a O = a.
68 (* If you stop the computation here, you will see on the right the two subgoals
70 - ∀x. add x 0 = x → add (S x) O = S x
71 After normalization, both goals are trivial.
76 (* In a similar way, it is convenient to state a lemma about the behaviour of
77 add when the second argument is not zero. *)
79 lemma add_S : ∀a,b. add a (S b) = S (add a b).
81 (* In the same way as before, we proceed by induction over a. *)
83 #a #b elim a normalize //
86 (* We are now in the position to prove the commutativity of the sum *)
88 theorem add_comm : ∀a,b. add a b = add b a.
92 (* We have two sub goals:
94 G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x).
95 G1 is just our lemma add_O. For G2, we start introducing x and the induction
96 hypothesis IH; then, the goal is proved by rewriting using add_S and IH.
97 For Matita, the task is trivial and we can simply close the goal with // *)
103 inductive bool : Type[0] ≝
107 definition nat_of_bool ≝ λb. match b with
112 (* coercion nat_of_bool. ?? *)
114 (******************************** Existential *********************************)
116 (* We are interested to prove that for any natural number n there exists a
117 natural number m that is the integer half of n. This will give us the
118 opportunity to introduce new connectives and quantifiers and, later on, to make
119 some interesting consideration on proofs and computations.
120 Here is the formal statement of the theorem we are interested in: *)
122 definition twice ≝ λn.add n n.
124 theorem ex_half: ∀n.∃m. n = twice m ∨ n = S (twice m).
127 (* We proceed by induction on n, that breaks down to the following goals:
128 G1: ∃m.O = add O O ∨ O = S (add m m)
129 G2: ∀x.(∃m. x = add m m ∨ x = S (add m m))→
130 ∃m. S x = add m m ∨ S x = S (add m m)
131 The only way we have to prove an existential goal is by exhibiting the witness,
132 that in the case of first goal is O. We do it by apply the term called ex_intro
133 instantiated by the witness. Then, it is clear that we must follow the left
134 branch of the disjunction. One way to do it is by applying the term or_introl,
135 that is the first constructor of the disjunction. However, remembering the names
136 of constructors can be annyoing: we can invoke the application of the n-th
137 constructor of an inductive type (inferred by the current goal) by typing %n. At
138 this point we are left with the subgoal O = add O O, that is closed by
139 computation. It is worth to observe that invoking automation at depth /3/ would
140 also automatically close G1.
143 [@(ex_intro … O) %1 //
145 (******************************* Decomposition ********************************)
147 (* The case of G2 is more complex. We should start introducing x and the
149 IH: ∃m. x = add m m ∨ x = S (add m m)
150 At this point we should assume the existence of m enjoying the inductive
151 hypothesis. To eliminate the existential from the context we can just use the
152 case tactic. This situation where we introduce something into the context and
153 immediately eliminate it by case analysis is so frequent that Matita provides a
154 convenient shorthand: you can just type a single "*".
155 The star symbol should be reminiscent of an explosion: the idea is that you have
156 a structured hypothesis, and you ask to explode it into its constituents. In the
157 case of the existential, it allows to pass from a goal of the shape
159 to a goal of the shape
163 (* At this point we are left with a new goal with the following shape
164 G3: ∀m. x = add m m ∨ x = S (add m m) → ....
165 We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and
166 then reason by cases on this hypothesis. It is the same situation as before:
167 we explode the disjunctive hypothesis into its possible consituents. In the case
168 of a disjunction, the * tactic allows to pass from a goal of the form
170 to two subgoals of the form
174 (* In the first subgoal, we are under the assumption that x = add m m. The half
175 of (S x) is hence m, and we have to prove the right branch of the disjunction.
176 In the second subgoal, we are under the assumption that x = S (add m m). The
177 halh of (S x) is hence (S m), and have to follow the left branch of the
179 [@(ex_intro … m) /2/ | @(ex_intro … (S m)) normalize /2/
183 (**************************** Computing vs. Proving ***************************)
185 (* Instead of proving the existence of a number corresponding to the half of n,
186 we could be interested in computing it. The best way to do it is to define this
187 division operation together with the remainder, that in our case is just a
188 boolean value: tt if the input term is even, and ff if the input term is odd.
189 Since we must return a pair, we could use a suitably defined record type, or
190 simply a product type nat × bool, defined in the basic library. The product type
191 is just a sort of general purpose record, with standard fields fst and snd,
193 A pair of values n and m is written (pair … m n) or \langle n,m \rangle -
194 visually rendered as 〈n,m〉.
195 We first write down the function, and then discuss it.*)
201 let 〈q,r〉 ≝ (div2 a) in
208 (* The function is computed by recursion over the input n. If n is 0, then the
209 quotient is 0 and the remainder is tt. If n = S a, we start computing the half
210 of a, say 〈q,b〉. Then we have two cases according to the possible values of b:
211 if b is tt, then we must return 〈q,ff〉, while if b = ff then we must return
214 It is important to point out the deep, substantial analogy between the algorithm
215 for computing div2 and the the proof of ex_half. In particular ex_half returns a
216 proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the
217 witness n and a boolean indicating which one between the two conditions A(n) and
218 B(n) is met. This is precisely the quotient-remainder pair returned by div2.
219 In both cases we proceed by recurrence (respectively, induction or recursion)
220 over the input argument n. In case n = 0, we conclude the proof in ex_half by
221 providing the witness O and a proof of A(O); this corresponds to returning the
222 pair 〈O,ff〉 in div2. Similarly, in the inductive case n = S a, we must exploit
223 the inductive hypothesis for a (i.e. the result of the recursive call),
224 distinguishing two subcases according to the the two possibilites A(a) or B(a)
225 (i.e. the two possibile values of the remainder for a). The reader is strongly
226 invited to check all remaining details. *)
228 (****************************** Destruct **************************************)
230 (* Let us now prove that our div2 function has the expected behaviour.
231 We start proving a few easy lemmas:
234 lemma div2SO: ∀n,q. div2 n = 〈q,ff〉 → div2 (S n) = 〈q,tt〉.
235 #n #q #H normalize >H normalize // qed.
237 lemma div2S1: ∀n,q. div2 n = 〈q,tt〉 → div2 (S n) = 〈S q,ff〉.
238 #n #q #H normalize >H normalize // qed.
240 (* Here is our statement, where $\mathit{nat\_of\_bool}$ is the above coercions:
243 lemma div2_ok: ∀n,q,r. div2 n = 〈q,r〉 → n = add (nat_of_bool r) (twice q).
245 (* We proceed by induction on $n$, that produces two subgoals. *)
250 (* After introducing the hypothesis q,r and H, the first subgoal looks like the
257 ---------------------------
259 (O=add (nat_of_bool r) (twice q))
261 Note that the right hand side of equation H is not in normal form, and we would
262 like to reduce it. We can do it by specifying a pattern for the normalize
263 tactic, introduced by the ``in'' keyword, and delimited by a semicolon. In this
264 case, the pattern is just the name of the hypothesis and we should write *)
268 (* that transforms H as follows:
272 From such an hypothesis we expect to be able to conclude that q=O$ and r=false.
273 The tactic that provides this functionality is called "destruct". The tactic
274 decomposes an equality between structured terms in smaller components: if an
275 absurd situation is recognized (like an equality between 0 and (S n)) the
276 current goal is automatically closed; otherwise, all derived equations where one
277 of the sides is a variable are automatically substituted in the proof, and the
278 remaining equations are added to the context (replacing the original equation).
280 In the above case, by invoking destruct we would get the two equations q=O and
281 r=false; these are immediately substituted in the goal, that can now be solved
282 by direct computation. *)
286 (********************************** Cut ***************************************)
288 (* Let's come to the second subgoal *)
290 (* After performing the previous introductions, the current goal looks like the
295 Hind : (∀q:nat.∀r:bool.div2 a=〈q,r〉→a=add (nat_of_bool r) (twice q))
298 ---------------------------
299 div2 (S a)=〈q,r〉→S a=add (nat_of_bool r) (twice q)
301 We should proceed by cases on the remainder of (div2 a), but before doing it we
302 should emphasize the fact that (div2 a) can be expressed as a pair of its two
303 projections. The tactics that allows to introduce a new hypothesis, splitting a
304 complex proofs into smaller components is called "cut".
305 The invocation of "cut A" transforms the current goal G into the two subgoals A
306 and A→G (A is called the cut formula).
308 In our case, the cut formula is
309 div2 a = 〈fst … (div2 a), snd … (div2 a)〉
310 whose proof is trivial
313 cut (div2 a = 〈fst … (div2 a), snd … (div2 a)〉) [//]
315 (* We now proceed by induction on (snd … (div2 a)); the two subgoals are
316 respectively closed using the two lemmas div2SO and div2S1 in conjunction with
317 the inductive hypothesis, and do not contain additional challenges. *)
319 cases (snd … (div2 a))
320 [#H >(div2S1 … H) #H1 destruct normalize @eq_f >add_S @(Hind … H)
321 |#H >(div2SO … H) #H1 destruct normalize @eq_f @(Hind … H)
325 (********************** Mixing proofs and computations ************************)
327 (* There is still another possibility, however, namely to mix the program and
328 its specification into a single entity. The idea is to refine the output type of
329 the div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers
330 but a specific pair satisfying the specification of the function. In other
331 words, we need the possibility to define, for a type A and a property P over A,
332 the subset type {a:A|P(a)} of all elements a of type A that satisfy the property
333 P. Subset types are just a particular case of the so called dependent types,
334 that is types that can depend over arguments (such as arrays of a specified
335 length, taken as a parameter).These kind of types are quite unusual in
336 traditional programming languages, and their study is one of the new frontiers
337 of the current research on type systems.
339 There is nothing special in a subset type {a:A|P(a)}: it is just a record
340 composed by an element of a of type A and a proof of P(a). The crucial point is
341 to have a language reach enough to comprise proofs among its expressions.
344 record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝
348 definition qr_spec ≝ λn.λp.∀q,r. p = 〈q,r〉 → n = add (nat_of_bool r) (twice q).
350 (* We can now construct a function from n to {p|qr_spec n p} by composing the
351 objects we already have *)
353 definition div2P: ∀n. Sub (nat×bool) (qr_spec n) ≝ λn.
354 mk_Sub ?? (div2 n) (div2_ok n).
356 (* But we can also try do directly build such an object *)
358 definition div2Pagain : ∀n.Sub (nat×bool) (qr_spec n).
360 [@(mk_Sub … 〈O,ff〉) normalize #q #r #H destruct //
362 cut (p = 〈fst … p, snd … p〉) [//]
364 [#H @(mk_Sub … 〈S (fst … p),ff〉) #q #r #H1 destruct @eq_f >add_S @(qrspec … H)
365 |#H @(mk_Sub … 〈fst … p,tt〉) #q #r #H1 destruct @eq_f @(qrspec … H)
369 example full7: (div2Pagain (S(S(S(S(S(S(S O)))))))) = ?.
372 example quotient7: witness … (div2Pagain (S(S(S(S(S(S(S O)))))))) = ?.
375 example quotient8: witness … (div2Pagain (twice (twice (twice (twice (S O))))))
376 = 〈twice (twice (twice (S O))), ff〉.