DraonAbyss

分类

C++(3) CodeForces(23) LeetCode(3) 函数语言程序设计(40) 安全编程(1) 密码学基础(17) 无线网络安全(5) 笔记(16) 算法设计与分析(22) 编译原理与技术(16) 网络安全数学基础(3) 计算机逻辑基础(8) 题解(37)

/ 注册

TA的专栏 167篇文章 11人订阅

【题解】SQL 入门

36篇文章 18251人学习

【学习】函数语言程序设计

39篇文章 1641人学习

【学习】密码学基础

16篇文章 1083人学习

【学习】算法设计与分析

22篇文章 1925人学习

【学习】无线网络安全

6篇文章 2960人学习

计算机逻辑基础

4篇文章 1462人学习

【学习】网络安全数学

7篇文章 883人学习

12篇文章 551人学习

2篇文章 530人学习

23篇文章 1665人学习

全部文章（共24篇）

【Coq】09 Induction III 更多练习来自专栏

更多练习 More Exercises 20: 3 stars, standard, especially useful (mul_comm) 使用[assert]帮助证明[add_shuffle3]。你还不需要使用归纳法。 Theorem add_shuffle Theorem add_shuff...

Coq 函数语言程序设计

2021-10-17

0 1641

【Coq】08 Induction II 证明中的证明 + 正式与非正式证明来自专栏

证明中的证明 Proofs Within Proofs 在Coq中，就像在非正式数学中一样，大的证明常常被分解成一系列定理，后面的证明引用了前面的定理。但有时，一个证明将需要一些杂七杂八的事实，这些事实太琐碎，也没有太多的普遍兴趣，以至于懒得给它起自己的顶级名称。在这种情况下，可以方便地在使用“子定...

Coq 函数语言程序设计

2021-10-17

0 895

【Coq】07 Induction I 归纳法证明来自专栏

单独编译 Separate Compilation 在开始本章之前，我们需要从上一章中导入我们的所有定义： From Coq Require Export String. Fixpoint even (n:nat) : bool := match n with | O =&g...

Coq 函数语言程序设计

2021-10-12

0 1489

【函数语言程序设计】Hw5 - Coq3 来自专栏

1.证明下列三条性质 Theorem plus_n_Sm Theorem plus_n_Sm : ∀ n m : nat, S (n + m) = n + (S m). Proof. (* FILL IN HERE *) Admitted. Coq代码 Theorem plus_n_Sm : f...

Coq 函数语言程序设计

2021-10-12

1 432

【Coq】06 Basics VI 更多练习来自专栏

更多练习 More Exercises 10: 1 star, standard (identity_fn_applied_twice) 使用您迄今学到的策略来证明有关 Boolean 函数以下定理。 Theorem identity_fn_applied_twice : forall (f :...

函数语言程序设计 Coq

2021-09-30

0 728

【Coq】05 Basics V （可选）更多关于符号固定点和结构递归来自专栏

更多关于符号（可选） More on Notation （一般来说，标有可选部分的章节不需要遵循书的其余部分，但可能的其他可选部分除外。一读时，您可能需要浏览这些部分，以便您知道哪些内容供将来参考。回想一下中缀加号和时间的符号定义： Notation "x + y" Nota...

函数语言程序设计 Coq

2021-09-30

0 627

【Coq】04 Basics IV 案例分析证明来自专栏

案例分析证明 Proof by Case Analysis 中止 Abort 当然，并不是所有的东西都能通过简单的计算和重写来证明：一般来说，未知的假设值（任意数字、布尔值、列表等）可以阻止简化。例如，如果我们试图用上面的 simpl 策略来证明以下事实，我们就会陷入困境。（然后，我们使用 Abor...

函数语言程序设计 Coq

2021-09-29

0 603

【Coq】03 Basics III 简化证明重写证明来自专栏

简化证明 Proof by Simplification 现在，我们已经定义了一些数据类型和功能，让我们来说明和证明其行为的属性。实际上，我们已经开始这样做：前几个部分的每个 Example 都对某些特定输入中某些功能的行为做出精确声明。这些声明的证据总是相同的：使用 simpl 来简化方程的两侧，...

函数语言程序设计 Coq

2021-09-29

1 855

【Coq】02 Basics II 类型旧类型模块多元组数字来自专栏

数据和功能 Data and Functions II 类型 Types 检查 Check Coq 中的每个表达式都有一个类型，描述它计算的事物类型。Check 命令要求 Coq 打印表示式的类型。 Check true. (* ===> true : bool *)如果 Check 后的表达...

函数语言程序设计 Coq

2021-09-29

1 690

【Coq】01 Basics I 枚举类型布尔值来自专栏

数据和功能 Data and Functions I 枚举类型 Enumerated Types Inductive day 以下声明告诉 Coq，我们正在定义一组数据值 - a type。 Inductive day : Type := | monday | tuesday | wed...

函数语言程序设计 Coq

2021-09-29

1 976