Exercices supplémentaires sur les entiers naturels (1ère partie)

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.

Exercice : Prouver le théorème suivant.

Il y a une petite difficulté, un peu artificielle, dans le deuxième cas du sens direct, due au fait que nous n'avons pas encore la commutativité de l'addition. On peut s'en sortir avec une nouvelle preuve par cas.

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).

Exercice : Prouver les deux règles de calcul qui suivent

Exercice : Prouver la règle suivante avec un raisonnement par cas.

Il y a un cas impossible. Penser à exfalso.

Exercice : En utilisant 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.

Exercice : prouver le lemme suivant.

Rappel : une inégalité de la 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.

Exercice : prouver le lemme suivant.

Exercice : prouver le lemme suivant sans utiliser discriminate.

Exercice : prouver le lemme suivant sans discriminate, avec juste succ_inj et neq_succ_0.