DraonAbyss

函数语言程序设计

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

/ 注册

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

LOGIC.逻辑.逻辑联结词来自专栏

LOGIC LOGIC IN COQ Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality". From LF Require Export Tactics. 我们已经看到了许多事实主张（命题）的...

2021-12-20

0 1588

INDPROP.归纳定义命题.附加练习来自专栏

Additional Exercises 附加练习 Exercise: 3 stars, standard, especially useful (nostutter_defn)

2021-12-20

0 425

INDPROP.归纳定义命题.案例研究：改进反思来自专栏

Case Study: Improving Reflection 我们在逻辑一章中看到，我们经常需要将布尔计算与Prop中的语句相关联。但是，在那里执行这种转换可能会导致冗长的验证脚本。考虑下面定理的证明：

2021-12-20

0 424

INDPROP.归纳定义命题.案例研究：正则表达式来自专栏

Case Study: Regular Expressions ev属性提供了一个简单的例子来说明归纳定义和对其进行推理的基本技术，但它并不十分令人兴奋——毕竟，它相当于我们已经看到的两个非归纳均匀度定义，并且似乎没有提供任何具体的好处。为了更好地理解归纳定义的威力，我们现在展示如何使用它们来模拟...

2021-12-20

0 525

INDPROP.归纳定义命题.归纳关系来自专栏

Inductive Relations 一个由数字（如ev）参数化的命题可以被认为是一个属性——也就是说，它定义了nat的子集，即命题可证明的那些数字。同样，一个双参数命题可以被认为是一种关系——也就是说，它定义了一组可证明命题的对。

2021-12-20

0 439

INDPROP.归纳定义命题.在证明中使用证据来自专栏

Using Evidence in Proofs 除了构建数字是偶数的证据外，我们还可以破坏这些证据，这相当于对如何构建数字的推理。引入带有归纳声明的ev不仅告诉Coq构造函数ev_0和ev_SS是证明某个数字是ev的有效方法，而且这两个构造函数是证明数字是ev的唯一方法。换句话说，如果有人给我...

2021-12-20

0 692

INDPROP.归纳定义命题.归纳定义命题来自专栏

INDPROP INDUCTIVELY DEFINED PROPOSITIONS 归纳定义命题 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality". From LF Require Export...

2021-12-20

0 660

IMP.简单命令式程序.Coq自动化来自专栏

Coq Automation 最后一个证明中重复的次数有点烦人。如果算术表达式的语言或被证明合理的优化明显更复杂，那么它将开始成为一个真正的问题。到目前为止，我们所做的所有证明都只使用了Coq的一小部分策略，而完全忽略了它自动构造部分证明的强大功能。本节将介绍其中的一些设施，我们将在接下来的几章中...

2021-12-19

0 713

IMP.简单命令式程序.算术和布尔表达式来自专栏

在本章中，我们将更认真地研究如何使用Coq来研究其他东西。我们的案例研究是一种简单的命令式编程语言Imp，它体现了传统主流语言（如C和Java）的一个微小核心片段。这是一个用Imp编写的熟悉的数学函数。 Z := X; Y := 1; while ~(Z = 0) do ...

2021-12-19

0 1021

【Coq】？Rel III 自反传递闭包来自专栏

自反传递闭包 Reflexive, Transitive Closure 关系R的自反传递闭包是包含R的最小关系，它既是自反的又是传递的。形式上，在Coq标准库的关系模块中定义如下： Inductive clos_refl_trans {A: Type} (R: relation A) Induct...

2021-12-13

0 967