一句话：在 Coq 中基于 Incone 库形式化可计算分析，给出连续结构上可执行算法的正确性证明。
本文在 Coq 中形式化可计算分析的一系列定理。许多结果给出作用于无限输入的可执行算法：算法通过有限逼近计算，并按可计算分析意义证明正确。开发依赖 Incone 库，该库以信息论连续性为核心，为连续结构上的算法推理提供通用接口。论文证明实数代数运算与高效极限算子可计算、某些可数无限乘积与函数空间同构、自然数子集枚举表示与开子集空间抽象定义相容，以及连续可实现性蕴含序列连续性。还形式化非可计算结果：Baire 空间上信息论连续性与度量连续性等价、不同连续性概念比较，以及无限制极限算子和闭子集选择不可计算。
We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of operating on finite approximations and are proven correct in the sense of computable analysis. The development is done in the proof assistant Coq and heavily relies on the Incone library for information theoretic continuity. This library is developed by one of the authors and the paper can be used as an introduction to the library as it describes many of its most important features in detail. While the ability to have full executability in a formal development of mathematical statements about real numbers and the like is not a feature that is unique to the Incone library, its original contribution is to adhere to the conventions of computable analysis to provide a general purpose interface for algorithmic reasoning on continuous structures. The results that provide complete computational content include that the algebraic operations and the efficient limit operator on the reals are computable, that certain countably infinite products are isomorphic to spaces of functions, compatibility of the enumeration representation of subsets of natural numbers with the abstract definition of the space of open subsets of the natural numbers, and that continuous realizability implies sequential continuity. We also formalize proofs of non-computational results that support the correctness of our definitions. These include that the information theoretic notion of continuity used in the library is equivalent to the metric notion of continuity on Baire space, a complete comparison of the different concepts of continuity that arise from metric and represented-space structures and the discontinuity of the unrestricted limit operator on the real numbers and the task of selecting an element of a closed subset of the natural numbers.
@article{paperbot1312,
title = {Computable analysis and notions of continuity in Coq},
author = {Florian Steinberg and Laurent Thery and Holger Thies},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 2},
year = {2021},
doi = {10.23638/lmcs-17(2:16)2021}
}