]> matita.cs.unibo.it Git - helm.git/blob - weblib/tutorial/chapter2.ma
commit by user andrea
[helm.git] / weblib / tutorial / chapter2.ma
1 include "basics/logic.ma".
2
3 (* Most of the types we have seen so far are enumerated types, composed by 
4 a finite set of alternatives, and records, composed by tuples of
5 heteregoneous elements. A more interesting case of type definition is
6 when some of the rules defining its elements are recursive, i.e. they
7 allow the formation of more elements of the type in terms of the already
8 defined ones. The most typical case is provided by the natural numbers,
9 that can be defined as the smallest set generated by a constant 0 and a
10 successor function from natural numbers to natural numbers *)
11
12 inductive nat : Type[0] ≝ 
13 | O :nat
14 | S: nat →nat.
15
16 (* The two terms O and S are called constructors: they define the
17 signature of the type, whose objects are the elements freely generated
18 by means of them. So, examples of natural numbers are O, S O, S (S O), 
19 S (S (S O)) and so on. 
20
21 The language of Matita allows the definition of well founded recursive functions
22 over inductive types; in order to guarantee termination of recursion you are
23 only allowed to make recursive calls on structurally smaller arguments than the 
24 ones your received in input. 
25 Most mathematical functions can be naturally defined in this way. For instance, 
26 the sum of two natural numbers can be defined as follows *)
27
28 let rec add n m ≝ 
29 match n with
30 [ O ⇒ m
31 | S a ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (add a m)
32 ].
33
34 (* It is worth to observe that the previous algorithm works by recursion over the
35 first argument. This means that, for instance, (add 0 x) will reduce to x, as expected, 
36 but (add x 0) is stack. How can we prove that, for a generic x, (add x 0) = x? The 
37 mathematical tool do it is called induction. The induction principle states that, 
38 given a property P(n) over natural numbers, if we prove P(0) and prove that, for any 
39 m, P(m) implies P(S m), than we can conclude P(n) for any n. 
40
41 The elim tactic, allow you to apply induction in a vcery simple way. If your
42 goal is P(n), the invocation of
43   elim n
44 will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m).
45 Let us apply it to our case *)
46
47 lemma add_0: ∀a. \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a.
48 #a elim a
49
50 (* If you stop the computation here, you will see on the right the two subgoals 
51     - add O O = O
52     - ∀x. add x 0 = x → add (S x) O = S x
53 After normalization, both goals are trivial.
54 *)
55
56 normalize // qed.
57
58  (* In a similar way, it is convenient to state a lemma about the behaviour of add when the 
59 second argument is not zero. *)
60
61 lemma add_S : ∀a,b. \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a b).
62
63 (* In the same way as before, we proceed by induction over a. *)
64
65 #a #b elim a normalize //
66 qed. 
67
68 (* We are now in the position to prove the commutativity of the sum *)
69
70 theorem add_comm : ∀a,b. \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 a b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 b a.
71 #a elim a normalize
72
73 (* We have two sub goals:
74   G1: ∀b. b = add b O
75   G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x). 
76 G1 is just our lemma add_O. For G2, we start introducing x and the induction
77 hypothesis IH; then, the goal is proved by rewriting using add_S and IH.
78 For Matita, the task is trivial and we can simply close the goal with // *)
79
80 // qed.
81
82 (* Let us now define the following function: *)
83
84 definition twice ≝ λn.\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 n n. 
85
86 (* We are interested to prove that for any natural number m there 
87 exists a natural number m that is the integer half of m. This
88 will give us the opportunity to introduce new connectives
89 and quantifiers, and later on to make some interesting consideration
90 on proofs and computations. *)
91
92 theorem ex_half: ∀n.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6m. n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 m \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 n \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"\ 6twice\ 5/a\ 6 m).
93 #n elim n normalize 
94
95 (* We proceed by induction on n, that breaks down to the following goals:
96   G1: ∃m.O = add O O ∨ O = S (add m m)
97   G2: ∀x.(∃m. x = add m m ∨ x = S (add m m))→ ∃m. S x = add m m ∨ S x = S (add m m)
98 The only way we have to prove an existential goal is by exhibiting the witness, that in the case 
99 of first goal is O. We do it by apply the term called ex_intro instantiated by the witness. 
100 Then, it is clear that we must follow the left branch of the disjunction. One way to do it is by 
101 applying the term or_introl, that is the first constructor of the disjunction. However, 
102 remembering the names of constructors can be annyoing: we can invoke the application of the n-th
103 constructor of an inductive type (inferred by the current goal) by typing %n. At this point 
104 we are left with the subgoal O = add O O, that is closed by computation.
105 It is worth to observe that invoking automation at depth /3/ would also automatically close G1.
106 *)
107   [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6) %1 //
108
109 (* The case of G2 is more complex. We should start introducing x and the inductive hypothesis
110      IH: ∃m. x = add m m ∨ x = S (add m m) 
111 At this point we should assume the existence of m enjoying the inductive hypothesis. To 
112 eliminate the existential from the context we can just use the case tactic. This situation where
113 we introduce something into the context and immediately eliminate it by case analysis is
114 so frequent that Matita provides a convenient shorthand: you can just type a single "*". 
115 The star symbol should be reminiscent of an explosion: the idea is that you have a structured
116 hypothesis, and you ask to explode it into its constituents. In the case of the existential,
117 it allows to pass from a goal of the shape 
118     (∃x.P x) → Q
119 to a goal of the shape
120     ∀x.P x → Q
121 *)
122   |#x *
123 (* At this point we are left with a new goal with the following shape
124   G3: ∀m. x = add m m ∨ x = S (add m m) → ....  
125 We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and then reason by
126 cases on this hypothesis. It is the same situation as before: we explode the disjunctive 
127 hypothesis into its possible consituents. In the case of a disjunction, the * tactic allows
128 to pass from a goal of the form
129     A∨B → Q
130 to two subgoals of the form
131     A → Q  and  B → Q
132 *)
133   #m * #eqx
134 (* In the first subgoal, we are under the assumption that x = add m m. The half of (S x)
135 is hence m, and we have to prove the right branch of the disjunction. 
136 In the second subgoal, we are under the assumption that x = S (add m m). The halh of (S x)
137 is hence (S m), and have to follow the left branch of the disjunction.
138 *)
139   [@(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … m) /2/ | @(\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"\ 6ex_intro\ 5/a\ 6 … (\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 m)) normalize /2/
140   ]
141 qed.