Bonjour,
Je ne sais pas quelle tactique je dois utiliser pour prouver la formule suivante:
forall A : Prop, A -> ~~A.
Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter
[COQ] Quelle tactique dois-je utiliser
Bonjour,
Je ne sais pas quelle tactique je dois utiliser pour prouver la formule suivante:
forall A : Prop, A -> ~~A.
J'imagine que tu as déjà essayé intros A H1. unfold not..
Ensuite :
intro H2. apply H2. exact H1.
Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
Avant de poser une question je lis les règles du forum.
merci de votre aide, c'était le unfold not que je ne connaissais pas.
Vous avez un bloqueur de publicités installé.
Le Club Developpez.com n'affiche que des publicités IT, discrètes et non intrusives.
Afin que nous puissions continuer à vous fournir gratuitement du contenu de qualité, merci de nous soutenir en désactivant votre bloqueur de publicités sur Developpez.com.
Répondre avec citation
Partager