2 include "tutorial/chapter2.ma".
3 include "basics/bool.ma".
5 (* Matita supports polymorphic data types. The most typical case are polymorphic
6 lists, parametric in the type of their elements: *)
8 inductive list (A:Type[0]) : Type[0] :=
10 | cons: A -> list A -> list A.
12 (* The type notation list A is the type of all lists with elements of type A: it is
13 defined by tow constructors: a polymorphic empty list (nil A) and a cons operation,
14 adding a new head element of type A to a previous list. For instance, (list nat) and
15 and (list bool) are lists of natural numbers and booleans, respectively. But we can
16 also form more complex data typea, like (list (list (nat → nat))), that is a list whose
17 elements are lists of functions from natural number to natural numbers.
19 Typical elements in (list bool) are for instance,
20 nil nat - the empty list of type nat
21 cons nat true (nil nat) - the list containing true
22 cons nat false (cons nat (true (nil nat))) - the list containing false and true
25 Note that both constructos nil and cons are expecting in input the type parameter -
28 We now add a bit of notation, in order to make the syntax more readable. In particular,
29 we would like to write [] instead of (nil A) and a::l instead of (cons A a l), leaving
30 the system the burden to infer A, whenever possible.
33 notation "hvbox(hd break :: tl)"
34 right associative with precedence 47
37 notation "[ list0 x sep ; ]"
38 non associative with precedence 90
39 for ${fold right @'nil rec acc @{'cons $x $acc}}.
41 notation "hvbox(l1 break @ l2)"
42 right associative with precedence 47
43 for @{'append $l1 $l2 }.
45 interpretation "nil" 'nil = (nil ?).
46 interpretation "cons" 'cons hd tl = (cons ? hd tl).
48 (* Let us define a few basic functions over lists. Our first example is the append
49 function, concatenating two lists l1 and l2. The natural way is to proceed by recursion
50 on l1: if it is empty the result is simply l2, while if l1 = hd::tl then we
51 recursively append tl and l2 , and then add hd as first element. Note that the append
52 function itself is polymorphic, and the first argument it takes in input is the type
53 A of the elements of two lists l1 and l2.
54 Moreover, since the append function takes in input several parameters, we must also
55 specify in the its defintion on which one of them we are recurring: in this case l1.
56 If not othewise specified, recursion is supposed to act on the first argument of the
59 let rec append A (l1:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) l2 on l1 ≝
62 | cons hd tl ⇒ hd
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6: append A tl l2 ].
64 interpretation "append" 'append l1 l2 = (append ? l1 l2).
66 (* As usual, the function is executable. For instance, (append A nil l) reduces to
67 l, as shown by the following example: *)
69 example nil_append: ∀A.∀l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 l
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 l.
70 #A #l normalize // qed.
72 (* Proving that l @ [] = l is just a bit more complex. The situation is exactly the
73 same as for the addition operation of the previous chapter: since append is defined
74 by recutsion over the first argument, the computation of l @ [] is stuck, and we must
75 proceed by induction on l *)
77 lemma append_nil: ∀A.∀l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.l
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 l.
78 #A #l (elim l) normalize // qed.
80 (* similarly, we can define the two functions head and tail. We should decide what to do in
81 case the input list is empty. For tl, it is natural to return the empty list; for hd, we take
82 in input a default element d of type A to return in this case. *)
84 definition head ≝ λA.λl:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.λd:A.
85 match l with [ nil ⇒ d | cons a _ ⇒ a].
87 definition tail ≝ λA.λl:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
88 match l with [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6] | cons hd tl ⇒ tl].
90 example ex_head: ∀A.∀a,d,l.
\ 5a href="cic:/matita/tutorial/chapter3/head.def(1)"
\ 6head
\ 5/a
\ 6 A (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l) d
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a.
91 #A #a #d #l normalize // qed.
93 (* Problemi con la notazione *)
94 example ex_tail:
\ 5a href="cic:/matita/tutorial/chapter3/tail.def(1)"
\ 6tail
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"
\ 6cons
\ 5/a
\ 6 ?
\ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6])
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6].
97 theorem associative_append:
98 ∀A.∀l1,l2,l3:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A. (l1
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 l2)
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 l3
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 l1
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 (l2
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 l3).
99 #A #l1 #l2 #l3 (elim l1) normalize // qed.
101 (* Problemi con la notazione *)
103 ∀A.∀a:A.∀l,l1:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.l
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6(a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l1)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 (l
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"
\ 6cons
\ 5/a
\ 6 ? a
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]))
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 l1.
107 theorem nil_to_nil: ∀A.∀l1,l2:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 \ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6A.
108 l1
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6l2
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6] → l1
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 l2
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6].
109 #A #l1 #l2 #isnil @(
\ 5a href="cic:/matita/tutorial/chapter3/nil_append_elim.def(3)"
\ 6nil_append_elim
\ 5/a
\ 6 A l1 l2) /2/
112 definition not_nil: ∀A:Type[0].
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A → Prop ≝
113 λA.λl.match l with [ nil ⇒
\ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"
\ 6True
\ 5/a
\ 6| cons hd tl ⇒
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6].
116 ∀A:Type[0].∀l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.∀a:A. a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6].
117 #A #l #a @
\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"
\ 6nmk
\ 5/a
\ 6 #Heq (change with (
\ 5a href="cic:/matita/tutorial/chapter3/not_nil.def(1)"
\ 6not_nil
\ 5/a
\ 6 ? (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l))) >Heq //
122 let rec map (A,B:Type[0]) (f: A → B) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) on l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 B ≝
123 match l with [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6] | cons x tl ⇒ f x
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6: (map A B f tl)].
125 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) on l :B ≝
126 match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
129 λT.λp:T →
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6.
130 \ 5a href="cic:/matita/tutorial/chapter3/foldr.fix(0,4,1)"
\ 6foldr
\ 5/a
\ 6 T (
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 T) (λx,l0.
\ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"
\ 6if_then_else
\ 5/a
\ 6 ? (p x) (x
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l0) l0)
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6].
132 lemma filter_true : ∀A,l,a,p. p a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 →
133 \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:
\ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p l.
134 #A #l #a #p #pa (elim l) normalize >pa // qed.
136 lemma filter_false : ∀A,l,a,p. p a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 →
137 \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p l.
138 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
140 theorem eq_map : ∀A,B,f,g,l. (∀x.f x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 g x) →
\ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"
\ 6map
\ 5/a
\ 6 \ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6A B f l
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter3/map.fix(0,3,1)"
\ 6map
\ 5/a
\ 6 A B g l.
141 #A #B #f #g #l #eqfg (elim l) normalize // qed.
144 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
147 | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
150 (**************************** length ******************************)
152 let rec length (A:Type[0]) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) on l ≝
154 [ nil ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6
155 | cons a tl ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (length A tl)].
157 let rec nth n (A:Type[0]) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) (d:A) ≝
159 [O ⇒
\ 5a href="cic:/matita/tutorial/chapter3/hd.def(1)"
\ 6hd
\ 5/a
\ 6 A l d
160 |S m ⇒ nth m A (
\ 5a href="cic:/matita/tutorial/chapter3/tail.def(1)"
\ 6tail
\ 5/a
\ 6 A l) d].
162 (**************************** fold *******************************)
164 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6) (f:A→B) (l:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) on l :B ≝
167 | cons a l ⇒
\ 5a href="cic:/matita/basics/bool/if_then_else.def(1)"
\ 6if_then_else
\ 5/a
\ 6 ? (p a) (op (f a) (fold A B op b p f l))
168 (fold A B op b p f l)].
170 notation "\fold [ op , nil ]_{ ident i ∈ l | p} f"
172 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
174 notation "\fold [ op , nil ]_{ident i ∈ l } f"
176 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
178 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
181 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6 →
182 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l| p i} (f i)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6
183 op (f a)
\ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ l| p i} (f i).
184 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
187 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
188 p a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"
\ 6false
\ 5/a
\ 6 →
\ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l| p i} (f i)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6
189 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ l| p i} (f i).
190 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
193 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
194 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ l| p i} (f i)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6
195 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ (
\ 5a href="cic:/matita/tutorial/chapter3/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p l)} (f i).
196 #A #B #a #l #p #op #nil #f elim l //
197 #a #tl #Hind cases(
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (p a)) #pa
198 [ >
\ 5a href="cic:/matita/tutorial/chapter3/filter_true.def(3)"
\ 6filter_true
\ 5/a
\ 6 // >
\ 5a href="cic:/matita/tutorial/chapter3/fold_true.def(3)"
\ 6fold_true
\ 5/a
\ 6 // >
\ 5a href="cic:/matita/tutorial/chapter3/fold_true.def(3)"
\ 6fold_true
\ 5/a
\ 6 //
199 | >
\ 5a href="cic:/matita/tutorial/chapter3/filter_false.def(3)"
\ 6filter_false
\ 5/a
\ 6 // >
\ 5a href="cic:/matita/tutorial/chapter3/fold_false.def(3)"
\ 6fold_false
\ 5/a
\ 6 // ]
202 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
204 nill:∀a. op nil a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a;
205 nilr:∀a. op a nil
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a;
206 assoc: ∀a,b,c.op a (op b c)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 op (op a b) c
209 theorem fold_sum: ∀A,B. ∀I,J:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.∀nil.∀op:
\ 5a href="cic:/matita/tutorial/chapter3/Aop.ind(1,0,2)"
\ 6Aop
\ 5/a
\ 6 B nil.∀f.
210 op (
\ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i∈I} (f i)) (
\ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i∈J} (f i))
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6
211 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i∈(I
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6J)} (f i).
212 #A #B #I #J #nil #op #f (elim I) normalize
213 [>
\ 5a href="cic:/matita/tutorial/chapter3/nill.fix(0,2,2)"
\ 6nill
\ 5/a
\ 6 //|#a #tl #Hind <
\ 5a href="cic:/matita/tutorial/chapter3/assoc.fix(0,2,2)"
\ 6assoc
\ 5/a
\ 6 //]