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).

2
APerson 28 nov. 2017 à 00:58

3 réponses

Meilleure réponse

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.

2
eponier 27 nov. 2017 à 23:02

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.
1
Anton Trunov 28 nov. 2017 à 14:49

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.

2
ejgallego 28 nov. 2017 à 14:00
47520531