关系和演绎数据库的Coq形式化和Datalog的机械化斯特凡尼亚-加布里埃拉·邓布拉瓦引用此版本：斯特凡尼亚-加布里埃拉·邓布拉瓦。关系和演绎数据库的Coq形式化- 和数据记录的机械化。计算机科学中的逻辑[cs.LO]。巴黎萨克雷大学（COmUE），2016年。法语。NNT：2016年SACLS525。电话-01534575HAL ID：电话：01534575https://theses.hal.science/tel-01534575提交日期：2017年HAL是一个多学科的开放存取档案馆，用于存放和传播科学研究论文，无论它们是否被公开。论文可以来自法国或国外的教学和研究机构，也可以来自公共或私人研究中心。L’archive ouverte pluridisciplinaireLLH，kyReaA*Ga8k8-*Q/2 AL1，yjjy/KyRTtH？DSE/E/OCTORATE/ELlMBpERSBTöSARBS@ACLAvTRöTARöE£LlMBpERSBTöSARBS@am/学校/八年级83 y信息与通信科学与技术由Jme te7ania @：abriela Dumbrap关系和演绎数据库的Coq形式化- 和数据记录的机械化hèse Trésente etsupporté Prsav-星期五k de +10月kyRe曲线的位置，航空公司BE MxA FE M桑德琳·B·拉十五莎拉·C·O？M@BOM FBA尤夫人velyneCOMTEDEAMM. Mohand-Said>AC B/M. Mi chaël_mSBM或rBTC？南巴黎大学教授_ennes大学教授南巴黎大学副教授（>D_）研究员（Claude Bernard Lyon大学教授导演_审查主任审查员- -希特勒，关系和演绎数据库的Coq形式化- 和DatalogJots@+le7s，形式化方法、证明助手、逻辑、数据库在计算机科学的几个领域中，基于测试、形式化建模或验证的技术已经被成功地用于帮助程序员创建可靠的系统。例如，在处理器开发中，自动定理证明器在设计中的深层错误变成代价高昂的硅胶错误之前就能揭示它们然而，此外，当前的数据管理系统处理越来越多的数据量。这些数据非常宝贵，其可用性、完整性和可靠性对企业、科学家和公民至关重要。因此，重要的是通过确定这些系统本身是安全和可靠的来确保对这些特性的强有力的保证。为了实现这一目标，必须使用正式的方法和成熟一个非常有前途的方法是在过去的几年里，对程序的验证和认证进行了深入的研究，并产生了令人印象深刻的结果和可靠的软件。令人惊讶的是，尽管由数据引擎存储和操作的数据量已经增加，但是很少注意其中，关系管理系统是最广泛的。演绎系统为多种查询语言提供了一个统一的框架，并在语义网的上下文中重新出现。因此，这些观察证明了我们选择形式化关系模型以及演绎模型的合理性--仅限于Datalog的情况本文提出了一种基于Coq的数据库这提供了来自定义数据模型的两种不同方法的形式化规范：一种基于代数，另一种因此，本文的第一个贡献是开发了一个用于关系模型的它包含关系代数和合取查询的模型 它还包含完整性约束及其推理过程的机械化。我们对两种类型的依赖关系进行建模，这两种类型最常见的是：函数依赖关系和多值依赖关系及其相应的公理化我们形式化地证明了它们的推理算法的正确性这些类型的依赖关系是一般依赖关系的实例：相等生成依赖关系和元组生成依赖关系。我们对一般依赖关系及其推理过程进行建模，即"追逐"，我们为它最后，形式化地证明了数据库的主要定理，即第二个贡献是开发了作为这项工作的一部分，我们给出了标准Datalog引擎的第一个机械化，以及该库包括它们在模型理论中的语义的形式化，该库由相应的更正、终止和完整性证明补充在此背景下，我们还构建了一个初步的框架来推理分层程序。该平台为以数据为中心的应用程序的认证铺平希特尔，埃夫罗德，关系和演绎数据库的Coq形式化- 和数据记录形式化方法、证明助手、逻辑、数据库在许多计算领域，从测试到正式建模再到全面验证的技术已经被成功地用于帮助程序员创建可靠的系统。例如，在处理器开发中，自动化定理证明在设计中的深度错误成为硅中的成本错误之前就发现了它们;航空电子设备开发人员使用程序分析来验证在飞机上运行的嵌入式软件的关键安全特性;操作系统供应商已经成功地使用模型检查来消除设备驱动程序中的所有类别的错误。然而，直到最近，数据密集型管理系统在很大程度上抵制使用正式技术进行的分析。然而，当前的数据管理应用程序和系统涉及越来越大的数据量。它们是有价值的，它们的可用性、完整性和可靠性是公司、科学家和普通公民的金矿。由于保护数据完整性和可靠性非常重要，因此应确保管理此类数据的系统是安全和可靠的。获得强有力的保证需要使用正式的方法和成熟的工具。一种非常有前途的方法是使用证明助手。在过去的几十年里，程序验证和认证已经得到了广泛的研究，产生了非常令人印象深刻的结果和高度可靠的软件。令人惊讶的是，虽然数据引擎存储和管理的数据量急剧增加，但很少有人关注确保如此复杂的系统是可靠的。其中，关系数据库管理系统是分布最广的。此外，演绎系统代表了用于大量查询系统的统一框架，并且是在语义网的上下文中重新引起兴趣的主题。因此，这些观察促使我们选择专注于关系数据模型的形式化，以及仅限于数据记录片段的演绎模型。本文提出了一种基本数据库语言和算法的Coq形式化。它提供了两种不同方法的正式词干规范来定义数据库模型：基于关系和基于逻辑。因此，本文的第一个贡献是为关系模型开发了一个公鸡库。它包含关系代数和合取查询的形式化。它还包括完整性约束及其失效程序的机械化。我们建立了两种最常用的依赖关系模型：函数依赖关系和多值依赖关系，以及它们各自的公理。我们正式证明了它们的推理算法的合理性，对于函数依赖的情况，我们还证明了它们的完整性。这些类型的依赖关系是更一般的依赖关系的实例，即一般依赖关系：等式生成依赖关系和元组生成依赖关系。我们对一般依赖性及其推理过程进行建模，即"追逐"，为之建立健全性。最后，我们形式化地证明了基本数据库定理，即代数等价性、同构定理和合取查询的最小化第二个贡献是开发了一个用于逻辑编程的Coq/ssre反射库，仅限于Datalog。作为这项工作的一部分，我们提供了一个标准的数据记录引擎的第一个机械化，该库包含其模型理论语义的形式化，与定点1一起，通过分层评估过程实现。该库包含相应的声音、终止和完整性证明。在此背景下，我们构建了一个初步的框架，用于对分层程序进行推理。该平台为以数据为中心的应用程序的认证铺平了道路。vi内容。I.引言11. 预备课程21.1. 动机21.2. 最新技术水平41.2.1.关系数据库设置中的化41.2.2.演绎数据库设置4中的形式化1.3. 问题陈述41.4. 论文贡献52. 方法论72.1. COQ72.2. S反射82.2.1.Ssreflect战术82.2.2.图书馆概述112.3. 论文大纲13二.理论概述143. 一阶逻辑153.1. 语法153.2. 语义学183.3. 范式203.4. 推论214. 关系模型234.1. 数据表示234.2. 数据提取254.2.1.关系代数254.2.2.关系演算264.3. 数据完整性284.3.1.函数依赖关系的逻辑含义294.3.2.多值依赖关系的逻辑含义324.3.3.一般依赖关系的逻辑含义vii5. 标准Datalog405.1. 语法405.2. 语义学435.2.1.最小模型语义435.2.2.定点语义456. 带否定的数据库496.1. 语法496.2. 分层语义学506.2.1.半阳性Datalog506.2.2.逻辑结果516.2.3.程序分层526.2.4.迭代固定点模型556.3. 替代语义学566.3.1.完美模型语义学566.3.2.稳定的模型语义566.3.3.基础完善的模型语义学57III. 形式化概述587. 关系模型的形式化597.1. 数据表示597.1.1.属性、域、值597.1.2.元组617.1.3.关系、模式和实例627.2. 数据提取：查询语言637.2.1.关系查询637.2.2.连词查询697.2.3.从代数到合取查询757.3. 数据完整性777.3.1.函数依赖关系的逻辑含义777.3.2.多值依赖关系的逻辑含义7.3.3.一般依赖关系的逻辑含义817.4. 讨论847.4.1.捐款847.4.2.第85课8. 标准Datalog86的形式化8.1. 建模选择868.1.1.有限与无限域878.1.2.分离语法和语义对象888.1.3.模拟地球原子888.1.4.建模基础和替换89viii8.2. 语言表示918.2.1.程序签名918.2.2.地面原始人918.2.3.开放基元948.2.4.安全条件958.3. 语义表示968.3.1.地面968.3.2.替代品978.3.3.相关基础和替代1018.3.4.程序语义学1028.4. 自下而上的评估1038.4.1.匹配算法1038.4.2.构建前链操作员1058.5. 自下而上的评估属性1068.5.1.匹配特征1068.5.2.前向链特征化1138.6. 正引擎116的特性8.6.1.固定点属性1168.6.2.强烈的声音和完整性1198.7. 讨论1208.7.1.捐款1248.7.2.第124章第一次见面9. 使用否定形式化数据记录1259.1. 语言表示1259.1.1.语法1269.1.2.语义学1279.2. 正嵌入1279.2.1.语法方面1279.2.2.语义学方面1309.3. 分层1329.3.1.地层特征1329.3.2.穷尽性分层计算1349.3.3.切片表征1359.4. 分层评估1379.4.1.补充解释1379.4.2.可满足性保存1409.4.3.分层评估算法1419.5. 分层评估属性1429.5.1."积极"项目评价的属性9.5.2."负面"程序评估的属性9.6. "负"发动机146的特性9.6.1.强有力-分层程序评估的完整性。1469.6.2.计算模型149的极小性和唯一性ix9.7. 讨论1529.7.1.捐款1529.7.2.第152章第一次见面IV. 评估15310.结论15410.1. 评估15410.2. 经验教训15511.前景15811.1. 语言扩展15811.1.1. D与存在主义者的目录15811.1.2. DATALOG与Disjunction15811.1.3. 带更新的目录15911.2. 应用程序15911.2.1. 执行安全15911.2.2. 系统认证159x确认文件我非常感谢我的论文顾问Véronique Benzaken和Evelyne Contejean，感谢他们的洞察力引导我探索这个非常富有成效的主题。因此，我们的合作对我来说是一个独特的机会，可以在各种具有挑战性的研究领域取得进展。如果没有他们与我分享的技术专长，这是不可能的，无论是在数据库上还是在定理证明方面。在个人层面上，我非常感谢他们坚定不移的耐心，支持，并相信我有能力成为一名独立的研究人员。谢谢!我非常感谢Sandrine Blazy和Mohand-Saïd Hacid同意审查我的论文，并感谢他们提供的反馈。我还要感谢莎拉·科恩·布拉基亚和迈克尔·鲁西诺维奇成为我的辩护陪审团的一员。我也要感谢VALS团队的所有成员。在这样一个充满挑战和友好的环境中工作是一种乐趣。特别是，我想感谢克里斯汀·保林、西尔万·康雄和蒂博·巴拉邦斯基，我很高兴教他们上课。 我还要感谢我在南巴黎大学理学院和非常感谢我过去所有的办公室伙伴：保罗，凯瑟琳，大卫和海!你照亮了我的日子，在我安分守己的时候同情我，鼓励我去波斯，在你身边是一种乐趣。我非常感谢迈克尔·科尔哈斯和弗洛里安·拉贝是第一个鼓励我追求计算机科学研究的人。在KWARC集团的时间对我的职业生涯至关重要。我还要感谢我在DFKI的实习主管、Max Plank研究所的逻辑小组和Inria Sophia-Antipolis的Marelle我很幸运，在我的研究生学习期间，我有很棒的室友（谢谢你，亚历山德拉!）在塞纳河畔伊夫里（谢谢你，克拉拉，巴尔萨泽，马蒂厄，索尼娅和艾德琳!）如果没有几年前我的朋友们一次又一次地向我展示的爱，我就不会走到这一步。谢谢你（没有特别的顺序），莫妮卡，伊莎贝尔，艾瓦拉斯，马达利娜，科迪，雷切尔，安卡，安杰拉，克莱门特，埃琳娜，乔治，埃米利奥，阿拉丁，让巴蒂斯特，阿林，托马斯，阿莱克塔，阿斯玛，卢安娜，嘉布遣会。谢谢你，加布里埃尔，艾琳，安妮和丹尼斯!我感谢我的父母一直在我身边。我拥有你的一切。1第一部分简介21. 初步1.1. 动机本文描述了一个基本的形式化工作桥梁形式验证和数据库理论。在本节中，我们将概述最近的发展，从两个领域的分支，这激发了我们的努力。计算机已经变得无处不在，处理着越来越多的敏感数据。因此，我们比以往任何时候都更依赖于它们的正确功能。从飞机、太空探测器和火箭爆炸到导弹拦截失败、贸易中断和致命的医疗机械故障，历史上有多少故障导致了经济和人类灾难这种对强有力的保证的需要已经在形式化方法的使用中得到了证明，这些方法将数学和逻辑工具应用于软件的设计和实现。这些方法不仅被纳入了安全关键系统的官方标准，而且它们在开发成本效益高、低缺陷产品方面的无可争议的作用使它们成为主流。Indeed在研究和工业领域的应用领域不断扩大这些现在的范围从语言语义、编译器、操作系统和安全协议到铁路、汽车、核、航空航天和商业处理器中的嵌入式系统此外，这种方法的显著进步和改进甚至导致了它们的辅助数学推理，正如大型机器验证证明的发展所证明的那样。形式方法结合了建模和技术分析，喜欢语言和系统的规范、验证和形式规范（英语：Formal specifications）（formal这种强有力的描述可以作为设计指南，在某些情况下，还可以作为正式实现的直接基础，从而生成正确的构造代码。形式验证喜欢静态地确保特征属性，例如，声音、终止和完整性被动态地保存，即在执行时。由于通过形式静态分析详尽地寻找潜在运行时缺陷的不可判定性，已经开发了各种各样的近似解。根据它们的性质和范围，它们可以大致分为两种主要的互补方法：基于证明的（即演绎验证，实现工具依赖于自动定理证明器和半自动证明助手）和基于探索的（即模型检查，实现工具依赖于符号）。1. 初步3和边界模型检查算法。虽然每种技术都有其优点和回报，但基于证据的技术都特别适合我们的目的，因为它们的表现力和可扩展性更复杂。CO q证明助手通过其对高阶逻辑、证明脚本自动化和代码提取的支持，以及通过其在许多领域的成功使用，将其自身与现有的证明工具区分开来。基于Coq的突出项目导致了 认 证 的 编 译 器 和 操 作 系 统 ， 例 如 ， C omp C ert Verified C 编 译 器[16][17][53][54][55][56][57]（[85]）和用于云计算的C erti KOS验证内核（[44]），形式化编程框架，例如，命令式程序的YNOT环境（[64]）和用于密码学证明的C加密环境（[11]），机械化编程语言语义，例如JSC ert formal JavaScript语义（[18]）和C akeML-ML的实现（[51]），来自认证的终止工具，即C i ME/C八进制库（[26]），以及形式化的数学证明，例如，四色定理（[37]）和费特-汤普森（奇数阶）定理（[39]）。这些结果为设想将防说谎助手使用下的方法转移到广泛的软件工程领域因此，计算项目中的深度规范远征标志着所谓的深度规范科学的出现。这一新范式的目标是基于其规范的完全形式化的现实世界系统的原则性发展。DATACERT项目将自己定位在这一总体设置的框架内，并喜欢以数据为中心的系统的深度规范。它的部分目标是一方面提供关系数据库管理系统背后的理论基础的机制化，另一方面提供数据集成和交换系统背后的理论基础。根据这些目标中的一些，我们将我们的基础形式化工作指向关系和演绎数据库。主要动机如下。关系数据库长期以来一直是一种流行的存储解决方案，尤其是用于处理安全关键数据（如安全凭据、敏感用户信息、财务、医疗和法律记录）的系统。因此，在尊重机密性和完整性的情况下获得强有力的安全保证变得至关重要。演绎数据库，虽然在实践中比它们的关系对应物使用得少得多，但具有简单、纯粹的声明性和更具表达性的形式。在理论层面上，它为大量特定于应用程序的查询语言提供了一个通用的、统一的框架。更重要的是，它的主要指数[48]中给出了概述。··1. 初步41.2. 最新技术水平1.2.1. 关系数据库设置在这方面的第一次努力是由[41]在AGDA证明系统中进行的。本文研究了未命名关系模型的不同形式化，重点是数据定义和关系代数方面。最近，[60]的形式化提供了一个完全验证的、轻量级的单用户关系数据库系统的实现，该系统也是基于未命名的关系模型。作者证明其实现符合正式要求，所有证明均以书面形式编写并验证C O q的YNOT扩展（参见[22]）。 与这些作品相比，我们认为关系模型的命名版本，因为它是在真实系统中实现的，如ORACLE、DB2、POSTGRESQL或MICROSOFT ACCESS。此外，我们还涵盖了合取查询、优化技术和完整性约束方面。1.2.2. 演绎数据库设置中的形式化[49]的工作基于PROLOG的高阶抽象语法，提供了前向和后向、自上而下和自下而上语义的正确性和等价性的COq形式化关于我们在第8节中描述的形式化，它提供了与定点语义学相关的形式声音证明，它与我们的工作不同，因为它遵循抽象的解释视角。此外，虽然我们在语法方面不考虑函数符号，在语义方面不考虑向前、向后和自上而下的方法，但我们支持否定并设法建立正确性，以及自下而上的推理引擎所采用的底层算法的完整性属性。[83]1中介绍的工作在表达分布式安全策略的上下文中给出了标准DATALOG的CO q机械化开发包括语言编码、自下而上的评估和与可判定性相对应的证据在我们相应的C Oq/SSR反射形式化中，我们不需要显式地需要证明可判定性，因为我们小心地设置了我们的基类型，因此这个属性是自动推断的（参见第8章）。虽然我们还没有考虑到安全策略方面建模的相关部分，但相比之下，我们提供的结果范围更广。1.3. 问题陈述在数据库世界中常规和广泛使用的许多技术和算法要么没有形式化，要么经常没有得到充分的说明。尽管如此，我们正处于开发所需机器的门槛上，以纳入强大的保证COq认证规定。根据第1.1节中详述的原因，我们将其视为1http://www.cs.nott.ac.uk/types06/slides/NathanWhitehead.pdf1. 初步5我们要解决的问题。为此，我们认为这是一个至关重要的步骤，也是对基础块进行正式建模的一个重要步骤，这些基础块是在这些基础块上构建的，作为深度规范。我们的目标是在一个探索性的证明工程努力中，从关系和演绎数据库设置中机械化底层模型和逻辑推理引擎，重点是组件的可扩展性和可重用性。1.4. 论文贡献本论文的技术贡献包含在两个形式化的开发中：第一，用于关系模型的COq库，第二，用于数据库片段中逻辑编程的SSREFLECT库我们详细介绍了以下内容。• [14]中描述的形式化关系模型– 数据模型的形式化（关系、元组等）– 完整性约束的机械化：我们对一般依赖性进行编码，并证明其推理过程的合理性;我们还对对应于两个一般依赖性子类（函数依赖性和多值依赖性）的实例进行编码;我们建立其推理的合理性，以及在函数依赖性的情况下的完整性。– 主关系查询语言的机械化：我们编码关系代数和关系演算的受限片段，即合取查询– 主数据库定理的证明代数等价、同构定理和合取查询最小化• 正DATALOG程序的形式化推理引擎– 在逻辑编程设置中使用SSREFLECT的有限机制：通过在核心论文开发中假设有限性，我们大大简化了验证工作，而不会失去通用性;事实上，众所周知，每个D目录程序都有一个有限模型，该模型在有限设置中工作就足够了。我们将这种减少与主要发展分开进行，在我们看来，主要发展允许更清楚地呈现。– 实证数据库语法和语义的可扩展机械化– 自下而上评估启发式的机制化：术语、原子和子句体的迭代单子匹配算法的形式化，具有相应的健全性和完整性证明– 正引擎的正式特征化：我们建立的关键性质是健全性、终结性、完整性和模型最小性，基于我们给出的单调性、边界性和稳定性的证明，以及定点理论的结果。1. 初步6• 具有否定的DATALOG程序的形式化推理引擎– 带否定的Datalog程序的语法和语义的机械化– 分层评估化：我们将程序的分层和切片形式化;为了重复使用正引擎，我们将否定的文字翻译为标记的正原子，并将解释的概念扩展为"补充的解释";– 正引擎理论的扩展：分层评价的一个关键部分与正引擎有关，以执行编码为正的负程序的形式评价;这种再利用需要扩展到具有增量性和模块性引理的– 负引擎的正式特征化：我们建立的关键属性是声音、终止性和完整性以及模型极简性72. 方法论在构建数据库模型和算法的正式规范时，如前一章所述，我们遵循基于定理证明技术的方法。这些都是喜欢建立和验证定理使用软件，其中可信的内核是基于一套特定的推理规则。这个概念可以追溯到Au-tomath项目[29]和Milner的可计算函数逻辑（LCF）体系结构[62]，后者实现了自然演绎（参见第3.4.2节）。定理证明可以是自动的或半自动的（交互式的），即要求用户与计算机协同工作。我们关注的是较新类型的规范语言，它们基于更具表达性的逻辑，使其应用范围非常广泛。在此设置中，典型的工作流包括提供输入程序及其规范，并帮助证明程序构造（机械化）证明程序的输出符合规范。因此，确保程序声音的问题被简化为确保被掩盖的物种的声音。遵循这种方法，我们开发了第7章、第8章和第9章中分别在CO q证明助手及其SSREFLECT扩展中提出的形式化在本章中，我们简要回顾了这些工具和库，突出了我们使用的主要功能。2.1. 公鸡CO q证明助手（[61]）属于交互式定理证明者的范畴，沿着HOL家族的边系统，例如ISABELLE/HOL（[65]）、 HOL-LIGHT（[45]）、PVS（[68]），-在经典高阶逻辑传统中-以及沿着NU PRL（[25]）、 AGDA（[66]）和MATITA（[6]）-在构造型理论传统中。它的核心形式是归纳结构演算（CIC），它对应于Barendregt's lambda cube中最具表现力的类型理论，即超承载多态性、类型运算符C O q系统及其背后的理论在[15]中有描述。归纳结构的演算是基于Curry-Howard的"命题作为类型和证明作为程序"范式（[27]，[47]）。因此，CO q既是一个证明系统，也是一种函数式编程语言（Gallina）。本质上，类型系统可以看到它只包含函数类型和归纳类型。CO q的强度和类型检查可决定。该系统在Objective Caml（ML的一种方言）中实现，并带有一个从CO q证明规范中自动提取的机制，可用于构建经过认证的高效函数程序。证明C中的一个定理TOq涉及找到一个程序p，即► p：T，i.e，that2. 方法论8（三）××（二）¬ ∀ ¬∃∃“For到目前为止，有限模型理论已经建立了一个庞大的工具库，可以很容易地被数据库理论家使用，而不需要进入基础知识。P不属于T型。或者，它涉及构造将类型T分配给程序p的类型派生。命题的一个经典例子是带有单个构造函数的"and"数据类型，它封装了两个证明，通常写为。为了证明A B，我们需要找到A的证明a和B的证明b，然后应用合取构造函数。更有趣的数据类型是。此数据类型有两个构造函数，指示其中一个找到了A或B的证明。很容易看出，要为排除的中间原则（即A A）提供证明，就必须为A或A中的任何一个找到证明。这在一般情况下是无法证明的，因为存在着不能以这种方式决定的命题。例如，如果一个图灵机表达了终止，那么这个原理就等价于停止问题。 类似地，为了证明x，PX，必须提供证人w和Pw的证明。 因此， （x、 Px）不包括在内 x，PX，因为这是等价的被排除在外的中间人。由于手工构建程序是cumbersome，CO q提供了一套所谓的策略，用于构建Gallina程序。我们将在下面的章节中进一步讨论战术2.2. 反射Datalog程序的模型理论语义深深植根于有限模型理论。引用[57]：在第8章和第9章的形式化中，我们选择依赖于使用CO q的SSREFLECT（[40]）扩展构建的M数学 COMPONENTS库1这个库特别适合我们的目的，因为它是有限模型理论广泛形式化的基础，在证明费特-汤普森定理（[39]）的背景下，费特-汤普森定理是有限群分类的核心。2.2.1. Ssreflect战术S反射函数的完整描述见[40]。 我们简要概述了下一个最重要的战术。一般来说，SSRFLECT提供的策略可以分为两种类型："缺陷"策略，即移动、案例、拥有、消除和应用，其行为类似于其对应方，以及重写策略，包括战术是通过将"缺陷"战术与上下文操纵"战术"（即：和⇒）相结合而额外构建的前一个移动事实和1http://math-comp.github.io/math-comp/2. 方法论9→约Lemmafwd_chain_cat定义p1 p2i：fwd_chain定义（p1 ++ p2）i =证明。fwd_chain定义p1 i= fwd_chain定义p2i。按应用/设置⇒ 所以，重写？(big_cat，inE）;重写orbACA orbb。Qed.常量到目标，而后者引入变量、局部定义和上下文假设。SSREFLECT支持所有战术通用的模式选择机制。有缺陷的移动战术暴露了目标中的第一个假设，即改变P到P为假。有缺陷的案例策略对（共）归纳类型进行案例分析，通过解构它们，暴露它们的构造函数和参数，并相应地实例化较晚的类型;如果它找到一个等式，它也会进行注入。有缺陷的ELIM战术在归纳类型上执行归纳消除。最后，通过应用实现反向链接推理。一个方便的特征是，这些策略可以与观点相关联，允许将布尔平等目标更改为等价命题。我们通过对下面的证据进行一步一步的说明来说明它们的用途。为了设置fwd_chain_cat引理，让我们假设一个默认常量ef、一个初始解释（有限组地原子）i以及（正数据库）程序p1和p2。我们证明了将前向链应用于p1和p2的连接等于将前向链应用于p1和p2的并。为此，我们使用有限集的一个关键性质，即集相等等价于广延集。这由finset库中的setP引理表示。注意，对于任何有限集A和B，=i2算子适用于x，x奏效于 A= x奏效于B。setP：（T：finType）（A B：{setT}）， A=i B A= B，用setP视图转换目标，命名并将普遍量化的仲裁集元素移到上下文中，证明义务变成：（GA（ga> fwd_chain ef（p1 ++ p2）i）=（f）因此，对于任意程序p，我们将前向链函数定义为fwd_chain ef pi = i=\bigcup_（cl← p）cons_clause efcl i目标相当于：(ga（p1 ++ p2）cons_clause定义cl i）=(ga（c）（d）（i≤\bigcup_（cl← p2）cons_子句定义cl i））。注意，iin=i与fwd_chain_cat引理中的解释参数i不同
我的内容管理
展开
