Les nombres réels de Coq sont définis d'une certaine manière dont on ne se souciera pas (bon, en fait avec les coupures de Dedekind, mais ce n'est qu'une façon parmi d'autre de les construire et ce que nous ferons n'en dépend pas). Ce qui faut retenir est :
<, qui est
total, compatible avec l'addition et la multiplication par un réel positif
🚧 On expérimente ici une nouvelle interface (maison) pour les réels (les corps en général). Ne pas hésiter à faire des retours !
NB: cette partie est assez technique et sans intéractions, elle peut être lue en diagonale
On suppose donné un module, c'est-à-dire un composant logiciel (un fichier, par exemple), définissant les choses suivantes. Si c'est trop abstrait pour vous, pensez juste qu'on travaille avec des nombres réels.
Avec des mots : un module qui satisfait AxiomesCorps définit :
t+ et
*x est noté
- xx est noté
/ xt deux éléments
0 et
1 qui sont distincts et
respectivement neutres (à gauche) pour l'addition et la multiplication
Pour faciliter les recherches, on cache tout ce qui est prédéfini dans Coq/Rocq :
Pour l'instant voici tous les résultats qu'on a sur l'addition :
Et voici même, tout ce qu'on connaît tout court :
N'hésitez pas à entrer ces commandes à tout moment pour pouvoir chercher les résultats utilisables.
Voici également deux lemmes évidents :
Les lemmes précédents n'ont aucun contenu mathématique, on voit dans les preuves qu'on n'utilise aucune propriété de l'addition. Mais ils sont utiles en raisonnement vers l'avant, pour ajouter un même élément à gauche et à droite d'une égalité. Voici un exemple un peu idiot :
Un opposé d'un réel
x est un réel
y tel que x + y = 0.
En fait, on peut prouver que l'opposé, quand il existe, est unique.
Cet opposé, étant unique, peut avoir sa propre notation et ici on suppose
qu'il existe toujours et est noté
- x.
Pour rappel, on a supposé :
Avec la commutativité, on en déduit facilement :
On peut faire "changer de côté" un terme dans une équation :
On peut aussi "simplifier" les équations.
Par commutativité, on a facilement :
Remarque :
add_eq_reg_l ou
add_eq_compat_l ?
On a des énoncés réciproques l'un de l'autre.
Comme dit précédemment,
add_eq_compat_l n'a pas de contenu mathématique
mais est utile pour ajouter un même nombre à un égalité
dans une hypothèse
(raisonnement vers l'avant).
Par contre,
add_eq_reg_l suppose l'existence d'un opposé, il sert à
En guise d'application, une petite équation du premier degré :
Il y a un peu de pénibilité avec l'associativité. Rappelez-vous qu'avec l'addition les parenthèses cachées sont à gauche. Si ça ne passe pas, vous pouvez sauter cet exercice et y revenir plus tard.
Sans rien supposer sur la multiplication, on a déjà (comme pour l'addition) :
De plus, on rappelle que la multiplication doit être distributive sur l'addition :
On en déduit :
On peut maintenant montrer que 0 est absorbant pour la multiplication.
Avant de se lancer sur la preuve formelle, on cherche une preuve en mathématiques plus informelles.
Beaucoup plus facile maintenant qu'on a le premier :
Dans un corps, 0 et 1 doivent être distincts.
Et enfin tout élément x non nul a un inverse. Cet inverse est unique (même preuve que pour l'unicité de l'opposé et c'est normal...) et est noté en mathématiques 1 / x, en Coq / x.
On en déduit immédiatement :
L'existence d'un inverse permet de simplifier les produits dans les égalités.
Le théorème précédent est-il encore vrai sans la condition sur
x ?
Si oui, le prouver, si non, trouver un contre-exemple.
On en déduit facilement :
Puis on montre que pour qu'un produit soit nul, il faut qu'un de ses facteurs soit nuls. Mais pour ça on a besoin du théorème disant qu'on peut raisonner par cas sur l'égalité ou non de deux réels avec le tiers exclu.
Maintenant, l'inverse d'un réel non nul est non nul :
Le produit de deux réels non nuls est non nul.
La division est définie à partir de la multiplication et de l'inverse :
Enfin, l'inverse de (x / y) vaut (y / x) à condition que ces réels soient non nuls.