如何使 Coq 形式化可重用？
How to make a Coq formalisation reusable?
我正在研究算法的 Coq 形式化。但是这个算法的组件（一些函数和引理）可以在不同的类型上是 "overloaded"（在 Haskell 意义上）。
我的目的是避免代码重复。我知道 Coq 有模块（如 ML）和类型 类（如 Haskell）。以可以在不同类型上进行参数化的方式实现引理和函数定义可重用性的最佳方法是什么？
最好避免将 Coq 模块用于命名空间或使定义不透明以外的任何事情。从属记录（类型 classes 背后的基础特性）在编写参数定义方面通常比模块更好，因为它们是第一个 class 对象，可以通过适用于其他对象的相同规则进行操作在科克。也就是说，当将 Coq 代码提取到 OCaml 中时，Coq 模块被提取到 OCaml 模块中，而依赖记录依赖于智能记录才能正常工作。因此，如果您关心提取到 OCaml 中，以及与提取的代码交互，模块可能是更好的选择。
Type classes 是建立在相关记录之上的一项功能，通过添加自动实例推断使它们更易于使用。不幸的是，Coq 中的 type-class 实例推断不是超级健壮，需要您调整实例或手动提供它们才能使其在实践中工作——无论如何，它们肯定比它们更难使用Haskell 对应项——并且还可以减慢编译时间。 MathClasses 库在很大程度上依赖于类型 classes 来定义数学结构，它似乎对它们很有效。
还有一个特性叫做规范结构，它也是基于依赖记录，完成的与classes类型大致相同，但编程模型和推理引擎略有不同。在某些情况下，它们比 type classes 工作得更好，但在其他情况下更难使用。例如，Ssreflect 库广泛使用它们。
关于使用模块或记录的小讨论here。
我正在研究算法的 Coq 形式化。但是这个算法的组件（一些函数和引理）可以在不同的类型上是 "overloaded"（在 Haskell 意义上）。
我的目的是避免代码重复。我知道 Coq 有模块（如 ML）和类型 类（如 Haskell）。以可以在不同类型上进行参数化的方式实现引理和函数定义可重用性的最佳方法是什么？
最好避免将 Coq 模块用于命名空间或使定义不透明以外的任何事情。从属记录（类型 classes 背后的基础特性）在编写参数定义方面通常比模块更好，因为它们是第一个 class 对象，可以通过适用于其他对象的相同规则进行操作在科克。也就是说，当将 Coq 代码提取到 OCaml 中时，Coq 模块被提取到 OCaml 模块中，而依赖记录依赖于智能记录才能正常工作。因此，如果您关心提取到 OCaml 中，以及与提取的代码交互，模块可能是更好的选择。
Type classes 是建立在相关记录之上的一项功能，通过添加自动实例推断使它们更易于使用。不幸的是，Coq 中的 type-class 实例推断不是超级健壮，需要您调整实例或手动提供它们才能使其在实践中工作——无论如何，它们肯定比它们更难使用Haskell 对应项——并且还可以减慢编译时间。 MathClasses 库在很大程度上依赖于类型 classes 来定义数学结构，它似乎对它们很有效。
还有一个特性叫做规范结构，它也是基于依赖记录，完成的与classes类型大致相同，但编程模型和推理引擎略有不同。在某些情况下，它们比 type classes 工作得更好，但在其他情况下更难使用。例如，Ssreflect 库广泛使用它们。
关于使用模块或记录的小讨论here。