Coq中平等类型证据的案例分析

Question

我对Coq中归纳定义的关系eq有一个查询。考虑Coq中eq的以下定义：

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x

这是一个归纳定义的关系，就像le (<=)。因此，我应该能够对任何这类证据进行案例分析。然而，当我试图证明以下结果时，我无法成功。

Lemma true_num: forall m :nat, forall x y: m=m, x=y.
  Proof. intros. destruct x.

(// Error: Abstracting over the terms "m" and "x" leads to a term
fun (m0 : nat) (x0 : m0 = m0) => x0 = y
which is ill-typed.
Reason is: Illegal application: 
The term "@eq" of type "forall A : Type, A -> A -> Prop"
cannot be applied to the terms
 "m0 = m0" : "Prop"
 "x0" : "m0 = m0"
 "y" : "m = m"
The 3rd term has type "m = m" which should be coercible to 
"m0 = m0". )  

我无法破译这个错误。

m=m的唯一证据应该是@eq_refl nat m，因为eq_refl是唯一的构造函数。因此，我们应该能够通过进行案例分析来证明x和y的等价性。

这种推理有什么问题？

Answer 1

m=m的唯一证明应该是@eq_refl nat m，因为eq_refl是唯一的构造函数。

不是的。您的定理碰巧是正确的，因为您正在讨论的是nat的等式，但是如果您用Type替换nat，那么您的推理也会进行得很好(或很差)，而用Type替换nat会使定理无法证明。

问题是平等型家庭是由反身证明自由生成的。因此，由于Coq中的所有东西都以正确的方式尊重等式(这是我有点模糊的一点)，为了证明一个家族中所有平等证明的性质(即对某些固定的x = y和所有y的所有证明)，就足以证明生成元的性质，即自反证明。但是，可以说，一旦修复了两个端点，您就不再具有此属性。换句话说，eq的归纳原理实际上是{ y | x = y }的归纳原则，而不是x = y的归纳原则。类似地，向量的归纳原则(长度索引列表)实际上是{ n & Vector.t A n }的归纳原则。

要解码错误消息，可以尝试手动应用eq的归纳原则。归纳原理指出:给定一个类型A、一个x : A项和一个性质P : forall y : A, x = y -> Prop来证明给定的y : A和任何证明e : x = y的P y e，那么证明P x eq_refl就足够了。(要了解为什么这是有意义的，请考虑非依赖版本:给定一个类型A、一个术语x : A和一个属性P : A -> Prop，对于任何y : A和任何证明e : x = y，证明P y就足够了。)

如果您尝试手工应用此方法，您将发现，当您试图通过第二个等式证明导入时，无法构造一个类型良好的函数P。

有一篇优秀的博客文章在这里更深入地解释了这一点：http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/

Answer 2

错误的原因是destruct的工作方式，回想一下这个策略试图构建一个match语句，为了做到这一点，它有一些启发来将依赖假设引入上下文。

特别是，在这种情况下，它试图抽象变量m，它是y : m = m中eq归纳的索引；但是y没有被带入上下文，因此出现了错误，因为m0是抽象的m。您可以通过进行“不太聪明”的匹配来解决这个问题，它不会修改m

refine (match x with | @eq_refl _ _ => _ end).

但通常情况下，最好的解决办法是将错误的假设纳入范围：

revert y; destruct x.

另一方面，证明你的目标，简单的模式匹配是不够的，因为其他优秀的答案。我最喜欢的解决像你这样的目标的实用方法是使用一个库：

From mathcomp Require Import all_ssreflect.

Lemma true_num (m : nat) (x y : m = m) : x = y.
Proof. exact: eq_irrelevance. Qed.

在这种情况下，nat类型的适当附带条件由库的机器自动推断。