如何在Coq中證明所有n：nat，〜n <n？

Question

我一直困惑了好幾個小時，我無法弄清楚如何證明

forall n:nat, ~n<n 

在勒柯克

。我真的需要你的幫助。有什麼建議麼？

Answer 1

這引理是在標準庫：

Require Import Arith. 
Lemma not_lt_refl : forall n:nat, ~n<n. 
Print Hint. 

當中的結果是lt_irrefl。意識到的更直接的辦法就是

info auto with arith. 

證明了該目標，並說明如何：

intro n; simple apply lt_irrefl. 

既然你知道在哪裏可以找到一個證明，我只是就如何做一個提示它從最初的原則（我認爲這是你作業的重點）。

首先，你需要證明一個否定。這幾乎意味着你推動n<n作爲一個假設，並證明你可以推斷出矛盾。然後，在n<n上推理，將其展開至其定義。

intros h H. 
red in H. (* or `unfold lt in H` *) 

現在您需要證明S n <= n不會發生。要做到這一點從第一原則，你有兩個選擇：你可以嘗試導入n，或者你可以嘗試導入<=。謂詞通過歸納定義，通常在這些情況下需要對它進行歸納 - 也就是說，通過對假設的證明進行歸納推理。在這裏，儘管如此，你最終需要對n進行推理，以表明n不能成爲S n的後繼者，並且你可以立即開始在n上進行歸納。

induction n之後，您需要證明基本情況：您有假設1 <= 0，並且您需要證明這是不可能的（目標是False）。通常，要將歸納假設分解爲案例，可以使用induction策略或其變體之一。這種策略對假設構建了一個相當複雜的依賴案例分析。看看發生了什麼的一種方法是撥打simple inversion，這留給你兩個子目標：或者假設1 <= 0的證明使用le_n構造函數，這要求1 = 0，或者證明使用le_S構造函數，這需要S m = 0。在這兩種情況下，要求與S的定義明顯矛盾，所以策略discriminate證明了子目標。您可以使用inversion H，而不是simple inversion H，在這種特殊情況下，它直接證明了目標（不可能的假設情況非常普遍，並且已經融入了全面的inversion策略）。

現在，我們轉到感應情況，我們很快來到我們想要從S (S n) <= S n證明S n <= n的點。我建議你把它作爲一個單獨的引理（首先要證明），這可以概括爲：forall n m, S n <= S m -> n <= m。

Answer 2

Require Import Arith. 
auto with arith.