Coq中文手册Word下载.docx
《Coq中文手册Word下载.docx》由会员分享，可在线阅读，更多相关《Coq中文手册Word下载.docx（13页珍藏版）》请在冰点文库上搜索。
SectionLoc.EndLoc.
Printident
打印定义，ident可以是本段定义的任何对象，类型以及本段所包括的库中定义的对象和类型。
Example:
PrintR.
Checkident
检查类型，check可以检查本段定义的对象和类型。
Variabletab:
Type.
Checktab.
Definitionident:
type:
=define
定义一个对象，可以选择性声明其类型，但是必须要有定义体，即:
=后的内容。
Definitionsetiod:
=nat.
Variableident:
type
声明一个局部变量，只需给出类型，不需要定义体。
当没有section包围时，顶级的局部变量等价于全局变量。
Variableck:
nat.
Parameterident:
声明一个全局变量，只需给出类型，不需要定义体。
Parameterck:
nat.
Inductiveident:
=
|constru:
type1‐>
typ2‐>
|…….
定义一个归纳体，可以包含若干个构造子（constru），但是每个构造子的类型的最后必须是归纳体类型。
Inductiveexpr:
Type:
|Evar:
ident‐>
expr
|Econst:
Z‐>
|Eadd:
expr‐>
|Esub:
.
Lemmaem:
定义一个猜想，其类型为type。
通常需要给出证明
Lemmanot_all_not_ex:
forallP:
U‐>
Prop,~（foralln:
U,~Pn）‐>
existsn:
U,Pn.
Fixpointfun（A:
type）（B:
type）:
type:
=tail.
fixpoint可以定义递归函数，其中括号中的是传入参数。
在tail中常使用match结构可以对归纳结构进行拆分。
Fixpointtail_plusnm:
nat:
matchnwith
|0=>
m
|Sn=>
tail_plusn（Sm）end.
Computeexpr
归纳演算expr的值。
Compute1+1.
Structureexp:
={
dom1:
typ1;
dom2:
typ2;
dom3:
typ3:
=value
}
定义结构体，可以包含若干个域，域的名字不能重复，通过dom1exp来访问域的值，利用
Build_exp来构造。
Structureperson:
={
name:
string;
age:
nat
}.
CoercionRela:
typ1>
‐>
typ2
建立从typ1到typ2的强制子类型约束，Rela是之前定义的转换关系。
Variabledog:
Type.Variablehusky:
Variablebelong:
husky‐>
dog.
Coercionbelong:
husky>
Searchkeyword
搜索关键字的定义
Searchnat.
SearchAboutkeyword
搜索所有关键字相关的定义
SearchAboutnat.
SearchPatternexp
搜索指定形式的定义式。
SearchAbout（_‐>
nat）.
特殊库的使用
String:
打开字符串库符之后字符串的表述：
“Ser”
Check“Ds”.
构造子有nil和n:
:
l两个，可用++连接两个列表。
Ensemble
需要先定义元素类型，然后可以声明集合。
VariableI:
Variableset1:
EnsembleI.
CheckUnionIset1set2.
CheckIntersectionIset1set2
证明相关
Proof.
开始证明
Qed.
证明结束
HintResolvelem
将lem加入auto库
证明策略：
intros/intro
用于goal里面有forall,~,P‐>
introsPH0.intros.
unfold
展开非递归函数
unfoldis_ture.unfoldis_trueinH.
rewriteH
将H的右边当作左边带入goal或者指定的目标
rewriteH.rewriteHinH0.
rewrite<
‐H
将H的左边当作右边带入goal或指定目标
‐H.rewrite<
‐HinH0.
existsX
向goal或指定的目标指定existx:
T的目标
existsXinH0.existsX.
subst
在指定地方或goal里面删去可去的参数或者指定的参数
subst.substi.substiingoal.
symmetry
换位，将goal的等号两边换位置，用于将a=b变成b=a
symmetry.
reflexivity
自反，用于证明a=a
reflexivity.
simpl
规约goal或者指定的目标
simpl.simplinH.
discriminate
从已知式子中导出矛盾
discriminate.
destruct
拆掉指定假设中的或和与，当H含forall时加上一个对象p。
destructHas[H1H2].destructHas[H1|H2].destruct（Hp）.
split
拆分goal中间的与
split.
left
指证goal中间的与的左边
left.
right
指证goal中间的与的右边
right.
applyH
应用指定假设到goal或者指定位置
apply.applyHinH0.
eapplyH
自动选择参数应用指定假设
eapplyH.
omega
需要omega库，自动证明加法和不等式
omega.
generalizeH
将H返回到goal中，产生forall
generalizeH.
inversionH
指出H的构造子
inversionH.
inductionn
在n上使用归纳法
inductionn.
casen
将goal中的n分构造子讨论
casen.
auto
自动证明
auto.
autowitharith.
tauto
自动证明布尔逻辑命题
tauto.
assert
指定一个新的假设
assert（H:
P‐>
Q）.
高级技法：
证明即程序：
Definitionhalf（n:
nat）:
{p:
nat&
{n=2*p}+{n=S（2*p）}}.
inductionn.
exists0;
left;
destructIHnas[x[Hx|Hx]].
existsx;
right;
exists（Sx）;
RequireImportArith.
rewriteHx;
ring.
Defined.
PrintsigT.
Computehalf3.
CheckexistT.
Definitionhalf'
（n:
nat）:
nat:
=matchhalfnwithexistTp_=>
pend.
附录1：
Ensemble定义：
LibraryCoq.Sets.Ensembles
SectionEnsembles.
VariableU:
Type.
DefinitionEnsemble:
=U‐>
Prop.
DefinitionIn（A:
Ensemble）（x:
U）:
Prop:
=Ax.
DefinitionIncluded（BC:
Ensemble）:
=forallx:
U,InBx‐>
InCx.
InductiveEmpty_set:
Ensemble:
=.
InductiveFull_set:
Full_intro:
forallx:
U,InFull_setx.
NB:
Thefollowingdefinitionbuilds‐inequalityofelementsinUasLeibnizequality.
ThismayhavetobechangedifwereplaceUbyaSetoidonUwithitsownequalityeqs,withIn_singleton:
（y:
U）（eqsxy）‐>
（In（Singletonx）y）.
InductiveSingleton（x:
In_singleton:
In（Singletonx）x.
InductiveUnion（BC:
|Union_introl:
In（UnionBC）x
|Union_intror:
U,InCx‐>
In（UnionBC）x.
DefinitionAdd（B:
=UnionB（Singletonx）.
InductiveIntersection（BC:
Intersection_intro:
InCx‐>
In（IntersectionBC）x.
InductiveCouple（xy:
|Couple_l:
In（Couplexy）x
|Couple_r:
In（Couplexy）y.
InductiveTriple（xyz:
|Triple_l:
In（Triplexyz）x
|Triple_m:
In（Triplexyz）y
|Triple_r:
In（Triplexyz）z.
DefinitionComplement（A:
=funx:
U=>
~InAx.
DefinitionSetminus（BC:
funx:
InBx/\~InCx.
DefinitionSubtract（B:
=SetminusB（Singletonx）.
InductiveDisjoint（BC:
Disjoint_intro:
（forallx:
U,~In（IntersectionBC）x）‐>
DisjointBC.
InductiveInhabited（B:
Inhabited_intro:
InhabitedB.
DefinitionStrict_Included（BC:
=IncludedBC/\B<
>
C.
DefinitionSame_set（BC:
=IncludedBC/\IncludedCB.
ExtensionalityAxiom
AxiomExtensionality_Ensembles:
forallAB:
Ensemble,Same_setAB‐>
A=B.
EndEnsembles.
HintUnfoldInIncludedSame_setStrict_IncludedAddSetminusSubtract:
sets
v62.
HintResolveUnion_introlUnion_introrIntersection_introIn_singleton
Couple_lCouple_rTriple_lTriple_mTriple_rDisjoint_introExtensionality_Ensembles:
setsv62.
升级会员 