这是Coq中不完整性的典型例子.在其基本理论中(即,不假设任何其他公理),不可能证明或反驳以下陈述:
exists (T : Type) (x y : T) (p q : x = y), p <> q.
因此,我们通常不能在两点之间展示不同的平等证明.这在实践中意味着什么？如果你想按原样使用Coq的理论,你必须避免谈论平等证明之间的平等,因为我们无法用它们做任何非常有用的事情.唯一的例外是具有可判定平等的类型,我们可以证明的类型forall x y : T, x = y \/ x <> y; 在这些情况下,我们可以展示身份证明的独特性:
UIP : forall (x y : T) (p q : x = y), p = q.
如果我们愿意添加公理,那么故事就会改变.我们可以添加的公理之一是证明不相关,这是上述UIP原理的概括.它说
proof_irrelevance : forall (P : Prop) (p q : P), p = q.
Coq的理论旨在允许这样的公理而不会产生矛盾,许多发展都是这样做的.在这种情况下,UIP适用于所有类型,而不仅仅是那些具有可判定平等性的类型.
在另一方面,是有用的公理,我们可以添加与UIP不兼容.最著名的一个是单叶公理从同伦型理论,大致说,对所有类型的A和B有平等的证据之间的一个一一对应A = B,并等价之间A和B-也就是说,功能A -> B是有两双向反转.这是一个简化版本,只是为了解释基本思想:
Record Equiv (A B : Type) : Type := {
equiv_l : A -> B;
equiv_r : B -> A;
_ : forall x, equiv_l (equiv_r x) = x;
_ : forall x, equiv_r (equiv_l x) = x
}.
Axiom univalence : forall A B, Equiv (A = B) (Equiv A B).
如果我们假设这个公理,我们可以证明,例如,有两个不同的相等证明bool = bool:一个对应于身份函数,另一个对应于布尔否定:
Definition id_Equiv : Equiv bool bool.
Proof.
apply (BuildEquiv _ _ (fun x => x) (fun x => x)); trivial.
Defined.
Definition negb_Equiv : Equiv bool bool.
Proof.
apply (BuildEquiv _ _ negb negb); intros []; trivial.
Defined.
Lemma not_UIP : exists p q : bool = bool :> Type , p <> q.
Proof.
exists (equiv_r _ _ (univalence bool bool) id_Equiv).
exists (equiv_r _ _ (univalence bool bool) negb_Equiv).
intros H.
assert (H' : id_Equiv = negb_Equiv).
{ now rewrite <- (equiv_lr _ _ (univalence bool bool)), <- H,
(equiv_lr _ _ (univalence bool bool)). }
assert (H'' : equiv_l _ _ id_Equiv true = equiv_l _ _ negb_Equiv true).
{ now rewrite H'. }
simpl in H''. discriminate.
Qed.
请记住,单数的实际定义比我上面提到的更为复杂,我甚至都不确定.你不能只复制我上面提到的内容并希望它能顺利运作.有关实际定义,请参阅IsEquiv 此处和isequiv_equiv_path 此处.如果你想使用公理,最好使用在线提供的Homotopy类型理论库之一:HoTT和UniMath.请注意,第一个实际上是Coq的略微修改版本.