coq - 证明 Sigma 类型上的相等性

Question

我定义了一个 Sygma-Type，如下所示:

{ R : nat -> nat -> bool | Reflexive R }

我有两个元素 r1 r2 : { R : nat -> nat -> bool |自反 R } 我要证明 r1 = r2。我怎样才能做到这一点？

Answer 1

如果您想显示这样的相等性，您需要 (1) 显示底层函数是相等的(即 sigma 类型的 R 组件)，并且 (2) 显示相应的证明是等价的。然而，有两个问题。

第一个是 Coq 中的函数相等性太弱。根据常见的数学实践，如果两个函数对任何输入产生相同的结果，我们期望它们相等。这一原则被称为功能扩展性:

Axiom functional_extensionality :
  forall A (B : A -> Type)
         (f g : forall a, B a),
         (forall x, f x = g x) ->
         f = g.

尽管听起来很自然，但是这个原理在 Coq 的逻辑中是无法证明的!粗略地说，两个函数相等的唯一方法是根据逻辑的计算规则将它们转换为语法上相等的项。例如，我们可以证明 fun n : nat => 0 + n 和 fun n : nat => n 相等，因为 + 是在 Coq 中通过第一个参数的模式匹配来定义，第一项的第一个参数是 0。

Goal (fun n : nat => 0 + n) = (fun n : nat => n). reflexivity. Qed.

我们可以期望通过类似的方法证明 fun n => n + 0 和 fun n => n 是相等的。然而，Coq 不接受这一点，因为当第一个参数是变量时 + 无法简化。

另一个问题是证明上的等式概念也不是很有趣。证明两个证明相等的唯一方法就是句法相等。然而，直觉上，人们想通过证明无关性来论证，这一原则指出同一事物的证明总是相等的:

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

但是，同样，这个原理在逻辑上是无法证明的。幸运的是，Coq 的逻辑被设计为允许人们以一种合理的方式将这些原则添加为公理。然后得到以下证明:

Axiom functional_extensionality :
  forall A (B : A -> Type)
         (f g : forall a, B a),
    (forall a, f a = g a) ->
    f = g.

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

Lemma l (r1 r2 : { R : nat -> nat -> bool |
                   forall n, R n n = true }) :
  (forall n1 n2, proj1_sig r1 n1 n2 = proj1_sig r2 n1 n2) ->
  r1 = r2.
Proof.
  destruct r1 as [r1 H1], r2 as [r2 H2].
  simpl.
  intros H.
  assert (H' : r1 = r2).
  { apply functional_extensionality.
    intros n1.
    apply functional_extensionality.
    intros n2.
    apply H. }
  subst r2.
  rename r1 into r.
  f_equal.
  apply proof_irrelevance.
Qed.

尽管公理可能很有用，但人们可能想避免使用它们。在这种情况下，实际上可以仅通过函数外延性来证明这个引理，但您至少需要这样。如果您想避免使用公理，并且 r1 和 r2 在计算时不等于，则必须使用差分等价关系根据您的类型，然后使用该关系进行形式化，例如

Definition rel_equiv (r1 r2 : { R : nat -> nat -> bool | forall n, R n n = true }) : Prop :=
  forall n1 n2, proj1_sig r1 n1 n2 = proj2_sig r2 n1 n2.

standard library对等价关系重写有良好的支持；参见例如this .