参数化 Coq 库的最佳实践

Question

我正在用 Coq 编写一个依赖于用户提供的类型参数的库。一个中心部分是沿着

的结构

Require Import Ascii.
Require Import String.
Parameter UserType : Set. (* <<- placeholder for this example *)
Parameter UserToString : UserType -> string.

Inductive Tag : Set := TBool | TNat | TUser | TList : Tag -> Tag | TSum : Tag -> Tag -> Tag.
Fixpoint decodeT (t : Tag) : Set :=
  match t with
  | TBool => bool
  | TNat => nat
  | TUser => UserType (* <<- needed here *)
  | TList t' => list (decodeT t')
  | TSum l r => sum (decodeT l) (decodeT r)
  end.
(* ...etc..., including: *)
Definition tostring (t : Tag) (v : decodeT t) : string := (* match t with ... end *) "dummy".
(* and other stuff *)

所以我无法以某种形式避免那些 Parameter。整个库分为多个文件，由于大小原因，将所有内容都放在一个文件中会很不舒服。

有一个导出所有子模块的顶级包装器。理想情况下，我想在导入库时传递参数 once，然后这个包装器可以做一些魔术将它们传播到所有子模块，这样之后我就不会再也不用担心了。

我研究了各种方法，但目前没有任何效果。

如果我将文件内容包裹在Sections中，那么Parameters将成为仅在使用它们的定义上的额外参数，然后我必须在使用时手动拼接它们图书馆的外部功能。

如果我不将它们包装在 Section 中，它们是模块参数，但我找不到实际提供值的方法。（所有形式的 with Definition 似乎都需要模块签名/Module Type？复制所有名称和类型以生成显式签名将是非常多余的，所以可能是一种让它工作的方法，但我找不到它。文档也相当无用......）就我测试的东西而言，使用 Context 之类的变体似乎有同样的问题。

我很高兴制作一个 Module Type UserDefs（或类型类，或其他），将所有用户定义组合到一个值中。我只是不知道如何将它实际放入子模块中。

那我该怎么做呢？上面的示例文件内部需要发生什么，外部需要发生什么，这样我就可以将 中的定义传递一次 ，然后将完全配置的库传递给 Import?

Answer 1

then I have to manually splice them in everywhere when using the library's functions from outside.

这通常通过混合使用隐式参数和类型 classes 来解决。

为 user-provided 个参数声明一个 class。

Class UserParams : Type :=
  { UserType : Set
  ; UserToString : UserType -> string
  }.

(* Make sure UserType and UserToString have UserParams as a maximally inserted implicit *)

然后在您的库中打开由 class:

的实例参数化的部分

Require Import Ascii.
Require Import String.

Section MyLib.
Context {userParams : UserParams}.  (* Context generalizes Variable and allows you to set implicitness *)

Inductive Tag : Set := TBool | TNat | TUser | TList : Tag -> Tag | TSum : Tag -> Tag -> Tag.
Fixpoint decodeT (t : Tag) : Set :=
  match t with
  | TBool => bool
  | TNat => nat
  | TUser => UserType (* <<- needed here *)
  | TList t' => list (decodeT t')
  | TSum l r => sum (decodeT l) (decodeT r)
  end.
(* ...etc..., including: *)
Definition tostring (t : Tag) (v : decodeT t) : string := (* match t with ... end *) "dummy".
(* and other stuff *)

End MyLib.

然后用户实例化 class

Require Import MyLib.

Instance myParams : UserParams :=
  {| UserType := ...
   ; UserToString := ... |}.

然后你的库函数会在你使用的时候自动实例化。

参数化 Coq 库的最佳实践

Best practices for parametrized Coq libraries

coq