coq - 在 Coq 中使用 eexists 构造记录项

Question

假设存在拒绝关系 R在某些类型 A .

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.