在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)作为新的子目标？棘手的部分是："假设存在某种图形，其中包含某某形式的v和a"。
到目前为止，我尝试了auto, eauto, trivial, intuition, apply H in H0, contradiction H, omega.
一般来说，你需要确保你的上下文与你的非正式推理相匹配。 你说：
假设某个图包含顶点
x0和x1(它们是相邻的)，x0和x1不能同时具有相同和不同的颜色。
但是，这不是您的上下文所说的。 您的上下文说"假设您有一个图形和两个顶点x0和x1(它们可能位于该图形的顶点集中，也可能不在该图形的顶点集中)。 如果碰巧x0和x1特别位于该图的顶点集中，并且相邻，那么它们必须具有不同的颜色(这是H0)。 但是，在这种情况下，我们已经有了，x0和x1具有相同的颜色(这是H1)。 得出的明显结论不是荒谬，而只是这些x0和x1不在图表上，或者不是相邻的。 对于具体性，图形可能为空，或者只有一个顶点而没有边。
我建议通过一个策略来逐步完成证明策略，将每个上下文和目标翻译回自然语言，并寻找你从真定理到假定理的点。