Coq:添加隐式变量

Question

假设我有一组函数,每个函数都可以依赖于一个或两个隐式变量A B: Type.我怎么指定这个？即将这些变量添加到它们的变量列表中并将它们设置为隐式变量.

最明显的方法是添加{A B: Type}到他们的定义中.然而,在现实生活和中等复杂的发展中,这些共享的隐含列表很容易就是6-10个条目,并且包括复杂的类型,因此使得函数定义难以阅读,甚至更难理解它们的相似性或对所提到的类型进行更改.因此,该解决方案不适用.

我可以在一个部分或模块中包含所有函数并Variables (A B: Type) etc在开头写入,但这不会使变量隐含,我将不得不在部分末尾手动设置所有函数的参数.更糟糕的是,这将使所有变量共享.即如果我宣布

Section sect.
  Variable A B: Type.

  Definition f (t: A -> Type) := (..).

  Definition g (t: A -> Type) (s: B -> Type) := G (f t) (f s).
End sect.

(G是一些双变量函数)然后g不会被接受,因为s不存在A -> Type,即使基本上f只需要一个任意类型的族.

我可以制作一个部分并宣布Context {A B: Type}.这将使这些变量隐含在所有函数中,但是像以前一样的共享问题仍将存在.因此,我必须随意将我的函数分成几个部分,以便我可以使用隐式参数的不同值来调用Sect.1中的函数.这很有效,但很难看,而且我可以很容易地想象出每个部分都必须有2-3个函数才能正常调用它们的情况.

有更好的解决方案吗？

Answer 1

您可以做两件不太困难的事情：

Generalizable All Variables.

Definition g `(t: A -> Type) `(s: B -> Type) := G (f t) (f s).

现在您可以使用反引号，它会自动插入使定义有效所需的隐式变量。这是我引入隐式的最常见方式。

另一种方法是按照您的部分：

Arguments g : default implicits.

您需要对每个定义的术语重复此操作，但至少不需要命名所有参数。