Assistant de démonstrations d’(in)égalités

Georges Abitbol

Bonsoir,

je voudrais savoir si vous connaîtriez un assistant de démonstration d’égalités et d’inégalités qui soit pratique.

Pour décrire un peu plus précisément mon problème : j’ai de grosses sommes avec de nombreux indices, je fais des simplifications, je majore des morceaux, je remplace par des valeurs déjà connues, simplifie les fractions rationnelles apparaissant dans le calcul, etc. Le tout est fastidieux sur le papier. Le recopier en $\LaTeX$ l’est tout autant, surtout quand on se rend compte d’une erreur.

Je voudrais donc une sorte de programme qui permette de démontrer pas à pas de telles choses, c’est-à-dire que ce programme produise un programme tel que toute personne désireuse de vérifier la démonstration de l’inégalité n’ait qu’à vérifier qu’il compile.
 

J’imagine que Coq est suffisant (à part pour le calcul formel). Mais est-il nécessaire ? Et pratique ? Par exemple, la démonstration que je connais du fait que $L^2$ est stable par addition, c’est quelque chose comme ça : $(f+g)^2 \leq (\vert f \vert + \vert g \vert)^2 \leq (2\cdot \max\{\vert f\vert, \vert g\vert\})^2 \leq 4\max\{\vert f\vert^2, \vert g\vert^2\}$. Est-ce qu’une telle démonstration est pratique à écrire en Coq ?