Pour résoudre ces exercices, vous pouvez utiliser les théorèmes suivants (déjà prouvés dans Naturels) :
add_0_l : ∀ n : nat, 0 + n = n
add_1_l : ∀ n : nat, 1 + n = S n
add_succ_l : ∀ n m : nat, S n + m = S (n + m)
ainsi, bien sûr, que les théorèmes prouvés précédemment dans ce sujet.
La fonction prédécesseur est définie de la façon suivante :
L'image de 0 est 0, c'est un peu pratique et surtout, on ne peut pas définir
de fonction partielle en Coq (en maths, on aurait plutôt dit que
pred 0
n'est pas défini).
exfalso
.
pred_succ
de droite à gauche, prouver :
Une telle propriété s'appelle l'injectivité de la fonction successeur qu'on pourrait aussi formuler de la façon suivante : "Deux entiers distincts ont des successeurs distincts."
D'ailleurs, allons-y, prouvons le aussi sous cette forme.
a <> b
n'est rien d'autre que la
proposition
a = b -> False
.
Nous allons maintenant voir que la *magie* derrière
discriminate
n'est
que de pouvoir définir une fonction qui fait la différence entre
0
et
S n
.
En fait, la tactique
discriminate
génère elle-même une fonction un peu
comme
pred
pour prouver
False
à partir de quelque chose comme
S n = 0
.
La fonction (à valeurs dans
Prop
) utilisée par discriminate sur
nat
est
à peu près la suivante :
On commence par prouver les deux propriétés attendues.
Pour la première, on vous la donne.
La proposition
True
est une proposition dont le seul constructeur, sans
argument, s'appelle
I
.
Autrement dit,
I
est une preuve de
True
qui n'a besoin de rien.
discriminate
.
discriminate
, avec juste
succ_inj
et
neq_succ_0
.