证明辅助工具Coq简介.ppt
证明辅助工具Coq简介郭宇2010-07-20中科大-耶鲁高可信软件联合研究中心http:/summer-school 课程主页http:/summer-school 问题如何表示数学证明？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 scriptVeriSoft芯片嵌入式内核汽车电子控制单元应用宝马汽车的应急呼叫系统证明：Isabelle 2005CompCert经过完全证明的C语言编译器Xavier Leroy CACM 09Power PC backend证明？机器可检查证明使用Coq代码编写并证明抽取出OCaml代码运行Certified SoftwareCertified Software=Program+ProofCoq是什么一个证明系统编写证明，检查证明一套形式化语言编写数学定义、算法、定理类型化 演算一个环境交互式证明其它证明辅助工具Isabelle 2005TwelfAgdaCoq介绍Coq环境函数式编程逻辑推理归纳运行 coq命令行解释器coqtop编译器 coqc用户界面CoqIDE用户界面emacs+proofgeneral(推荐)运行 Coq运行 coqtop检查一个表达式的类型Coq Check 3.3:natCoq 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 Inductive bool:Set:=true:bool|false:boolCoq false|false=true end.Coq Eval compute in(negb true).示例一：布尔值计算Coq Inductive bool:Set:=true:bool|false:boolCoq b|false=false end.Coq Eval compute in(andb true false).示例一：布尔值计算Coq Inductive bool:Set:=true:bool|false:boolCoq b|false=false end.Coq Check(andb).Coq Check(andb true).示例一：布尔值计算Coq Inductive bool:Set:=true:bool|false:boolCoq 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偶数判定FixpointFixpoint 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-ACurry-Howard 同构类型形如 A-B 的证明是一个函数以命题A的证明为参数，返回B的证明程序即证明Definition T1:=fun(H:A)=H.Check T1.程序即证明Definition T1:=fun(H:A)=T1 H.Check T1.证明的构造方式并不唯一构造 ConstructionDefinition 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的证明构造答案：OEqLemma 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 LEqNatnLEqNatn(n:nat):EqNat n n:=match n return(EqNat n n)with|O=OEq|S n=SEq n n(LEqNatnLEqNatn 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=LEqNatn=fun n:nat=fun n:nat=nat_ind(fun n0:nat=EqNat n0 n0)OEqnat_ind(fun n0:nat=EqNat n0 n0)OEq (fun(n0:nat)(IHn:EqNat n0 n0)=SEq n0 n0 IHn)n (fun(n0:nat)(IHn:EqNat n0 n0)=SEq n0 n0 IHn)n :forall n:nat,EqNat n n :forall n:nat,EqNat n nPrint LEqNatn.Print LEqNatn.Lemma LEqNatn:forall n,EqNat n n.Lemma LEqNatn:forall n,EqNat n n.通用归纳原理nat_rect=nat_rect=fun(P:nat-Type)(f:P 0)(f0:forall n:nat,P n-P(S n)=fun(P:nat-Type)(f:P 0)(f0:forall n:nat,P n-P(S n)=fix F(n:nat):P n:=fix F(n:nat):P n:=match n as n0 return(P n0)with match n as n0 return(P n0)with|0=f|0=f|S n0=f0 n0(F n0)|S n0=f0 n0(F n0)end end :forall P:nat-Type,:forall P:nat-Type,P 0-(forall n:nat,P n-P(S n)-forall n:nat,P n P 0-(forall n:nat,P n-P(S n)-forall n:nat,P nnat_ind=nat_ind=fun P:nat-Prop=nat_rect Pfun P:nat-Prop=nat_rect P :forall P:nat-Prop,:forall P:nat-Prop,P 0-(forall n:nat,P n-P(S n)P 0-(forall n:nat,P n-P(S n)-forall n:nat,P n -forall n:nat,P nCoq&CICCC:Calculus of ConstructionsCiC:Calculus of Inductive ConstructionsCoq不能做什么Coq不能自动给出问题的形式化描述我们要明确问题，并形式化问题Coq不能自动证明出所有定理给出证明思路Coq不能直接证明程序只是一个基础而且底层的逻辑工具需要开发更多更有效的基于Coq的工具我们用Coq做什么内核原型150 lines of assembly code 证明：82,000 lines of coq scriptsMachine modelSafety policySpecificationsLogics&their soundness proofCode safety proof谢谢逻辑推理与计算莱布尼兹之梦罗素悖论希尔伯特计划哥德尔定理图灵机与 演算Lambda Cube2PPP2P
