tp2.mv

TP2 : Premiers pas en Coq
=========================

Introduction
------------

Coq est un "assistant de preuve", ou un "prouveur interactif de théorèmes", c'est-à-dire un logiciel qui permet d'énoncer des théorèmes mathématiques dans un langage formel, compréhensible par l'ordinateur, similaire à un langage de programmation. Il permet ensuite de prouver ces théorèmes, notamment en utilisant des tactiques qui permettent d'effectuer des étapes de preuve. L'assistant de preuve interagit avec l'utilisateur en lui fournissant des informations sur l'état de la preuve en cours, notamment les buts à prouver et les hypothèses disponibles.

Les assistants de preuve sont des outils qui sont développés depuis les années 70. Ils ont beaucoup gagné en popularité dans les deux dernières décennies. Ils ont trois applications principales :

- la vérification de programmes critiques
- la vérification de preuves mathématiques
- l'enseignement de la logique et des mathématiques

Coq est l'un des assistants de preuve les plus célèbres et les plus utilisés. Il a été utilisé dans ces trois applications, mais la plus commune est la vérification de programmes. Par exemple, le compilateur CompCert est un compilateur C formellement vérifié en Coq, qui garantit que le code machine produit par le compilateur est équivalent au code source C. CompCert est écrit et prouvé correct en Coq, puis "extrait" automatiquement en OCaml, pour être compilé et exécuté.

### Utilisation de Coq ###

Le fichier courant est un fichier `.mv`, mélangeant syntaxe Markdown et bloc de code Coq.

Si vous utilisez l'environnement de travail fourni dans le cadre du TP, vous êtes actuellement en train de lire ce fichier dans un éditeur VS Code avec l'extension coq-lsp. Lorsque vous placez le curseur quelque part dans un bloc de code Coq, l'extension affiche dans le panneau de droite soit le résultat de la commande sous le curseur, soit (si vous êtes au milieu d'une preuve) l'état courant de la preuve en cours (les buts à prouver, les hypothèses disponibles, etc.).

Si vous souhaitez utiliser Coq en dehors de cet environnement, vous devez [installer Coq](https://coq.inria.fr/download) ainsi qu'une [interface utilisateur](https://coq.inria.fr/user-interfaces.html). La plupart des interfaces historiques (CoqIDE, Proof General pour l'éditeur Emacs, etc.) ont un mode d'utilisation différent de coq-lsp, où vous naviguez dans un fichier Coq (extension `.v`) en utilisant des boutons ou des raccourcis clavier pour voir l'état de la preuve. La disposition de l'interface est en revanche similaire.

### Commandes Coq ###

En Coq, une commande est formée d'un nom de commande (commençant par une majuscule), éventuellement suivie d'un ou plusieurs arguments, et terminée par un point.  Exemples :

```coq
  Check 0.
  Check S.
  Check nat.
  Search nat.
  Check 2 + 2 = 5.
  Check forall x, exists y, x = 2 * y \/ x = 2 * y + 1.
```

Placez votre curseur successivement sur ces différentes lignes pour en voir le résultat dans le panneau de droite.

Quel est le but de la commande `Check` ?

On peut déjà remarquer à ce stade qu'en Coq, les termes ont des types, mais les types aussi ont des types.

### Preuve interactive en Coq ###

L'utilisateur déclare son intention d'effectuer une preuve avec une commande de la forme :

```coq
Lemma and_commut (A B : Prop) : A /\ B <-> B /\ A.
Proof.
```

On notera que cette commande donne un nom (ici: `and_commut`) au lemme, ce qui permettra de le référencer par la suite. On peut éventuellement remplacer `Lemma` par `Theorem` ou quelques autres mots-clés équivalents comme `Example`, `Proposition` ou `Fact`. On marquera le début de la preuve par la commmande `Proof` (très fortement recommandée même si facultative).

### Sous-buts et tactiques ###

Une fois le mode preuve lancé, le panneau de droite affiche en permanence un ou plusieurs sous-buts (**subgoals**) qu'il s'agit de démontrer. Ces sous-buts sont essentiellement des séquents de la déduction naturelle écrits verticalement: les hypothèses (nommées) sont en haut, et la conclusion figure en bas sous un trait. Dans la partie haute figurent également des déclarations de variables.

La preuve se fait à l'aide de **tactiques** (distinguées des commandes par une minuscule initiale), qui effectuent des transformations plus ou moins complexes sur le but courant. À chaque règle d'inférence de la déduction naturelle correspond une ou plusieurs tactiques (cf. plus bas), mais certaines tactiques permettent également d'effectuer des morceaux de preuve plus complexes, comme par exemple la résolution de contraintes linéaires en arithmétique de Presburger (tactique `lia`).

Les tactiques sont susceptibles d'engendrer de nouveaux sous-buts (correspondant aux prémisses), ou au contraire de faire disparaître le but courant (lorsque celui-ci est résolu). La preuve est terminée lorsqu'il n'y a plus de sous-but à démontrer. On doit alors utiliser la commande `Qed` (d'après *Quod erat demonstrandum*, le CQFD latin) pour conclure la preuve et repasser au mode *commande*. Voici par exemple une preuve complète pour l'énoncé précédent :

