4
Y at-il un moyen de prouver automatiquement les inégalités simples comme 1/2 >= 0?, À savoirComment prouver automatiquement l'inégalité simple des nombres réels dans Coq?
Require Export Coq.Reals.RIneq.
Local Open Scope Z_scope.
Local Open Scope R_scope.
Example test: /2 >= 0.
j'ai l'expérience avec pas beaucoup ring ou field et I am having trouble with even proving simple equalities such as 1/2 = 2/4. Ce que je cherche est quelque chose comme omega mais fonctionne pour les nombres réels et les inégalités.
@Johan, j'ai annulé le changement de tag du nombre réel au nombre à virgule flottante parce que je voulais poser des questions sur les nombres réels réels, pas leurs approximations à virgule flottante. – tinlyx
Le problème est que le nombre réel a seulement 7 hits, donc je pense que vous feriez mieux de chercher une balise qui est utilisée régulièrement. Je suis sûr qu'il y a un synonyme qui couvre ce que vous voulez. – Johan