Le 19 mars 2015 à 19:09, Micaela Mayero <mayero@lipn.univ-paris13.fr> a écrit :
Par contre, pour l'exo 1 du TD1, comme je l'avais dit à Pierre et Damiano, il faut que vous commenciez par avoir la preuve papier (ou dans la tête) très clairement. C'est comme lorsque vous écrivez un programme, si vous avez l'algo c'est mieux ;-)
Pour faire la preuve il faut commencer par eliminer A\/~A avec A=rac(2)^rac(2) est rationnel. Ensuite, suivant que vous êtes dans le cas gauche ou droit, vous donnez les valeurs adéquates à x et y.
Pour ceux qui voudraient finir l’exercice mais qui butent sur les tactiques, voici la liste de celles que j’ai utilisé : - exists, qui permet d’introduire un témoin d’existence (utilisation «exists t») - elim, qui fait toutes les éliminations en déduction naturelle - split, qui casse les conjonctions dans les buts en plusieurs sous-buts (\with-intro) - exact, qui permet d’utiliser une hypothèse globale (utilisation «exact hyp») - assumption, la règle identité - apply, qui remonte le long d’une implication - rewrite, qui ré-écrit le long d’une égalité, orientée de gauche à droite (utilisation «rewrite hyp», où hop est de la forme a=b) Je ne prétends pas que ce soit optimal ou quoi que ce soit :) À demain, — Luc