```coq
 split.
 - intros H.
   destruct H.
   split.
   + assumption.
   + assumption.
 - intros H.
   destruct H.
   split; assumption.
Qed.
```

Placez le curseur successivement sur ces différentes lignes pour voir la preuve se dérouler dans le panneau de droite.

Lorsque les tactiques sont séparées par des points, Coq va alors les exécuter pas-à-pas. On peut aussi utiliser le `;` pour **chaîner** des tactiques. Ainsi `split; assumption` fait agir `assumption` sur les deux sous-buts créés par `split`.

Devant des tactiques, on peut éventuellement placer une **puce**, c'est-à-dire un des marqueurs `-` ou `+` ou `*`. Ces puces sont optionnelles mais aident grandement à hiérarchiser la preuve en cours en délimitant chaque sous-partie.

Enfin, les commentaires sont introduits par `(*` et terminés par `*)`, comme en OCaml.

Un *script de preuve*, sauvegardé dans un fichier avec l'extension `.v`, peut ensuite être *compilé*.  Si les preuves que contient ce fichier sont correctes, un fichier compilé `.vo` est alors produit, qui permettra de recharger les définitions et lemmes depuis un autre fichier (commande `Require Import`). L'extension coq-lsp pour VS Code fournit également une commande `Coq LSP: Save .vo file for the current buffer` qui permet de compiler le fichier courant, y compris un fichier `.mv`.

Logique propositionnelle
------------------------

On pose l'existence de variables propositionnelles `A`, `B` et `C` :

```coq
Parameters A B C : Prop.
```

Nous allons prouver différents lemmes avec des tactiques que nous introduirons au fur et à mesure en les mettant en correspondance avec les règles de la déduction naturelle.

### Implication ###

L'implication en Coq s'écrit `->`. Par exemple, `A -> B` est la proposition "A implique B".

La tactique `intros` est équivalente à la règle `=>I` de la déduction naturelle. Elle permet d'introduire une hypothèse dans le contexte. Par exemple, si le but est `A -> B`, la tactique `intros H` introduit l'hypothèse `H : A` dans le contexte et remplace le but par `B` (remplacer `H` par un nom qui ne soit pas déjà utilisé dans le contexte). On pourra aussi passer plusieurs noms d'hypothèses à `intros` en les séparant par des espaces pour introduire plusieurs hypothèses à la fois (par exemple `intros H1 H2 H3`).

La tactique `apply` est équivalente à la règle `=>E` de la déduction naturelle. Elle permet d'utiliser une hypothèse ou un lemme pour prouver le but. Par exemple, si le but est `B` et que l'hypothèse `H : A -> B` est dans le contexte, alors `apply H` remplace le but par `A`.

La tactique `assumption` est équivalente à la règle `Axiom` de la déduction naturelle. Elle permet de conclure en utilisant une hypothèse du contexte. Par exemple, si le but est `B` et que l'hypothèse `H : B` est dans le contexte, alors `assumption` conclut le but.

Prouver en Coq les formules suivantes:

```coq
Lemma refl_impl : A -> A.
Proof.

Qed.

Lemma trans_impl : (A -> B) -> (B -> C) -> A -> C.
Proof.

Qed.
```

### Conjonction, disjonction et équivalence ###

La conjonction en Coq s'écrit `/\` : `A /\ B` est la proposition "A et B". La disjonction s'écrit `\/` : `A \/ B` est la proposition "A ou B". L'équivalence s'écrit `<->` : `A <-> B` est la proposition "A équivaut à B".

