证明Sigma类型的相等性 [英] Prove equality on Sigma-types

问题描述

我定义了一个Sygma类型，如下所示：

I have defined a Sygma-Type that looks like:

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

我有两个元素 r1 r2：{R：nat- > nat->布尔|自反R} ，我要证明 r1 = r2 。我该怎么做？

I have two elements r1 r2 : { R : nat -> nat -> bool | Reflexive R } and I am to prove r1 = r2. How can I do that?

推荐答案

如果要显示这样的等式，则需要（1）显示底层函数是相等的（即sigma类型的 R 分量），并且（2）显示相应的证明是相等的。但是，有两个问题。

If you want to show such an equality, you need to (1) show that the underlying functions are equal (i.e., the R component of your sigma type), and (2) show that the corresponding proofs are equal. There are two problems, however.

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

The first one is that equality of functions is too weak in Coq. According to common mathematical practice, we expect two functions to be equal if they yield equal results for any inputs. This principle is known as functional extensionality:

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 。

As natural as it sounds, however, this principle is not provable in Coq's logic! Roughly speaking, the only way two functions can be equal is if they can be converted to a syntactically equal terms according to the computation rules of the logic. For instance, we can show that fun n : nat => 0 + n and fun n : nat => n are equal because + is defined in Coq by pattern-matching on the first argument, and the first argument on the first term is 0.

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

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

We could expect to show that fun n => n + 0 and fun n => n are equal by similar means. However, Coq does not accept this, because + cannot be simplified when the first argument is a variable.

另一个问题是，证明平等的概念也不是很有趣。同样，证明两个证明相等的唯一方法是句法相等。但是，从直觉上讲，人们想用不相关证明来争辩，该原则指出同一事物的证明总是相等的。

The other problem is that the notion of equality on proofs is not very interesting as well. The only way one can show that two proofs are equal is, again, syntactic equality. Intuitively, however, one would like to argue by proof irrelevance, a principle that states that proofs of the same thing are always equal:

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

但同样，该原理在逻辑上也不成立。幸运的是，Coq的逻辑旨在允许人们以合理的方式将这些原理添加为公理。然后得到以下证明：

but, again, this principle is not provable in the logic. Fortunately, Coq's logic was designed to allow one to add these principles as axioms in a sound way. One then gets the following proof:

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 和 not 等于计算中，您必须在类型上使用差异等价关系，并使用该关系进行形式化，例如

Even though axioms can be useful, one might like to avoid them. In this case, it is actually possible to prove this lemma just with functional extensionality, but you do need at least that. If you want to avoid using axioms, and r1 and r2 are not equal up to computation, you'll have to use a difference equivalence relation on your type, and do your formalization using that relation instead, e.g.

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.

标准库为具有等价关系的重写提供了良好的支持； cf.例如此。

The standard library has good support for rewriting with equivalence relations; cf. for instance this.

这篇关于证明Sigma类型的相等性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！