]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/tutorial/chapter3.ma
- probe: new application to compute some data on the proof objects of
[helm.git] / matita / matita / lib / tutorial / chapter3.ma
1 (*
2 Polymorphism and Higher Order
3
4 *)
5 include "tutorial/chapter2.ma".
6 include "basics/bool.ma".
7
8 (* Matita supports polymorphic data types. The most typical case are polymorphic
9 lists, parametric in the type of their elements: *)
10
11 inductive list (A:Type[0]) : Type[0] ≝
12   | nil: list A
13   | cons: A -> list A -> list A.
14
15 (* The type notation list A is the type of all lists with elements of type A: 
16 it is defined by two constructors: a polymorphic empty list (nil A) and a cons 
17 operation, adding a new head element of type A to a previous list. For instance, 
18 (list nat) and and (list bool) are lists of natural numbers and booleans, 
19 respectively. But we can also form more complex data types, like 
20 (list (list (nat → nat))), that is a list whose elements are lists of functions 
21 from natural numbers to natural numbers.
22
23 Typical elements in (list bool) are for instance,
24   nil nat                                    - the empty list of type nat
25   cons nat true (nil nat)                    - the list containing true
26   cons nat false (cons nat (true (nil nat))) - the list containing false and true
27 and so on. 
28
29 Note that both constructos nil and cons are expecting in input the type parameter:
30 in this case, bool.
31 *)
32
33 (*
34 Defining your own notation
35
36 We now add a bit of notation, in order to make the syntax more readable. In 
37 particular, we would like to write [] instead of (nil A) and a::l instead of 
38 (cons A a l), leaving the system the burden to infer A, whenever possible.
39 *)
40
41 notation "hvbox(hd break :: tl)"
42   right associative with precedence 47
43   for @{'cons $hd $tl}.
44
45 notation "[ list0 x sep ; ]"
46   non associative with precedence 90
47   for ${fold right @'nil rec acc @{'cons $x $acc}}.
48
49 notation "hvbox(l1 break @ l2)"
50   right associative with precedence 47
51   for @{'append $l1 $l2 }.
52
53 interpretation "nil" 'nil = (nil ?).
54 interpretation "cons" 'cons hd tl = (cons ? hd tl).
55
56 (* 
57 Basic operations on lists
58
59 Let us define a few basic functions over lists. Our first example is the 
60 append function, concatenating two lists l1 and l2. The natural way is to proceed 
61 by recursion on l1: if it is empty the result is simply l2, while if l1 = hd::tl 
62 then we recursively append tl and l2 , and then add hd as first element. Note that 
63 the append function itself is polymorphic, and the first argument it takes in input 
64 is the type A of the elements of two lists l1 and l2. 
65 Moreover, since the append function takes in input several parameters, we must also 
66 specify in the its defintion on which one of them we are recurring: in this case l1.
67 If not othewise specified, recursion is supposed to act on the first argument of the
68 function.*)
69
70 let rec append A (l1: list A) l2 on l1 ≝ 
71   match l1 with
72   [ nil ⇒  l2
73   | cons hd tl ⇒  hd :: append A tl l2 ].
74
75 interpretation "append" 'append l1 l2 = (append ? l1 l2).
76
77 (* As usual, the function is executable. For instance, (append A nil l) reduces to
78 l, as shown by the following example: *)
79
80 example nil_append: ∀A.∀l:list A. [] @ l = l.
81 #A #l normalize // qed.
82
83 (* Proving that l @ [] = l is just a bit more complex. The situation is exactly 
84 the same as for the addition operation of the previous chapter: since append is 
85 defined by recutsion over the first argument, the computation of l @ [] is stuck, 
86 and we must proceed by induction on l *) 
87
88 lemma append_nil: ∀A.∀l:list A.l @ [] = l.
89 #A #l (elim l) normalize // qed.
90
91 (* similarly, we can define the two functions head and tail. Since we can only define
92 total functions, we should decide what to do in case the input list is empty. 
93 For tl, it is natural to return the empty list; for hd, we take in input a default 
94 element d of type A to return in this case. *)
95
96 definition head ≝ λA.λl: list A.λd:A.
97   match l with [ nil ⇒ d | cons a _ ⇒ a].
98
99 definition tail ≝  λA.λl: list A.
100   match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
101
102 example ex_head: ∀A.∀a,d,l. head A (a::l) d = a.
103 #A #a #d #l normalize // qed.
104
105 example ex_tail: tail ? (cons ? true []) = [].
106 normalize // qed.
107
108 theorem associative_append: 
109 ∀A.∀l1,l2,l3: list A. (l1 @ l2) @ l3 = l1 @ (l2 @ l3).
110 #A #l1 #l2 #l3 (elim l1) normalize // qed.
111
112 (* Problemi con la notazione *)
113 lemma a_append: ∀A.∀a.∀l:list A. (a::[]) @ l = a::l.
114 // qed.
115
116 theorem append_cons:
117 ∀A.∀a:A.∀l,l1: list A.l@(a::l1)= (l @ (cons ? a [])) @ l1.
118 // qed. 
119
120 (* Other typical functions over lists are those computing the length 
121 of a list, and the function returning the nth element *)
122
123 let rec length (A:Type[0]) (l:list A) on l ≝ 
124 match l with 
125   [ nil ⇒ O
126     | cons a tl ⇒ S (length A tl)].
127
128 let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
129   match n with
130     [O ⇒ head A l d
131     |S m ⇒ nth m A (tail A l) d].
132
133 example ex_length: length ? (cons ? O []) = S O.
134 normalize // qed.
135
136 example ex_nth: nth (S O) ? (cons ? (S O) (cons ? O [])) O = O.
137 normalize // qed.
138
139 (* Proving that the length of l1@l2 is the sum of the lengths of l1
140 and l2 just requires a trivial induction on the first list. *)
141
142  lemma  length_add: ∀A.∀l1,l2:list A. 
143   length ? (l1@l2) = add (length ? l1) (length ? l2).
144 #A #l1 elim l1 normalize // qed. 
145
146 (* 
147 Comparing Costructors
148
149 Let us come to a more interesting question. How can we prove that the empty 
150 list is different from any list with at least one element, that is from any list 
151 of the kind (a::l)? We start defining a simple predicate stating if a list is 
152 empty or not. The predicate is computed by inspection over the list *)
153
154 definition is_nil: ∀A:Type[0].list A → Prop ≝
155 λA.λl.match l with [ nil ⇒ l = [] | cons hd tl ⇒ (l ≠ [])].
156
157 (* Next we need a simple result about negation: if you wish to prove ¬P you are
158 authorized to add P to your hypothesis: *)
159
160 lemma neg_aux : ∀P:Prop. (P → ¬P) → ¬P.
161 #P #PtonegP % /3/ qed. 
162
163 theorem diff_cons_nil:
164 ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
165 #A #l #a @neg_aux #Heq 
166 (* we start assuming the new hypothesis Heq of type a::l = [] using neg_aux. 
167 Next we use the change tactic to pass from the current goal a::l≠ [] to the 
168 expression is_nil a::l, convertible with it. *)
169 (change with (is_nil ? (a::l))) 
170 (* Now, we rewrite with Heq, obtaining (is_nil A []), that reduces to the trivial 
171 goal [] = [] *)
172 >Heq // qed.
173
174 (* As an application of the previous result let us prove that l1@l2 is empty if 
175 and only if both l1 and l2 are empty. 
176 The idea is to proceed by cases on l1: if l1=[] the statement is trivial; on the 
177 other side, if l1 = a::tl, then the hypothesis (a::tl)@l2 = [] is absurd, hence we 
178 can prove anything from it. 
179 When we know we can prove both A and ¬A, a sensible way to proceed is to apply 
180 False_ind: ∀P.False → P to the current goal, that breaks down to prove False, and 
181 then absurd: ∀A:Prop. A → ¬A → False to reduce to the contradictory cases. 
182 Usually, you may invoke automation to take care to solve the absurd case. *)
183
184 lemma nil_to_nil:  ∀A.∀l1,l2:list A.
185   l1@l2 = [] → l1 = [] ∧ l2 = [].
186 #A #l1 cases l1 normalize /2/ #a #tl #l2 #H @False_ind /2/ qed. 
187
188 (* 
189 Higher Order Functionals
190
191 Let us come to some important, higher order, polymorphic functionals 
192 acting over lists. A typical example is the map function, taking a function
193 f:A → B, a list l = [a1; a2; ... ; an] and returning the list 
194 [f a1; f a2; ... ; f an]. *)
195
196 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
197  match l with [ nil ⇒ [] | cons x tl ⇒ f x :: (map A B f tl)].
198
199 (* Another major example is the fold function, that taken a list 
200 l = [a1; a2; ... ;an], a base value b:B, and a function f: A → B → B returns 
201 (f a1 (f a2 (... (f an b)...))). *)
202
203 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
204   match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
205
206 (* As an example of application of foldr, let us use it to define a filter 
207 function that given a list l: list A and a boolean test p:A → bool returns the 
208 sublist of elements satisfying the test. In this case, the result type B of 
209 foldr should be (list A), the base value is [], and f: A → list A →list A is 
210 the function that taken x and l returns x::l, if x satisfies the test, and l 
211 otherwise. We use an if_then_else function included from bool.ma to this purpose. *)
212
213 definition filter ≝ 
214   λT.λp:T → bool.
215   foldr T (list T) (λx,l0. if p x then x::l0 else l0) [].
216
217 (* Here are a couple of simple lemmas on the behaviour of the filter function. 
218 It is often convenient to state such lemmas, in order to be able to use rewriting
219 as an alternative to reduction in proofs: reduction is a bit difficult to control.
220 *)
221
222 lemma filter_true : ∀A,l,a,p. p a = true → 
223   filter A p (a::l) = a :: filter A p l.
224 #A #l #a #p #pa (elim l) normalize >pa // qed.
225
226 lemma filter_false : ∀A,l,a,p. p a = false → 
227   filter A p (a::l) = filter A p l.
228 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
229
230 (* As another example, let us redefine the map function using foldr. The
231 result type B is (list B), the base value b is [], and the fold function 
232 of type A → list B → list B is the function mapping a and l to (f a)::l.
233 *)
234
235 definition map_again ≝ λA,B,f,l. foldr A (list B) (λa,l.f a::l) [] l.
236
237 (* 
238 Extensional equality
239
240 Can we prove that map_again is "the same" as map? We should first of all
241 clarify in which sense we expect the two functions to be equal. Equality in
242 Matita has an intentional meaning: it is the smallest predicate induced by 
243 convertibility, i.e. syntactical equality up to normalization. From an 
244 intentional point of view, map and map_again are not functions, but programs,
245 and they are clearly different. What we would like to say is that the two
246 programs behave in the same way: this is a different, extensional equality 
247 that can be defined in the following way. *)
248
249 definition ExtEq ≝ λA,B:Type[0].λf,g:A→B.∀a:A.f a = g a.
250
251 (* Proving that map and map_again are extentionally equal in the 
252 previous sense can be proved by a trivial structural induction on the list *)
253
254 lemma eq_maps: ∀A,B,f. ExtEq ?? (map A B f) (map_again A B f).
255 #A #B #f #n (elim n) normalize // qed. 
256
257 (* Let us make another remark about extensional equality. It is clear that,
258 if f is extensionally equal to g, then (map A B f) is extensionally equal to
259 (map A B g). Let us prove it. *)
260
261 theorem eq_map : ∀A,B,f,g. ExtEq A B f g → ExtEq ?? (map A B f) (map A B g).
262 #A #B #f #g #eqfg
263  
264 (* the relevant point is that we cannot proceed by rewriting f with g via
265 eqfg, here. Rewriting only works with Matita intensional equality, while here
266 we are dealing with a different predicate, defined by the user. The right way 
267 to proceed is to unfold the definition of ExtEq, and work by induction on l, 
268 as usual when we want to prove extensional equality between functions over 
269 inductive types; again the rest of the proof is trivial. *)
270
271 #l (elim l) normalize // qed.
272
273 (*
274 Big Operators
275
276 Building a library of basic functions, it is important to achieve a 
277 good degree of abstraction and generality, in order to be able to reuse
278 suitable instances of the same function in different context. This has not
279 only the obvious benefit of factorizing code, but especially to avoid 
280 repeating proofs of generic properties over and over again.
281 A really convenient tool is the following combination of fold and filter,
282 that essentially allow you to iterate on every subset of a given enumerated
283 (finite) type, represented as a list. *) 
284
285  let rec fold (A,B:Type[0]) (op:B→B→B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l:B ≝  
286  match l with 
287   [ nil ⇒ b 
288   | cons a l ⇒ if p a then op (f a) (fold A B op b p f l) else
289       (fold A B op b p f l)].
290
291 (* It is also important to spend a few time to introduce some fancy notation
292 for these iterators. *)
293
294  notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
295   with precedence 80
296 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
297
298 notation "\fold [ op , nil ]_{ident i ∈ l } f"
299   with precedence 80
300 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
301
302 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
303
304 theorem fold_true: 
305 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → 
306   \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
307     op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). 
308 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
309
310 theorem fold_false: 
311 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
312 p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
313   \fold[op,nil]_{i ∈ l| p i} (f i).
314 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
315
316 theorem fold_filter: 
317 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
318   \fold[op,nil]_{i ∈ l| p i} (f i) = 
319     \fold[op,nil]_{i ∈ (filter A p l)} (f i).
320 #A #B #a #l #p #op #nil #f elim l //  
321 #a #tl #Hind cases(true_or_false (p a)) #pa 
322   [ >filter_true // > fold_true // >fold_true //
323   | >filter_false // >fold_false // ]
324 qed.
325
326 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
327 {op :2> A → A → A; 
328   nill:∀a. op nil a = a; 
329   nilr:∀a. op a nil = a;
330   assoc: ∀a,b,c.op a (op b c) = op (op a b) c
331 }.
332
333 theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f:A → B.
334  op (\fold[op,nil]_{i ∈ I} (f i)) (\fold[op,nil]_{i ∈ J} (f i)) = 
335    \fold[op,nil]_{i ∈ (I@J)} (f i).
336 #A #B #I #J #nil #op #f (elim I) normalize 
337   [>nill//|#a #tl #Hind <assoc //]
338 qed.