Pas du tout, à des souvenirs traumatisants du professeur qui ponctuait ses corrections par des références à l'évidence même sans réel explication.
Au temps pour moi, avec le sujet de la dépêche, j'ai du me sentir visé : dans l'autre journal j'avais fait un appel à l'évidence et tu m'avais répondu que même si cela paraissait évident, il fallait démontrer que la solution proposée apportait quelque chose.
Pour ce qui est de l'appel à l'évidence, dans l'enseignement, c'est toujours délicat : l'évidence est très subjective (ce qui est évident pour l'un, ne l'est pas forcément pour l'autre) et dans une correction, ce n'est pas le meilleur endroit pour y faire appel.
Ceci étant, même Coq a une notion d'évidence avec la tactique trivial :
Remarka:foralln,0+n=n+0.Proof.trivial.Qed.
mais en réalité, il trouve cela trivial car il applique directement un théorème qui est dans sa base de données (et qui énonce la même chose). En revanche, la preuve du théorème initial n'est pas triviale pour la machine, il faut la faire à la main par récurrence; là où avec un interlocuteur humain, un mathématicien serait tenté d'écrire : évident par récurrence sur n (en précisant toutefois le mode de démonstration à utiliser).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: l'assignation ne va jamais venir
Posté par kantien . En réponse à la dépêche Seconde mise en demeure pour l'association LinuxFr. Évalué à 4.
Au temps pour moi, avec le sujet de la dépêche, j'ai du me sentir visé : dans l'autre journal j'avais fait un appel à l'évidence et tu m'avais répondu que même si cela paraissait évident, il fallait démontrer que la solution proposée apportait quelque chose.
Pour ce qui est de l'appel à l'évidence, dans l'enseignement, c'est toujours délicat : l'évidence est très subjective (ce qui est évident pour l'un, ne l'est pas forcément pour l'autre) et dans une correction, ce n'est pas le meilleur endroit pour y faire appel.
Ceci étant, même Coq a une notion d'évidence avec la tactique
trivial:mais en réalité, il trouve cela trivial car il applique directement un théorème qui est dans sa base de données (et qui énonce la même chose). En revanche, la preuve du théorème initial n'est pas triviale pour la machine, il faut la faire à la main par récurrence; là où avec un interlocuteur humain, un mathématicien serait tenté d'écrire : évident par récurrence sur
n(en précisant toutefois le mode de démonstration à utiliser).Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.