weblib/tutorial/chapter3.ma

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