证明辅助工具Coq简介.ppt

证明辅助工具Coq简介,郭宇 2010-07-20 中科大-耶鲁高可信软件联合研究中心,/summer-school,课程主页,/summer-school,问题,如何表示数学证明？,Miracles often occur,费马大定理 (1673),Xn = Yn + Zn 当n2时无整数解 A. Wiles 1993 证明? 超过一百页 世界上能看懂的人屈指可数 原始证明有错，一年多以后更正,四色定理,K. Appel & W. Haken 1976年证明 证明？ 分1,936种情况讨论 利用计算机程序来自动分析，不产生证明 一些数学家拒绝承认 仍然难以检查证明是否正确,四色定理,G. Gonthier & B. Werner 2004年证明 证明？ 完整详细的Coq证明 机器可检查 没有跳过任何步骤 证明检查程序规模小,高可信软件,嵌入式系统内核seL4 G. Klein 等人 OSDI09 Best Paper 8700 lines of C 经过形式化验证 证明？ 机器可检查证明 200,000 lines of Isabelle script,VeriSoft,芯片 嵌入式内核 汽车电子控制单元 应用 宝马汽车的应急呼叫系统 证明： Isabelle 2005,CompCert,经过完全证明的C语言编译器 Xavier Leroy CACM 09 Power PC backend 证明？ 机器可检查证明 使用Coq代码编写并证明 抽取出OCaml代码运行,Certified Software,Certified Software = Program + Proof,Coq是什么,一个证明系统 编写证明，检查证明 一套形式化语言 编写数学定义、算法、定理 类型化 演算 一个环境 交互式证明,其它证明辅助工具,Isabelle 2005 Twelf Agda,Coq介绍,Coq环境 函数式编程 逻辑推理 归纳,运行 coq,命令行解释器 coqtop 编译器 coqc,用户界面,CoqIDE,用户界面,emacs + proofgeneral(推荐),运行 Coq,运行 coqtop 检查一个表达式的类型 Coq Check 3. 3 : nat Coq 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 : nat Coq Set Printing All. Coq Print b. b = plus a (S (S (S (S (S (S O) : nat,自然数加法,Coq nat - nat Coq Unset Printing All. Coq Eval compute in (plus 7 8). = 15 : nat,自然数加法,Coq m | S p = S (plus p m) end : nat - nat - nat Argument scopes are nat_scope nat_scope,函数式语言编程,函数式语言编程,函数是一等公民 First-class 可以做参数，也可以作为函数返回值 高阶函数,示例一：布尔值计算,Coq Inductive bool : Set := true : bool | false : bool. bool is defined bool_rect is defined bool_ind is defined bool_rec is defined Coq 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 defined nat_rect is defined nat_ind is defined nat_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 -