Require Import Bool Arith List.
(* 1. Define a recursive function that takes as input a list of numbers
and returns the product of these numbers, *)
Fixpoint prodlist ...
Compute prodlist nil.
Compute prodlist (0 :: 3 :: 7 :: nil).
Compute prodlist (3 :: 4 :: 2 :: nil).
(* 2. Define a recursive function that takes a list of numbers and
returns true if and only if this list contains the number 0.
Hint: pattern match on both the list and the elements of the list. *)
Fixpoint has_a_0 ...
Compute has_a_0 (2 :: 3 :: 0 :: 7 :: nil).
Compute has_a_0 nil.
Compute has_a_0 (3 :: 5 :: nil).
(* 3. Define a recursive function that takes as input two numbers and
returns true if and only if these two numbers are the same natural
number (such a function already exists in the Coq libraries
(function beq_nat, but how would you define such a function), using
only pattern-matching and recursion. *)
... beq ...
Compute beq 4 5.
Compute beq 7 7.
(* 4. Define a recursive function that takes a number n and a number
a as input and returns a list of numbers containing n elements
that are all a. *)
... mklist ...
Compute mklist 3 0.
(* 5. Define a function that takes a number n and a number a and returns
the list of n elements a ::a + 1:: · · · ::a + n:: nil. *)
... mklist1 ...
Compute mklist1 3 0.
(* 6. Define a function that takes as input a natural number and returns
an element of option nat containing the predecessor if it exists or
None if the input is 0. *)
... pred ...
Compute pred 0.
Compute pred 6.
(* 7. Define a recursive function that takes as input a list of numbers
and returns the length of this list. *)
... length ...
Compute length nil.
Compute length (2 :: 3 :: nil).
(* 8. Can you write a recursive function values that takes as input a
function f of type nat -> nat, an initial value a of type nat
and a count n of type nat and produces the list
a :: f a :: f (f a) :: ... *)
Fixpoint fold (f : nat -> nat) (a : nat) (n : nat) := ...
Compute fold (fun x : nat => x) 0 5.
Compute fold (fun x : nat => x + 1) 3 4.
Compute fold S 3 4.
(* 9. To every natural number, we can associate the list of its digits
from right to left. For instance, 239 should be associated to the list
9::3::2::nil. We also consider that 0 can be mapped to nil. If l is
such a list, we can consider the successor of a list of digits.
For instance, the successor of 9::3::2::nil is 0::4::2.
Define the algorithm on lists of natural numbers that computes the
successor of that list. *)
... lsucc ...
Compute lsucc (3 :: 9 :: 1 :: nil).
Compute lsucc (9 :: 3 :: 1 :: nil).
Compute lsucc (9 :: 9 :: 1 :: nil).
Compute lsucc nil.
Compute lsucc (9 :: nil).
(* 10. Assuming that lsuc is the function defined at the previous
exercise, define the function nat_digits that maps every natural
number to the corresponding list of digits (naive solutions are
welcome, as long as they run). *)
Fixpoint nat_digits_aux ...
Definition nat_digits n := ...
Compute nat_digits 2990.
(* 11. In the same context as the previous two exercises, define a function
value that maps every list of digits to the natural number it
represents. Thus, value (9::3::2::nil) should compute to 239. *)
... value ...
Compute value (0 :: 2 :: 3 :: 4 :: nil).
(* 12. In the same context as the previous exercises, define a function
licit that tells whether a list of integers corresponds to the digits
of natural number: no digit should be larger than 9. For instance,
licit (9::3::2::0::nil) should compute to true and licit (239::nil)
should compute to false. *)
... licit ...
Compute licit (9 :: 3 :: 2 :: 0 :: nil).
Compute licit (239 :: nil).
(* 13. In the same context as the previous exercises, define functions
to add two lists of digits so that the result represents the sum of
the numbers represented by the lists of digits. In other words
addl (7::2::nil) (5::3::nil) should return 2::6::nil
(Hint: you should implement the algorithm you learned in elementary
school for adding numbers). *)
... addl ...
Compute addl (7 :: 2 :: nil) (5 :: 3 :: nil).
(* 14. In the same context as the previous exercises, define a function
for multiplying a list by a small natural number (by successive
additions) and then a function mull for multiplying two lists of
digits. *)
... mulln ...
Compute mulln 3 (2 :: 1 :: nil).
... mull ...
Compute 14 * 13.
Compute mull (4 :: 1 :: nil) (3 :: 1 :: nil).
Compute 437 * 25.
Compute mull (7 :: 3 :: 4 :: nil) (5 :: 2 :: nil).
Compute 97 * 75.
Compute mull (7 :: 9 :: nil) (5 :: 7 :: nil).