Commit dac30ec1 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

TD2 : revision + english version

parent 19e81a51
......@@ -8,29 +8,29 @@ Import ListNotations.
Fixpoint fib n :=
match n with
| 0 => 1
| 1 => 2
| 0 => 0
| 1 => 1
| S ((S n) as p) => fib p + fib n
end.
Compute List.map fib (List.seq 0 10).
Compute List.map fib (List.seq 0 20).
(** Un premier exemple de test de fonction
via une specification executable *)
Definition fib_spec n := fib (n+2) =? fib n + fib (n+1).
Time Compute List.forallb fib_spec (List.seq 0 30).
Time Compute List.forallb fib_spec (List.seq 0 20).
Fixpoint fib2 n :=
match n with
| 0 => (1,2)
| 0 => (0,1)
| S n => let (a,b) := fib2 n in (b,a+b)
end.
Definition fib_opt n := fst (fib2 n).
Compute List.map fib_opt (List.seq 0 10).
Compute List.map fib_opt (List.seq 0 20).
Fixpoint fibloop n a b :=
match n with
......@@ -38,9 +38,9 @@ Fixpoint fibloop n a b :=
| S n => fibloop n b (a+b)
end.
Definition fib_tailrec n := fibloop n 1 2.
Definition fib_tailrec n := fibloop n 0 1.
Compute List.map fib_tailrec (List.seq 0 10).
Compute List.map fib_tailrec (List.seq 0 20).
(** En essayant de calculer des "gros" fibonacci on obtient
"stack overflow" avec les trois versions précédentes.
......@@ -56,14 +56,14 @@ Time Compute (N.of_nat (fib_tailrec 35)). (** 4s *)
Fixpoint fibN n :=
match n with
| 0 => 1%N
| 1 => 2%N
| 0 => 0%N
| 1 => 1%N
| S ((S n) as p) => (fibN p + fibN n)%N
end.
Fixpoint fibN2 n :=
match n with
| 0 => (1,2)%N
| 0 => (0,1)%N
| S n => let (a,b) := fibN2 n in (b,a+b)%N
end.
......@@ -75,7 +75,7 @@ Fixpoint fibNloop n a b :=
| S n => fibNloop n b (a+b)%N
end.
Definition fibN_tailrec n := fibNloop n 1%N 2%N.
Definition fibN_tailrec n := fibNloop n 0%N 1%N.
Time Compute (fibN 35). (** 2s *)
Time Compute (fibN_opt 35). (** 0s *)
......@@ -101,7 +101,7 @@ Check N.peano_rect.
Definition fibNN2 n :=
N.peano_rect
_
(1,2)%N
(0,1)%N
(fun n p => let '(a,b) := p in (b,a+b)%N)
n.
......@@ -112,7 +112,7 @@ Definition fibNN n := fst (fibNN2 n).
(les résultats ont toujours le même type, indépendemment de n).
*)
Compute List.map fibNN [1;2;3;4;5;6;7;8;9]%N.
Compute List.map fibNN [0;1;2;3;4;5;6;7;8;9;10]%N.
Time Compute fibNN 10000.
......@@ -123,9 +123,9 @@ Definition fibNNloop n :=
(fun _ p a b => p b (a+b)%N)
n.
Definition fibNN_tail n := fibNNloop n 1%N 2%N.
Definition fibNN_tail n := fibNNloop n 0%N 1%N.
Compute List.map fibNN [1;2;3;4;5;6;7;8;9]%N.
Compute List.map fibNN [0;1;2;3;4;5;6;7;8;9;10]%N.
Time Compute fibNN_tail 10000.
......@@ -150,9 +150,9 @@ Fixpoint powmat m p :=
end%positive.
Definition fib_m p :=
let '(a,_,_,_) := powmat fibmat (p+1) in a.
let '(_,a,_,_) := powmat fibmat p in a.
Compute List.map fib_m [1;2;3;4;5;6;7;8;9]%positive.
Compute List.map fib_m [1;2;3;4;5;6;7;8;9;10]%positive.
Time Compute fibNN (10000). (* 1s *)
Time Compute fib_m (10000). (* 2s *)
......@@ -168,16 +168,18 @@ Fixpoint fib_inv_loop n a b k cpt :=
else fib_inv_loop n b (a+b) (S k) cpt
end.
Definition fib_inv n := fib_inv_loop n 1 2 0 n.
Definition fib_inv n :=
if n =? 0 then 0 else fib_inv_loop n 1 2 2 n.
Compute fib_inv 0.
Compute fib_inv 1.
Compute fib_inv 2.
Compute fib_inv 5.
Compute (fib 3, fib 4).
Compute (fib 5, fib 6).
Compute fib_inv 10.
Compute (fib 4, fib 5).
Compute (fib 6, fib 7).
Compute fib_inv 1000.
Compute (fib 14, fib 15).
Compute (fib 16, fib 17).
(** Test plus systématique, via une spécification exécutable *)
......@@ -207,10 +209,10 @@ Fixpoint sumfib l :=
end.
Compute decomp 10.
Compute sumfib [4;1].
Compute sumfib [6;3].
Compute decomp 100.
Compute sumfib [9;4;2].
Compute sumfib [11;6;4].
(** Specification exécutable de [decomp].
C'est une spécification partielle : on ne vérifie pas que
......@@ -243,11 +245,11 @@ Fixpoint normalise_loop l n :=
Definition normalise l := normalise_loop l (length l).
Compute normalise [0;1;2;3;4].
Compute (sumfib [0;1;2;3;4], sumfib [0;3;5]).
Compute normalise [2;3;4;5;6].
Compute (sumfib [2;3;4;5;6], sumfib [2;5;7]).
Compute normalise [0;1;2;3;4;5].
Compute (sumfib [0;1;2;3;4;5], sumfib [2;4;6]).
Compute normalise [2;3;4;5;6;7].
Compute (sumfib [2;3;4;5;6;7], sumfib [4;6;8]).
(** Bonus : équation de la fonction qui décroit de 1 les décompositions *)
......@@ -255,4 +257,4 @@ Definition g n := sumfib (List.map pred (decomp n)).
Definition g_spec n := (g n =? n - g (g (n-1))).
Compute List.forallb g_spec (seq 0 1000).
\ No newline at end of file
Compute List.forallb g_spec (seq 0 1000).
Functional Programming in Coq : TD2
===================================
**M2 LMFI**
#### Exercise 1 : usual functions on natural numbers
Load first the unary arithmetics : `Require Import Arith`.
If not done last week, define the following functions on `nat` (without using the ones of Coq standard library):
- addition
- multiplication
- subtraction
- factorial
- power
- gcd
#### Exercise 2 : Fibonacci
- Define a function `fib` such that `fib 0 = 0`, `fib 1 = 1` then `fib (n+2) = fib (n+1) + fib n`.
(you may use a `as` keyword to name some subpart of the `match` pattern ("motif" en français)).
- Define an optimized version of `fib` that computes faster that the previous one by using Coq pairs.
- Same question with just natural numbers, no pairs. Hint: use a special recursive style call "tail recursion".
- Load the library of binary numbers via `Require Import NArith`.
Adapt you previous functions for them now to have type `nat -> N`.
What impact does it have on efficiency ?
Is it possible to simply obtain functions of type `N -> N` ?
#### Exercise 3 : Fibonacci though matrices
- Define a type of 2x2 matrices of numbers (for instance via a quadruple).
- Define the multiplication and the power of these matrices.
Hint: the power may use an argument of type `positive`.
- Define a fibonacci function through power of the following matrix:
```
1 1
1 0
```
#### Exercise 4 : Fibonacci decomposition of numbers
We aim here at programming the Zeckendorf theorem in practice : every number can be decomposed in a sum of Fibonacci numbers, and moreover this decomposition is unique as soon as these Fibonacci numbers are distinct and non-successive and with index at least 2.
Load the list library:
```
Require Import List.
Import ListNotations.
```
- Write a function `fib_inv : nat -> nat` such that if `fib_inv n = k` then `fib k <= n < fib (k+1)`.
- Write a function `fib_sum : list nat -> nat` such that `fib_sum [k_1;...;k_p] = fib k_1 + ... + fib k_p`.
- Write a function `decomp : nat -> list nat` such that `fib_sum (decomp n) = n` and `decomp n` does not contain 0 nor 1 nor any redundancy nor any successive numbers.
- (Optional) Write a function `normalise : list nat -> list nat` which receives a decomposition without 0 nor 1 nor redundancy, but may contains successive numbers, and builds a decomposition without 0 nor 1 nor redundancy nor successive numbers. You might assume here that the input list of this function is sorted in the way you prefer.
......@@ -18,7 +18,7 @@ Si vous ne l'avez pas déjà fait la semaine dernière, définissez les fonction
#### Exercice 2 : Fibonacci
- Définir une fonction `fib` telle que `fib 0 = 1`, `fib 1 = 2` puis `fib (n+2) = fib (n+1) + fib n`.
- Définir une fonction `fib` telle que `fib 0 = 0`, `fib 1 = 1` puis `fib (n+2) = fib (n+1) + fib n`.
(on pourra éventuellement utiliser un `as` dans les motifs du match).
- Produire une version de `fib` nettement plus rapide en utilisant des paires.
......@@ -42,9 +42,9 @@ Si vous ne l'avez pas déjà fait la semaine dernière, définissez les fonction
1 0
```
#### Exercice 3 : écriture en base Fibonacci
#### Exercice 4 : écriture en base Fibonacci
On cherche ici à mettre en pratique le théorème de Zeckendorf : tout entier s'écrit de manière unique en une somme de nombres de Fibonacci distincts et non consécutifs.
On cherche ici à mettre en pratique le théorème de Zeckendorf : tout entier se décompose en une somme de nombres de Fibonacci, et de plus cette décomposition est unique si ces Fibonacci sont distincts, non consécutifs, et d'indices au moins 2.
Chargez la bibliothèque des listes:
```
......@@ -52,11 +52,10 @@ Require Import List.
Import ListNotations.
```
- Ecrire une fonction `fib_inv : nat -> nat` telle que si `n<>0` et `fib_inv n = k` alors `fib k <= n < fib (k+1)`.
- Ecrire une fonction `fib_inv : nat -> nat` telle que si `fib_inv n = k` alors `fib k <= n < fib (k+1)`.
- Ecrire une fonction `fib_sum : list nat -> nat` telle que `fib_sum [k_1;...;k_p] = fib k_1 + ... + fib k_p`.
- Ecrire une fonction `decomp : nat -> list nat` telle que `fib_sum (decomp n) = n` et que `decomp n` soit sans doublons ni entiers consécutifs.
- (Bonus) Ecrire une fonction `normalise : list nat -> list nat` qui construit une décomposition sans doublons ni consécutifs à partir d'une décomposition sans doublons, tout en préservant évidemment la somme totale. On pourra supposer que l'entrée est triée dans l'ordre croissant.
- Ecrire une fonction `decomp : nat -> list nat` telle que `fib_sum (decomp n) = n` et que `decomp n` soit sans 0, sans 1, sans doublons ni entiers consécutifs.
- (Bonus) Ecrire une fonction `normalise : list nat -> list nat` qui part d'une décomposition sans 0 ni 1 ni doublons, mais peut-être avec des entiers consécutifs, et qui construit une décomposition sans 0 sans 1 sans doublons sans consécutifs, tout en préservant évidemment la somme totale. On pourra supposer que l'entrée est triée dans l'ordre croissant.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment