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矛盾的假設

回答

相關問題