基于Coq的杨忠道定理形式化证明  

Formalization of C.T.Yang’s Theorem in Coq

作　　者：严升 郁文生[1] 付尧顺 YAN Sheng;YU Wen-Sheng;FU Yao-Shun(Beijing Key Laboratory of Space-ground Interconnection and Convergence(School of Electronic Engineering,Beijing University of Posts and Telecommunications),Beijing 100876,China)

机构地区：[1]天地互联与融合北京市重点实验室(北京邮电大学电子工程学院),北京100876

出　　处：《软件学报》2022年第6期2208-2223,共16页Journal of Software

基　　金：国家自然科学基金(61936008)。

摘　　要：实现拓扑学定理的机器证明,是吴文俊院士生前的宿愿.杨忠道定理涉及一般拓扑学中的诸多基本概念,对深刻理解拓扑空间的本质有重要意义.该定理表明,拓扑空间中每一个子集的导集为闭集当且仅当此空间中的每一个单点集的导集为闭集,是一般拓扑学中的一个重要定理.基于定理证明辅助工具Coq,从公理化集合论机器证明系统出发,对一般拓扑学中的开集、闭集、邻域、凝聚点和导集等拓扑基本概念进行形式化描述,给出这些概念基本性质的形式化验证,建立了拓扑空间的形式化框架.在此基础上,实现基于Coq的杨忠道定理形式化证明.全部引理、定理和推论均完整给出Coq的形式化描述和机器证明代码,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,其证明过程规范、严谨、可靠.杨忠道定理的形式化证明是一般拓扑学形式化内容的一个深刻体现.It was a wish for Academician Wu Wen-tsun to mechanically prove a class theorem in topology. The C.T.Yang’s Theorem includes many basic concepts in general topology, which has great significance for understanding essential content of topological space.The C.T.Yang’s Theorem is an important theorem in general topology, which states that in any topological space, if the derived set of a singleton set is closed, then the derived set of any subset is also closed. Based on the interactive theorem prover Coq, this paper presents a formalization of the basic concepts in general topology from mechanized axiomatic set theory, including open sets, closed sets,neighborhoods, condensation point, derived sets, and gives a formal verification of the corresponding properties. Furthermore, a formal framework of topological space is proposed and the formal proof of C.T.Yang’s Theorem is realized in general topology. The proof code of all the theorems is given without exception, the formalization process has been verified, which reflects that the formal proof of mathematics theorem has the characteristics of readability and interactivity in Coq. The proof process is standardized, rigorous, and reliable, and the formal proof of C.T.Yang’s Theorem is a profound embodiment of general topology formalization.

关 键 词：COQ 形式化证明 公理化集合论 一般拓扑 拓扑空间 杨忠道定理 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]