证明辅助工具Coq简介ppt课件

1、郭宇2021-07-20中科大-耶鲁高可信软件结合研讨中心/summer-school /summer-school 如何表示数学证明？ Miracles often occurXn = Yn + Zn 当n2时无整数解A. Wiles1993证明?超越一百页世界上能看懂的人屈指可数原始证明有错，一年多以后更正K. Appel & W. Haken 1976年证明证明？分1,936种情况讨论利用计算机程序来自动分析，不产生证明一些数学家回绝成认依然难以检查证明能否正确G. Gonthier & B. Werner2

2、004年证明证明？完好详细的Coq证明机器可检查没有跳过任何步骤证明检查程序规模小嵌入式系统内核seL4G. Klein 等人OSDI09 Best Paper8700 lines of C经过方式化验证证明？机器可检查证明200,000 lines of Isabelle script芯片嵌入式内核汽车电子控制单元运用宝马汽车的应急呼叫系统证明：Isabelle 2005经过完全证明的C言语编译器Xavier Leroy CACM 09Power PC backend证明？机器可检查证明运用Coq代码编写并证明抽取出OCaml代码运转Certified Software = Program

3、+ Proof一个证明系统编写证明，检查证明一套方式化言语编写数学定义、算法、定理类型化 演算一个环境交互式证明Isabelle 2005TwelfAgdaCoq环境函数式编程逻辑推理归纳命令行解释器coqtop编译器 coqcCoqIDEemacs + proofgeneral(引荐)运转 coqtop检查一个表达式的类型Coq Check 3.3 : natCoq Check 3 + true.Error: The term “true has type “boolWhile it is expected to have type “nat. Definition a := 5.a is

4、defined Definition b := a + 6.b is defined Eval compute in b. = 11 : nat Coq Print b.b = a + 6 : natCoq Set Printing All.Coq Print b.b = plus a (S (S (S (S (S (S O) : natCoq nat - natCoq Unset Printing All.Coq Eval compute in (plus 7 8). = 15 : natCoq m | S p = S (plus p m) end : nat - nat - natArgu

5、ment 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.C

6、oq 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

7、 : 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 defin

8、ednat_rec is definedFixpoint evenb (n:nat) : bool := Fixpoint evenb (n:nat) : bool := match n with match n with | O = true | O = true | S O = false | S O = false | S (S n) = evenb n | S (S n) = evenb n end. end. 原始递归函数Primitive Recursion保证函数的终止性Fixpoint plus (n : nat) (m : nat) struct n: nat := matc

9、h 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

10、 (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

11、/ 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) =

12、 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 - FalseTheorem T9 : forall A B C: Prop, (A - B) - (B - C) - (A - C).Proof ?. 函数复合Inductive EqNat : nat - nat - Prop := | OEq : E

13、qNat 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 LE

14、qNat1 : 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, EqNa

15、t 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 (L

16、EqNatn 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_i

17、nd (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

18、.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) -