Trocq：免费的证明传输机制，超越等价性与单值性

《ACM Transactions on Programming Languages and Systems》：Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence

本文提出Trocq框架，一种基于新型类型等价关系的通用证明转移框架，支持参数化翻译、子类型和商关系等异构关系的处理，并实现为Coq的插件。该框架通过层次化分析关系结构，避免依赖正合性公理，适用于多种数学证明场景，如整数表示转换和模运算性质推导。

　　在现代数学形式化过程中，依赖类型理论的交互式定理证明器成为了一个重要的工具。然而，形式化过程中仍然存在许多繁琐的步骤，例如需要证明某些类型变换不影响其可证明性。为了简化这一过程，研究人员提出了一种名为Trocq的新框架，旨在自动化依赖类型理论中的证明转移。

证明转移的难点在于如何确保类型变换不会破坏原有的逻辑关系。现有的工具通常针对特定类型的转换，比如等价关系或结构等价，但它们的适用范围有限，且可能依赖于某些强假设，如选择公理或未ivalence公理。Trocq框架则通过引入一种更为通用的类型等价结构，使得证明转移可以适用于更广泛的关系类型，从而减少了对未ivalence公理的依赖。这种新框架基于一种对称的类型等价定义，将类型之间的关系分解为多个层次的结构，从而实现更细粒度的证明转移。

Trocq框架的核心在于其对类型等价的处理方式。传统的未ivalence参数化翻译依赖于未ivalence公理，以确保类型之间的等价性，从而进行证明转移。然而，这种依赖在某些情况下是不必要的，尤其是在涉及更复杂的类型结构时。Trocq通过一种新的方法，允许用户在不依赖未ivalence公理的情况下，进行更灵活的证明转移。这使得该框架在处理某些经典数学形式化任务时更加实用，例如在Lean的mathlib库或Rocq/Coq的mathcomp-analysis库中，这些库通常假设了某种形式的证明不可靠性，与未ivalence公理不兼容。

此外，Trocq框架还结合了依赖类型理论中的某些特性，如泛型的结构等价性，以及更广泛的类型关系。这些特性使得框架能够处理诸如自然数与模9整数、列表与向量等不同类型的转换。通过引入一种层次化的结构分析，Trocq能够更精确地识别类型之间的关系，从而生成更有效的证明转移策略。这一框架不仅适用于等价关系，还适用于更复杂的类型结构，如非等价的类型或带有参数的类型。

Trocq的实现基于Rocq/Coq的交互式定理证明器，使用了Elpi元语言作为插件的实现基础。该插件通过一个库中的原始形式化证明，生成用于证明转移的工具，并且提供了多个应用示例。插件有两个版本，一个基于HoTT库，使用了HoTT中的路径类型；另一个基于Rocq/Coq的标准库，支持Prop类型。这些版本展示了Trocq框架在不同类型系统中的适用性。

Trocq的框架为证明转移提供了一种新的思路，即通过类型之间的关系来指导证明的合成。这种思路不仅适用于等价关系，还适用于其他类型的结构，如单射或满射。框架中的规则和策略可以处理更复杂的证明，包括涉及量化、函数应用和依赖类型的证明。此外，Trocq还引入了一种更精细的层次结构，使得不同类型之间的转换可以被系统地管理。

在实际应用中，Trocq插件通过一系列预定义的关系和转换规则，帮助用户在形式化过程中自动化地进行证明转移。这些规则可以处理诸如自然数与二进制整数、列表与向量、模运算等不同的类型转换。通过这种方式，Trocq框架减少了用户在形式化过程中需要手动处理的证明步骤，使得整个过程更加高效和可靠。

Trocq框架的实现不仅依赖于元编程技术，还结合了逻辑编程的思路，通过定义一系列规则和策略，使得证明转移的过程可以被系统地自动化。该框架的规则基于一种形式化的类型理论，使得每个转换步骤都可以被精确地描述和验证。通过这种方式，Trocq能够确保生成的证明不仅正确，而且具有良好的可读性和可维护性。

Trocq框架的出现为依赖类型理论的证明转移提供了一种新的解决方案，其优势在于能够处理更广泛的关系类型，并减少对未ivalence公理的依赖。这使得该框架在形式化经典数学时更加适用，因为许多经典数学库不依赖于未ivalence公理。此外，Trocq还支持用户自定义的关系，使得其应用范围更加广泛。

Trocq框架的实现是一个重要的进展，它不仅提供了更灵活的证明转移工具，还展示了如何通过元编程和逻辑编程的结合，实现更高效的数学形式化。该框架的出现为依赖类型理论的研究和应用提供了新的思路，使得形式化数学的过程更加自动化和高效。