coq - 为什么我不能在 Coq 中将 `app` 与 `fold_right` 一起使用？

Question

我在以下程序的最后一行收到类型错误:

Require Import List.
Import ListNotations.

(* This computes to 10 *)
Compute (fold_right plus 0 [1;2;3;4]).

(* I want this to compute to [5;6;7;8] but it gives a type error instead *)
Compute (fold_right app [] [[5;6]; [7;8]]).

这是我得到的错误:

Error:
The term "app" has type "forall A : Type, list A -> list A -> list A" while it is expected to have type
 "Type -> ?A -> ?A" (cannot instantiate "?A" because "A" is not in its scope).

我真的不明白为什么我会收到这个错误。 app有什么不同和 plus这里？。和 app有关系吗？多态同时 plus是单态的 nat -> nat -> nat功能？

以防万一，我的 Coq 版本是 8.5。

Answer 1

你猜对了:它确实与app有关。是多态的。问题在于 Coq 允许根据相应的术语是否应用于参数以不同的方式推断隐式参数。更准确地说，非最大隐式仅在该术语应用于某事物时才插入，但如果该术语单独使用，则不会插入，例如您的 app .有两种方法可以补救这种情况:

1- 强制 Coq 为该实例推断某些内容，如 fold_right (@app _) [] [[5; 6]; [7; 8]] .

2- 使用一个全局声明来最大程度地插入类型参数:Arguments app {_} _ _. .有关此操作的更多详细信息，请查看 reference manual