如何使用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也在证明中使用了模式匹配。