La tactique `split` est équivalente à la règle `/\I` de la déduction naturelle. Elle permet de prouver un `/\` en prouvant les deux côtés. Par exemple, si le but est `A /\ B`, alors `split` crée deux sous-buts, le premier avec le but `A` et le second avec le but `B`.

Les tactiques `left` et `right` sont équivalentes aux règles `\/I1` et `\/I2` de la déduction naturelle. Elles permettent de prouver un `\/` en prouvant l'un des deux côtés. Par exemple, si le but est `A \/ B`, alors `left` remplace le but par `A` tandis que `right` remplace le but par `B`.

Attention : il peut être tentant d'essayer `left` ou `right` dès qu'on rencontre un but de la forme `A \/ B`, mais il vaut généralement mieux retarder le plus tard possible cette décision de prouver la gauche ou la droite de la disjonction. Par exemple, il vaut mieux au préalable avoir extrait le maximum d'informations des hypothèses du contexte, notamment avec la tactique `destruct` que nous présentons ci-dessous. (Mais bon, vous savez déjà comment vous y prendre pour faire des preuves en maths, donc ce conseil a surtout pour but de vous rappeler de ne pas perdre vos bonnes intuitions et de ne pas vous laisser embarquer par une preuve Coq qui "semble" progresser. L'assistant de preuve "assiste", mais ne remplace pas votre intuition mathématique.)

La tactique `destruct` est équivalente aux règles `/\E` et `\/E` de la déduction naturelle. Elle permet de déstructurer un `/\` ou un `\/` dans le contexte. Par exemple, si le but est `C` et que l'hypothèse `H : A /\ B` est dans le contexte, alors `destruct H as (HA, HB)` introduit les hypothèses `HA : A` et `HB : B` dans le contexte sans changer le but. Si le but est `C` et que l'hypothèse `H : A \/ B` est dans le contexte, alors `destruct H as [HA | HB]` crée deux sous-buts, le premier avec l'hypothèse `HA : A` dans le contexte et le second avec l'hypothèse `HB : B` dans le contexte. Dans les deux sous-buts, le but est toujours `C`.

À noter que `<->` est défini comme une conjonction de deux implications, c'est-à-dire que `A <-> B` doit être lu comme `(A -> B) /\ (B -> A)`. Par conséquent, `split` peut être utilisé pour prouver un `<->` en prouvant les deux implications.

Prouver en Coq les formules suivantes:

```coq
Lemma comm_conj : A /\ B <-> B /\ A.
Proof.

Qed.

Lemma comm_disj : A \/ B <-> B \/ A.
Proof.

Qed.

Lemma assoc_conj : (A /\ B) /\ C <-> A /\ (B /\ C).
Proof.

Qed.

Lemma assoc_disj : (A \/ B) \/ C <-> A \/ (B \/ C).
Proof.

Qed.
```

### True et False ###

La proposition `True` est toujours vraie. La proposition `False` est toujours fausse. On peut prouver `True` avec la tactique `exact I` (équivalent de la règle d'introduction du ⊤ de la déduction naturelle). On peut remplacer n'importe quel but par `False` avec la tactique `exfalso` (équivalent de la règle d'élimination du ⊥ de la déduction naturelle). De même, on peut prouver n'importe quel but si le contexte contient une hypothèse `H : False` (`exfalso; assumption` fonctionnerait, mais on peut aussi utiliser `destruct H`). Nous expliquerons plus tard comment `destruct` fait pour être capable de gérer à la fois les conjonctions, les disjonctions et le cas de `False`.

Prouver en Coq les formules suivantes:

```coq
Lemma true_impl : True.
Proof.

Qed.

Lemma false_impl : False -> A.
Proof.

Qed.

Lemma true_conj : True /\ A <-> A.
Proof.

Qed.

Lemma false_conj : False /\ A <-> False.
Proof.

Qed.

Lemma true_disj : True \/ A <-> True.
Proof.

Qed.

Lemma false_disj : False \/ A <-> A.
Proof.

Qed.
```

### Négation ###

La négation `~A` est définie comme `A -> False`. Par conséquent, face à un but `~A`, `intros H` introduit l'hypothèse `H : A` dans le contexte et remplace le but par `False`. Face à un but `False`, vous pouvez utiliser une hypothèse ou un lemme dont la conclusion est une négation avec la tactique `apply`. Si vous préférez travailler sur un but dans lequel on a remplacé la négation par sa définition, vous pouvez utiliser la tactique `unfold "~"` (ou `unfold "~" in *` pour agir également dans le contexte).

Prouver en Coq les formules suivantes:

```coq
Lemma double_neg : A -> ~~A.
Proof.

