Trocq：无需代价即可进行证明迁移，无论是否使用单值性
计算机科学中的逻辑
2024-02-21 v2
摘要
形式化数学库对同一数学概念可能采用范围较广的不同表示。然而，在获取定理的相应变体时，通常仍需要用户从轻微到大量的手工输入，而此类显然的替换在纸面证明中一般被隐去。本文提出 Trocq，一种用于依赖类型理论的新型证明迁移框架。Trocq 基于一种新颖的类型等价表述，用于推广单值参数化翻译。该框架尽可能避免对单值性公理的依赖，且可使用比等价关系更多的关係。我们已在 Coq 证明助手的 CoqElpi 元语言中实现相应插件。我们在交互式定理证明中一组具代表性的证明迁移问题示例上使用该插件，并说明 Trocq 如何覆盖若干现有工具的范围，这些工具用于程序验证以及广义上的形式化数学。
引用
@article{arxiv.2310.14022,
title = {Trocq: Proof Transfer for Free, With or Without Univalence},
author = {Cyril Cohen and Enzo Crance and Assia Mahboubi},
journal= {arXiv preprint arXiv:2310.14022},
year = {2024}
}