software foundations LF Induction
更多内容见 https://github.com/january147/software_foundations_notes
software foundations LF Induction
导入经过编译的模块
From LF Require Export Basics.
LF
表示项目目录,Basics
是导入的模块名称(对应Basics.vo
文件)
First create a file named
_CoqProject
containing the following line (if you obtained the whole volume “Logical Foundations” as a single archive, a _CoqProject should already exist and you can skip this step):-Q . LF
This maps the current directory (".", which contains Basics.v, Induction.v, etc.) to the prefix (or “logical directory”) “LF”.
通过创建_CoqProject
文件,指定-Q . LF
可以将本地目录.
映射到逻辑目录LF
。
Proof by induction
对于无法逐个列举所有情况的命题(即使用destruct
无法完成证明),可以通过数学归纳法来证明,即对于命题P(n)P(n)P(n), 证明P(0)P(0)P(0)为真,并且P(n)→P(n+1)P(n) \to P(n+1)P(n)→P(n+1)为真,根据数学归纳法则有P(n)P(n)P(n)为真。
Theorem plus_n_Sm : forall n m : nat,S (n + m) = n + (S m).
Proof.intros n m.(* seems impossible to induction m? *)induction n as [| n' Hn].-simpl. reflexivity.-simpl. rewrite <- Hn. reflexivity.
Qed.
tactic
induction
induction
和destruct
有点类似,都是将变量进行分类讨论。不同的是,induction
即采用数学归纳法进行证明,即将变量分为初始值和后续任意一个值两种情况进行讨论。
Theorem plus_n_O : forall n:nat, n = n + 0.
Proof.intros n. induction n as [| n' IHn'].(* n = 0 *) - reflexivity.(* n = S n', n' = n' + 0 *)- simpl. rewrite <- IHn'. reflexivity. Qed.
assert
使用assert
可以在一个定理的证明过程中定义一个子定理(通常称为引理lemma
),通过证明这个子定理来证明最终的定理。通常很简单或者泛用性较差(不在其他定理证明中使用)的子定理才使用assert
在证明过程中定义,复杂或者通用的子定理通过使用Theorem
或者Lemma
直接定义。
Theorem mult_0_plus' : ∀ n m : nat,(0 + n) × m = n × m.
Proof.intros n m.assert (H: 0 + n = n). { reflexivity. }rewrite → H.reflexivity. Qed.
rewrite
可以配合assert
实现指定具体的改写目标。例如在下面这个定理的证明过程中,存在一个等式中有多个可以rewrite
的地方,仅使用rewrite
无法指定特定的部分进行rewrite
,导致定理难以证明,通过assert
声明针对该证明过程中特定变量名称的子定理可以使得rewrite
仅改写我们所需的部分
Theorem mult_n_Sm: forall n m : nat, n * S m = n + n * m.
Proof.intros n m. induction n as [|n' Hn].-simpl. reflexivity.-simpl. rewrite -> Hn. rewrite -> plus_assoc.rewrite -> plus_assoc.(* 这一步需要时证明目标为S (m + n' + n' * m) = S (n' + m + n' * m),可以看到使用加法交换律改写m + n'即可得证,然而等式中存在多个加号,使用一般得加法交换律会导致rewrite无法确定应该改写哪一个(例如改写等式左边第二个加号则会导致无法证明),因此我们使用assert针对上述目标中的变量名称以及需要交换的部分(m + n')定义一个特定的加法交换律,实现对所需特定位置的rewrite*)assert(H: m + n' = n' + m).(* 使用通用的交换律证明这里特定的交换律 *)--rewrite -> plus_comm. reflexivity.(* 使用特定的交换律实现目标中指定部分的rewrite从而证明目标 *)--rewrite -> H. reflexivity.
Qed.
replace
上边提到在rewrite
无法确定正确的改写位置时可以使用assert
来定义一个针对目标中需要改写位置的子定理来实现控制rewrite
的改写位置。除了该方法外,还可以使用replace
来实现。使用replace
可以将目标中的某部分t
替换为q
,替换之后会生成一个t = q
的子目标,需要证明t=q
,相当于使用assert
定义了一个t=q
的子定理,然后使用该子定理rewrite
原目标。
replace (t) with (p)
下面是一个小例子,该例子使用加法交换律plus_comm
,然而在目标中存在多个可交换的地方,因此使用replace
对指定位置进行替换。
Theorem plus_swap' : forall n m p : nat,n + (m + p) = m + (n + p).
Proof.intros n m p. induction n as [|n' Hn].-simpl. reflexivity.(* 这里后续会补充当前目标,方便理解replace的使用 *)(* 为了证明目标,使用S (n' + p) + m替换了目标中的m + S (n' + p)另外生成了一个子目标m + S (n' + p) = S (n' + p) + m需要证明*)-simpl. replace (m + S (n' + p)) with (S (n' + p) + m).--simpl. rewrite -> Hn. rewrite <- plus_comm. reflexivity.--rewrite <- plus_comm. reflexivity.
Qed.
重点练习
定义unary
表示转换为binary
表示的函数
Fixpoint nat_to_bin (n:nat) : bin :=match n with(* 0到0的转换 *)| O => Z(* >= 1的数使用incr函数(第一章basics中定义)结合递归定义来实现 *)| S n' => incr (nat_to_bin n')end.
证明转换函数的正确性,即证明
Theorem nat_bin_nat : forall n, bin_to_nat (nat_to_bin n) = n.
在使用数学归纳法证明该定理的过程中,存在一个bin_to_nat (incr (nat_to_bin n')) = S n'
的中间目标,而归纳假设为bin_to_nat (nat_to_bin n') = n'
。为了使用归纳假设,我们需要将incr
函数转换到最外层去,因此,我们定义如下引理
Lemma bin_incr: forall n : bin, bin_to_nat (incr n) = S (bin_to_nat n).
Proof.intros n. induction n as [|n1 Hn1 |n2 Hn2].-simpl. reflexivity.-simpl. reflexivity.-simpl. rewrite -> Hn2. simpl. rewrite <- plus_comm. reflexivity.
Qed.
使用该引理即可证明转换函数的正确性定理。
Theorem nat_bin_nat : forall n, bin_to_nat (nat_to_bin n) = n.
Proof.intros n. induction n as [|n' Hn].-simpl. reflexivity.-simpl. rewrite -> bin_incr. rewrite -> Hn. reflexivity.
Qed.
software foundations LF Induction相关推荐
- software foundations LF Tactics
更多内容见 https://github.com/january147/software_foundations_notes 原始章节参考 software foundations LF Tactic ...
- software foundations LF Basics
更多内容见 https://github.com/january147/software_foundations_notes 原始章节参考 Software Foundations (upenn.ed ...
- 编程的本质:第一章 foundations
编程的本质,是数学,是函数.针对现实世界的问题,我们首先要建立模型,界定标准,定义属性和行为. 然后呢,让这些模型对象实体动起来,于是计算机世界就有了生命.这跟大自然造物还真是一个道理. 谁能道透宇宙 ...
- 去中心化 去区块链_使用JavaScript和坚固性在以太坊区块链上构建去中心化应用程序dapp...
去中心化 去区块链 In this blog, I build a decentralized application, also known as a "dapp". While ...
- IndProp章节中pumping lemma的证明
在software foundations–Logic foudations–IndProp中,有一个证明pumping lemma的练习,本文介绍了一种证明方法. 辅助引理 为了证明pumping ...
- What every computer science major should know 每一个计算机专业的学生应该知道什么
Given the expansive growth in the field, it's become challenging to discern what belongs in a modern ...
- Eric S. Raymond 五部曲 之 《开拓智域》
4 开拓智域 在观察由开放源代码版权所定义的"官方"意识形态与真正玩家的行为后,发现到一些矛盾之处.重新检 视真正掌控开放源代码拥有权的文化.我们发现暗藏着一个源自于Locke 的 ...
- 个人网页、博客、课程--不断更新
论文和相关代码 :https://paperswithcode.com/ Caiming Xiong http://www.stat.ucla.edu/~caiming/ 论文,代码,博客 肖小粤的啵 ...
- Purism FAQ
<font size="37" color="#006248" face="幼圆"> <p align="cen ...
最新文章
- Scala’s parallel collections
- JavaWeb(十一)——登录注册小案例
- Heap(堆结构/优先队列)-Swift实现
- spring框架三层架构_Spring框架架构
- MobileNet V3简单总结
- Magento模型集合addFieldToFilter常用过滤条件
- TensorFlow运作方式入门
- c语言识别按了esc键_憋了三年,史上最全的 F1~F12 键用法整理出来了
- Spring源码全解
- Python网络爬虫
- 系统识别matlab,系统辨识MATLAB
- 蓄力一纪,可以远矣!十二年的百度地图和他的AI新征程
- 苹果手机黑屏怎么办,苹果手机不能开机怎么办
- java利用poi导出excel功能-附带图片导出
- Easyui Tree扁平化数据不显示父节点的一种解决方法
- python算法1.5百钱百鸡
- zxing换行_让文字自动换行
- poi替换word内容
- 2022年值得购买的拍照手机推荐 这五款出片率极强
- 我是技术总监,我出来求职,竟然找不到工作!