澆鑄COQ轉換類型

Lemma test: 
    forall n j (jn : j < n) (ln : j + 0 < n) (P: forall {x} {y}, (x<y) -> nat), 
    P ln = P jn.

類型LN一個JN似乎是可兌換的情況下（從視圖算術點）。我怎樣才能用這個事實來證明上面的引理？我可以很容易地證明assert(JL: j < n -> j + 0 < n) by auto.，但我沒有看到如何將此應用於類型。

2015-11-05 krokodil

這些類型是而不是因爲在Coq中定義了自然數的加法（即通過對第一個參數進行遞歸）而相互轉換。事實上，您的引理可以輸入Coq的唯一原因是P的第一個隱含參數在右側實例化爲j + 0。

不幸的是，即使這些類型爲兌換，也不可能證明這個引理，無需額外的假設，因爲它需要命題外延性公理（見here，例如）。

2015-11-05 05:34:10

感謝。我知道這是不可證明的，但我能夠證明它對於特別的P. – krokodil

我很抱歉，但我仍然不明白。即使我讓'x'和'y'非隱式，'P'也是自然數，所以'j'和'j + 0'是'nat'類型，我可以證明它們是等價的。從常理上來說，從證明'j + 0 krokodil

並非所有「m gallais

引理不可證明。嘗試intros. remember (j+0) as Q. rewrite <- plus_n_O in HeqQ. subst Q.它將擺脫+ 0。你的目標是

P j n ln = P j n jn

雙方都是nat類型。但現在你需要證明這兩個nat s爲平等的，不知道什麼對他們...

編輯：

其實我是有點太快......函數的值P不能由於它們是Prop s，因此取決於ln和jn。但爲了證明這一點，你需要proof irrelevance。

如果你Require Import ProofIrrelevance.你得到的公理

Axiom proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2.

這不是勒柯克的邏輯的結果，但它符合它（而且往往正是我們的意思用一個證明 - 兩個形式上正確的參數即使他們的細節有所不同，也是一樣的）。

現在你只是做

rewrite (proof_irrelevance _ ln jn). reflexivity. Qed.

2015-11-05 19:32:11 larsr

謝謝！這有助於 – krokodil

我添加了一些關於使用*證明不相關*來完成證明的評論。 – larsr

回答