Ce sujet contient trois parties :
forall.
exists, ainsi que les
tactiques nécessaires pour
utiliser
une hypothèse ainsi quantifiée
(
destruct comme toujours...) et pour
prouver
ou introduire
une formule du type « il existe ... ».
forall
Un prédicat sur un certain type
X est une fonction de
X vers
Prop,
donc une proposition qui dépend d'une variable à valeur dans un certain
type.
Par exemple, on peut définir le prédicat
est_pair : nat -> Prop qui est
satisfait uniquement par les entiers naturels pairs.
On peut donc voir un prédicat comme une certaine propriété des éléments
d'un type.
Comme premier prédicat très simple, définissons
est_nul sur
nat.
Bien sûr on prouve facilement que
0 est nul :
On peut même aller plus loin :
N'oubliez pas
discriminate H, si H est est une preuve d'un égalité
fausse.
On se donne maintenant un type abstrait, noté
X (penser, par exemple
au type
nat) et deux prédicats sur
X.
Le quantificateur « pour tout » s'écrit
forall ou
forall en Coq :
forall x : X, P x
est la proposition qui dit que pour tout
x de type
X, la proposition
P x est vraie.
Avec le point de vue « prédicat », cela signifie qu'une certaine propriété
est satisfaite par tous les habitants d'un type.
L'énoncé
forall x : X, (P x) est encore une proposition.
La tactique
specialize n'est jamais indispensable mais souvent pratique.
L'idée est de fournir des arguments à une hypothèse universellement
quantifiée de façon à en avoir une version spécialisée.
On peut voir
specialize comme la tactique qui "utilise le
forall".
Voyons tout de suite des exemples :
On peut utiliser des "intro patterns" dans la partie "as ..."
Un exemple de tautologie du calcul des prédicats est le suivant.
Il faudrait vraiment connaître et comprendre intuitivement le théorème
précédent. En fait, on peut voir le quantificateur
forall comme
une généralisation du
/\.
Par exemple, pour un prédicat
P : nat -> Prop, dire que
forall n : nat, (P n) signifie qu'on a
(P 0) /\ (P 1) /\ (P 2) /\ (P 3) /\ ...
Avec la disjonction, en revanche, les choses sont différentes.
Prenez bien le temps de comprendre l'énoncé de façon intuitive avant de commencer la preuve.
La réciproque est-elle vraie ? Non, et c'est très important que vous le compreniez. Dans un premier temps, on peut essayer de voir ce qui bloque dans la preuve.
Voir où vous êtes bloqué et pourquoi. Laisser
Abort. (abandonner) à la
fin, le théorème est faux de toute façon.
Dans un second temps, c'est important de se convaincre que c'est faux
avec un contre-exemple.
Pour le type
X, on va prendre
nat, pour
P, notre prédicat
est_nul et pour
Q un nouveau prédicat
est_non_nul.
La prémisse du faux théorème précédent est bien sûr satisfaite.
Mais sa conclusion est fausse.
Indices :
H1 : forall (n : nat), n = 0.
Vous pouvez spécialiser cette hypothèse avant d'utiliser
discriminate.
False en utilisant une
hypothèse du type
H2 : forall (n : nat), n = 0 -> False.
Encore une fois, vous pouvez spécialiser cette hypothèse.
Vous devriez vraiment vous arrêter deux minutes pour bien noter qu'en
général il est FAUX que
(forall x, (P x \/ Q x)) -> (forall x, P x) \/ (forall x, Q x).
et noter le contre-exemple.
exists
Le quantificateur « il existe » s'écrit
exists
ou
exists dans des mathématiques en Coq.
Il se lit « il existe » :
exists x : X, P x est la proposition qui dit
qu'il y a (au moins) un
x de type
X tel que la proposition
P x
est vraie.
exists
En logique intuitionniste, pour prouver une proposition du type
« il existe un élément ayant telle propriété »,
la seule possibilité est
d'exhiber un tel élément
(appelé témoin). La tactique
exists, suivie de
ce témoin pressenti permet d'éliminer le quantificateur
exists.
Pour montrer qu'il existe
n tel que
n + 3 = 8,
il suffit
de montrer que
5 + 3 = 8
(c'est une intuition géniale qui m'a fait penser à
5).
exists.
On se donne de nouveau un type
X quelconque et deux prédicats
sur
X.
La formule
exists x, P x est encore de type
Prop.
Pour un type habité (c'est-à-dire ayant au moins un élément), on a le résultat très intuitif suivant.
Attention, une erreur très courante en mathématiques (ou même dans la logique de tous les jours) consiste à penser qu'avec un ou quelques exemples (donc des preuves de « il existe »), on montre « pour tout » :
X^2 - 4 a des racines réelles donc tous les polynômes en ont.
destruct
Pour utiliser une proposition avec
exists, on utilise de nouveau
la tactique
destruct. Noter la syntaxe
as [y H], où y est la
variable pour laquelle la propriété va être vraie, et
H la preuve que
cette propriété est vraie pour
y.
On peut aussi
destruct immédiatement une hypothèse avec un
«
intro pattern
».
On remplace
intros H2 par
intros [y H'] directement.
Le théorème précédent est important et intéressant.
Si on y réfléchit, le quantificateur
exists est d'une certaine façon une
généralisation de la disjonction
\/.
Par exemple, sur
nat, on peut penser à la proposition
exists (n : nat), P n
comme
(P 0) \/ (P 1) \/ (P 2) \/ (P 3) \/ ...
Voir où vous êtes bloqué et pourquoi. Laisser
Abort. (abandonner) à la
fin, le théorème est faux de toute façon.
Comme pour la propriété analogue avec
forall et
\/, nous allons
construire un contre-exemple pour montrer qu'il est
faux
que
(exists x : X, P x) /\ (exists y : X, Q y) -> (exists x, P x /\ Q x).
On va encore prendre
X = nat,
P = est_nul et
Q = est_non_nul.
La prémisse du faux théorème précédent est satisfaite par
nat,
est_nul
et
est_non_nul.
Mais la conclusion est évidemment fausse.
Les deux résultats suivants ont une réciproque en logique classique (c'est-à-dire une fois qu'on a ajouté le tiers exclu).
Remarquer la similitude avec l'une des lois de de Morgan :
Le lemme suivant dit en substance qu'un contre-exemple permet de nier une formule universellement quantifiée.
Encore une fois, remarquer la similitude avec :
On considère maintenant deux types quelconques
X et
Y.
Une fonction injective de
X vers
Y est telle que chaque élément
y de
Y a au plus un antécédent.
Une fonction surjective de
X vers
Y est telle que chaque élément
y
de
Y a au moins un antécédent.
Voyons tout de suite des exemples :
On va commencer par la fonction S (successeur) et une nouvelle fonction appelée « prédécesseur ».
Cette fonction est définie par un petit programme qui raisonne par cas sur la nullité ou non de son argument.
Les valeurs sont bien celles qu'on attend :
Sauf que c'est une fonction totale, le prédécesseur de 0 est (de façon un peu arbitraire) 0.
Comme il se doit, on définit deux petits lemmes pour ne pas avoir à se
reposer entièrement sur
simpl.
En fait, le lemme
pred_succ est assez fondamental : il dit que
la
composée
des fonctions
pred et
S est l'identité, autrement dit,
que
pred est réciproque à gauche de
S.
On va maintenant étudier l'injectivité et la surjectivité (ou non) des
fonctions
S et
pred.
Indice : utiliser
pred_succ pour réécrire dans le but.
En fait, on peut être plus précis:
Passons à des résultats généraux sur la composition des fonctions