在 Coq 中重写假设，保持蕴涵

Question

我正在做一个 Coq 证明。我有 P -> Q 作为假设，(P -> Q) -> (~Q -> ~P) 作为引理。如何将假设转换为 ~Q -> ~P?

当我尝试 apply 它时，我只是产生了新的子目标，这没有帮助。

换句话说，我希望开始于：

P : Prop
Q : Prop
H : P -> Q

并以

结束

P : Prop
Q : Prop
H : ~Q -> ~P

鉴于上述引理 - 即 (P -> Q) -> (~Q -> ~P).

Answer 1

这不像 apply 那样优雅，但您可以使用 pose proof (lemma _ _ H) as H0，其中 lemma 是引理的名称。这将向上下文添加另一个具有正确类型的假设，名称为 H0.

Answer 2

这是 ssreflect 视图提供帮助的一种情况：

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 也可以，但是它太聪明了，而且做得太多了。

Answer 3

如果我想转换 H 就地我会选择@ejgallego 的回答，因为 SSReflect 现在（从 Coq 8.7.0 开始）是标准 Coq，但这是另一种选择：

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.

一个简单的测试：

Variable (P Q : Prop).
Axiom u : (P -> Q) -> (~Q -> ~P).

Lemma test (H : P -> Q) : False.
Proof. dumb apply u in H. Abort.

在 Coq 中重写假设，保持蕴涵

Rewrite hypothesis in Coq, keeping implication

coq

coq-tactic