Coq:添加隐式变量

Question

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

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

我可以在一个部分或模块中包含所有功能并写Variables (A B: Type) etc一开始，但这不会使变量隐含，我必须在部分末尾手动设置所有函数的参数。更糟糕的是，这会使所有变量共享。 IE。如果我声明

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.

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