在 Coq 中使用 eexists 构造记录项

Question

假设在某种类型 A 上有一个拒绝关系 R。

Variable A : Type.
Variable R : A -> A -> A -> A -> A -> A -> A -> A -> A -> A -> Prop.

X 和 Y 是略有不同的命题，它们都断言 R 持有大约 10 个 A.

类型的项

Inductive X : Prop :=
| X_intro : forall a0 a1 a2 a3 a4 a5 a6 a7 a8 a9, 
R a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 -> X. 

Record Y : Prop :=
{ a0 : A; a1 : A; a2 : A; a3 : A; a4 : A;
  a5 : A; a6 : A; a7 : A; a8 : A; a9 : A;
  RY : R a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 }.

由于X和Y断言相同的东西，证明X -> Y应该很容易。例如，我们可以通过显式构造 Y.

的证明来做到这一点

Theorem XY : X -> Y.
inversion 1. exists a0 a1 a2 a3 a4 
a5 a6 a7 a8 a9. apply H0. Qed.

但这似乎没有必要。 inversion 在前提下得到的最后一个命题完全决定了这 10 个词，所以我们不应该把它们的名字拼出来。我们可以用 eexists 推迟他们的身份，稍后统一他们。

Theorem XY' : X -> Y.
intro. eexists. inversion H. apply H0.

但是统一在这里失败了。这是我之前的目标 apply H0:

H0 : R a0 a1 a2 a3 a4 a5 a6 a7 a8 a9

======================== ( 1 / 1 )
R ?46 ?47 ?48 ?49 ?50 ?51 ?52 ?53 ?54 ?55

R的所有参数都未确定，所以应该可以统一?46和a0，?47和a1，等等.为什么会失败？

Answer 1

您收到的错误消息大致如下：

unable to unify "?a0" with "a0" (cannot instantiate "?a0" because "a0" is not in its scope)

这是一个相当常见的错误。让我用一个简单的例子来解释它。

让我们从定义一个包含类型 A:

的值的归纳数据类型开始

Variable A : Type.

Inductive Box :=
| elem : A -> Box.

接下来，让我们定义一个关于这种数据类型的定理，它指出如果你有一个盒子，那么存在一个元素等于盒子里的东西：

Theorem boxOk (b:Box) : exists a, match b with elem a' => a = a' end.

我们可以尝试用您的方式证明这一点：

  eexists.
  destruct b.
  Fail reflexivity.
Restart.

但是 reflexivity 失败了，出现可怕的错误消息：

Unable to unify "?a" with "a" (cannot instantiate "?a" because "a" is not in its scope: available arguments are "elem a").

那么这里发生了什么？这些策略构造的术语如下所示：

ex_intro _ ?a (match b with elem a => eq_refl end).

而你现在要求 Coq 用 a 填充 ?a，这是行不通的，因为 a 没有定义在 ?a 的范围内。 此错误最常见的问题是 eexists 被调用得太早。

因此，我们应该先 destruct，然后调用 eexists。它有效：

  destruct b.
  eexists.
  reflexivity.
Qed.

这些策略构造的术语如下所示：

match b with elem a => (ex_intro _ ?a eq_refl) end.

现在 a 在 ?a 的范围内，可以轻松填写。

在您的示例中，您应该执行以下操作（这实际上是您在手动证明中所做的）。

Theorem XY' : X -> Y.
  intro h. 
  inversion h as [? ? ? ? ? ? ? ? ? ? h'].
  eexists. 
  apply h'.
Qed.

在 Coq 中使用 eexists 构造记录项

Using eexists to construct record terms in Coq

coq