DraonAbyss

函数语言程序设计

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

/ 注册

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

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

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

【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】10 Lists I 数对来自专栏

在开始本章之前，我们需要从上一章中导入我们的所有定义： From Coq Require Export String. Theorem add_comm : forall n m : nat, n + m = m + n. Proof. induction n as [| n' IHn']. ...

Coq 函数语言程序设计

2021-10-17

0 514