我正在尝试使用方程软件包来定义COQ中的向量的函数。显示我将要描述的问题的最小代码可在以下要点。
。我的想法是编码某种类型对向量的所有元素所包含的"证明"查找的函数，该元素具有标准定义：
Inductive vec (A : Type) : nat -> Type :=
| VNil : vec A 0
| VCons : forall n, A -> vec A n -> vec A (S n).
使用以前的类型，我定义了以下（也是标准）查找操作（使用等式）：
Equations vlookup {A}{n}(i : fin n) (v : vec A n) : A :=
vlookup FZero (VCons x _) := x ;
vlookup (FSucc ix) (VCons _ xs) := vlookup ix xs.
现在，麻烦开始了。我想定义一些"证明"的类型属性属于向量中的所有元素。以下归纳类型可以完成此工作：
Inductive vforall {A : Type}(P : A -> Type) : forall n, vec A n -> Type :=
| VFNil : vforall P _ VNil
| VFCons : forall n x xs,
P x -> vforall P n xs -> vforall P (S n) (VCons x xs).
最后，我要定义的功能是
Equations vforall_lookup
{n}
{A : Type}
{P : A -> Type}
{xs : vec A n}
(idx : fin n) :
vforall P xs -> P (vlookup idx xs) :=
vforall_lookup FZero (VFCons _ _ pf _) := pf ;
vforall_lookup (FSucc ix) (VFCons _ _ _ ps) := vforall_lookup ix ps.
在我对我来说，这个定义很有意义，并且应该输入检查。但是，方程式显示了以下警告，并给我留下了证据义务，我不知道如何完成它。
以前函数的定义后显示的消息是：
Warning:
In environment
eos : end_of_section
fix_0 : forall (n : nat) (A : Type) (P : A -> Type) (xs : vec A n)
(idx : fin n) (v : vforall P xs),
vforall_lookup_ind n A P xs idx v (vforall_lookup idx v)
A : Type
P : A -> Type
n0 : nat
x : A
xs0 : vec A n0
idx : fin n0
p : P x
v : vforall P xs0
Unable to unify "VFCons P n0 x xs0 p v" with "v".
剩下的义务为
Obligation 1 of vforall_lookup_ind_fun:
(forall (n : nat) (A : Type) (P : A -> Type) (xs : vec A n)
(idx : fin n) (v : vforall P xs),
vforall_lookup_ind n A P xs idx v (vforall_lookup idx v)).
稍后，在AGDA标准库中查看了类似的定义后，我意识到上一个函数定义缺少了空置的案例：
lookup : ∀ {a p} {A : Set a} {P : A → Set p} {k} {xs : Vec A k} →
(i : Fin k) → All P xs → P (Vec.lookup i xs)
lookup () []
lookup zero (px ∷ pxs) = px
lookup (suc i) (px ∷ pxs) = lookup i pxs
我的问题是，我该如何指定，对于空的向量案例，右手应该是空的，即矛盾？方程手册显示了平等的示例，但我可以将其适应此情况。我对我做错了什么想法？
我想我终于通过仔细查看生成的义务来理解了这个示例中的情况。
定义是正确的，并且被接受（您可以在不解决义务的情况下使用vforall_lookup）。无法生成的是与该功能相关的归纳原理。
更确切地说，方程在"消除原理"部分中以三个步骤（参考手册中详细介绍）生成正确的归纳原理：
-
它生成函数的图（在我的方程式中，它称为
vforall_lookup_graph，在以前的版本中，称为vforall_lookup_ind）。我不确定我完全了解它是什么。直观地，它反映了功能主体的结构。无论如何，这是生成归纳原理的关键组成部分。 -
证明该功能尊重此图（在称为
vforall_lookup_graph_correct或vforall_lookup_ind_fun的引理中）; -
它结合了最后两个结果以生成与该功能相关的诱导原理（此引理在所有版本中称为
vforall_lookup_elim）。
在您的情况下，该图是正确生成的，但方程无法自动证明该功能尊重其图（步骤2），因此它留给您。
让我们尝试一下！
Next Obligation.
induction v.
- inversion idx.
- dependent elimination idx.
(* a powerful destruct provided by Equations
that correctly working with dependent types
*)
+ constructor.
+ constructor.
COQ拒绝使用错误
的最后一次呼叫constructor Unable to unify "VFCons P n1 x xs p v" with "v".
这实际上看起来像是首先获得的错误，因此我认为自动分辨率达到了同一点并失败了。这是否意味着我们走了错误的道路？让我们仔细观察第二个constructor之前的目标。
我们必须证明
vforall_lookup_graph (S n1) A P (VCons x xs) (FSucc f) (VFCons P n1 x xs p v) (vforall_lookup (FSucc f) (VFCons P n1 x xs p v))
虽然vforall_lookup_graph_equation_2的类型，vforall_lookup_graph_equation的第二个构造函数是
forall (n : nat) (A : Type) (P : A -> Type) (x : A) (xs0 : vec A n) (f : fin n) (p : P x) (v : vforall P xs0),
vforall_lookup_graph n A P xs0 f v (vforall_lookup f v) -> vforall_lookup_graph (S n) A P (VCons x xs0) (FSucc f) (VFCons P n x xs0 p v) (vforall_lookup f v)
差异在于对vforall_lookup的调用。在第一种情况下，我们有
vforall_lookup (FSucc f) (VFCons P n1 x xs p v)
，在第二种情况下
vforall_lookup f v
，但根据vforall_lookup的定义，这些都是相同的！但是默认情况下，统一无法认识到这一点。我们需要有所帮助。我们可以给出一些参数的价值，例如
apply (vforall_lookup_graph_equation_2 n0).
，或者我们可以使用比apply更积极地统一的exact或refine，因为它们得到了整个期限，而不仅仅是其头
refine (vforall_lookup_graph_equation_2 _ _ _ _ _ _ _ _ _).
我们可以通过诱导假说很容易得出结论。这给出以下证明
Next Obligation.
induction v.
- inversion idx.
- dependent elimination idx.
+ constructor.
+ (* IHv is the induction hypothesis *)
exact (vforall_lookup_graph_equation_2 _ _ _ _ _ _ _ _ (IHv _)).
Defined.
由于我喜欢手工做依赖类型的证据，所以我不禁提供不使用 dependent elimination的证据。
Next Obligation.
induction v.
- inversion idx.
- revert dependent xs.
refine (
match idx as id in fin k return
match k return fin k -> Type with
| 0 => fun _ => IDProp
| S n => fun _ => _
end id
with
| FZero => _
| FSucc f => _
end); intros.
+ constructor.
+ exact (vforall_lookup_graph_equation_2 _ _ _ _ _ _ _ _ (IHv _)).
Defined.