形式化方法 Assignment 2: Proof engineering

LAB2

lab2总体来说比lab1有意思很多，做完感觉像通关打游戏一样，看一个例子，写一个练习，不知不觉就写完了，感觉意犹未尽。实现过程参考了https://blog.csdn.net/m0_37714470/article/details/105375686.

做之前需要了解一下coq程序基本的结构：

Theorem (题目名字): forall P Q(所有变量) :Prop,需要证明的结论。
Proof.证明的过程。
Qed.

另外其他需要注意的主要如下：

ctrl + ↓ 让程序执行到光标的下一行，ctrl + ↑ 让程序执行到上一行。类似于可以回退的单步调试。
证明的过程中每一句后面必须加上.
原则：先有前提(inversion)后有结论(spilt) 先提出的结论必须先证. （详细见exercise4）
如果要证明 A->(B->C)->D->(E->F)->G 其中A,(B->C),D,(E->F)均为前提，而G为结论。
intros 蕴含得到命题所有前提
inversion H 反演将前提H左边拆成两份（合取析取均可）
spilt 拆分将结论拆成两份
unford not 非将条件中的~变成false
elim 消除谬误如果条件中有H0：P->false此时使用命令elim H0命令相当于只需要证明P的正确性
left 和 right 分别选择结论选择析取的左半部分和右半部分
apply 应用如果条件H与结论相同，可直接使用apply H完成证明
apply A in B 以B为前提，结合A能够推出的结果,这里一定要注意顺序

具体结果如下：

Theorem exercise1: forall P Q :Prop,P -> (Q -> P).
Proof.intros.apply H.Qed.Theorem exercise2: forall P Q H:Prop,(P->Q) -> (Q->H) -> (P->H).
Proof.intros.apply H0 in H2.apply H1 in H2.apply H2.
Qed.Theorem exercise3: forall P Q :Prop,P /\ (P -> Q) -> Q.
Proof.intros.inversion H.apply H1 in H0.apply H0.
Qed.Theorem exercise4: forall P Q R:Prop,(P /\ (Q /\ R)) -> ((P /\ Q) /\ R).
Proof.intros.inversion H.inversion H1.split.split.apply H0.apply H2.apply H3.
Qed.Theorem exercise5: forall P Q R:Prop,(P \/ (Q \/ R)) -> ((P \/ Q) \/ R).
Proof.intros.inversion H.left.left.apply H0.inversion H0.left.right.apply H1.right.apply H1.
Qed.Theorem exercise6: forall P Q R:Prop,((P -> R) /\ (Q -> R)) -> (P /\ Q -> R).
Proof.intros.inversion H.inversion H0.apply H1 in H3.apply H3.
Qed.    Theorem exercise7: forall P Q R:Prop,   (P -> Q /\ R) -> ((P -> Q) /\ (P -> R)).
Proof.intros.split.apply H.apply H.
Qed.Theorem challenge1: forall P Q R S T:Prop,(((P /\ Q) /\ R) /\ (S /\ T)) -> (Q /\ S).
Proof.intros.inversion H.inversion H0.inversion H1.inversion H2.split.apply H7.apply H4.
Qed.Theorem challenge2: forall P Q:Prop,(P -> Q) -> (~Q -> ~P).
Proof.unfold not.intros.apply H in H1.apply H0 in H1.apply H1.
Qed.

形式化方法 Assignment 2: Proof engineering相关推荐

形式化方法 Assignment 3: SAT
作业3 软件解决SAT问题 Part A: SAT基本问题的编码 /\ And 与 \/ Or 或 ~ Not 非 -> Implies 蕴含判断命题是否具有SAT性质 F = Or(P, Q ...
ChinaSoft 论坛巡礼 | CCF-华为胡杨林基金-形式化方法专项论坛
2022年CCF中国软件大会(CCF ChinaSoft 2022)将于2022年11月25-27日在线上举行.预期将有林惠民.陈左宁.邬江兴.何积丰.梅宏.吕建.柴洪峰.廖湘科.王怀民.郑纬民.蒋昌 ...
1、阅读和了解什么是形式化方法 2、推荐阅读书籍《大象——thinking in UML》
什么是软件形式化方法软件形式化方法是指建立在严格数学基础上的软件开发方法.形式化方法模型的主要活动是生成计算机软件形式化的数学规格说明.形式化方法使软件开发人员可以应用严格的数学符号来说明.开发和验 ...
形式化方法、《大象：Thinking in UML》
形式化方法英文的名称是formal methods.在逻辑科学中是指分析.研究思维形式结构的方法.它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式,如命题中包 ...
【形式化方法：VDM++系列】4.VDM实战1——铁路费用计算
又有将近2个月没更新博客了啊!winter holiday简直玩儿疯了的说!结果假期前学习的形式化方法已经忘了大半!面对期末作业,大脑一片空白.于是,赶快复习了一下之前学习的姿势! 这次的主要任务是完 ...
形式化方法｜形式化方法对软件开发的挑战：历史与发展
几年前到某著名大学参加学术活动,无意中听到该校两位老师闲聊,现在还记得的一句话就是"形式化方法已经不行了".看来真是隔行如隔山,评价自己不熟悉的领域,而且随便说,难免出错.在对形式 ...
形式化方法-- petri net
形式化方法-Petri net Petri net是由C.A.Petri在其博士论文中提到的,petri net 通常包含以下几个元素,分别是:库所.变迁.流关系.容量函数.初始标识.权值函数.所以p ...
2022 CCF形式化方法工业应用前沿分论坛暨中科国创高可信联合上海控安新品发布会顺利召开！...
11月27日,2022年CCF中国软件大会"形式化方法工业应用前沿"技术分论坛暨中科国创高可信联合上海控安新品发布会于线上顺利召开.本次活动由CCF形式化方法专业委员会主办,华东师 ...
CCF ChinaSoft 2022预告丨形式化方法工业应用前沿分论坛暨中科国创高可信联合上海控安新品发布...
2022年11月25-27日,2022年CCF中国软件大会(CCF ChinaSoft 2022)将于线上举行.大会将围绕"聚焦产教研用协同创新,提升关键软件供给能力"主题,举办包 ...
软件工程——形式化方法概述
目录前言一.形式化方法定义二.形式化方法分类三.形式化方法意义四.形式化方法作用五.形式化方法优缺点 1.优点 2.缺点前言形式化方法英文的名称是formalmethods,形式化方法 ...

形式化方法 Assignment 2: Proof engineering

LAB2

形式化方法 Assignment 2: Proof engineering相关推荐

最新文章

热门文章