Formalization of C.T.Yang’s Theorem in Coq
Author:
Affiliation:

Clc Number:

TP311

  • Article
  • | |
  • Metrics
  • |
  • Reference [53]
  • |
  • Related
  • |
  • Cited by
  • | |
  • Comments
    Abstract:

    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.

    Reference
    [1] Wu WT. Mechanical Theorem Proving in Geometries:Basic Principles. Berlin:Springer-Verlag, 1994.
    [2] Wu WT. Mathematics Mechanization:Mechanical Geometry Theorem-proving, Mechanical Geometry Problem-solving, and Polynomial Equations-solving. In:Hazewinkel M, ed. Mathematics and Its Applications, Vol.489. Beijing and Dordrecht:Science Press and Kluwer Academic Publishers, 2000.
    [3] Xia BC, Yang L. Automated Inequality Proving and Discovering. Singapore:World Scientific, 2016.
    [4] Bertot Y, Castéran P. Interactive Theorem Proving and Program Development-Coq'Art:The Calculus of Inductive Constructions. Berlin:Spring-Verlag, 2004.
    [5] Pierce BC, de Amorim AA, Casinghino C, Gaboardi M, Greenberg M, Hriţcu C, Sjöberg V, Yorgey B. Software foundations. 2017. https://softwarefoundations.cis.upenn.edu/
    [6] The Coq Development Team. The Coq reference manual. Version 8.9.1. 2019. https://coq.inria.fr/distrib/V8.9.1/refman/
    [7] Nipow T, Paulson LC, Wenzel M. Isabelle/HOL:A Proof Assistant for Higher-order Logic. Berlin:Springer-Verlag, 2002.
    [8] Hales TC. Formal proof. Notices of the American Mathematical Society, 2008, 55(11):1370-1380.
    [9] Harrision J. Formal proof-Theory and practice. Notices of the American Mathematical Society, 2008, 55(11):1395-1406.
    [10] Bancerek G, Bylinski C, Grabowski A, Kornilowicz A, Matuszewski R, Naumowicz A, Pak K, Urban J. Mizar:State-of-the-art and beyond. In:Proc. of the Int'l Conf. on Intelligent Computer Mathematics, Vol.9150. 2015. 261-279.
    [11] Gonthier G. Formal proof-The four color theorem. Notices of the American Mathematical Society, 2008, 55(11):1382-1393.
    [12] Beeson M. Mixing computations and proofs. Journal of Formalized Reasoning, 2016, 9(1):71-99.
    [13] Gonthier G, Asperti A, Avigad J, Bertot Y, Cohen C, Garillot F, Roux SL, Mahboubi A, O'Connor R, Biha SO, Pasca I, Rideau L, Solovyev A, Tassi E, Thery L. A machine-checked proof of the odd order theorem. In:Blazy S, Paulin-Mohring C, Picharidie D, eds. Proc. of the Interactive Theorem Proving. LNCS 7998, Rennes:Springer-Verlag, 2013. 163-179.
    [14] Hales T, Adams M, Bauer G, Harrison J, Hoang TL, Kaliszyk C, Magron V, Mclaughlin S, Nguyen TT, Nguyen TQ, Nipkow T, Obua S, Pleso J, Rute J, Solovyev A, Ta AHT, Tran TN, Trieu DT, Urban J, Vu K, Zumkeller R. A formal proof of the Kepler conjecture. Forum of Mathematics, Pi, 5, 2017, e2. https://doi.org/10.1017/fmp.2017.1
    [15] Guo LQ, Fu YS, Yu WS. A mechanized proof system of the third generation calculus in Coq. Scientia Sinica Mathematica, 2021, 51(1):115-136(in Chinese with English abstract).
    [16] Wiedijk F. Formal proof-Getting started. Notices of the American Mathematical Society, 2008, 55(11):1408-1414.
    [17] Chen G. Formalized mathematics and proof engineering. Communications of CCF, 2016, 12(9):40-44(in Chinese with English abstract).
    [18] Formalizing 100 theorems. http://www.cs.ru.nl/~freek/100/
    [19] Voevodsky V. Univalent foundations of mathematics. In:Beklemishev LD, de Queiroz R, eds. Proc. of the 18th Int'l Workshop on Logic, Language, Information and Computation. LNAI 6642, Berlin, Heidelberg:Springer-Verlag, 2011. https://doi.org/10.1007/978-3-642-20920-8_4
    [20] Gowers WT. Rough structure and classification. In:Alon N, Bourgain J, Connes A, Gromov M, Milman V, eds. Visions in Mathematics (Part of the Modern Birkhäuser Classics). Basel:Birkhäuser Verlag, 2010.[doi:10.1007/978-3-0346-0422-2_4]
    [21] Holden H, Piene R. The Abel Prize 2003-2007:The First Five Years. New York:Springer-Verlag, 2010.
    [22] Yu WS, Sun TY, Fu YS. Machine Proof System of Axiomatic Set Theory. Beijing:Science Press, 2020(in Chinese).
    [23] Yu WS, Fu YS, Guo LQ. Machine Proof System of Foundations of Analysis. Beijing:Science Press, 2022(in Chinese).
    [24] Zeng ZB, Wang JL, Yang ZF, Xiao LYH. A mechanical proof of the C.T. Yang's Theorem related to property of derived sets in general topology. Scientia Sinica Mathematica, 2021, 51(1):257-288(in Chinese with English abstract).
    [25] Kelley JL. General Topology. New York:Springer-Verlag, 1955.
    [26] Han G. The historical study of two important theories in topology[Ph.D. Thesis]. Huhehaote:Inner Mongolia Normal University, 2016(in Chinese with English abstract).
    [27] Pu BM, Liu YM. Fuzzy topology. I. Neighborhood structure of a fuzzy point and Moore-Smith convergence. Journal of Mathematical Analysis and Applications, 1980, 76(2):571-599. https://doi.org/10.1016/0022-247X (80)90048-7
    [28] Liu YM, Luo MK. Fuzzy topology. In:Advances in Fuzzy Systems-Applications and Theory, 9. World Scientific, 1998. https://doi.org/10.1142/3281
    [29] Wang GJ. Theory of L-fuzzy Topological Space. Xi'an:Shaanxi Normal University Press, 1988(in Chinese).
    [30] Huang Y, Luo MK. The l-accumulation point and w-accumulation point in L-fuzzy topological spaces. Journal of Sichuan University (Natural Science Edition), 2004(5):940-947(in Chinese with English abstract).
    [31] Ji ZF, Wang RY, Shuang L. C.T.Yang's Theorem in L-fuzzy topology spaces. Journal of Mathematical Research and Exposition, 2003(1):182-184(in Chinese with English abstract).
    [32] Zou XF. The Generalization s of C.T.Yang's Theorem in L-fuzzifying topological spaces. Fuzzy Systems and Mathematics, 2009, 23(2):59-63(in Chinese with English abstract).
    [33] Wang JL. Mechanization of general topology and related problems in automatic deduction based on Isabelle[Ph.D. Thesis]. Shanghai:East China Normal University, 2012(in Chinese with English abstract).
    [34] Schepler D. Topology:General topology in Coq. 2011. https://github.com/coq-community/topology
    [35] Wang SY. FormalMath:A side project about formalization of mathematics (Topology). 2021. https://github.com/txyyss/FormalMath/tree/master/Topology
    [36] Hölzl J, Immler F, Huffman B. Type classes and filters for mathematical analysis in Isabelle/HOL. In:Blazy S, Paulin-Mohring C, Picharidie D, eds. Proc. of the Interactive Theorem Proving. LNCS 7998, Rennes:Springer-Verlag, 2013. 279-294.
    [37] Gammie P, Gioiosa G. The Kuratowski closure-complement theorem. Archive of Formal Proofs. 2017. https://www.isa-afp.org/entries/Kuratowski_Closure_Complement.html
    [38] Friedrich S. The topology of lazy lists. In:Archive of Formal Proofs. 2004. https://www.isa-afp.org/entries/Topology.html
    [39] Enderton HB. Elements of Set Theory. New York:Spring-Verlag, 1977.
    [40] Zhang QP. Set-theory:Coq encoding of ZFC and formalization of the textbook elements of set theory. https://github.com/choukh/Set-Theory
    [41] Xiong JC. Set-theoretical Topology Lecture. 4th ed., Beijing:Higher Education Press, 2011(in Chinese).
    附中文参考文献:
    [15] 郭礼权,付尧顺,郁文生.基于Coq的第三代微积分机器证明系统.中国科学:数学, 2021, 51(1):115-136.
    [17] 陈钢.形式化数学和证明工程.中国计算机学会通讯, 2016, 12(9):40-44.
    [22] 郁文生,孙天宇,付尧顺.公理化集合论机器证明系统.北京:科学出版社, 2020.
    [23] 郁文生,付尧顺,郭礼权.分析基础机器证明系统.北京:科学出版社, 2022.
    [24] 曾振柄,王建林,杨争峰,小林英恒.点集拓扑学之杨忠道定理的一个机械化证明.中国科学:数学, 2021, 51(1):257-288.
    [26] 韩刚.拓扑学中两个重要定理的历史研究[博士学位论文].呼和浩特:内蒙古师范大学, 2016.
    [29] 王国俊. L-fuzzy拓扑空间论.西安:陕西师范大学出版社, 1988.
    [30] 黄勇,罗懋康. L-fuzzy拓扑空间中的l-聚点和w-聚点.四川大学学报(自然科学版), 2004(5):940-947.
    [31] 吉智方,王瑞英,双龙. L-fuzzy拓扑空间中的杨忠道定理.数学研究与评论, 2003(1):182-184.
    [32] 邹祥福.杨忠道定理在L-不分明化拓扑中的推广.模糊系统与数学, 2009, 23(2):59-63.
    [33] 王建林.基于Isabelle平台的一般拓扑学机械化及自动定理证明研究[博士学位论文].上海:华东师范大学, 2012.
    [41] 熊金城.点集拓扑讲义.第4版,北京:高等教育出版社, 2011.
    Related
    Cited by
Get Citation

严升,郁文生,付尧顺.基于Coq的杨忠道定理形式化证明.软件学报,2022,33(6):2208-2223

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 05,2021
  • Revised:October 14,2021
  • Online: January 28,2022
  • Published: June 06,2022
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063