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