在 Coq 中重写假设，保留含义答案

【问题标题】：Rewrite hypothesis in Coq, keeping implication在 Coq 中重写假设，保留含义
【发布时间】：2017-11-27 21:58:35
【问题描述】：

我正在做 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)。

【问题讨论】：

标签： coq coq-tactic

【解决方案1】：

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

【讨论】：

【解决方案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 也可以工作，但是它太聪明了，而且做得太多了。

【讨论】：

【解决方案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.

【讨论】：