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.
106 (* Other typical functions over lists are those computing the length
107 of a list, and the function returning the nth element *)
109 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 ≝
111 [ nil ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6
112 | cons a tl ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (length A tl)].
114 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) ≝
116 [O ⇒
\ 5a href="cic:/matita/tutorial/chapter3/hd.def(1)"
\ 6hd
\ 5/a
\ 6 A l d
117 |S m ⇒ nth m A (
\ 5a href="cic:/matita/tutorial/chapter3/tail.def(1)"
\ 6tail
\ 5/a
\ 6 A l) d].
119 example ex_length:
\ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"
\ 6length
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"
\ 6cons
\ 5/a
\ 6 ?
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 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 href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6.
122 example ex_nth:
\ 5a href="cic:/matita/tutorial/chapter3/nth.fix(0,0,2)"
\ 6nth
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6) ? (
\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"
\ 6cons
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6) (
\ 5a href="cic:/matita/tutorial/chapter3/list.con(0,2,1)"
\ 6cons
\ 5/a
\ 6 ?
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]))
\ 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 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6.
125 lemma length_add: ∀A.∀l1,l2:
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A.
126 \ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"
\ 6length
\ 5/a
\ 6 ? (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 href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"
\ 6length
\ 5/a
\ 6 ? l1) (
\ 5a href="cic:/matita/tutorial/chapter3/length.fix(0,1,1)"
\ 6length
\ 5/a
\ 6 ? l2).
127 #A #l1 elim l1 normalize // qed.
129 (* Let us come to a more interesting question. How can we prove that the empty list is
130 different from any list with at least one element, that is from any list of the kind (a::l)?
131 We start defining a simple predicate stating if a list is empty or not. The predicate
132 is computed by inspection over the list *)
134 definition is_nil: ∀A:Type[0].
\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A → Prop ≝
135 λA.λl.match l with [ nil ⇒ l
\ 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] | cons hd tl ⇒ (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])].
137 (* Next we need a simple result about negation: if you wish to prove ¬P you are
138 authorized to add P to your hypothesis: *)
140 lemma neg_aux : ∀P:Prop. (P →
\ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6P) →
\ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6P.
141 #P #PtonegP % /3/ qed.
143 theorem diff_cons_nil:
144 ∀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].
145 #A #l #a @
\ 5a href="cic:/matita/tutorial/chapter3/neg_aux.def(3)"
\ 6neg_aux
\ 5/a
\ 6 #Heq
146 (* we start assuming the new hypothesis Heq of type a::l = [] using neg_aux.
147 Next we use the change tactic to pass from the current goal a::l≠ [] to the expression
148 is_nil a::l, convertible with it. *)
149 (change with (
\ 5a href="cic:/matita/tutorial/chapter3/is_nil.def(1)"
\ 6is_nil
\ 5/a
\ 6 ? (a
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l)))
150 (* Now, we rewrite with Heq, obtaining (is_nil A []), that reduces to the trivial
154 (* As an application of the previous result let us prove that l1@l2 is empty if and
155 only if both l1 and l2 are empty. The idea is to proceed by cases on l1: if l1=[] the
156 statement is trivial; on the other side, if l1 = a::tl, then the hypothesis
157 (a::tl)@l2 = [] is absurd, hence we can prove anything from it. When we know we can
158 prove both A and ¬A, a sensible way to proceed is to apply False_ind: ∀P.False → P to the
159 current goal, that breaks down to prove False, and then absurd: ∀A:Prop. A → ¬A → False
160 to reduce to the contradictory cases. Usually, you may invoke automation to take care
161 to solve the absurd case. *)
163 lemma 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.
164 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].
165 #A #l1 cases l1 normalize /2/ #a #tl #l2 #H @
\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"
\ 6False_ind
\ 5/a
\ 6 /2/ qed.
169 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 ≝
170 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)].
172 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 ≝
173 match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
176 λT.λp:T →
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6.
177 \ 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].
179 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 →
180 \ 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.
181 #A #l #a #p #pa (elim l) normalize >pa // qed.
183 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 →
184 \ 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.
185 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
187 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.
188 #A #B #f #g #l #eqfg (elim l) normalize // qed.
191 let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
194 | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
197 (**************************** fold *******************************)
199 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 ≝
202 | 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))
203 (fold A B op b p f l)].
205 notation "\fold [ op , nil ]_{ ident i ∈ l | p} f"
207 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
209 notation "\fold [ op , nil ]_{ident i ∈ l } f"
211 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
213 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
216 ∀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 →
217 \ 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
218 op (f a)
\ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ l| p i} (f i).
219 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
222 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
223 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
224 \ 5a title="\fold" href="cic:/fakeuri.def(1)"
\ 6\fold
\ 5/a
\ 6[op,nil]_{i ∈ l| p i} (f i).
225 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
228 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
229 \ 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
230 \ 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).
231 #A #B #a #l #p #op #nil #f elim l //
232 #a #tl #Hind cases(
\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"
\ 6true_or_false
\ 5/a
\ 6 (p a)) #pa
233 [ >
\ 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 //
234 | >
\ 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 // ]
237 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
239 nill:∀a. op nil a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a;
240 nilr:∀a. op a nil
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a;
241 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
244 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.
245 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
246 \ 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).
247 #A #B #I #J #nil #op #f (elim I) normalize
248 [>
\ 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 //]