Travaux dirigés pour le 25 janvier 2011

Le but de cette séance est d'apprendre à programmer dans le langage de Coq.

Questions à faire en classe

Définir une fonction qui prend en entrée un nombre et retourne le double de ce nombre
Définir une fonction qui prend en entrée un nombre et retourne le triple de ce nombre
Définir une fonction qui prend en entrée une fonction des nombres naturels vers les nombres naturels et un entier naturel et retourne le résultat de l'application de son premier argument à son deuxième argument
Définir une fonction qui prend en entrée une fonction des nombres naturels vers les nombres naturels et un entier naturel et retourne le résultat de l'application du premier argument à la valeur obtenue en appliquant le premier argument au second
Définir une fonction qui prend en entrée un nombre naturel et retourne 10 si ce nombre naturel est 3, et 0 dans tous les autres cas
Définir une fonction qui prend en entrée un nombre naturel et retourne 10 si ce nombre naturel est 3, et retourne son entrée dans tous les autres cas
Définir une fonction qui prend en entrée un nombre naturel et retourne une valeur booléenne de votre choix.
Définir une fonction qui prend en entrée un nombre naturel n et retourne en sortie la liste (n::n-1::...::0::nil)
Sachant que (n - m) est égal à 0 si et seulement si n ≤ m, écrire une fonction qui retourne true si n ≤ m et false sinon.
Définir une fonction qui prend en entrée un nombre a et une liste ordonnée croissante et retourne la même liste dont on a enlevé tous les multiples de a
Développez un code qui effectue le crible d'Eratosthène: commencer par produire la liste de tous les nombres entiers supérieurs à 2 jusqu'à un certain nombre n, puis enlevez de cette liste tous les multiples de 2, puis tous les multiples de 3, puis à chaque fois, tous les multiple du prochain nombre premier.

Quelques exemples et outils

Pour écrire des fonctions sur les listes il faut d'abord faire exécuter la commande suivante:
```
Require Import List.
```
La fonction suivante prend en entrée un nombre et retourne en sortie le nombre 3 si l'entrée était 0 et l'entrée plus 10 dans les autres cas.
```
Definition bizarre3et10 (x:nat) :=
  match x with
    0 => 3
  | _ => x + 10
  end.
```

La fonction rev donnée ci-dessous prend en entrée un type et une liste d'éléments de ce type et retourne la liste renversé

Fixpoint rev_r (A : Type) (l l': list A) :=
  match l with nil => l' | a::l1 => rev_r A l1 (a::l') end.

Definition rev (A : Type) (l : list A) := rev_r A l nil.

On peut tester cette fonction en appliquant la commande suivante
```
Eval vm_compute in rev _ (1::2::3::4::nil).
```
La fonction suivante prend en entrée une fonction p des entiers naturels vers les booléens et une liste d'entiers naturels et enlève tous les éléments pour lesquels la fonction p retourne true.
```
Fixpoint remove (p:nat -> bool) (l: list nat) :=
  match l with
    nil => nil
  | a::l' =>
    match p a with true => remove p l | false => a::remove p l end
  end.
```
L'expression match p a with true => remove p l | false => a::remove p l end peut aussi s'écrire if p a then remove p l else a:: remove p l
La fonction suivante prend en entrée un nombre n et additionne tous les nombres compris entre 0 et n-1. Fixpoint tsum (n:nat) := match n with 0 => 0 | S p => p + tsum p end.

Last modified: Mon Jan 24 23:25:06 CET 2011