为示例提供部分参数

Question

考虑这一部分：

Section MyMap.

Variables D R : Type.

Fixpoint mymap (f : D -> R) (l : list D) : list R :=
  match l with
  | nil => nil
  | d :: t => f d :: mymap f t
  end.

End MyMap.

这里我使用 Variables 来声明我的域和范围类型。作为对我的函数定义的完整性检查，我想包含一个 Example:

Example example_map_S : mymap S [0; 1; 2] = [1; 2; 3].
Proof.
  simpl; trivial.
Qed.

但是我似乎不能在我的部门内这样做。相反，我得到：

Error: The term "S" has type "nat -> nat" while it is expected to have type "D -> R".

这并不奇怪，让我们换个方式试试：

Example example_map_S : @mymap nat nat S [0; 1; 2] = [1; 2; 3].
Proof.
  simpl; trivial.
Qed.

产生：

Error: The term "nat" has type "Set" while it is expected to have type "D -> R".

我想这很公平，分段 Variables 与隐式参数不同。但是还是留下了问题！

如何在关闭该部分之前向术语提供具体的 Variables，以便创建有用的 Examples？

Answer 1

Section MyMap.
...

如果我们检查mymap在部分的类型，我们得到

Check mymap.
(* mymap : (D -> R) -> list D -> list R *)

当然，我们不能将D和R与nat统一起来，因为D和R是一些局部假设类型。

但是，我们可以在这种通用设置中模拟您的示例，显示 mymap 函数的预期属性：

Example example_nil (f : D -> R) :
  mymap f [] = [] := eq_refl.

Example example_3elems (f : D -> R) (d0 d1 d2 : D) :
  mymap f [d0; d1; d2] = [f d0; f d1; f d2] := eq_refl.

End MyMap.

为示例提供部分参数

Supplying section arguments for examples

coq