假设中的 Coq 矛盾
Coq contradiction in hypotheses
在 Coq 中，我有两个相互矛盾的假设 H 和 H0。问题是，它们只是在某些专业上相互矛盾，而在证明的这一刻，上下文并不是那么专业。
此刻我的证明上下文是这样的：
color : Vertex -> bool
v : V_set
a : A_set
x0, x1 : Vertex
H : v x0 -> v x1 -> a (A_ends x0 x1) \/ a (A_ends x1 x0) -> color x0 <> color x1
H0 : v x0 -> v x1 -> a (A_ends x0 x1) \/ a (A_ends x1 x0) -> color x0 = color x1
______________________________________
False
因为这个证明是关于图的（v = 顶点集，a = 弧集，color = 顶点的颜色），我可以很容易地证明矛盾在自然语言中：假设一些图包含顶点 x0 和 x1 （并且它们是相邻的）， x0 和 x1 不能同时具有相同和不同的颜色。因此 H 和 H0 不能同时为真，因此当前上下文暗示了目标。
我应该如何在 Coq 中解决这个问题，而不总是生成 v x0、v x1 和 a (A_ends x0 x1) \/ a (A_ends x1 x0) 作为新的子目标？棘手的部分是："suppose some graph exists with v and a of such and such forms".
到目前为止，我已经尝试了 auto, eauto, trivial, intuition, apply H in H0, contradiction H, omega。
一般来说，您需要确保您的上下文与您的非正式推理相符。你说：
suppose some graph contains vertices x0 and x1 (and they are neighbouring), x0 and x1 cannot have the same and different color at the same time.
但是，这不是您的上下文所说的。你的上下文说 "suppose you have a graph and two vertices x0 and x1 (which may or may not be in the vertex set of that graph). If it happens that x0 and x1 in particular are in the vertex set of that graph, and are neighboring, then they must have different colors (this is H0). However, we already have that in this case, x0 and x1 have the same color (this is H1)." 得出的明显结论并不荒谬，而只是这些 x0 和 x1 不在图上，或者不相邻。具体来说，该图可能是空的，或者只有一个顶点而没有边。
我建议逐个证明策略，将每个上下文和目标转换回自然语言，并寻找从真定理到假定理的点。
在 Coq 中，我有两个相互矛盾的假设 H 和 H0。问题是，它们只是在某些专业上相互矛盾，而在证明的这一刻，上下文并不是那么专业。
此刻我的证明上下文是这样的：
color : Vertex -> bool
v : V_set
a : A_set
x0, x1 : Vertex
H : v x0 -> v x1 -> a (A_ends x0 x1) \/ a (A_ends x1 x0) -> color x0 <> color x1
H0 : v x0 -> v x1 -> a (A_ends x0 x1) \/ a (A_ends x1 x0) -> color x0 = color x1
______________________________________
False
因为这个证明是关于图的（v = 顶点集，a = 弧集，color = 顶点的颜色），我可以很容易地证明矛盾在自然语言中：假设一些图包含顶点 x0 和 x1 （并且它们是相邻的）， x0 和 x1 不能同时具有相同和不同的颜色。因此 H 和 H0 不能同时为真，因此当前上下文暗示了目标。
我应该如何在 Coq 中解决这个问题，而不总是生成 v x0、v x1 和 a (A_ends x0 x1) \/ a (A_ends x1 x0) 作为新的子目标？棘手的部分是："suppose some graph exists with v and a of such and such forms".
到目前为止，我已经尝试了 auto, eauto, trivial, intuition, apply H in H0, contradiction H, omega。
一般来说，您需要确保您的上下文与您的非正式推理相符。你说：
suppose some graph contains vertices
x0andx1(and they are neighbouring),x0andx1cannot have the same and different color at the same time.
但是，这不是您的上下文所说的。你的上下文说 "suppose you have a graph and two vertices x0 and x1 (which may or may not be in the vertex set of that graph). If it happens that x0 and x1 in particular are in the vertex set of that graph, and are neighboring, then they must have different colors (this is H0). However, we already have that in this case, x0 and x1 have the same color (this is H1)." 得出的明显结论并不荒谬，而只是这些 x0 和 x1 不在图上，或者不相邻。具体来说，该图可能是空的，或者只有一个顶点而没有边。
我建议逐个证明策略，将每个上下文和目标转换回自然语言，并寻找从真定理到假定理的点。