Arithmétique: preuves d'algorithmes.
L'ensemble Nat des entiers de Peano.
C'est un ensemble qu'on définit par récurrence. Il est constitué d'une constante, o, et de ses successeurs, obtenus par la fonction s: Nat={o, (s o), (s (s o)), ...}
C'est exactement l'ensemble des termes construits avec la signature {o,s}.
Une première propriété facile:
L'ensemble Nat est défini par récurrence, aussi on va pouvoir faire de démonstrations par cas (destruct) ou par récurrence (induction) des propriétés de ses éléments.
Un premier exemple de démonstration :
La structure récursive de Nat permet aussi de définir des fonctions par récurrence, i.e. des fonctions récursives.
Définissons par exemple la fonction double
qui à x associe 2x:
si x=o, (double x)=o
si x=(s n), (double x) = (s (s (double n)))
La construction Fixpoint
permet de définir des fonctions récursives.
double (n:Nat) : Nat
signifie qu'on définit une fonction nommée double
définie par récurrence sur son argument n, de type Nat, et qui rend un élément de Nat.
match n with ... ... end
signifie que le résultat est un objet de type Nat, calculé selon les valeurs possibles de n, qui sont ici données par les deux formes que n peut avoir (puisque c'est un élément de Nat): soit o, soit (s n1).
On donne les valeurs voulues dans chacun de ces cas à l'intérieur de cette structure.
Cette fonction est vraiment un algorithme de calcul:
Et on peut montrer qu'elle a des propriétés:
Définissons maintenant l'addition (en mettant en commentaire des indications sur les cas traités, pour la compréhension de la définition).
C'est une définition par récurrence sur son second argument:
Montrons maintenant quelques propriétés de l'addition.
Dans le lemme suivant, on peut faire une récurrence sur n ou sur m.
Le bon choix est m, car l'addition est définie par récurrence sur son second argument. Si on choisit n, on a du mal...
Revenons à notre fonction double:
Montrons maintenant que notre addition est commutative:
Les premiers lemmes que l'on a démontrés semblent un peu triviaux...Mais sans eux, on aurait eu un mal fou à démontrer la commutativité. Du moins on se serait aperçu au cours de la preuve de leur utilité!
Maintenant l'associativité: