用Coq重写假设，保持含义 [英] Rewrite hypothesis in Coq, keeping implication

问题描述

我正在做Coq证明。我有 P-> Q 作为假设，而（P-> Q）-> （〜Q->〜P）作为引理。如何将假设转换为〜Q-> 〜P ？

I'm doing a Coq proof. I have P -> Q as a hypothesis, and (P -> Q) -> (~Q -> ~P) as a lemma. How can I transform the hypothesis into ~Q -> ~P?

当我尝试应用时，我只是生成了新的子目标，这无济于事。

When I try to apply it, I just spawn new subgoals, which isn't helpful.

换一种说法，我想从以下开始：

Put another way, I wish to start with:

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

最终以

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

鉴于上述引理-即（P-> Q） -> （〜Q->〜P）。

推荐答案

应用，但是您可以将姿势证明（引理_ _ H）用作H0 ，其中引理是引理的名称。这将为上下文添加另一个具有正确类型的假设，其名称为 H0 。

This is not as elegant as just an apply, but you can use pose proof (lemma _ _ H) as H0, where lemma is the name of your lemma. This will add another hypothesis with the correct type to the context, with the name H0.

这篇关于用Coq重写假设，保持含义的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！