Operations on NFA states 伪代码 put ε-closure({s0}) as an unmarked state into the set of DFA (DStates) //ε-闭包（{s0}）是通过ε-跃迁从s0可以访问的所有状态的集合。 while (there is one unmarked S1in DStates) do begin mark S1 for each input symbol a do begin S2 ← ε-closure(move(S1,a))//set of states to w...

知识 2.1.1 结构 typedef struct student{ char name[20]; char sex; int age; }Student; Student studA; 2.3.1 指针 &取地址运算符 *间接引用运算符 指针定义和运算 自引用结构 2.3.2 单链表 单链表结构 习题 21. 合并两个有序链表 https://leetcode-cn.com/problems/merge-two-sorted-lists/ 递归 链表 题目 将两个升序链表合并为一个新的 升序 链表并返回。新链表是通过拼接给定的两个链表的所有节点...

使用Miller-Rabin素性检验随机生成一个120比特的素数 120比特数 Miller-Rabin素性检验 实现Miller-Rabin素性检验的 C++ 程序 C++ Program to Implement Miller Rabin Primality Test /* * C++ Program to Implement Miller Rabin Primality Test */ #include <iostream> #include <cstring> #include <cstdlib> #define ll long long u...

LOGIC LOGIC IN COQ Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality". From LF Require Export Tactics. 我们已经看到了许多事实主张（命题）的例子，以及证明其真实性的方法（证据）。特别是，我们广泛研究了等式命题（e1=e2）、含义（P→ Q） ，以及量化命题(∀ x、 P）。在本章中，我们将看到如何使用Coq进行其他常见形式的逻辑推理。 在深入讨论细节之前，让我们先谈谈Coq中数学语句的状态。回想一下，Coq是一种类型化语言，这意味着其世...

Additional Exercises 附加练习 Exercise: 3 stars, standard, especially useful (nostutter_defn)

Case Study: Improving Reflection 我们在逻辑一章中看到，我们经常需要将布尔计算与Prop中的语句相关联。但是，在那里执行这种转换可能会导致冗长的验证脚本。考虑下面定理的证明：

Case Study: Regular Expressions ev属性提供了一个简单的例子来说明归纳定义和对其进行推理的基本技术，但它并不十分令人兴奋——毕竟，它相当于我们已经看到的两个非归纳均匀度定义，并且似乎没有提供任何具体的好处。 为了更好地理解归纳定义的威力，我们现在展示如何使用它们来模拟计算机科学中的一个经典概念：正则表达式。 正则表达式是一种描述字符串集的简单语言。其语法定义如下：

Inductive Relations 一个由数字（如ev）参数化的命题可以被认为是一个属性——也就是说，它定义了nat的子集，即命题可证明的那些数字。同样，一个双参数命题可以被认为是一种关系——也就是说，它定义了一组可证明命题的对。

Using Evidence in Proofs 除了构建数字是偶数的证据外，我们还可以破坏这些证据，这相当于对如何构建数字的推理。 引入带有归纳声明的ev不仅告诉Coq构造函数ev_0和ev_SS是证明某个数字是ev的有效方法，而且这两个构造函数是证明数字是ev的唯一方法。 换句话说，如果有人给我们证据E来证明ev n，那么我们知道E必须是两件事之一： E是ev_0（n是O），或 E是ev_SS n'E'（n是S（sn'），其中E'是ev n'的证据）。 这表明，应该可以像分析归纳定义的数据结构一样，分析ev n形式的假设；特别是，应该能够通过归纳和案例分析对这些证据进行论证。让...

INDPROP INDUCTIVELY DEFINED PROPOSITIONS 归纳定义命题 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality". From LF Require Export Logic. From Coq Require Import Lia. Inductively Defined Propositions 在逻辑学一章中，我们研究了几种书写命题的方法，包括连接、析取和存在量化。在本章中，我们将引入另一种新工具：归纳定义命题。 注：为了简单起见，本章大部分内容都使...

Coq Automation 最后一个证明中重复的次数有点烦人。如果算术表达式的语言或被证明合理的优化明显更复杂，那么它将开始成为一个真正的问题。 到目前为止，我们所做的所有证明都只使用了Coq的一小部分策略，而完全忽略了它自动构造部分证明的强大功能。本节将介绍其中的一些设施，我们将在接下来的几章中看到更多内容。习惯它们需要一些精力——Coq的自动化是一个强有力的工具——但它将允许我们扩大我们的工作范围，以获得更复杂的定义和更有趣的属性，而不会被无聊、重复、低级的细节所淹没。 Tacticals 战术是Coq对以其他战术为论据的战术的术语——“高阶战术”，如果你愿意的话。 The try Ta...

在本章中，我们将更认真地研究如何使用Coq来研究其他东西。我们的案例研究是一种简单的命令式编程语言Imp，它体现了传统主流语言（如C和Java）的一个微小核心片段。这是一个用Imp编写的熟悉的数学函数。 Z := X; Y := 1; while ~(Z = 0) do Y := Y * Z; Z := Z - 1 end 我们在这里集中定义Imp的语法和语义；《编程语言基础》（软件基础，第2卷）的后面几章发展了程序等价理论，并介绍了霍尔逻辑，这是一种广泛用于推理命令式程序的逻辑。 Set Warnings "-n...

Patrick教授希望找到一条从菲尼克斯(Phoenix)到印第安纳波利斯(Indianapolis)的最短路径。给定一幅美国的道路交通图，上面标有所有相邻城市之间的距离，Patrick教授怎样才能找出这样一条最短的路径呢? 一种可能的办法当然是，先将从菲尼克斯到印第安纳波利斯的所有路径都找出来，将每条路径上的距离累加起来，然后选择其中最短的路径。但是，即使在不允许环路的情况下，也可以看得出来，Patrick教授需要检查无数种可能的路径，而其中的大多数路径根本不值得检查。例如，一条从菲尼克斯经过西雅图再到印第安纳波利斯的路径显然不符合要求，因为西雅图已经偏离了目标方向好几百英里。 最短路径问题...