假设中的 Coq 矛盾

Question

在 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 不能都为真，因此当前上下文暗示了目标。

我应该如何在 Coq 中解决这个问题，而不是一直生成 H0 、 v x0 和 v x1 作为新的子目标？棘手的部分是:“假设一些图形存在于 a (A_ends x0 x1) \/ a (A_ends x1 x0) 和 v 的这种形式”。

到目前为止，我尝试了 a 。

Answer 1

一般来说，您需要确保您的上下文与您的非正式推理相匹配。你说:

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.

但是，这不是您的上下文所说的。你的上下文说“假设你有一个图和两个顶点 x0 和 x1(它可能在也可能不在该图的顶点集中)。如果碰巧 x0 和 x1 特别是在该图中，则是相邻的，那么它们必须具有不同的颜色(这是 H0 )。但是，在这种情况下，我们已经有了 x0 和 x1 具有相同的颜色(这是 H1 )。得出的明显结论并不荒谬，只是这些 x0 和 x1 不在图形上，或者不相邻。为了具体起见，该图可能是空的，或者只有一个顶点而没有边。

我建议一个接一个地逐步完成证明策略，将每个上下文和目标翻译回自然语言，并寻找从真定理到假定理的点。