证明辅助工具Coq简介.ppt
证明辅助工具Coq简介,郭宇2010-07-20中科大-耶鲁高可信软件联合研究中心,http:/,课程主页,http:/,问题,如何表示数学证明？,Miracles often occur,费马大定理(1673),Xn=Yn+Zn 当n2时无整数解A.Wiles1993证明?超过一百页世界上能看懂的人屈指可数原始证明有错，一年多以后更正,四色定理,K.Appel&W.Haken 1976年证明证明？分1,936种情况讨论利用计算机程序来自动分析，不产生证明一些数学家拒绝承认仍然难以检查证明是否正确,四色定理,G.Gonthier&B.Werner2004年证明证明？完整详细的Coq证明机器可检查没有跳过任何步骤证明检查程序规模小,高可信软件,嵌入式系统内核seL4G.Klein 等人OSDI09 Best Paper8700 lines of C经过形式化验证证明？机器可检查证明200,000 lines of Isabelle script,VeriSoft,芯片嵌入式内核汽车电子控制单元应用宝马汽车的应急呼叫系统证明：Isabelle 2005,CompCert,经过完全证明的C语言编译器Xavier Leroy CACM 09Power PC backend证明？机器可检查证明使用Coq代码编写并证明抽取出OCaml代码运行,Certified Software,Certified Software=Program+Proof,Coq是什么,一个证明系统编写证明，检查证明一套形式化语言编写数学定义、算法、定理类型化 演算一个环境交互式证明,其它证明辅助工具,Isabelle 2005TwelfAgda,Coq介绍,Coq环境函数式编程逻辑推理归纳,运行 coq,命令行解释器coqtop编译器 coqc,用户界面,CoqIDE,用户界面,emacs+proofgeneral(推荐),运行 Coq,运行 coqtop检查一个表达式的类型Coq Check 3.3:natCoq Check 3+5.3+5:nat,Coq 命令(以.结尾),类型检查,每一个合式的项都有一个类型每一个类型也是一个项 Check 3+true.Error:The term“true”has type“bool”While it is expected to have type“nat”.,定义,Definition a:=5.a is defined Definition b:=a+6.b is defined Eval compute in b.=11:nat,Coq 命令打印,Coq Print b.b=a+6:natCoq Set Printing All.Coq Print b.b=plus a(S(S(S(S(S(S O):nat,自然数加法,Coq nat-natCoq Unset Printing All.Coq Eval compute in(plus 7 8).=15:nat,自然数加法,Coq m|S p=S(plus p m)end:nat-nat-natArgument scopes are nat_scope nat_scope,函数式语言编程,函数式语言编程,函数是一等公民First-class可以做参数，也可以作为函数返回值高阶函数,示例一：布尔值计算,Coq Inductive bool:Set:=true:bool|false:bool.bool is definedbool_rect is definedbool_ind is definedbool_rec is definedCoq Print bool.,示例一：布尔值计算,Coq false|false=true end.Coq Eval compute in(negb true).,示例一：布尔值计算,Coq b|false=false end.Coq Eval compute in(andb true false).,示例一：布尔值计算,Coq b|false=false end.Coq Check(andb).Coq Check(andb true).,示例一：布尔值计算,Coq bool:=match a with|true=fun(b:bool)=b|false=fun(b:bool)=false end.Coq Check(andb).Coq Check(andb true).,示例一：布尔值计算,Coq bool):bool-bool:=fun(a:bool)=f(f a).Coq Eval compute in(double negb true).,示例二：自然数,Coq nat.nat is definednat_rect is definednat_ind is definednat_rec is defined,偶数判定,Fixpoint evenb(n:nat):bool:=match n with|O=true|S O=false|S(S n)=evenb n end.,加法,原始递归函数（Primitive Recursion）保证函数的终止性,Fixpoint plus(n:nat)(m:nat)struct n:nat:=match n with|O=m|S n=S(plus n m)end.,基本逻辑推理,原子命题定义,Variables A B C:Prop.,定理证明演示,Theorem T1:A-A.,证明构造的编程,打印证明,Theorem T1:A-A.Coq H:A-A,Curry-Howard 同构类型形如 A-B 的证明是一个函数以命题A的证明为参数，返回B的证明,程序即证明,Definition T1:=fun(H:A)=H.Check T1.,程序即证明,Definition T1:=fun(H:A)=T1 H.Check T1.,证明的构造方式并不唯一构造 Construction,Definition T1:=fun(H:A)=H.Check T1.,练习,Theorem T2:A-B-A.Proof?,答案,Theorem T2:A-B-A.Proof fun(H:A)=fun(H2:B)=H.,T2是定理 A-B-A 的“构造”,合取连接词,Theorem T3:A/B-A.Proof fun(H:A/B)=(proj1 H).,Theorem T4:A/B-B.Proof fun(H:A/B)=(proj2 H).,析取连接词,Theorem T6:A/B-A/B.Proof?,Theorem T5:A-A/B.Proof fun(H:A)=or_intro1 H.,析取连接词,Theorem T6:A/B-A/B.Proof fun(H:A/B)=T5(T3 H).,Theorem T5:A-A/B.,Theorem T3:A/B-A.,全称量词,Theorem T7:forall A:Prop,A-A.,Curry-Howard 同构类型形如 forall x:A,B 的证明仍然是一个函数以 x 为参数，返回B的证明,全称量词,Theorem T7:forall A:Prop,A-A.Proof fun(A:Prop)=fun(x:A)=x.,【思考】下面证明构造的含义：Definition T4:=T3(forall A:Prop,A),全称量词,Theorem T7:forall A:Prop,A-A.,【思考】下面证明构造的含义：Definition T8:=T7(forall A:Prop,A),T8:False-False,练习,Theorem T9:forall A B C:Prop,(A-B)-(B-C)-(A-C).Proof?.,函数复合,归纳,归纳谓词,Inductive EqNat:nat-nat-Prop:=|OEq:EqNat O O|SEq:forall m n:nat,EqNat m n-EqNat(S m)(S n).,P(m,n)iff m=n,归纳谓词,问题：证明 EqNat 0 0?写出类型为EqNat 0 0的证明构造答案：OEq,Lemma LEqNat1:EqNat O O.Proof OEq.,Definition LEqNat1:EqNat O O:=OEq.,归纳谓词,问题：证明 EqNat 1 1?写出类型为EqNat 1 1的证明构造,Lemma LEqNat1:EqNat 1 1.Proof(SEq 0 0 LEqNat0).,Definition LEqNat1:EqNat O O:=(SEq 0 0 LEqNat0).,Inductive EqNat:nat-nat-Prop:=|OEq:EqNat O O|SEq:forall m n:nat,EqNat m n-EqNat(S m)(S n).,归纳谓词,练习：证明 EqNat 2 2?,Inductive EqNat:nat-nat-Prop:=|OEq:EqNat O O|SEq:forall m n:nat,EqNat m n-EqNat(S m)(S n).,归纳谓词,问题：证明 forall n,EqNat n n?,Definition LEqNatn:forall n,EqNat n n:=?,Inductive EqNat:nat-nat-Prop:=|OEq:EqNat O O|SEq:forall m n:nat,EqNat m n-EqNat(S m)(S n).,归纳谓词,问题：证明 forall n,EqNat n n?答案：递归函数,Fixpoint LEqNatn(n:nat):EqNat n n:=match n return(EqNat n n)with|O=OEq|S n=SEq n n(LEqNatn n)end.,Inductive EqNat:nat-nat-Prop:=|OEq:EqNat O O|SEq:forall m n:nat,EqNat m n-EqNat(S m)(S n).,归纳谓词,问题：证明 forall n,EqNat n n?交互式证明（演示）,Lemma LEqNatn:forall n,EqNat n n.,归纳谓词,交互式证明产生的证明构造？,LEqNatn=fun n:nat=nat_ind(fun n0:nat=EqNat n0 n0)OEq(fun(n0:nat)(IHn:EqNat n0 n0)=SEq n0 n0 IHn)n:forall n:nat,EqNat n n,Print LEqNatn.,Lemma LEqNatn:forall n,EqNat n n.,通用归纳原理,nat_rect=fun(P:nat-Type)(f:P 0)(f0:forall n:nat,P n-P(S n)=fix F(n:nat):P n:=match n as n0 return(P n0)with|0=f|S n0=f0 n0(F n0)end:forall P:nat-Type,P 0-(forall n:nat,P n-P(S n)-forall n:nat,P n,nat_ind=fun P:nat-Prop=nat_rect P:forall P:nat-Prop,P 0-(forall n:nat,P n-P(S n)-forall n:nat,P n,Coq&CIC,CC:Calculus of ConstructionsCiC:Calculus of Inductive Constructions,Coq不能做什么,Coq不能自动给出问题的形式化描述我们要明确问题，并形式化问题Coq不能自动证明出所有定理给出证明思路Coq不能直接证明程序只是一个基础而且底层的逻辑工具需要开发更多更有效的基于Coq的工具,我们用Coq做什么,内核原型150 lines of assembly code 证明：82,000 lines of coq scriptsMachine modelSafety policySpecificationsLogics&their soundness proofCode safety proof,谢谢,逻辑推理与计算,莱布尼兹之梦罗素悖论希尔伯特计划哥德尔定理图灵机与 演算,Lambda Cube,2,P,P,P2,P,
