如何在 Coq 中显式提供隐式参数？答案

【问题标题】：How do I provide implicit arguments explicitly in Coq?如何在 Coq 中显式提供隐式参数？
【发布时间】：2017-12-18 18:33:21
【问题描述】：

假设我有一个定义f : x -> y -> z，其中x 可以很容易地推断出来。因此，我选择使用 Arguments 使 x 成为隐式参数。

考虑以下示例：

Definition id : forall (S : Set), S -> S :=
fun S s => s.

Arguments id {_} s.

Check (id 1).

显然S = nat 可以并且被 Coq 推断出来，Coq 回复：

id 1
     : nat

但是，稍后，我想让隐式参数显式化，例如为了可读性。

换句话说，我想要这样的东西：

Definition foo :=
 id {nat} 1. (* We want to make it clear that the 2nd argument is nat*)

这可能吗？如果是，合适的语法是什么？

【问题讨论】：

标签： coq

【解决方案1】：

您可以在名称前加上 @ 以删除所有隐含并明确提供它们：

Check @id nat 1.

您还可以使用(a:=v) 按名称传递隐式参数。这既可以澄清正在传递的参数，也允许您传递一些隐含而不传递 _ 给其他参数：

Check id (S:=nat) 1.

Definition third {A B C:Type} (a:A) (b:B) (c:C) := c.
Check third (B:=nat) (A:=unit) tt 1 2.

【讨论】：

【解决方案2】：

一种可能的方法是在定义前添加@。例如：

Definition id : forall (S : Set), S -> S :=
fun S s => s.

Arguments id {_} s.

Check @id nat 1.

结果：

id 1
     : nat

【讨论】：