使用eexists在Coq中构造记录项

Question

假设有一个十进制关系R针对某种类型A。

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

< p >< code >X< /code >和< code >Y< /code >是稍有不同的命题，它们都声称在< code >A< /code >类型的10个术语中，< code >R< /code >成立。< /p >

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.

但是这似乎是不必要的。通过对前提进行反演得到的最后一个命题完全确定了这10个术语，因此我们不需要拼写它们的名称。我们可以使用eexists推迟它们的识别并稍后统一它们。

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

但是统一在这里失败了。 这是应用 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 统一，等等。为什么会失败？

- user287393

---

将来请尽量缩小您的测试用例，例如我相信三元关系已经足够了。此外，请不要引用自动生成的名称，如 H0。这会使使用不同 Coq 版本的用户难以帮助您。 - Konstantin Weitz

Answer 1

你得到的错误信息大致是：

无法将“?a0”与“a0”统一（无法实例化“?a0”，因为“a0”不在其范围内）

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

让我们从定义一个包装类型为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.

但是，反射性失败了，并显示以下错误信息：

无法将“?a”与“a”统一（无法实例化“?a”，因为“a”不在其范围内：可用参数为“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.

- Konstantin Weitz