本文介绍了用Coq重写假设，保持含义的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！
问题描述
我正在做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重写假设，保持含义的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！