| nil: list A
| cons: A -> list A -> list A.
-(* The type notation list A is the type of all lists with elements of type A: it is
-defined by two constructors: a polymorphic empty list (nil A) and a cons operation,
-adding a new head element of type A to a previous list. For instance, (list nat) and
-and (list bool) are lists of natural numbers and booleans, respectively. But we can
-also form more complex data types, like (list (list (nat → nat))), that is a list whose
-elements are lists of functions from natural numbers to natural numbers.
+(* The type notation list A is the type of all lists with elements of type A:
+it is defined by two constructors: a polymorphic empty list (nil A) and a cons
+operation, adding a new head element of type A to a previous list. For instance,
+(list nat) and and (list bool) are lists of natural numbers and booleans,
+respectively. But we can also form more complex data types, like
+(list (list (nat → nat))), that is a list whose elements are lists of functions
+from natural numbers to natural numbers.
Typical elements in (list bool) are for instance,
- nil nat - the empty list of type nat
- cons nat true (nil nat) - the list containing true
- cons nat false (cons nat (true (nil nat))) - the list containing false and true
+ nil nat - the empty list of type nat
+ cons nat true (nil nat) - the list containing true
+ cons nat false (cons nat (true (nil nat))) - the list containing false and true
and so on.
-Note that both constructos nil and cons are expecting in input the type parameter -
+Note that both constructos nil and cons are expecting in input the type parameter:
in this case, bool.
-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.
+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.
*)
notation "hvbox(hd break :: tl)"
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 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 the append
-function itself is polymorphic, and the first argument it takes in input is the type
-A of the elements of two lists l1 and l2.
+(* 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
+the append function itself is polymorphic, and the first argument it takes in input
+is the type A of the elements of two lists l1 and l2.
Moreover, since the append function takes in input several parameters, we must also
specify in the its defintion on which one of them we are recurring: in this case l1.
If not othewise specified, recursion is supposed to act on the first argument of the
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.
#A #l normalize // qed.
-(* Proving that l @ [] = l is just a bit more complex. The situation is exactly the
-same as for the addition operation of the previous chapter: since append is defined
-by recutsion over the first argument, the computation of l @ [] is stuck, and we must
-proceed by induction on l *)
+(* Proving that l @ [] = l is just a bit more complex. The situation is exactly
+the same as for the addition operation of the previous chapter: since append is
+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.
#A #l (elim l) normalize // qed.
(* similarly, we can define the two functions head and tail. Since we can only define
-total functions, we should decide what to do in case the input list is empty. 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. *)
+total functions, we should decide what to do in case the input list is empty.
+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.
match l with [ nil ⇒ d | cons a _ ⇒ 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 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 *)
+(* 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])].
∀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].
#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. *)
+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)))
(* Now, we rewrite with Heq, obtaining (is_nil A []), that reduces to the trivial
goal [] = [] *)
>Heq // qed.
-(* As an application of the previous result let us prove that l1@l2 is empty if and
-only if both l1 and l2 are empty. The idea is to proceed by cases on l1: if l1=[] the
-statement is trivial; on the other side, if l1 = a::tl, then the hypothesis
-(a::tl)@l2 = [] is absurd, hence we can prove anything from it. When we know we can
-prove both A and ¬A, a sensible way to proceed is to apply False_ind: ∀P.False → P to the
-current goal, that breaks down to prove False, and 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. *)
+(* As an application of the previous result let us prove that l1@l2 is empty if
+and only if both l1 and l2 are empty.
+The idea is to proceed by cases on l1: if l1=[] the statement is trivial; on the
+other side, if l1 = a::tl, then the hypothesis (a::tl)@l2 = [] is absurd, hence we
+can prove anything from it.
+When we know we can prove both A and ¬A, a sensible way to proceed is to apply
+False_ind: ∀P.False → P to the current goal, that breaks down to prove False, and
+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].
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 ≝
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 function
-that given a list l: list A and a boolean test p:A → bool returns the sublist of elements
-satisfying the test. In this case, the result type B of foldr should be (list A), the base
-value is [], and f: A → list A →list A is 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
-bbol.ma to this purpose. *)
+(* As an example of application of foldr, let us use it to define a filter
+function that given a list l: list A and a boolean test p:A → bool returns the
+sublist of elements satisfying the test. In this case, the result type B of
+foldr should be (list A), the base value is [], and f: A → list A →list A is
+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 ≝
λT.λp:T → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
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 ≝
+ 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 ≝
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))
projects / helm.git / commitdiff