weblib/tutorial/chapter3.ma

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