如何使用Streicher_K_公理
有人可以告诉我一个简单的例子如何使用从Coq.Logic.EqdepFacts
公理Streicher_K_
公理?如何使用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.
但问题是,我不知道为什么这个工作。我不明白底层的类型检查。
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也在证明中使用了模式匹配。
我想你忘了为第二个证明添加代码段。 –
这是相同的证据,但我忘了两个变数。 – Cryptostasis