DraonAbyss

函数语言程序设计

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

/ 注册

全部文章 / 函数语言程序设计（共40篇）

【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 992

【函数语言程序设计】Hw4 - Coq2 来自专栏

1.定义函数定义函数gtb，使得gtb n m 返回布尔值 true当且仅当 n > m。至少用两种方法定义这个函数。（请用【Example】语句测试 n>m, n=m, n<m 三种情况下你定义的gtb函数(含两种方式)的输出）方法一根据先前定义的函数来定义 Coq代...

函数语言程序设计 Coq

2021-09-28

0 666

【函数语言程序设计】4 来自专栏

定义函数square，目的是计算给定自然数n的平方，但是不能用乘法运算。 Coq代码 Fixpoint square( n : nat ): nat := match n with |0&n...

函数语言程序设计

2021-09-27

0 363

【函数语言程序设计】3

1.为下面这个类型判断构造一棵推导树。解析：我们用记号 M : A 来表示项 M 的类型是 A。类型规则是通过类型判断（typing judgments）来表述的。一个类型判断是下面形式的表达式： x1 : A1, x2...

函数语言程序设计

2021-09-26

0 354

【函数语言程序设计】3 来自专栏

1.为下面这个类型判断构造一棵推导树。解析：我们用记号 M : A 来表示项 M 的类型是 A。类型规则是通过类型判断（typing judgments）来表述的。一个类型判断是下面形式的表达式： x1 : A1, x2...

函数语言程序设计

2021-09-26

0 0