Je fais une preuve Coq. J'ai P -> Q comme hypothèse et (P -> Q) -> (~Q -> ~P) comme lemme. Comment puis-je transformer l'hypothèse en ~Q -> ~P?
Quand j'essaye de apply cela, je crée juste de nouveaux sous-objectifs, ce qui n'est pas utile.
En d'autres termes, je souhaite commencer par:
P : Prop
Q : Prop
H : P -> Q
Et se retrouver avec
P : Prop
Q : Prop
H : ~Q -> ~P
Étant donné le lemme ci-dessus - c'est-à-dire (P -> Q) -> (~Q -> ~P).
3 réponses
Ce n'est pas aussi élégant qu'un simple apply, mais vous pouvez utiliser pose proof (lemma _ _ H) as H0, où lemma est le nom de votre lemme. Cela ajoutera une autre hypothèse avec le type correct au contexte, avec le nom H0.
Si je voulais transformer H en place , j'irais avec la réponse de @ ejgallego, puisque SSReflect fait maintenant (à partir de Coq 8.7.0) une partie du Coq standard, mais voici une autre option :
Ltac dumb_apply_in f H := generalize (f H); clear H; intros H.
Tactic Notation "dumb" "apply" constr(f) "in" hyp(H) := dumb_apply_in f H.
Un test simple:
Variable (P Q : Prop).
Axiom u : (P -> Q) -> (~Q -> ~P).
Lemma test (H : P -> Q) : False.
Proof. dumb apply u in H. Abort.
C'est un cas où les vues ssreflect aident:
From Coq Require Import ssreflect.
Variable (P Q : Prop).
Axiom u : (P -> Q) -> (~Q -> ~P).
Lemma test (H : P -> Q) : False.
Proof. move/u in H. Abort.
apply u in H fonctionne également, mais il est trop intelligent pour son propre bien et en fait trop.
De nouvelles questions
coq
Coq est un système de gestion de preuves formel, un prouveur de théorèmes semi-interactif et un langage de programmation fonctionnel. Coq est utilisé pour la vérification de logiciels, la formalisation de langages de programmation, la formalisation de théorèmes mathématiques, l'enseignement, etc. En raison de la nature interactive de Coq, nous recommandons des questions à lier à des exemples exécutables sur https://x80.org/collacoq/ si cela est jugé approprié.