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 (l : list nat) :=
match l with
| nil => 1
| x :: xs => x * prodlist xs
end.
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 (l : list nat) :=
match l with
| nil => false
| O :: _ => true
| _ :: xs => has_a_0 xs
end.
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. *)
Fixpoint beq (n m : nat) :=
match n, m with
| O, O => true
| S n1, S m1 => beq n1 m1
| _, _ => false
end.
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. *)
Fixpoint mklist (n a : nat) :=
match n with
| O => nil
| S n1 => a :: mklist n1 a
end.
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. *)
Fixpoint mklist1 (n a : nat) :=
match n with
| O => nil
| S n1 => a :: mklist1 n1 (S a)
end.
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. *)
Definition pred (n : nat) :=
match n with
| O => None
| S m => Some m
end.
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. *)
Fixpoint length (l : list nat) :=
match l with
| nil => 0
| _ :: xs => S (length xs)
end.
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) :=
match n with
| O => nil
| S n1 => a :: fold f (f a) n1
end.
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. *)
Fixpoint lsucc (l : list nat) :=
match l with
| nil => 1 :: nil
| 9 :: xs => 0 :: lsucc xs
| x :: xs => S x :: xs
end.
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 (n : nat) (acc : list nat) :=
match n with
| O => acc
| S n1 => lsucc (nat_digits_aux n1 acc)
end.
Definition nat_digits n := nat_digits_aux n nil.
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. *)
Fixpoint value_aux n weigth :=
match n with
| nil => 0
| x :: xs => weigth * x + value_aux xs (10 * weigth)
end.
Definition value n := value_aux n 1.
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. *)
Fixpoint licit l :=
match l with
| nil => true
| x :: xs => (leb x 9) && (licit xs)
end.
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). *)
Fixpoint addl (l1 l2 : list nat) :=
match l1, l2 with
| nil, nil => nil
| x :: xs, y :: ys =>
if leb (x + y) 9 then x + y :: addl xs ys
else x + y - 10 :: lsucc (addl xs ys)
| _, nil => l1
| nil, _ => l2
end.
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. *)
Fixpoint mulln n l :=
match n with
| O => nil
| 1 => l
| S n1 => addl l (mulln n1 l)
end.
Compute mulln 3 (2 :: 1 :: nil).
Fixpoint mull l1 l2 :=
match l1 with
| nil => nil
| x :: xs => addl (mulln x l2) (0 :: (mull xs l2))
end.
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).