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人学习

全部文章（共22篇）

【Coq】18 Tactics I 应用策略来自专栏

本章介绍了几个额外的证明策略和策略，使我们能够开始证明函数程序更有趣的属性。我们将看到：如何在“向前”和“向后”证明中使用辅助引理；如何对数据构造函数进行推理——特别是如何利用它们是内射的和不相交的事实；如何强化归纳假设，以及何时需要强化；和关于如何通过案例分析进行推理的更多详细信息。 ...

Coq 函数语言程序设计

2021-11-11

1 854

【Coq】17 Poly III 附加练习来自专栏

附加练习 Additional Exercises 57: 2 stars, standard (fold_length) 列表上的许多常见功能可以按折叠方式实现。例如，以下是长度的替代定义： Definition fold_length {X : Type} (l : list X) : nat ...

Coq 函数语言程序设计

2021-11-11

0 979

【Coq】16 Poly II 作为数据的函数来自专栏

作为数据的函数 Functions as Data 与大多数现代编程语言一样——特别是其他“函数”语言，包括OCaml、Haskell、Racket、Scala、Clojure等——Coq将函数视为一级公民，允许它们作为参数传递给其他函数、作为结果返回、存储在数据结构中等。高阶函数 Higher-...

Coq 函数语言程序设计

2021-11-11

0 604

【Coq】15 Poly I 多态性来自专栏

多态性 Polymorphism 在本章中，我们将继续发展函数式编程的基本概念。关键的新思想是多态性（将函数抽象为它们所操作的数据类型）和高阶函数（将函数视为数据）。我们从多态性开始。多态列表 Polymorphic Lists 在上一章中，我们一直在处理只包含数字的列表。显然，有趣的程序还需要能...

Coq 函数语言程序设计

2021-10-27

0 1081

【Coq】14 Lists V 局部映射来自专栏

局部映射 Partial Maps 作为在Coq中如何定义数据结构的最后一个例子，这里有一个simple _partial map_data类型，类似于大多数编程语言中的map或dictionary数据结构。首先，我们定义一个新的归纳数据类型id作为部分映射的“键”。 Inductive id I...

Coq 函数语言程序设计

2021-10-27

0 655

【Coq】13 Lists IV 选项来自专栏

选项 Options 假设我们要编写一个函数，返回某个列表的第n个元素。如果我们给它类型nat→ natlist→ nat，那么当列表太短的时候，我们必须选择一些数字返回… Fixpoint nth_bad Fixpoint nth_bad (l:natlist) (n:nat) : nat := ...

Coq 函数语言程序设计

2021-10-27

0 504

【函数语言程序设计】Hw7 - Coq5 来自专栏

1. 2. 把上面的函数maxPair改造成maxPair'，返回类型为option nat * option nat。当要找的数字不存在时用None而不是0替代。 Example test_maxPair‘1: maxPair’ [1;2;5;4;8;10;3] = (Some 5, Some ...

Coq 函数语言程序设计

2021-10-27

0 562

【Coq】12 Lists III 关于列表的推理来自专栏

关于列表的推理 Reasoning About Lists 与数字一样，关于列表处理函数的简单事实有时完全可以通过简化来证明。例如，对于这个定理来说，仅仅通过自反性进行简化就足够了。。。 Theorem nil_app : forall l : natlist, [] ++ l = l. Pro...

Coq 函数语言程序设计

2021-10-25

0 792

【函数语言程序设计】Hw6 - Coq4 来自专栏

1. 补充完整下面的定义，判断一个集合是否为另一个集合的子集。 Fixpoint subset (s1 : bag) (s2 : bag) : bool (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitt...

Coq 函数语言程序设计

2021-10-22

0 446

【Coq】11 Lists II 数字表来自专栏

数字表 Lists of Numbers 概括成对的定义，我们可以这样描述数字列表的类型：“一个列表要么是空列表，要么是一个数字和另一个列表的一对。” Inductive natlist Inductive natlist : Type := | nil | cons (n : nat) (...

Coq

2021-10-17

0 0