针对教学场景的ZFC集合论Coq形式化.pdf

软件学报 ISSN 1000-9825,CODEN RUXUEW E-mail: Journal of Software,2023,34(8):35493573 doi:10.13328/ki.jos.006868 http:/ 中国科学院软件研究所版权所有.Tel:[phone] 针对教学场景的 ZFC 集合论 Coq 形式化 万新熠,徐 轲,曹钦翔(上海交通大学 电子信息与电气工程学院,上海 200240)通信作者:曹钦翔,E-mail: 摘 要:离散数学是计算机类专业的基础课程之一,命题逻辑、一阶逻辑与公理集合论是其重要组成部分.教学实践表明,初学者准确理解语法、语义、推理系统等抽象概念是有一定难度的.近年来,已有一些学者开始在教学中引入交互式定理证明工具,以帮助学生构造形式化证明,更透彻地理解逻辑系统.然而,现有的定理证明器有较高上手门槛,直接使用会增加学生的学习负担.鉴于此,在Coq 中开发了针对教学场景的 ZFC 公理集合论证明器.首先,形式化了一阶逻辑推理系统和 ZFC 公理集合论;之后,开发了数条自动化推理规则证明策略.学生可以在与教科书风格相同的简洁证明环境中使用自动化证明策略完成定理的形式化证明.该工具被用在了大一新生离散数学课程的教学中,没有定理证明经验的学生使用该工具可以快速完成数学归纳法和皮亚诺算术系统等定理的形式化证明,验证了该工具的实际效果.关键词:Coq;ZFC 公理集合论;一阶逻辑 中图法分类号:TP311 中文引用格式:万新熠,徐轲,曹钦翔.针对教学场景的 ZFC 集合论 Coq 形式化.软件学报,2023,34(8):35493573.http:/ 英文引用格式:Wan XY,Xu K,Cao QX.Coq Formalization of ZFC Set Theory for Teaching Scenarios.Ruan Jian Xue Bao/Journal of Software,2023,34(8):35493573(in Chinese).http:/ Coq Formalization of ZFC Set Theory for Teaching Scenarios WAN Xin-Yi,XU Ke,CAO Qin-Xiang(School of Electronic Information and Electrical Engineering,Shanghai Jiao Tong University,Shanghai 200240,China)Abstract:Discrete mathematics is one of the foundation courses of computer science,whose components include propositional logic,first-order logic and axiomatic set theory.Teaching practice shows that it is difficult for beginners to accurately understand abstract concepts such as syntax,semantics and deduction system.In recent years,some scholars have begun to introduce interactive theorem provers into teaching to help students construct formal proofs so that they can understand logical systems more thoroughly.However,existing theorem provers have a high threshold for getting started,directly employing these tools will increase students learning burden.To address this problem,this study proposes a ZFC axiomatic set theory prover developed in Coq for teaching scenarios.First-order deduction system and ZFC axiomatic set theory are formalized,then several automated reasoning tactics are developed.Students can utilize these tactics to reason formally in a concise,textbook-style proving environment.This tool has been introduced into the discrete mathematics course for freshmen.Students with no prior theorem proving experience can exploit this tool to quickly construct formal proofs of theorems like mathematical induction and Peano arithmetic system,which verifies the practical effect of this tool.Key words:Coq;ZFC axiomatic set theory;first-order logic 近些年来,数学定理的形式化证明得到了广泛的发展和研究.定理证明工具如 Coq1,Isabelle2,Mizar3,Lean4等逐渐趋向成熟,基于这些工具,大量数学定理的证明得到了形式化,包括著名的四色定理5、哥德 本文由“约束求解与定理证明”专题特约编辑蔡少伟研究员、陈振邦教授、王戟研究员、詹博华副研究员、赵永望教授推荐.收稿时间:2022-09-05;修改时间:2022-10-13;采用时间:2022-12-14;jos 在线出版时间:2022-12-30 3550 软件学报 2023 年第 34 卷第 8 期 尔不完全性定理6、Cauchy-Schwarz 不等式等.菲尔兹奖得主 Gowers 认为,计算机将在定理证明中起到关键作用,并将改变理论数学未来的研究模式7.Hanna 和 Yan8指出:定理证明器不仅可以帮助数学家进行理论研究,还能够改变面向数理逻辑初学者的教学方式.在我国高校计算机类专业的本科课程设置中,大多数高校院所都将离散数学课程设置为基础类必修课.而命题逻辑、一阶逻辑与公理集合论是离散数学课程的重要组成部分.教学实践中发现:初学数理逻辑的本科学生要学习并明晰语法、语义、推理系统等抽象概念是有一定难度的;同时,学生在学习使用一阶逻辑与公理集合论描述数学命题与数学证明时也往往难以通过具体的例子形成直观理解.在教学中引入交互式定理证明器有望改善这一问题,计算机辅助的自动检查能够及时准确地反馈学生写的命题是否具有正确的语法、是否遵循逻辑系统的推理规则等情况,帮助学生构造一个正确且严格的证明,而无需等待助教可能长达数周的反馈.交互式定理证明器实时交互的特点,也能够让学生动态地看到推理过程,有助于加深对逻辑系统的理解.近年来,国际上越来越多的学者开始在数理逻辑课程,特别是计算机专业的相关课程中引入定理证明工具来辅助教学.例如:牛津大学开发了 Jape 用于谓词逻辑的教学9,Cezary 和 Freek 基于 Coq 开发了在线教学工具 ProofWeb10,Avigad 使用 Lean 进行一阶逻辑和集合论的概念的教学11.然而,以上工作大都使用了定理证明器的内置逻辑,这在教学中会有很多缺陷.(1)大部分定理证明工具如 Coq 采用了“自底向上”的反向证明模式,用户不断应用证明策略将待证目标分解为一系列子目标,最终得到所有子目标均为前提完成证明.而常用证明模式还包括从前提推导出新条件最终得出待证目标的正向推理;(2)学生应当根据当前学习的逻辑系统的推理规则进行推理,而不是使用定理证明器中内置的逻辑,偏离教学目标;(3)直接使用定理证明器进行证明更像是学习一门编程语言,学生需要额外付出大量时间熟悉操作该特定定理证明器的命令,不仅增加学习成本,而且容易忽视逻辑系统本身;(4)由于仅提供了基本的证明策略,证明代码通常十分冗长,较大的工作量限制了学生完成更加复杂定理的形式化证明;(5)缺乏简洁的教科书风格的符号系统,不利于学生理解.简而言之,以辅助数学理论研究为目的开发的定理证明工具具有较高的上手门槛,在形式上与教科书中的逻辑系统差别较大,简单地直接引入教学中反而可能会加大学习成本,甚至使学生将定理证明器的内置逻辑与他正在学习的逻辑系统相混淆.考虑到这些问题,部分学者没有使用定理证明器,转而使用编程语言从头开发专用于教学的简易证明工具.Breitner12开发了 Incredible Proof Machine12,学生在可视化界面中使用鼠标将代表命题和一阶逻辑推理规则的方块连接起来就可以构造证明.Lerner 等人提出了 Polymorprphic block13可视化界面,学生可以采用类似于拼拼图的方式将命题和推理块连接起来,完成自然演绎系统的推理.这些工具能够提供交互更简便、趣味性更强的体验,但从头开发需要极大的工作量.现有的交互式定理证明工具已经提供了完善的用户界面,包括证明界面、证明状态和错误信息,基于定理证明器开发教学工具能够极大减少开发成本,例如,本工作仅花费了 2 300 行 Coq 代码,在教学中是更为实际的选项;同时,针对不同教学场景进行调整也更加简便.作为辅助逻辑学习的工具,需要降低定理证明器中的形式化证明与教科书中逻辑系统证明间的差距,使学生专注于他所学习的逻辑系统而非定理证明器的使用技巧.一款合格的基于定理证明概念的教学工具应当具有以下特点.(1)支持的推理模式应当与传统逻辑教材中使用的推理模式相同;(2)使用与教学内容相同的逻辑系统,所有操作都基于该系统的推理规则,尽可能少地暴露定理证明器的内置逻辑.此外,应当使用教科书上的逻辑术语和符号,而非定理证明器中新创建的变量名;(3)只需要简单的几条指令就可以完成证明,降低学生使用定理证明器的学习成本.这几条证明指令需 万新熠 等:针对教学场景的 ZFC 集合论 Coq 形式化 3551 要具有较高的自动化程度,从而减少代码量,帮助学生完成更复杂命题的严格证明.针对上述问题,本文在 Coq 中开发了一个包含自动化证明策略的 ZFC 公理集合论证明器,用于辅助一阶逻辑和公理集合论的教学.本文在 Coq 中从抽象语法树开始形式化了基于一阶逻辑的 ZFC 公理集合论,采用sequent calculus 式的逻辑系统,并利用 notation 机制提供了简洁的符号.我们开发了数条自动化证明策略以简化证明过程,包括命题逻辑自动证明指令 FOL_Tauto,该指令将可证问题转化为合取范式的布尔可满足性问题,并调用我们在Coq中实现的DPLL可满足性求解器自动求解,实现了逻辑连接词的完全自动化处理.对于量词推理规则,我们分别开发了指令以支持多层量词的同时引入和消去;对等号替换规则开发了指令peq_sub_tac 自动替换命题中的一阶逻辑项.以上所有指令均能自动处理-等价,且采用了与教材相同的正向推理模式.通过以上方法,我们构造了一个简洁快速的集合论证明环境,隐藏了 Coq本身的诸多细节,更贴近教科书风格的证明且更加自动化.学生使用该工具进行集合论定理的证明相比直接使用现有的定理证明器更为容易.图 1 给出了一个证明示例,两个集合的交集必然是其中一个集合的子集.(a)证明代码 (b)最后一步之前的 Coq 证明状态栏 图 1 ZFC 集合论证明器证明环境示例 我们在离散数学课程的实际教学中引入了该工具,并取得了良好效果.作为课程项目之一,学生需要使用该证明器完成数学归纳法的证明.实践表明,首次接触一阶逻辑和公理集合论的大一新生经过简单学习后就可以完成该定理的形式化证明.较为优秀的学生可以在完成离散数学课程后,利用该工具进一步构造皮亚诺算术系统并证明了加法和乘法的相关性质,体现了该工具的简洁性和有效性.本文第 1节介绍研究背景,包括 Coq交互式定理证明器和基于定理证明器的逻辑教学工具研究现状.第 2节阐述 ZFC 集合论证明器的设计框架.第 3 节给出对 ZFC 公理集合论的形式化.第 4 节介绍自动证明策略的实现.第 5 节展示我们在离散数学课程教学中引入该证明器的实际效果.最后总结全文.1 研究背景 1.1 基于定理证明器的逻辑教学工具研究现状 引入定理证明器辅助教学的主要问题在于:定理证明器在形式上与教科书中的逻辑系统有较大差距,如何缩小这一差距成为主要研究方向.一种思路试图在证明形式上逐渐使定理证明器的代码证明向教科书证明靠拢.Bhne 等人14在 Coq 中为每一条推理规则提供了一条证明指令,要求学生首先在 Coq 中完成命题的证明,之后在每一行证明代码前后通过注释写出此时对应的待证一阶逻辑命题,最后要求学生根据 Coq 证明写出与其结构相同的、教科书风格的纸笔证明,这样的证明具有与 Coq 相同的反向推理模式.实践表明,学生能够完成并理解 Coq 中的证明与逻辑系统之间的对应关系.Avigad11使用 Lean 的内置逻辑进行一阶逻辑和集合论的教学,并让学生比较理解证明代码和纸笔证明.在系统学习 Lean 的使用方法后,学生也能够成功完成证明.另一种思路试图直接开发与教科书风格更相近的定理证明工具.早在 20 世纪末,牛津大学开发的 Jape9就提供了良好的可视化界面,可以将证明显示成树状或盒状的形式.受此启发,Kaliszyk 等人基于 Coq 开发了ProofWeb10,其采用了 Gentzen风格的自然演绎系统,并提供了轻量化的在线 GUI,学生同样通过应用每一条推理规则对应的指令自底向上进行证明.Theorem intersect_subset1:ZF?u,v,uvu.Proof.pose proof Intersection_iff.universal instantiation H,u,v,z.assert ZF?zuvzu by FOL_Tauto.universal generalization H1,u,v,z.The conclusion is already proved.Qed.1 subgoal H:ZF?x,y,z,zxyzxzy H0:ZF?zuvzuzv H1:ZF?zuvzu H2:ZF?u,v,z,zuvzu _(1/1)ZF?u,v,uvu 3552 软件学报 2023 年第 34 卷第 8 期 国内的集合论相关研究大多关注重要集合论定理的形式化,如杨忠道定理15、Tukey 引理16等,目前,对定理证明在教学中的应用研究较少,且都处于讨论和探索阶段.李沁17探讨了在计算机专业的数理逻辑课程中使用 Isabelle 辅助教学的可行性,江南等人18则比较了慕尼黑工业大学与国内高校有关逻辑与验证相关课程的开设情况,并呼吁计算机专业的理论课程和实践教学中需要设置更多的定理证明相关内容.据我们所知,本文是国内首次将交互式定理证明实际应用在面对数理逻辑初学者的课堂教学中.1.2 Coq交互式定理证明器 Coq 是一个交互式定理证明工具,具有强大的表达能力和优秀的扩展性,是国际上主流的证明助手之一,在数理逻辑、算法和高可靠性软件的形式化验证方面得到了广泛应用.Coq 的理论基础是归纳构造演算,为用户提供归纳类型,比大多数函数式编程语言中的归纳类型更具表达力.用户可以在 Coq 中形式化定义数学概念、程序语言、逻辑系统等,并证明相关的性质和定理.在证明时,用户首先通过 Proof 指令开始证明,之后,应用一系列证明策略与 Coq 进行交互,证明策略会根据当前证明状态以及已经得到证明的定理、公理等将待证目标分解为数个更简单的子目标或者直接证明目标,而 Coq 证明检查器中的类型检查算法会根据归纳构造演算的性质机械化地进行检查.证明完成后,用户运行 Qed 指令退出证明.表 1 列出了 Coq 中的一些常用证明策略及其功能.表 1 Coq 常用证明策略 Coq 证明策略功能 intros 引入待证目标中的条件 destruct 根据构造子进行分类讨论 induction 根据构造子进行结构归纳 apply 对待证目标应用一个假设或已证定理 eapply 应用时无需指定变元,推迟变元的实例化 pose proof 在条件中引入一个已证定理 assert 声明一个新的待证目标 assert by 声明新待证目标并由 by 后的策略直接解决rewrite 根据等式重写 congreunce 等式重写自动证明策略 reflexivity 自动比较待证目标等号两侧是否相同 tauto 直觉逻辑自动证明策略 Coq 允许用户通过 Ltac 语言组合现有的证明策略构成新策略,简化证明过程,提高证明的自动化程度.本文所开发的自动证明策略就依赖 Ltac 语言实现,学生在使用中不需要学习 Coq 自带的证明指令语言,而只需要使用本文所开发的 7 条自动证明指令,其中一条与分离公理相关的证明策略没有出现在课程项目中,本文不做介绍.2 公理集合论证明器的设计框架 介绍 ZFC 定理证明器的实现框架之前,需要特别说明,该定理证明器是针对特定的数理逻辑教学场景开发的.教学的对象是已经掌握了命题逻辑的学生,并且当前阶段的教学重点是 sequent calclulus 式的逻辑系统中的 4 条量词推理规则以及 ZFC 公理集合论与日常数学之间的联系.因此,我们形式化 ZFC 公理集合论时采用了与教材相同的 sequent calculus 系统,开发证明策略时,将所有命题逻辑相关的证明完全自动化地集成在了证明策略 FOL_Tauto 中,而为每一条量词推理规则提供了单独的证明策略.此外,我们引入了符号二元交、二元并、单元集作为一阶逻辑中的函数符号以及空集作为常量符号.通常,教材中的 ZFC 集合论并不包含这些符号,但引入这些符号不会改变整个推理系统的可靠性,具体证明可见教材19.尽管该定理证明工具在 Coq 中实现,但本文目标是提供一个教学用的定理证明工具而非被验证的证明器,因此我们未验证其中涉及到的求解器等模块的正确性.该证明器的设计分为两个部分:ZFC 公理集合论的形式化和交互式定理证明环境.两部分均在 Coq 中实现,详情如图 2 所示.万新熠 等:针对教学场景的 ZFC 集合论 Coq 形式化 3553 图 2 ZFC 集合论证明器设计框架 第 1 部分在 Coq 中形式化定义 ZFC 公理集合论的相关概念,构造可靠的推理系统,包含以下 4 个方面.(1)显式变量名库 StringName.我们没有使用 Coq 内置的变量名系统,而是基于 Coq 原有的 String 字符串库为该推理系统专门开发了显式变量名库 StringName.该库允许我们对变量名有更好的控制,可以自行定义新变量名的引入、变量名的比较等方法,有利于之后对替换、-等价等语法操作的自动化.此外,从基于字符串的抽象语法树开始形式化逻辑系统,还能够避免在证明环境中暴露 Coq 的内置逻辑.如图 1(b)所示:我们的证明环境中只会显示一系列命题可证的条件,而不会有形如x:String 的条件,证明开始时,也无需对各个变量进行 intros 引入操作,保持与教科书风格证明高度一致;(2)一阶逻辑命题.一阶逻辑的研究对象是一阶逻辑命题,需要在 Coq 中对命题和项进行形式化;(3)ZFC 集合论推理系统.本文的推理系统采用与教材中相同的 sequent calculus 逻辑系统,证明过程中的每一步都由多个前提和一个结论组成.推理系统只涉及语法结构,因此,本文仅形式化了可证性质 derivable,没有形式化该系统的语义;(4)符号系统.定理证明器的证明代码通常可读性较差,不易于学生理解,Coq 的 notation 机制能够很好地解决这一问题.例如:实质蕴涵的形式化定义为PImpl P Q,若定义 Notation“P1P2”:=(PImpl P1 P2),之后的证明中就可以将其简写为“PQ”.第 2 部分为交互式定理证明环境,待证定理由之前形式化的命题构成.用户使用我们提供的自动证明策略,决定如何应用推理规则.本文开发的指令全部采用与教材相同的正向推理模式,每当用户成功应用一条指令,证明环境中就会根据当前的条件加入由推理规则产生的新推导关系.当结论可以通过现有前提进行命题逻辑推理得到时,用户最后调用 The conclusion is already proved 指令(FOL_Tauto 的别名,用于结束证明)来完成定理的证明.用户无需除了 pose proof 外的任何 Coq 内置证明策略,自动证明策略的具体实现在第 4 节中详细阐述.3 ZFC 集合论的形式化 3.1 显式变量名库 利用 Coq 中的模块机制,我们首先实现了命名系统模块 NAME_SYSTEM_EXT,该模组接受如表 2 所示的参数.基于这些参数,可以进一步定义其他 Coq 函数并证明相关性质.定义根据名字列表引入新名字的函数 list_new_name,返回列表中最大名字的下一个名字.Definition list_new_name(xs:list t):=next_name(list_max xs).交互式定理证明环境 ZFC 集合论的形式化 变量名库 一阶逻辑命题 推理系统 符号系统 待证目标 自动化证明策略 量词策略等号替换策略命题逻辑自动策略 FOL_Tauto 合取范式生成和可满足性求解 3554 软件学报 2023 年第 34 卷第 8 期 表 2 NAME_SYSTEM_EXT 模块参数 参数及需要满足的性质 描述 t:Type 名字的类型 max:ttt 比较并返回较大名字的函数 next_name:tt 返回输入的下一个名字 le:ttProp 小于等于二元关系 default:t 默认名字 eq_dec:v1,v2:t,v1=v2+v1v2 名字具有可比性,要么相同要么不同 Transitive le 小于等于关系具有传递性 u,v,le u,vu next_name v 任何名字的下一个名字都比自身大 v1,v2,le v1(max v1,v2)max 函数正确性 1,比第 1 个参数大 v1,v2,le v2(max v1,v2)max 函数正确性 2,比第 2 个参数大 v1,v2,max v1,v2=max v2,v1 max 函数交换律 v1,v2,v3,max v1(max v2,v3)=max(max v1,v2)v3max 函数结合律 实际使用时,只需要实例化表 2 中的各项参数,并证明实例化后的类型和函数满足表 2 中的性质,就可以得到用户指定类型的命名系统模块.我们将参数 t 实例化为 String 库中的 string 类型,max 和 le 使用字符串的字典序,next_name 实例化为在输入字符串后加上后缀“”,default 实例化为字符串“x”,得到字符串模块StringName.上述类型符合表 2 性质的证明并非本文关键,此处不列出.在后续开发中,会以不同的名字引用 StringName 库作不同用途.在推理系统中,令 V:=StringName,使用V.t 作命题中变量名的类型;而在 DPLL 求解器中,令 PV:=StringName,使用 ident:=PV.t 作为命题变元的类型.虽然两者本质上均为字符串类型,但采用不同名称以避免混淆.此外,我们为常用字符串分配了 Coq 内置变量名,例如:Definition x:=EVAL“x”%string;Definition x0:=EVAL(V.next_name x).这样,在证明环境中就会直接显示 x 等字母而非带引号的字符串,x 的下一个名字也可以依次显示为 x0,x1,x2,如图 1 所示.3.2 命题及其相关性质的形式化 一阶逻辑的基本研究对象是一阶逻辑项,在 ZFC 公理集合论中,项代表一个集合,归纳定义如下:t:=|x|t|t1t2|t1t2(1)表示空集常量,x 为变量,t表示单元集,和分别为二元交和二元并.使用 Coq 的 Inductive 关键字,项的形式化定义 term 为:1.Inductive term:=;2.|var(v:V.t)|empty_set|singleton(x:term)|union(x y:term)|intersection(x y:term),其中,empty_set 构造子对应空集常量,var 构造子对应字符串表示的变量,singleton 对应单元集,union 和intersection 对应二元并和二元交.之后,使用 notation 进行如下简写,使 Coq 中的符号与式(1)一致.为保证所作符号不与 Coq 内置的符号冲突,新定义的命题符号只在双括号“”内有效.1.Notation“e”:=e(at level0,e custom set at level99);2.Notation“”:=empty_set(in custom set at level5,no associativity);3.Notation“xy”:=(intersection x y)(in custom set at level11,left associativity).其余简写方式类似.命题的归纳定义为 P:=t1=t2|t1t2|?|P|P1P2|P1P2|P1P2|P1P2|x,P|x,P(2)其中,t1=t2和 t1t2为原子命题,表示集合的相等和属于关系;?和分别表示真命题和假命题;其余构造子分 别对应取否、合取、析取、实质蕴涵、当且仅当、全称量词和存在量词.命题的形式化定义 prop 如下.1.Inductive prop:Type:=;万新熠 等:针对教学场景的 ZFC 集合论 Coq 形式化 3555 2.|PEq(t1 t2:term)|PRel(t1 t2:term)|PFalse|PTrue;3.|PNot(P:prop)|PAnd(P Q:prop)|POr(P Q:prop)|PImpl(P Q:prop)|PIff(P Q:prop);4.|PForall(x:V.t)(P:prop)|PExists(x:V.t)(P:prop).在 Coq 中,同样可以使用 notation 给出与式(2)相同的记号.接下来给出对命题中自由变元进行替换的方法,定义替换目标为变量名和项的有序对构成的列表,记录每一个变量要被替换成的项,对命题 P 作替换的结果记作 P:121212121212:;.:;:():():():(,ttPPxxx xttx ytxttttttPPx=?):,if()(,):,;,if()Px PxVx Pu P xuxV=?对项作替换时,空集常量在替换前后不变,变量x会从头依次比较替换目标中直到找到x对应的项t,否则不会替换,单元集和二元交并分别替换子项.对命题作替换时类似,值得关注的是量词的情况,此时需要检查被量词绑定的变量是否在替换目标中出现:若没有出现,继续替换子命题;否则,需要引入一个当前环境 中没有的新变量u,并将x?u加入替换目标前,将子命题P中的x先替换成u以避免冲突.以下列出其形式化 定义prop_sub关键的量词部分,subst_task_occur判断名字在替换目标中出现的次数,函数new_var负责引入新变量名,其定义基于第3.1节中的list_new_name.1.Fixpoint prop_sub(st:subst_task)(d:prop):prop:=2.match d with 3.|x,Pmatch subst_task_occur x st with 4.|OPForall x(prop_sub st P)5.|_let x:=new_var P st in 6.PForall x(prop_sub(cons(x,var x)st)P)7.end 8.|9.end.命题的另一重要语法性质是-等价,它描述了对量词绑定变量的重命名,如x,x=x和y,y=y,-等价的 命题具有相同的语义.-等价的定义通常被描述为多次对量词绑定变量的重命名,即x,P=y,Px?y,但 基于替换的定义不利于自动化,本文提出了一种带环境的、不依赖替换的归纳定义.环境是一个三元组列表:=|(u,v,b);(3)其中,u,v为变量名,记录两个命题中被量词约束的变量的对应关系;b是布尔值,true表示该对应关系当前有效,false表示该对应已被新对应覆盖,因此无效.环境记录了两个命题自顶向下检查量词对应关系时经过的路径,以下先给出一阶逻辑项的带环境-等价=的部分归纳定义:12341324(,true),(),.u vsVABindAFtt ttAAuvssttetrte=A规则表示在任何环境下,空集都只与自身等价;ABind规则处理约束变量,如果u和v在环境中存在有效对应,则u与v等价;AFree规则处理自由变量,如果变量s不在环境中,那么该变量自由出现,只能和自身等价;二元交判断子项是否各自等价;单元集和二元并的情况类似.3556 软件学报 2023年第34卷第8期 基于项的-等价,可以给出命题的带环境-等价,以下为部分典型规则:(,true);(,)1234112213241212,.,x yx yPQtAt ttPQ PQAAttAttx Py QPPQQ=?量词对应的规则是唯一会修改环境的规则,在自顶向下的检查过程中,若遇到x,P和y,Q,此时有P中的x与Q中的y对应,因此需要将(x,y,true)记录到环境中再检查子命题,而中原先左侧为x或右侧为y的记录(相当于外层量词的对应)在子命题P不再有效,需要置为false,用(x,y)表示.在最外层环境为空,可以自然得到原始-等价的定义P=Q:=P=Q.容易看出,这一过程是可判定的,Coq中将判定-等价的过程形式化为返回布尔值的递归函数alpha_eq,以便于自动计算.1.Fixpoint alpha_eq(l:binder_list)(P Q:prop):bool:=2.match P,Q with 3.|t1t2,t3t4term_alpha_eq l t1 t3&term_alpha_eq l t2 t4 4.|P1P2,Q1Q2alpha_eq l P1 Q1&alpha_eq l P2 Q2 5.|x,P1,y,Q1alpha_eq(x,y,true):(update x y l)P1 Q1 6.|7.|_,_false 8.end.9.Definition aeq(P Q:prop):bool:=alpha_eq nil P Q.3.3 推理系统的形式化 推理系统采用sequent calculus形式的逻辑系统,证明中的每一步是一个命题序列1 2n,其中,前n 个命题为前提,末尾的命题为结论,记作1 2n?.之后,使用表示命题序列,表示命题,?表示在命 题序列后增加命题构成新的命题序列.推理规则描述了证明过程中的一步,它接受多个条件并得到一个新的公式序列作为结论.本文采用的推理规则全部来自实际教学中使用的逻辑教材19,此处选择性列出一部分,包括:有关逻辑连接词的推理规则:,;IntroContraCongruenceAssuWeakenPQPQPQPPQModusPQPQPPQPPPPQ =?有关量词的4条推理规则,其中,FV()表示命题中所有自由出现的变量构成的集合:,(),()(),;,ElimIntroIntroElimx PP xtxFVPP xtx Px PxFVFV QxPQx PQ?有关等号的推理规则:,;ReflSubsttttxttP xtP=?ZFC集合论公理:,(,)()(),;,(),x xx yz zxzyxyxFV PFV PInfiniEmptyExtensiontySeparationxxaliyyxyyxxyz zyztyyxP=?集合相关符号的公理:万新熠 等:针对教学场景的ZFC集合论Coq形式化 3557 ,se.,c Singletonzxyzxzyx y yxUnionx y zIntertionyxx y z zxyzxzy=?在Coq中,将前提和结论构成的公式序列分开进行形式化,结论命题即为上一节中的prop类型,前提定义为context:=propProp类型,即命题的集合.之后,可以进一步定义不包含任何命题的空前提,简写为ZF;以及在前提后加入新命题的方法,简写为;.1.Definition empty_context:context:=fun_False;2.Notation“ZF”:=empty_context(in custom set at level20);3.Notation“Phi;x”:=(Union_Phi(Singleton_x)(in custom set at level31,left associativity).使用Inductive关键字,可以形式化地归纳定义上述推理规则,得到可证关系derivable,其类型为contextpropProp,“derivable?”即形式化地表示一阶逻辑命题可由前提经过推理规则推导得到.在 Coq中,将derivable简记为?:Notation“Phi?P”:=(derivable Phi P)(in custom set at level41,no associativity).接下来,以Intro规则、外延公理和无穷公理展示derivable的形式化定义.(1)Intro规则可以形式化地表示为:1.|PAnd_intros:forall Phi P Q;2.derivable Phi P;3.derivable Phi Q;4.derivable Phi PQ.如果证明时Coq的前提条件中分别有P和Q能够从同一个前提Phi推导得到,那么可以进一步得到Phi能够推导出PQ.(2)外延公理可以形式化地表示为|Extensionality:derivable empty_contextx,y,(z,zxzy)x=y.外延公理的形式化具有与教材中的公理完全相同的形式.我们直接将公理中的命题作为结论,此处x,y等变量名为第3.1节中已定义的字符串,因此,形式化时不需要通过forall来引入Coq中的变量.证明时,通 过pose proof Extensionality指令引入外延公理,Coq证明状态中就会直接加入新条件ZF?x,y,(z,zx zy)x=y.之后,可以应用消去全称量词的证明策略将x,y实例化成实际需要的项继续证明.(3)形式化无穷公理时,我们希望能将目标集合是归纳集这一命题简写成谓词的形式.定义带参数t的命题is_inductive_def为:Definition is_inductive_def(t:term):=(xy,(yxyyx)x?t,表示空集在集合t中,并且t中任意元素的后继都在集合t中.引入x?t的替换操作是为了在当参数 t为变量y时,利用替换将原命题中全称量词绑定的y重命名成其他变量,避免出现y,yyyyy的错误命题.之后,使用notation将is_inductive_def t在命题中简记为is_inductive t:Notation“is_inductive t”:=(is_inductive_def t)(in custom set at level20,t1 at level15,no associa