为什么我不能在Coq中使用`app`和`fol​​d_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 {_} _ _..有关这方面的更多详细信息,请查看参考手册