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 = nadd_1_l : ∀ n : nat, 1 + n = S nadd_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.