Coq contradiction in hypotheses

Question

In Coq I have two hypotheses H and H0, that contradict each other. Problem is, they only contradict each other for some specializations and at this moment of the proof the context is not that specialized.

At this moment my proof context looks like this:

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

As this proof is about graphs (v = set of vertices, a = set of arcs, color = color of a vertex), I could easily show the contradiction in natural language: 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. Therefore H and H0 cannot both be true and therefore the goal is implied by the current context.

How should I go about this in Coq, without generating v x0, v x1 and a (A_ends x0 x1) \/ a (A_ends x1 x0) as new subgoals all the time? The tricky part is the: "suppose some graph exists with v and a of such and such forms".

So far I tried auto, eauto, trivial, intuition, apply H in H0, contradiction H, omega.

Answer 1

In general, you need to make sure that your context matches your informal reasoning. You say:

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.

However, this is not what your context says. Your context says "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)." The obvious conclusion to draw is not absurdity, but simply that these x0 and x1 are not on the graph, or are not neighboring. For concreteness, the graph might be empty, or have only one vertex and no edges.

I would suggest stepping through the proof tactic by tactic, translating each context and goal back into natural language, and looking for the point at which you go from a true theorem to a false one.