Je ne prétends pas débattre avec le niveau requis, mais peut on encore parler de démonstration quand c'est "trivial" et que cela tient en une ligne ?
Oui, pourquoi pas ? De même que les maths ont fait un bond en avant quand zéro a été reconnu comme un vrai nombre, la logique marche mieux quand on reconnaît aussi les démonstrations triviales comme de vraies démonstrations :-)
De ce que je comprends il y a une sorte de consensus qui considère que les preuves formelles n'ont pas besoin d'aller au delà d'un certain niveau de détail. Les résultats "triviaux" n'ont pas à être démontrés et peuvent simplement être placés dans une bibliothèque.
Je ne sais pas d'où tu tires cette impression mais soit j'ai mal compris ce que tu veux dire, soit c'est faux.
C'est quand même un peu le but de la preuve formelle que tout soit fait dans tous les détails y compris triviaux. Bien sûr, quand on est en plein développement, on peut laisser des lemmes triviaux comme admis pour les prouver plus tard, et il peut arriver qu'on les garde non prouvés dans le résultat fini, mais ce n'est pas commun (et quand c'est le cas, ça va normalement être mentionné explicitement).
Les projets de formalisation réussis que j'ai mentionnés (retournement de la sphère, etc.) n'utilisent aucun lemme admis (seulement des axiomes « logiques » comme le tiers exclu).
Et cette preuve « rfl » de 2+2=4 (plus généralement de l'égalité entre deux termes définitionnellement égaux) est bien une preuve, pas un appel à un lemme admis.
[^] # Re: Preuves de programme et preuves de théorèmes
Posté par jeanas (site web personnel, Mastodon) . En réponse à la dépêche Programmer des démonstrations : une modeste invitation aux assistants de preuve. Évalué à 4.
Oui, pourquoi pas ? De même que les maths ont fait un bond en avant quand zéro a été reconnu comme un vrai nombre, la logique marche mieux quand on reconnaît aussi les démonstrations triviales comme de vraies démonstrations :-)
Je ne sais pas d'où tu tires cette impression mais soit j'ai mal compris ce que tu veux dire, soit c'est faux.
C'est quand même un peu le but de la preuve formelle que tout soit fait dans tous les détails y compris triviaux. Bien sûr, quand on est en plein développement, on peut laisser des lemmes triviaux comme admis pour les prouver plus tard, et il peut arriver qu'on les garde non prouvés dans le résultat fini, mais ce n'est pas commun (et quand c'est le cas, ça va normalement être mentionné explicitement).
Les projets de formalisation réussis que j'ai mentionnés (retournement de la sphère, etc.) n'utilisent aucun lemme admis (seulement des axiomes « logiques » comme le tiers exclu).
Et cette preuve « rfl » de 2+2=4 (plus généralement de l'égalité entre deux termes définitionnellement égaux) est bien une preuve, pas un appel à un lemme admis.