+(*
+\ 5h1 class="section"\ 6Polymorphism and Higher Order\ 5/h1\ 6
+*)
include "tutorial/chapter2.ma".
include "basics/bool.ma".
(* Matita supports polymorphic data types. The most typical case are polymorphic
lists, parametric in the type of their elements: *)
-inductive list (A:Type[0]) : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="list"\ 6inductive list (A:Type[0]) : Type[0] ≝
| nil: list A
| cons: A -> list A -> list A.
Note that both constructos nil and cons are expecting in input the type parameter:
in this case, bool.
+*)
+(*
+\ 5h2 class="section"\ 6Defining your own notation\ 5/h2\ 6
We now add a bit of notation, in order to make the syntax more readable. In
particular, we would like to write [] instead of (nil A) and a::l instead of
(cons A a l), leaving the system the burden to infer A, whenever possible.
interpretation "nil" 'nil = (nil ?).
interpretation "cons" 'cons hd tl = (cons ? hd tl).
-(* Let us define a few basic functions over lists. Our first example is the
+(*
+\ 5h2 class="section"\ 6Basic operations on lists\ 5/h2\ 6
+Let us define a few basic functions over lists. Our first example is the
append function, concatenating two lists l1 and l2. The natural way is to proceed
by recursion on l1: if it is empty the result is simply l2, while if l1 = hd::tl
then we recursively append tl and l2 , and then add hd as first element. Note that
If not othewise specified, recursion is supposed to act on the first argument of the
function.*)
-let rec append A (l1: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) l2 on l1 ≝
+\ 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 ≝
match l1 with
[ nil ⇒ l2
- | cons hd tl ⇒ hd \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6: append A tl l2 ].
+ | 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 ].
interpretation "append" 'append l1 l2 = (append ? l1 l2).
(* As usual, the function is executable. For instance, (append A nil l) reduces to
l, as shown by the following example: *)
-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.
+\ 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.
#A #l normalize // qed.
(* Proving that l @ [] = l is just a bit more complex. The situation is exactly
defined by recutsion over the first argument, the computation of l @ [] is stuck,
and we must proceed by induction on l *)
-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.
+\ 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.
#A #l (elim l) normalize // qed.
(* similarly, we can define the two functions head and tail. Since we can only define
For tl, it is natural to return the empty list; for hd, we take in input a default
element d of type A to return in this case. *)
-definition head ≝ λA.λl: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.
+\ 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.
match l with [ nil ⇒ d | cons a _ ⇒ a].
-definition tail ≝ λA.λl: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
- match l with [ nil ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] | cons hd tl ⇒ tl].
+\ 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.
+ 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].
-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.
+\ 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.
#A #a #d #l normalize // qed.
-(* Problemi con la notazione *)
-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].
+\ 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.
normalize // qed.
-theorem associative_append:
+\ 5img class="anchor" src="icons/tick.png" id="associative_append"\ 6theorem associative_append:
∀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).
#A #l1 #l2 #l3 (elim l1) normalize // qed.
(* Problemi con la notazione *)
-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.
+\ 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.
// qed.
-theorem append_cons:
-∀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.
+\ 5img class="anchor" src="icons/tick.png" id="append_cons"\ 6theorem append_cons:
+∀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.
// qed.
(* Other typical functions over lists are those computing the length
of a list, and the function returning the nth element *)
-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 ≝
+\ 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 ≝
match l with
[ nil ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6
| cons a tl ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (length A tl)].
-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) ≝
+\ 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) ≝
match n with
[O ⇒ \ 5a href="cic:/matita/tutorial/chapter3/head.def(1)"\ 6head\ 5/a\ 6 A l d
|S m ⇒ nth m A (\ 5a href="cic:/matita/tutorial/chapter3/tail.def(1)"\ 6tail\ 5/a\ 6 A l) d].
-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.
+\ 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.
normalize // qed.
-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.
+\ 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.
normalize // qed.
(* Proving that the length of l1@l2 is the sum of the lengths of l1
and l2 just requires a trivial induction on the first list. *)
- lemma length_add: ∀A.∀l1,l2:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.
+ \ 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.
\ 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).
#A #l1 elim l1 normalize // qed.
-(* Let us come to a more interesting question. How can we prove that the empty
+(*
+\ 5h2 class="section"\ 6Comparing Costructors\ 5/h2\ 6
+Let us come to a more interesting question. How can we prove that the empty
list is different from any list with at least one element, that is from any list
of the kind (a::l)? We start defining a simple predicate stating if a list is
empty or not. The predicate is computed by inspection over the list *)
-definition is_nil: ∀A:Type[0].\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
-λ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])].
+\ 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 ≝
+λ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)].
(* Next we need a simple result about negation: if you wish to prove ¬P you are
authorized to add P to your hypothesis: *)
-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.
+\ 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.
#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.
-theorem diff_cons_nil:
-∀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].
+\ 5img class="anchor" src="icons/tick.png" id="diff_cons_nil"\ 6theorem diff_cons_nil:
+∀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.
#A #l #a @\ 5a href="cic:/matita/tutorial/chapter3/neg_aux.def(3)"\ 6neg_aux\ 5/a\ 6 #Heq
(* we start assuming the new hypothesis Heq of type a::l = [] using neg_aux.
Next we use the change tactic to pass from the current goal a::l≠ [] to the
expression is_nil a::l, convertible with it. *)
-(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)))
+(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)))
(* Now, we rewrite with Heq, obtaining (is_nil A []), that reduces to the trivial
goal [] = [] *)
>Heq // qed.
then absurd: ∀A:Prop. A → ¬A → False to reduce to the contradictory cases.
Usually, you may invoke automation to take care to solve the absurd case. *)
-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.
- 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].
+\ 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.
+ 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.
#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.
-(* Let us come to some important, higher order, polymorphic functionals
+(*
+\ 5h2 class="section"\ 6Higher Order Functionals\ 5/h2\ 6
+Let us come to some important, higher order, polymorphic functionals
acting over lists. A typical example is the map function, taking a function
f:A → B, a list l = [a1; a2; ... ; an] and returning the list
[f a1; f a2; ... ; f an]. *)
-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 ≝
- 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)].
+\ 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 ≝
+ 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)].
(* Another major example is the fold function, that taken a list
l = [a1; a2; ... ;an], a base value b:B, and a function f: A → B → B returns
(f a1 (f a2 (... (f an b)...))). *)
-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 ≝
+\ 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 ≝
match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
(* As an example of application of foldr, let us use it to define a filter
the function that taken x and l returns x::l, if x satisfies the test, and l
otherwise. We use an if_then_else function included from bool.ma to this purpose. *)
-definition filter ≝
+\ 5img class="anchor" src="icons/tick.png" id="filter"\ 6definition filter ≝
λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
- \ 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].
+ \ 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.
(* Here are a couple of simple lemmas on the behaviour of the filter function.
It is often convenient to state such lemmas, in order to be able to use rewriting
as an alternative to reduction in proofs: reduction is a bit difficult to control.
*)
-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 →
- \ 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.
+\ 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 →
+ \ 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.
#A #l #a #p #pa (elim l) normalize >pa // qed.
-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 →
- \ 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.
+\ 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 →
+ \ 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.
#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
(* As another example, let us redefine the map function using foldr. The
of type A → list B → list B is the function mapping a and l to (f a)::l.
*)
-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.
+\ 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.
-(* Can we prove that map_again is "the same" as map? We should first of all
+(*
+\ 5h2 class="section"\ 6Extensional equality\ 5/h2\ 6
+Can we prove that map_again is "the same" as map? We should first of all
clarify in which sense we expect the two functions to be equal. Equality in
Matita has an intentional meaning: it is the smallest predicate induced by
convertibility, i.e. syntactical equality up to normalization. From an
programs behave in the same way: this is a different, extensional equality
that can be defined in the following way. *)
-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.
+\ 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.
(* Proving that map and map_again are extentionally equal in the
previous sense can be proved by a trivial structural induction on the list *)
-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).
+\ 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).
#A #B #f #n (elim n) normalize // qed.
(* Let us make another remark about extensional equality. It is clear that,
if f is extensionally equal to g, then (map A B f) is extensionally equal to
(map A B g). Let us prove it. *)
-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).
+\ 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).
#A #B #f #g #eqfg
(* the relevant point is that we cannot proceed by rewriting f with g via
#l (elim l) normalize // qed.
-(**************************** BIGOPS *******************************)
-
-(* Building a library of basic functions, it is important to achieve a
+(*
+\ 5h2 class="section"\ 6Big Operators\ 5/h2\ 6
+Building a library of basic functions, it is important to achieve a
good degree of abstraction and generality, in order to be able to reuse
suitable instances of the same function in different context. This has not
only the obvious benefit of factorizing code, but especially to avoid
that essentially allow you to iterate on every subset of a given enumerated
(finite) type, represented as a list. *)
- 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 ≝
+ \ 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 ≝
match l with
[ nil ⇒ b
- | 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))
+ | cons a l ⇒ if p a then op (f a) (fold A B op b p f l) else
(fold A B op b p f l)].
(* It is also important to spend a few time to introduce some fancy notation
interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
-theorem fold_true:
+\ 5img class="anchor" src="icons/tick.png" id="fold_true"\ 6theorem fold_true:
∀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 →
- \ 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
- op (f a) \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i).
+ \ 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
+ 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).
#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
-theorem fold_false:
+\ 5img class="anchor" src="icons/tick.png" id="fold_false"\ 6theorem fold_false:
∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
-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
- \ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ l| p i} (f i).
+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
+ \ 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).
#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
-theorem fold_filter:
+\ 5img class="anchor" src="icons/tick.png" id="fold_filter"\ 6theorem fold_filter:
∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
- \ 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
- \ 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).
+ \ 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
+ \ 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).
#A #B #a #l #p #op #nil #f elim l //
#a #tl #Hind cases(\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (p a)) #pa
[ >\ 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 //
| >\ 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 // ]
qed.
-record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="Aop"\ 6record Aop (A:Type[0]) (nil:A) : Type[0] ≝
{op :2> A → A → A;
nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
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
}.
-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.
- 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
- \ 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).
+\ 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.
+ 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
+ \ 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).
#A #B #I #J #nil #op #f (elim I) normalize
[>\ 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 //]
qed.
\ No newline at end of file
projects / helm.git / blobdiff