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) ≝
35 (* Observe that the definition of a recursive function requires the keyword
36 "let rec" instead of "definition". The specification of formal parameters is
37 different too. In this case, they come before the body, and do not require a λ.
38 If you need to specify the type of some argument, you need to enclose it in
39 brackets, as follows: (n:nat).
41 By convention, recursion is supposed to operate over the first argument (that
42 means that this is the only argument that is supposed to decrease in the
43 recursive calls). In case you need to work on a different argument, say foo, you
44 can specify it by explicitly mention "on foo" just after the declaration of all
47 (******************************* Elimination **********************************)
49 (* It is worth to observe that the previous algorithm works by recursion over
50 the first argument. This means that, for instance, (add O x) will reduce to x,
51 as expected, but (add x O) is stuck.
52 How can we prove that, for a generic x, (add x O) = x? The mathematical tool to
53 do it is called induction. The induction principle states that, given a property
54 P(n) over natural numbers, if we prove P(0) and prove that, for any m, P(m)
55 implies P(S m), than we can conclude P(n) for any n.
57 The elim tactic, allow you to apply induction in a very simple way. If your goal
58 is P(n), the invocation of elim n will break down your task to prove the two
59 subgoals P(0) and ∀m.P(m) → P(S m).
61 Let us apply it to our case *)
63 lemma add_0: ∀a. add a O = a.
66 (* If you stop the computation here, you will see on the right the two subgoals
68 - ∀x. add x 0 = x → add (S x) O = S x
69 After normalization, both goals are trivial.
74 (* In a similar way, it is convenient to state a lemma about the behaviour of
75 add when the second argument is not zero. *)
77 lemma add_S : ∀a,b. add a (S b) = S (add a b).
79 (* In the same way as before, we proceed by induction over a. *)
81 #a #b elim a normalize //
84 (* We are now in the position to prove the commutativity of the sum *)
86 theorem add_comm : ∀a,b. add a b = add b a.
90 (* We have two sub goals:
92 G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x).
93 G1 is just our lemma add_O. For G2, we start introducing x and the induction
94 hypothesis IH; then, the goal is proved by rewriting using add_S and IH.
95 For Matita, the task is trivial and we can simply close the goal with // *)
101 inductive bool : Type[0] ≝
105 definition nat_of_bool ≝ λb. match b with
110 (* coercion nat_of_bool. ?? *)
112 (******************************** Existential *********************************)
114 (* We are interested to prove that for any natural number n there exists a
115 natural number m that is the integer half of n. This will give us the
116 opportunity to introduce new connectives and quantifiers and, later on, to make
117 some interesting consideration on proofs and computations.
118 Here is the formal statement of the theorem we are interested in: *)
120 definition twice ≝ λn.add n n.
122 theorem ex_half: ∀n.∃m. n = twice m ∨ n = S (twice m).
125 (* We proceed by induction on n, that breaks down to the following goals:
126 G1: ∃m.O = add O O ∨ O = S (add m m)
127 G2: ∀x.(∃m. x = add m m ∨ x = S (add m m))→
128 ∃m. S x = add m m ∨ S x = S (add m m)
129 The only way we have to prove an existential goal is by exhibiting the witness,
130 that in the case of first goal is O. We do it by apply the term called ex_intro
131 instantiated by the witness. Then, it is clear that we must follow the left
132 branch of the disjunction. One way to do it is by applying the term or_introl,
133 that is the first constructor of the disjunction. However, remembering the names
134 of constructors can be annyoing: we can invoke the application of the n-th
135 constructor of an inductive type (inferred by the current goal) by typing %n. At
136 this point we are left with the subgoal O = add O O, that is closed by
137 computation. It is worth to observe that invoking automation at depth /3/ would
138 also automatically close G1.
141 [@(ex_intro … O) %1 //
143 (******************************* Decomposition ********************************)
145 (* The case of G2 is more complex. We should start introducing x and the
147 IH: ∃m. x = add m m ∨ x = S (add m m)
148 At this point we should assume the existence of m enjoying the inductive
149 hypothesis. To eliminate the existential from the context we can just use the
150 case tactic. This situation where we introduce something into the context and
151 immediately eliminate it by case analysis is so frequent that Matita provides a
152 convenient shorthand: you can just type a single "*".
153 The star symbol should be reminiscent of an explosion: the idea is that you have
154 a structured hypothesis, and you ask to explode it into its constituents. In the
155 case of the existential, it allows to pass from a goal of the shape
157 to a goal of the shape
161 (* At this point we are left with a new goal with the following shape
162 G3: ∀m. x = add m m ∨ x = S (add m m) → ....
163 We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and
164 then reason by cases on this hypothesis. It is the same situation as before:
165 we explode the disjunctive hypothesis into its possible consituents. In the case
166 of a disjunction, the * tactic allows to pass from a goal of the form
168 to two subgoals of the form
172 (* In the first subgoal, we are under the assumption that x = add m m. The half
173 of (S x) is hence m, and we have to prove the right branch of the disjunction.
174 In the second subgoal, we are under the assumption that x = S (add m m). The
175 halh of (S x) is hence (S m), and have to follow the left branch of the
177 [@(ex_intro … m) /2/ | @(ex_intro … (S m)) normalize /2/
181 (**************************** Computing vs. Proving ***************************)
183 (* Instead of proving the existence of a number corresponding to the half of n,
184 we could be interested in computing it. The best way to do it is to define this
185 division operation together with the remainder, that in our case is just a
186 boolean value: tt if the input term is even, and ff if the input term is odd.
187 Since we must return a pair, we could use a suitably defined record type, or
188 simply a product type nat × bool, defined in the basic library. The product type
189 is just a sort of general purpose record, with standard fields fst and snd,
191 A pair of values n and m is written (pair … m n) or \langle n,m \rangle -
192 visually rendered as 〈n,m〉.
193 We first write down the function, and then discuss it.*)
199 let 〈q,r〉 ≝ (div2 a) in
206 (* The function is computed by recursion over the input n. If n is 0, then the
207 quotient is 0 and the remainder is tt. If n = S a, we start computing the half
208 of a, say 〈q,b〉. Then we have two cases according to the possible values of b:
209 if b is tt, then we must return 〈q,ff〉, while if b = ff then we must return
212 It is important to point out the deep, substantial analogy between the algorithm
213 for computing div2 and the the proof of ex_half. In particular ex_half returns a
214 proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the
215 witness n and a boolean indicating which one between the two conditions A(n) and
216 B(n) is met. This is precisely the quotient-remainder pair returned by div2.
217 In both cases we proceed by recurrence (respectively, induction or recursion)
218 over the input argument n. In case n = 0, we conclude the proof in ex_half by
219 providing the witness O and a proof of A(O); this corresponds to returning the
220 pair 〈O,ff〉 in div2. Similarly, in the inductive case n = S a, we must exploit
221 the inductive hypothesis for a (i.e. the result of the recursive call),
222 distinguishing two subcases according to the the two possibilites A(a) or B(a)
223 (i.e. the two possibile values of the remainder for a). The reader is strongly
224 invited to check all remaining details. *)
226 (****************************** Destruct **************************************)
228 (* Let us now prove that our div2 function has the expected behaviour.
229 We start proving a few easy lemmas:
232 lemma div2SO: ∀n,q. div2 n = 〈q,ff〉 → div2 (S n) = 〈q,tt〉.
233 #n #q #H normalize >H normalize // qed.
235 lemma div2S1: ∀n,q. div2 n = 〈q,tt〉 → div2 (S n) = 〈S q,ff〉.
236 #n #q #H normalize >H normalize // qed.
238 (* Here is our statement, where $\mathit{nat\_of\_bool}$ is the above coercions:
241 lemma div2_ok: ∀n,q,r. div2 n = 〈q,r〉 → n = add (nat_of_bool r) (twice q).
243 (* We proceed by induction on $n$, that produces two subgoals. *)
248 (* After introducing the hypothesis q,r and H, the first subgoal looks like the
255 ---------------------------
257 (O=add (nat_of_bool r) (twice q))
259 Note that the right hand side of equation H is not in normal form, and we would
260 like to reduce it. We can do it by specifying a pattern for the normalize
261 tactic, introduced by the ``in'' keyword, and delimited by a semicolon. In this
262 case, the pattern is just the name of the hypothesis and we should write *)
266 (* that transforms H as follows:
270 From such an hypothesis we expect to be able to conclude that q=O$ and r=false.
271 The tactic that provides this functionality is called "destruct". The tactic
272 decomposes an equality between structured terms in smaller components: if an
273 absurd situation is recognized (like an equality between 0 and (S n)) the
274 current goal is automatically closed; otherwise, all derived equations where one
275 of the sides is a variable are automatically substituted in the proof, and the
276 remaining equations are added to the context (replacing the original equation).
278 In the above case, by invoking destruct we would get the two equations q=O and
279 r=false; these are immediately substituted in the goal, that can now be solved
280 by direct computation. *)
284 (********************************** Cut ***************************************)
286 (* Let's come to the second subgoal *)
288 (* After performing the previous introductions, the current goal looks like the
293 Hind : (∀q:nat.∀r:bool.div2 a=〈q,r〉→a=add (nat_of_bool r) (twice q))
296 ---------------------------
297 div2 (S a)=〈q,r〉→S a=add (nat_of_bool r) (twice q)
299 We should proceed by cases on the remainder of (div2 a), but before doing it we
300 should emphasize the fact that (div2 a) can be expressed as a pair of its two
301 projections. The tactics that allows to introduce a new hypothesis, splitting a
302 complex proofs into smaller components is called "cut".
303 The invocation of "cut A" transforms the current goal G into the two subgoals A
304 and A→G (A is called the cut formula).
306 In our case, the cut formula is
307 div2 a = 〈fst … (div2 a), snd … (div2 a)〉
308 whose proof is trivial
311 cut (div2 a = 〈fst … (div2 a), snd … (div2 a)〉) [//]
313 (* We now proceed by induction on (snd … (div2 a)); the two subgoals are
314 respectively closed using the two lemmas div2SO and div2S1 in conjunction with
315 the inductive hypothesis, and do not contain additional challenges. *)
317 cases (snd … (div2 a))
318 [#H >(div2S1 … H) #H1 destruct normalize @eq_f >add_S @(Hind … H)
319 |#H >(div2SO … H) #H1 destruct normalize @eq_f @(Hind … H)
323 (********************** Mixing proofs and computations ************************)
325 (* There is still another possibility, however, namely to mix the program and
326 its specification into a single entity. The idea is to refine the output type of
327 the div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers
328 but a specific pair satisfying the specification of the function. In other
329 words, we need the possibility to define, for a type A and a property P over A,
330 the subset type {a:A|P(a)} of all elements a of type A that satisfy the property
331 P. Subset types are just a particular case of the so called dependent types,
332 that is types that can depend over arguments (such as arrays of a specified
333 length, taken as a parameter).These kind of types are quite unusual in
334 traditional programming languages, and their study is one of the new frontiers
335 of the current research on type systems.
337 There is nothing special in a subset type {a:A|P(a)}: it is just a record
338 composed by an element of a of type A and a proof of P(a). The crucial point is
339 to have a language reach enough to comprise proofs among its expressions.
342 record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝
346 definition qr_spec ≝ λn.λp.∀q,r. p = 〈q,r〉 → n = add (nat_of_bool r) (twice q).
348 (* We can now construct a function from n to {p|qr_spec n p} by composing the
349 objects we already have *)
351 definition div2P: ∀n. Sub (nat×bool) (qr_spec n) ≝ λn.
352 mk_Sub ?? (div2 n) (div2_ok n).
354 (* But we can also try do directly build such an object *)
356 definition div2Pagain : ∀n.Sub (nat×bool) (qr_spec n).
358 [@(mk_Sub … 〈O,ff〉) normalize #q #r #H destruct //
360 cut (p = 〈fst … p, snd … p〉) [//]
362 [#H @(mk_Sub … 〈S (fst … p),ff〉) #q #r #H1 destruct @eq_f >add_S @(qrspec … H)
363 |#H @(mk_Sub … 〈fst … p,tt〉) #q #r #H1 destruct @eq_f @(qrspec … H)
367 example full7: (div2Pagain (S(S(S(S(S(S(S O)))))))) = ?.
370 example quotient7: witness … (div2Pagain (S(S(S(S(S(S(S O)))))))) = ?.
373 example quotient8: witness … (div2Pagain (twice (twice (twice (twice (S O))))))
374 = 〈twice (twice (twice (S O))), ff〉.
377 (********************)
379 inductive Pari : nat → Prop ≝
381 | pari2 : ∀x. Pari x → Pari (S (S x)).
383 definition natPari ≝ Sub nat Pari.
385 definition addPari: natPari → natPari → natPari.
386 * #a #Ha * #b #Hb check mk_Sub @(mk_Sub … (add a b))
389 |#x #Hx #Hind normalize @pari2 @Hind