假定COQ中的目标否定
我正在尝试在COQ中证明以下定理：
Theorem slot_company:
forall s x, PPs s x -> exists t, PPs t x /\ s <> t.
我当前的上下文和目标是：
1 subgoal
s, x : Entity
Pssx : Ps s x
nFxs : ~ F x s
Sx : Entity
PsSxx : Ps Sx x
FxSx : F x Sx
______________________________________(1/1)
exists t : Entity,
PPs t x /\ s <> t
我想提出这样的假设：pps tx /\ s＆lt;＆gt;＆gt; t。通过这样做，我可以得到s = sx，然后得到矛盾（我将拥有f xs/\ 〜f x s。这样，我会知道目标是正确的
。
I'm trying to prove in Coq the following theorem:
Theorem slot_company:
forall s x, PPs s x -> exists t, PPs t x /\ s <> t.
My current context and goal are:
1 subgoal
s, x : Entity
Pssx : Ps s x
nFxs : ~ F x s
Sx : Entity
PsSxx : Ps Sx x
FxSx : F x Sx
______________________________________(1/1)
exists t : Entity,
PPs t x /\ s <> t
I would like to pose the hypothesis that there are no t with PPs t x /\ s <> t. By doing so, I can get that s = Sx, and then get a contradiction (I would have F x s /\ ~ F x s. This way, I will know that the goal is true.
The problem is that I don't know how to do so.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
我对矛盾的证据是一种持怀疑态度，这是去这里的方式，但是很难看出，而不必看到这些关系的定义。
以下是通过矛盾进行证明的一种方法：
来自Coq的coq需要经典。应用peirce; Intros Hcontra。I'm skeptical that proof by contradiction is the way to go here, but it's hard to tell without seeing the definition of those relations.
Here's one way to do proof by contradiction:
From Coq Require Import Classical.apply Peirce; intros Hcontra.