Qed.

Lemma contra : (A -> B) -> ~B -> ~A.
Proof.

Qed.
```

La preuve suivante n'est pas très intuitive. Pour la trouver, on peut chercher la "seule voie" raisonnable à chaque étape de la preuve. Demandez un indice à vos voisins si vous bloquez trop longtemps sur cette preuve.

Attention à ne pas être tenté d'utiliser `destruct` sur une hypothèse de la forme `~(A \/ B)`. Cela aurait le malheur de fonctionner, mais en vous faisant perdre de l'information précieuse pour la suite de la preuve. Pour le moment, on réservera `destruct` aux hypothèses de la forme `A /\ B`, `A \/ B` ou `False` (or, `~(A \/ B)` n'est pas de cette forme à cause de la négation).

```coq
Lemma double_neg_excluded_middle : ~~(A \/ ~A).
Proof.

Qed.
```

### Quelques exercices supplémentaires ###

Notons que la tactique `unfold` peut aussi être utilisée pour remplacer `<->` par sa définition. Par exemple, `unfold "<->"` remplace le but `A <-> B` par `(A -> B) /\ (B -> A)`.

Jusqu'à présent, on a plutôt fait du raisonnement "en arrière" (du but, vers les hypothèses). Parfois, il peut être utile de raisonner "en avant". La tactique `apply` a une variante qui le permet : `apply ... in ...`. Par exemple, si le contexte contient les hypothèses `H : A -> B` et `HA : A`, alors `apply H in HA` remplace `HA : A` par `HA : B`.

Prouver en Coq les formules suivantes:

```coq
Lemma iso_curry : (A /\ B -> C) <-> (A -> B -> C).
Proof.

Qed.

Lemma distrib_conj : A /\ (B \/ C) <-> (A /\ B) \/ (A /\ C).
Proof.

Qed.

Lemma distrib_disj : A \/ (B /\ C) <-> (A \/ B) /\ (A \/ C).
Proof.

Qed.

Lemma distrib_conj_impl : (A -> (B /\ C)) <-> (A -> B) /\ (A -> C).
Proof.

Qed.

Lemma distrib_disj_impl : ((A \/ B) -> C) <-> (A -> C) /\ (B -> C).
Proof.

Qed.
```

Programmation fonctionnelle en Coq
----------------------------------

Laissons de côté les preuves pour l'instant. Pour pouvoir prouver des programmes corrects en Coq, encore faut-il pouvoir les définir. Par conséquent, Coq intègre un langage de programmation (fonctionnel), appelé Gallina, qui permet de définir des fonctions et des types de données.

Ce langage est très proche d'OCaml, mais il y a quelques différences. Par exemple, les fonctions sont définies avec `Definition` au lieu de `let`, les définitions récursives avec `Fixpoint` au lieu de `let rec` et les types sont définis avec `Inductive` au lieu de `type`. Il n'y a pas de restrictions sur les noms des constructeurs et les noms de variables, qui peuvent commencer aussi bien par une minuscule qu'une majuscule.

Mais la plus grande différence, à la fois avec OCaml et avec les autres langages de programmation que vous connaissez, est que Gallina n'est pas un langage "Turing-complet". Pour pouvoir définir une fonction en Gallina, il faut pouvoir prouver qu'elle termine. Le plus souvent, cela se fait en utilisant la récursion structurelle, ce qui veut dire que la fonction a un argument qui diminue (structurellement) à chaque appel récursif. Nous définirons des fonctions récursives structurelles dans la suite de ce TP. Mais commençons par quelques exemples de fonctions non récursives.

### Types énumérés ###

Une autre différence notable de Coq par rapport à d'autres langages de programmation est que Coq ne fournit quasiment aucune fonctionnalité "pré-définie". Par exemple, il n'y a pas de type `bool` prédéfini dans le langage (mais la bibliothèque standard en fournit une définition). Par conséquent, nous pouvons redéfinir nous-mêmes le type `bool` :

```coq
Module Bool.

Inductive bool : Type :=
  | true : bool
  | false : bool.
