使用Coq的案例證明

Question

我有一個簡單的定理，我想證明使用案例證明。下面給出一個例子。

 
Goal forall a b : Set, a = b \/ a <> b. 
Proof 
    intros a b. 
    ... 

我該如何解決這個問題。而且，究竟如何使用兩個可能的平等值（True或False）來定義證據？

任何幫助，將不勝感激。 謝謝，

Answer 1

我很確定Set s的等同性在coq中是不可判定的。原因（根據我的理解）應該是它不是一個歸納定義的集合（因此，對您而言沒有案例分析......），也不是一個封閉的集合：每次定義新的數據類型時，您創建一個新的Set居民家庭。因此，證明您顯示的目標的術語需要更新以反映這些新的居民。

由於@hardmath在他的評論中提到，你可以使用Classical假設（Axiom classic : forall P:Prop, P \/ ~ P.）來證明你的目標。

正如@Robin Green在評論中提到的那樣，你可以證明這種類型的目標是可以相等的。爲此，您可能需要從decide equality策略中獲得幫助。請參閱：http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic121

Answer 2

您的問題涉及Coq的一個有趣方面：命題（即Prop的成員）和布爾（即bool的成員）之間的差異。詳細解釋這種差異會有點過於技術性，所以我會試着專注於你的特殊例子。

粗略地說，Coq中的Prop不像True或False那樣評估，就像普通的布爾值一樣。相反，Prop s有推理規則可以結合推斷事實。使用這些，我們可以證明一個命題是成立的，或者表明它是矛盾的。讓事情微妙的是，還有第三種可能性，即我們無法證明或反駁這個命題。發生這種情況是因爲Coq是建設性邏輯。其中最爲衆所周知的後果之一是，在Coq中不能證明被排除在中間的（forall P : Prop, P \/ ~ P）之類熟悉的推理原則：如果您斷言P \/ ~ P，這意味着您要麼能夠證明P或證明~ P。如果不知道哪一個成立，你就無法斷言。

事實證明，對於一些命題，我們可以證明P \/ ~ P成立。例如，要顯示forall n m : nat, n = m \/ n <> m並不困難。遵循上述說法，這意味着對於每一對自然數，我們都能夠證明它們是平等的或證明它們不是。另一方面，如果我們將nat更改爲Set，就像在您的示例中一樣，那麼我們將永遠無法證明該定理。要明白爲什麼，請考慮自然數對的Setnat * nat。如果我們能夠證明你的定理，那麼它會遵循那個nat = nat * nat \/ nat <> nat * nat。同樣，通過上述評論，這意味着我們要麼能夠證明nat = nat * nat或nat <> nat * nat。然而，由於兩種類型之間存在雙射，所以我們不能說假設nat = nat * nat是矛盾的，但是因爲類型在語法上不是相同的，所以假設它們是不同的也是可以的。從技術上說，命題nat = nat * nat的有效性是Coq邏輯的獨立。

如果你真的需要，你所提到的，那麼你需要斷言排中作爲公理（Axiom classical : forall P, P \/ ~ P.），這將讓你產生\/證明，而無需任何一方的明確證據和推理的事實案例。那麼你將能夠用類似

intros a b. destruct (classical (a = b)). 
    left. assumption. 
    right. assumption.

希望這有助於證明你的例子定理。