TP Logique : preuves inductives en Coq
Dans ce TP nous allons prouver des propriétés simples à l'aide de Coq.

Table des Matières


Nous allons commencer par travailler sur les entiers naturels. Créez un fichier
entiers.v
, et ajoutez la définition suivante :
Inductive entier : Type := | O : entier | S : entier -> entier.
Attention : le constructeur du cas de base est la lettre O majuscule, pas le chiffre 0.

Addition

Commençons par démontrer quelques propriétés de l'addition. L'addition elle-même est définie comme suit :
Fixpoint plus (n m : entier) : entier := match n with | O => m | S n' => S (plus n' m) end.
Les preuves de ce TP seront en général faites par induction.

Associativité

L'associativité de l'addition est définie comme suit :
n + (m + p) = (n + m) + p
.
Prouvez ce théorème :
Theorem associativite (n m p : entier) : plus n (plus m p) = plus (plus n m) p.

Symétrie

La symétrie s'exprime par
n + p = p + n
. Aussi simple soit cette formule, elle est plus compliquée à démontrer que l'associativité. Nous allons démontrer quelques lemmes, puisles utiliser avec la tactique
rewrite
.
Prouvez le lemme suivant :
Lemma plus0 (n : entier) : plus n O = n.
Prouvez le lemme suivant :
Lemma plusS (n p : entier) : plus n (S p) = S (plus n p).
Vous êtes maintenat équipés pour prouver le théorème suivant :
Theorem symetrie (n m : entier) : plus n m = plus m n.

Simplification

Nous voulons montrer que l'on peut simplifier une expression de cette façon :
n + a = p + a ⇒ n = p
Démontrez tout d'abord le lemme suivant :
Lemma egalS (n m : entier) : n = m <-> S n = S m.
Vous aurez besoin de la tactique
injection
, qui utilise le fait que les constructeurs des types inductifs sont injectifs.
Vous pouvez maintenant démontrer le théorème suivant :
Theorem simplification (a n m : entier) : plus a n = plus a m <-> n = m.

Multiplication

Nous allons maintenant passer à la multiplication. Elle est définie comme suit :
Fixpoint mult (n m : entier) : entier := match n with | O => O | S n' => plus m (mult n' m) end.

Symétrie

Nous allons commencer par la symétrie, et deux lemmes préliminaires.
Démontrez tout d'abord le lemme suivant :
Lemma multO (n : entier) : mult n O = O.
Puis démontrez ce lemme :
Lemma assoc2 (n m p : entier) : plus n (plus m p) = plus m (plus n p).
Démontrez ensuite le lemme suivant :
Lemma multsn (n m : entier) : mult n (S m) = plus n (mult n m).
Enfin, démontrez le théorème :
Theorem symetriemult (n m : entier) : mult n m = mult m n.

Distributivité

La distributivité de la multiplication sur l'addition correspond à la formule suivante :
a × (b + c) = (a × b) + (a × c)
Démontrez ce théorème :
Theorem distributivite (n m p : entier) : mult (plus n m) p = plus (mult n p) (mult m p).
Vous pouvez avoir besoin de la tactique
symmetry
, qui est la symétrie de l'égalité.

Associativité

Démontrez l'associativité de la multiplication :
Theorem associativitemult (n m p : entier) : mult n (mult m p) = mult (mult n m) p.

Listes

Nous allons maintenant travailler sur les listes d'entiers. Créez un fichier
listes.v
dans lequel vous travaillerez sur les questions suivantes. Nous utiliserons le type
nat
de la librairie de Coq.
Inductive liste : Type := | nil : liste | C : nat -> liste -> liste.
Définissez la fonction
longueur
, qui calcule la longueur d'une liste. Vous pouvez vérifier si elle fonctionne à l'aide de la commande
Compute
.
Définissez la fonction
concat
, qui concatène deux listes.
Démontrez ce théorème :
Theorem long (l m : liste) : longueur(concat l m) = longueur l + longueur m.
Définissez la fonction
ajoutqueue
, qui ajoute un élément en queue d'une liste.
Démontrez ce théorème :
Theorem lgajout (x : nat) (l : liste) : longueur(ajoutqueue x l) = 1 + longueur l.