```

Nous pouvons ensuite définir des fonctions sur ce type par pattern-matching :

```coq
Definition negb (b : bool) : bool :=
  match b with
  | true => false
  | false => true
  end.
```

On pourra remarquer quelques différences syntaxiques avec l'équivalent OCaml :

```ocaml
type bool = True | False

let negb (b : bool) : bool =
  match b with
  | True -> False
  | False -> True
```

En particulier, dans les clauses du `match`, le séparateur entre le motif et le corps est `=>` au lieu de `->`, et les `match` de Coq doivent toujours finir par un `end`.

Vous pouvez évaluer cette fonction sur des exemples en utilisant la commande `Eval compute` :

```coq
Eval compute in negb true.
Eval compute in negb false.
```

Placez le curseur sur chacune de ces lignes pour voir le résultat dans le panneau de droite.

Nous pouvons aussi prouver des propriétés sur cette fonction. Pour le moment, nous allons nous limiter à des propriétés triviales, mais nous verrons plus tard comment prouver des propriétés plus intéressantes.

```coq
Example negb_true : negb true = false.
Proof.
  simpl.
  reflexivity.
Qed.

Example negb_false : negb false = true.
Proof.
  simpl.
  reflexivity.
Qed.
```

Ces preuves contiennent deux nouvelles tactiques : `simpl` permet de simplifier le but en effectuant des étapes de calcul, et `reflexivity` permet de conclure lorsque le but est une égalité entre deux termes que Coq reconnaît comme égaux. En fait, `reflexivity` est capable de faire des étapes de calcul pour arriver à des termes égaux, donc dans ces preuves, `simpl` est inutile. (Vous pouvez le vérifier en supprimant les `simpl`).

Définir les fonctions `andb`, `orb` et `xorb` sur `bool` (se limiter à un seul `match` sur le premier argument) :

```coq
Definition andb (b1 b2 : bool) : bool (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de andb à la place *)
  . Admitted.
