DraonAbyss

函数语言程序设计

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

/ 注册

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

【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

【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

【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