不同等式证明的示例

Question

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

Answer 1

这是 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.

如果我们愿意添加公理，情况就会改变。我们可以添加的公理之一是 proof irrelevance，这是上述 UIP 原理的概括。它说

proof_irrelevance : forall (P : Prop) (p q : P), p = q.

Coq 的理论旨在允许这样的公理而不会引起矛盾，并且许多发展都是这样做的。在这种情况下，UIP 适用于所有类型，而不仅仅是那些具有可判定相等性的类型。

另一方面，我们可以添加个与 UIP 不兼容的有用公理。最著名的是来自 Homotopy type theory 的 univalence axiom，它粗略地说对于所有类型 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 here and isequiv_equiv_path here. If you want to use the axiom, it is better to work with one of the Homotopy type theory libraries available online: HoTT and UniMath。请注意，第一个实际上是 Coq 的略微修改版本。

不同等式证明的示例

Example for different equality proofs

coq

equality