如何使用Streicher_K_ Axiom

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 : forall (T : Type) (x y : T) (p q : x = y), p = q

("UIP" 代表 "unicity of identity proofs.")

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 感到困惑。答案就在下面的语句中：

Definition J (A : Type) (x : A) (P : forall y, x = y -> Prop) :
  P x eq_refl -> forall y (p : x = y), P y p :=
  fun H y p =>
    match p with
    | eq_refl => H
    end.

乍一看，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 由等式 P 的谓词 x = y 参数化] 相对于右侧 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 还在您的证明中使用模式匹配

如何使用Streicher_K_ Axiom

How to use Streicher_K_ Axiom

equality

coq

K 及其许多等效语句

但是我们如何用 K 来证明呢？