```

Si votre définition est correcte, les tests suivants (qui correspondent à la table de vérité de `andb`) devraient passer :

```coq
Example test_andb1: (andb true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_andb2: (andb true false) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb3: (andb false true) = false.
Proof. simpl. reflexivity. Qed.
Example test_andb4: (andb false false) = false.
Proof. simpl. reflexivity. Qed.
```

```coq
Definition orb (b1 b2 : bool) : bool (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de orb à la place *)
  . Admitted.

Example test_orb1: (orb true true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
```

```coq
Definition xorb (b1 b2 : bool) : bool (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de xorb à la place *)
  . Admitted.

Example test_xorb1: (xorb true true) = false.
Proof. simpl. reflexivity. Qed.
Example test_xorb2: (xorb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_xorb3: (xorb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_xorb4: (xorb false false) = false.
Proof. simpl. reflexivity. Qed.
```

Coq fournit une syntaxe simplifiée pour le pattern-matching sur les booléens. Par exemple, la définition de `negb` peut être simplifiée comme suit :

```coq
Definition negb' (b : bool) : bool :=
  if b then false else true.

End Bool.
```

On remarquera qu'on a pu se servir du `if` alors que nous sommes en train de manipuler les booléens que nous avons nous-même définis, et pas ceux de la bibliothèque standard. Comment est-ce possible ? En fait, la syntaxe if ... then ... else ... est juste du sucre syntaxique pour du pattern-matching sur des types inductifs à deux constructeurs. Comme on peut le voir dans l'exemple suivant, le nom du type ou des constructeurs n'a pas d'importance :

```coq
Inductive toto : Type :=
  | tata : toto
  | tutu : toto.

Definition negt (t : toto) : toto :=
  if t then tutu else tata.

Eval compute in negt tata.
```

### Types paramétrés ###

Un type paramétré bien connu est le type `option` d'OCaml :

```ocaml
type 'a option = None | Some of 'a
```

L'équivalent en Coq est le suivant :

```coq
Module Option.

Inductive option (A : Type) : Type :=
  | None : option A
  | Some : A -> option A.
```

En Coq, le polymorphisme est toujours explicite. `option` est donc une fonction qui prend un type en argument et renvoie un type :

```coq
Check option.
```

De même, `None` est une fonction qui prend le type `A` en argument et renvoie une valeur de type `option A` et `Some` est une fonction de deux arguments, le premier de type `A` et le second de type `option A`.

```coq
Eval compute in None bool.
Eval compute in Some bool true.
```

Pour éviter d'avoir à expliciter le type `A` à chaque fois que l'on utilise les constructeurs, on dit à Coq de considérer ces arguments comme implicites (syntaxe `{...}` ci-dessous) :

```coq
Arguments None {A}.
Arguments Some {A} _.
```

Désormais, on peut écrire `None` au lieu de `None bool` et `Some true` au lieu de `Some bool true`.

```coq
Eval compute in None. (* Coq ne sait pas encore quel sera la valeur de A *)
Eval compute in Some true.
```

Nous pouvons maintenant définir des fonctions par pattern-matching sur les valeurs de type `option` :

```coq
Definition with_default {A : Type} (default : A) (o : option A) : A :=
  match o with
  | None => default
  | Some x => x
  end.

Lemma with_default_some (A : Type) (default : A) (x : A) :
  with_default default (Some x) = x.
Proof. simpl. reflexivity. Qed.
```

Définir la fonction `is_none` qui renvoie `true` si son argument est `None` et `false` sinon :

```coq
Definition is_none {A : Type} (o : option A) : bool (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de is_none à la place *)
  . Admitted.

Example test_is_none_none (A : Type) : is_none (A := A) None = true.
Proof. simpl. reflexivity. Qed.
Example test_is_none_some (A : Type) (x : A) : is_none (Some x) = false.
Proof. simpl. reflexivity. Qed.
```
```

Définir la fonction `map_option` qui applique une fonction à l'intérieur d'un `option` :

```coq
Definition map_option {A B : Type} (f : A -> B) (o : option A) : option B (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de map_option à la place *)
  . Admitted.

Example test_map_option_none (A B : Type) (f : A -> B) :
  map_option f None = None.
Proof. simpl. reflexivity. Qed.
Example test_map_option_some (A B : Type) (f : A -> B) (x : A) :
  map_option f (Some x) = Some (f x).
Proof. simpl. reflexivity. Qed.
```

Lorsqu'on définit des fonctions qui prennent d'autres fonctions en argument, comme `map_option` ci-dessus, il est souvent utile de pouvoir utiliser des fonctions anonymes. En Coq, on peut définir des fonctions anonymes avec la syntaxe `fun x => ...` :

```coq
Example test_map_option_double (x : nat) :
  map_option (fun y => y + y) (Some x) = Some (x + x).
Proof. simpl. reflexivity. Qed.

End Option.
```

À noter que dans les langages de programmation (qu'ils soient principalement fonctionnels ou non), les fonctions anonymes sont parfois aussi appelées lamdbas (ou plus préciément des λ-abstractions) en référence au lambda-calcul.

### Types récursifs ###

Le type des entiers n'est pas non plus prédéfini en Coq (mais à nouveau, la bibliothèque standard en fournit une définition). Nous pouvons le définir comme suit :

```coq
Module NatDef.

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

End NatDef.
```

Cette représentation des entiers naturels utilise le symbole `S` (pour "successeur") pour représenter l'entier `n+1` à partir de l'entier `n`. Par exemple, `S (S (S O))` représente l'entier `3`. Elle est dite "unaire", car cela revient à compter avec des bâtons (le nombre de `S`). Il est également possible de représenter les entiers en base 2, qui est la base préférée des ordinateurs, mais la représentation unaire est plus simple à manipuler dans les définitions et les preuves.

La bibliothèque standard de Coq fournit une notation permettant d'écrire `0`, `1`, `2`, etc. au lieu de `O`, `S O`, `S (S O)`, etc. :

```coq
Check 0.
Check 1.
Check (S (S 0)).
```

Définir la fonction `pred` qui calcule le prédécesseur d'un entier :

```coq
Definition pred (n : nat) : nat (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de pred à la place *)
  . Admitted.

Example test_pred_0 : pred 0 = 0.
Proof. simpl. reflexivity. Qed.

Example test_pred_Sn (n : nat) : pred (S n) = n.
Proof. simpl. reflexivity. Qed.
```

Nous pouvons définir des fonctions par récursion structurelle sur les entiers. Par exemple, la fonction `add` qui calcule la somme de deux entiers peut être définie comme suit :

```coq
Fixpoint add (n m : nat) : nat :=
  match n with
  | O => m
  | S n' => S (add n' m)
  end.
```

Si besoin, on peut préciser à Coq quel est l'argument qui diminue structurellement à chaque appel récursif :

```coq
Fixpoint add' (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S n' => S (add' n' m)
  end.
```

Coq infère cette information automatiquement lorsqu'on ne la fournit pas explicitement, mais il n'y arrive pas toujours.

Définir la fonction `mul` qui calcule le produit de deux entiers :

```coq
Fixpoint mul (n m : nat) : nat (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de mul à la place *)
  . Admitted.

Example test_mul_0_0 : mul 0 0 = 0.
Proof. simpl. reflexivity. Qed.

Example test_mul_10_10 : mul 10 10 = 100.
Proof. simpl. reflexivity. Qed.
```

Définir la fonction `fact` qui calcule la factorielle d'un entier :

```coq
Fixpoint fact (n : nat) : nat (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de fact à la place *)
  . Admitted.

Example test_fact_0 : fact 0 = 1.
Proof. simpl. reflexivity. Qed.

Example test_fact_3 : fact 3 = 6.
Proof. simpl. reflexivity. Qed.
```

### Limites de la récursion structurelle ###

On souhaite définir la fonction `fib` qui calcule le `n`-ième nombre de Fibonacci.

La définition suivante ne fonctionne pas :

```coq
Fixpoint fib (n : nat) : nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | S (S n') => fib n' + fib (S n')
  end.
```

Trouver une manière de la corriger (toujours sans utiliser de fonction auxiliaire récursive), puis proposer une version alternative `fib'` qui utilise une fonction auxiliaire récursive.

```coq
Example test_fib_0 : fib 0 = 0.
Proof. simpl. reflexivity. Qed.

Example test_fib_10 : fib 10 = 55.
Proof. simpl. reflexivity. Qed.

Definition fib' (n : nat) : nat (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de fib' à la place *)
  . Admitted.

Example test_fib'_0 : fib' 0 = 0.
Proof. compute. reflexivity. Qed.

Example test_fib'_10 : fib' 10 = 55.
Proof. compute. reflexivity. Qed.
```

On rappelle que la fonction Ackermann est définie comme suit :

- `A(m, n, 0) = m + n`
- `A(m, 1, k + 1) = m`
- `A(m, n + 1, k + 1) = A(m, A(m, n, k + 1), k)`

Cette définition présente l'inconvénient de ne pas être totale (pas de cas pour `A(m, 0, k + 1)`). On peut la rendre totale en ajoutant :

- `A(m, 0, 1) = 0`
- `A(m, 0, k + 2) = 1`

Auquel cas, la deuxième équation devient redondante et peut être supprimée.

Définir la fonction `Ack` qui calcule la fonction d'Ackermann. On commencera par remarquer que définir `Ack` de manière naïve ne fonctionne pas. Pour contourner cette difficulté, on pourra remarquer que la fonction d'Ackermann peut aussi s'exprimer ainsi :

`A(m,n,k+1)` = «appliquer `n−1` fois `n ↦ A(m,n,k)` à `m`»

Par conséquent, commencer par définir la fonction `iterate` qui applique une fonction `f` `n` fois à un argument `x`, puis s'en servir pour définir `Ack` :

```coq
Fixpoint iterate {A : Type} (f : A -> A) (n : nat) (x : A) {struct n} : A (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de iterate à la place *)
  . Admitted.

Example test_iterate_0 (A : Type) (f : A -> A) (x : A) :
  iterate f 0 x = x.
Proof. simpl. reflexivity. Qed.

Example test_iterate_1 (A : Type) (f : A -> A) (x : A) :
  iterate f 1 x = f x.
Proof. simpl. reflexivity. Qed.

Example test_iterate_2 (A : Type) (f : A -> A) (x : A) :
  iterate f 2 x = f (f x).
Proof. simpl. reflexivity. Qed.
```

```coq
Fixpoint Ack (m n k : nat) : nat (* := *)
  (* Supprimer la ligne ci-dessous et écrire la définition de Ack à la place *)
  . Admitted.

Example test_Ack_2_5_0 (m n : nat) : Ack 2 5 0 = 7.
Proof. simpl. reflexivity. Qed.

Example test_Ack_2_5_1 (m n : nat) : Ack 2 5 1 = 10.
Proof. simpl. reflexivity. Qed.

Example test_Ack_2_5_2 (m n : nat) : Ack 2 5 2 = 32.
Proof. simpl. reflexivity. Qed.
```