使用eexists在Coq中构建记录术语

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都是未定的,所以应该可以统一?46with a0,?47with a1等等.为什么会失败？

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.

但reflexivity失败了,带有可怕的错误消息:

无法将"？a"与"a"统一(无法实例化"？a",因为"a"不在其范围内:可用参数为"elem a").

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

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

而你现在要求勒柯克填写?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.