DraonAbyss

函数语言程序设计

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

/ 注册

全部文章 / 函数语言程序设计（共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 605

【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