Travaux dirigés pour le 24 janvier 2012

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

Questions à faire en classe (les deux dernières plus dures, sont facultatives)

• 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.