coq - 不同等式证明的示例

Question

我正在 Coq 中寻找不同等式证明的示例。
这意味着:
给出一些类型 T 和两个元素 x,y : T 和两个证明 p1 , p2 : x=y 和 p1<>p2。

Answer 1

这是 Coq 中不完备性的典型例子。在其基本理论中(即不假设任何附加公理)，无法证明或反驳以下陈述:

exists (T : Type) (x y : T) (p q : x = y), p <> q.

因此，我们通常不能在两点之间展示不同的相等证明。这在实践中意味着什么？如果你想按原样使用 Coq 的理论，你必须避免谈论等式证明之间的等式，因为我们无法用它们做任何有用的事情。唯一的异常(exception)是具有可判定相等性的类型，我们可以证明这些类型 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 不兼容的有用公理。最著名的是来自 Homotopy type theory 的单价公理，粗略地说，对于所有类型 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 中有两种不同的等式证明。 : 一个对应于恒等函数，另一个对应于 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 here和 isequiv_equiv_path here .如果您想使用公理，最好使用在线提供的同伦类型理论库之一: HoTT和 UniMath .请注意，第一个实际上是 Coq 的稍微修改版本。