Coq矛盾的假设

在Coq我有两个假设H和H0，这相互矛盾。问题是，他们只是为了一些专业而互相矛盾，在这个证明的背景下，情况并不那么专业化。Coq矛盾的假设

这时我的证明背景是这样的：

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。

来源

2017-09-11 Alexander Boll

恐怕你必须产生缺失的证明义务，否则证明为什么他们不需要。 Coq是关于_proof verification_所以你不能指望非正式推理在这里继续工作。如果不知道更多信息，很难知道，但是关键可能在于您遵循该目标的路径。你写下“假设”，以便假设，应该出现在某个地方，对吗？ – ejgallego

证明自动化的第一步是手动证明。所以，现在忽略了产生子目标的烦恼，你怎么证明'v x0'，'v x1'和'a ... \/a ...'？ –

我想我需要像'v'和'a'这样的_specialization_，它具有所需的形式。非正式地说，这应该再好，“当这些假设一般存在时，那么他们必须为这个特殊情况而持有”。但是Coq在这里不允许有这样的专业化，因为在其他假设中使用'v'和'a'。 –

一般来说，您需要确保您的上下文符合您的非正式推理。你说：

想一些图包括顶点x0和x1（和他们是邻国）x0和x1不能在同一时间相同和不同的颜色。

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

我建议使用策略逐步完成证明策略，将每个上下文和目标翻译成自然语言，并寻找从真正的定理转到错误的定理。

来源

2017-09-12 13:49:58

Coq矛盾的假设

回答

相关问题