如何使用Streicher_K_公理

Question

有人可以告訴我一個簡單的例子如何使用從Coq.Logic.EqdepFacts公理Streicher_K_公理？

也許用於顯示簡單的事實：

Lemma single_proof : forall (A:Type)(x y:A) (u v:x = y), u = v. 

我設法與Streicher_K_on_來證明這一點：

Variable A:Type. 
Variable x:A. 
Axiom SK:Streicher_K_on_ A x (fun p:x=x => (eq_refl x) = p). 

Lemma single_proof : forall (y:A)(u v:x = y), u = v. 
intros. 
destruct u. 
apply (SK). 
reflexivity. 
Qed. 

通過試驗和錯誤我也發現瞭如何與Streicher_K_證明這一點，這是甚至更簡單：

Axiom SK:Streicher_K_ A. 

但問題是，我不知道爲什麼這個工作。我不明白底層的類型檢查。

Answer 1

K和它的許多等效聲明

公理K的說法是有點困難一見鍾情把握。由於額外的參數，在標準庫中更難以理解。幸運的是，它相當於下面的替代，從而推廣您試圖證明之一，往往是什麼，我們需要在實踐中：（「身份證明的唯一性」，「UIP」代表）

UIP : forall (T : Type) (x y : T) (p q : x = y), p = q 

Coq標準庫有一個EqdepTheory模塊，它顯示了這兩個語句和其他一些類似語句的等價關係。它使我們能夠自由地使用這些聲明，而一個假定其中的一個，eq_rect_eq：

Require Import Coq.Logic.EqdepFacts. 

Module Ax : EqdepElimination. 

Axiom eq_rect_eq : 
    forall (U:Type) (p:U) (Q:U -> Type) (x:Q p) (h:p = p), 
     x = eq_rect p Q x p h. 

End Ax. 

Module Export UIPM := EqdepTheory Ax. 

這個片段後，我們就可以運行，例如，

Check UIP. 

但是我們怎麼證明的東西與K？

您對我們如何使用K來證明UIP似乎也感到困惑。答案在於以下聲明：乍一看，K和J非常相似。讓我們比較一下它們的類型：

J : forall (A : Type) (x : A) (P : forall y : A, x = y -> Prop), 
    P x eq_refl -> forall (y : A) (p : x = y), P y p 

K : forall (A : Type) (x : A) (P :    x = x -> Prop), 
    P eq_refl -> forall   (p : x = x), P p 

（我寫K而不是Streicher_K只是爲了易讀性）的一個區別是J由謂詞參數平等x = y的P是通用相對於右手側y 。 K也有一個謂詞P，但它只考慮等於x = x。

另一個區別是，儘管J可以在Coq理論中證明，但是如上所述，K只能通過在理論中增加額外的公理來證明。考慮到K中使用的謂詞P比J中使用的更具體，但這是match語句在Coq中的鍵入方式的結果，這可能看起來令人驚訝。

通過結合K和J，我們可以得出UIP的證據。讓我們先來證明它的專業版，即僅適用於反身等式：

Definition UIP_refl (A : Type) (x : A) (p : x = x) : eq_refl = p := 
    Streicher_K A x (fun q => eq_refl = q) eq_refl p. 

然後，J讓我們來概括這個任意等式：

Definition UIP (A : Type) (x y : A) (p q : x = y) : p = q := 
    J A x (fun y p => forall q : x = y, p = q) (UIP_refl A x) y p q. 

注意的J定義使用模式匹配。在引擎蓋下，當您調用destruct (SK).時，Coq也在證明中使用了模式匹配。