Coq/SSReflect/MathComp による定理証明サンプルページこの本の定価判型などは, 以下の URL からご覧いただけます. このサンプルページの内容は, 初版 1 刷発行時のものです.

Size: px

Start display at page:

Download "Coq/SSReflect/MathComp による定理証明サンプルページこの本の定価判型などは, 以下の URL からご覧いただけます. このサンプルページの内容は, 初版 1 刷発行時のものです."

やすもりいさやま
5 years ago
Views:

2 Coq/SSReflect/MathComp による定理証明サンプルページこの本の定価判型などは, 以下の URL からご覧いただけます. このサンプルページの内容は, 初版 1 刷発行時のものです.

4 i Coq/SS- Reflect/MathComp 1 1 Coq/SSReflect/MathComp

5 ii 1 Coq/SSReflect/MathComp

6 iii 1 Coq/SSReflect/MathComp Coq/SSReflect/MathComp Microsoft Windows Coq/SSReflect/MathComp move=>, move:, move: =>, move/ apply, apply=>, apply:, apply: =>, apply/ case, case:, case=>, case: =>, case=> [ ], case/ elim, elim:, elim=>, elim: =>, elim=> [ ] rewrite move/, apply/, case/ have suff wlog Definition, Lemma, Theorem, Corollary, Fact, Proposition, Remark, Proof, Qed, Fixpoint Compute Check About Print Search Locate Abort Admitted Variable(s) Hypothesis Axiom Inductive 117

7 iv 3.15 Record Canonical Coq split left right exists MathComp ssrbool.v bool eqtype.v eqtype ssrnat.v SSReflect nat seq.v seq fintype.v bigop.v fintype finset Infotheo

8 1 1 Coq/SSReflect/MathComp Coq SSReflect MathComp Coq/SSReflect/MathComp

9 2 1 Coq/SSReflect/MathComp 1.1 Coq/SSReflect 1 /MathComp 1 Coq SSReflect MathComp Coq/SSReflect/ MathComp Coq/SSReflect/MathComp Coq/SSReflect/MathComp SSReflect 2 SSReflect Coq 1.1 Coq move=> A B C. forall A B C : Prop, (A -> B) /\ (B -> C) -> (A -> C) move=> A B C. A, B, C : Prop (A -> B) /\ (B -> C) -> (A -> C) 1.1 move=> A B C 1 2 Ssreflect Small Scale Reflection SSReflect

10 SSReflect A, B, C (A B) (B C) (A C) SSReflect forall A B C : Prop, (A -> B) /\ (B -> C) -> (A -> C). Proof. A, B, C move=> A B C. (A B) (B C) (A B) (B C) A B Hyp1 B C Hyp2 A C A Hyp3 C Hyp2 B B Hyp1 A A Hyp3 case. move=> Hyp1. move=> Hyp2. move=> Hyp3. apply: Hyp2. apply: Hyp1. by []. Qed. SSReflect 1.1 SSReflect SSReflect

11 4 1 Coq/SSReflect/MathComp Coq SSReflect INRIA Coq/SSReflect 15 7 MathComp Coq SSReflect 2 Coq, SSReflect Coq ACM (Association for Computing Machinery) 2013 ACM ACM SIGPLAN SSReflect 2011 EADS Georges Gonthier, 1962 Vladimir Voevodsky, EADS

12 Flyspeck Formal Proof of Kepler Conjecture IT C CompCert sel4 1 2 Johannes Kepler, Thomas Hales, 1958

13 6 1 Coq/SSReflect/MathComp Coq/SSReflect/MathComp ICT

14 1.2 7 Coq/SSReflect Coq/SSReflect Coq Coq Mizar 1 HOL Light 2 Agda Isabelle 3 Mizar a : A A a Mizar: HOL Light: Isabelle: Ernst Zermelo, Bertrand Russell, int, float

15 8 1 Coq/SSReflect/MathComp a A a A a A 1 a : A A a A B 1.2 A B A + B A B A B Σx : A, B A B A B Πx : A, B A B x A, B(x) Πx : A, B(x) A x B(x) x A, B(x) Σx : A, B(x) A x B(x) A B A + B A + B A B A + B A B A + B A B A B A + B B + A B + A b : B a : A A B Σx : A, B Σx : A, B (a, b) a : A b : B A B A, B A B A, B Σx : A, B Σx : A, B A, B A B 1 a A a : A a i A int i : int

16 25 2 Coq/SSReflect/MathComp Coq/SSReflect/MathComp

17 Coq 2.1 CoqIDE Proof General Coq Coq 2.1 P, Q : Prop Hyp : P P Q Prop Hyp P -> forall 1 -> 2.1 (P -> Q) -> P (P -> Q), P 2.1 1

18 Coq/SSReflect/MathComp Coq/SSReflect/MathComp CoqIDE From mathcomp Require Import ssreflect. Section ModusPonens. Variables X Y : Prop. Hypothesis XtoY_is_true : X -> Y. Hypothesis X_is_true : X. Theorem MP : Y. Proof. move: X_is_true. by []. Qed. End ModusPonens. Coq CoqIDE Coq 1 Coq 1

28 2 2.2 CoqIDE [Loading ML file ssreflect.cmxs.

19 CoqIDE [Loading ML file ssreflect.cmxs... done] Coq SSReflect From mathcomp Require Import mathcomp ssreflect Coq SSReflect ssreflect div From mathcomp Require Import ssreflect div. From mathcomp Require Import ssreflect. From mathcomp Require Import div. 1 Section ModusPonens. Section ModusPonens End 1 Variables X Y : Prop. X is assumed Y is assumed

20 Variables 1 ModusPonens X, Y Variable Variable :. Variables... :. 2 X Y Prop Coq/SSReflect/MathComp 1 Hypothesis XtoY_is_true : X -> Y. XtoY_is_true is assumed Hypothesis X -> Y XtoY_is_true X Y > -> - > Coq X -> Y X -> Y X -> Y 1 X X_is_true 1 Theorem MP : Y. 1 2 Variables Variable Coq Variable Variables A E Variables A B... E Variables A B C D E

21 subgoal X, Y : Prop XtoY_is_true : X -> Y X_is_true : X (1/1) Y 1 Theorem Theorem... :. MP Y subgoal Theorem 4 subgoals X, Y : Prop X Y Prop Variable XtoY_is_true : X -> Y X_is_true : X Hypothesis (1/1) n / m 2.1 Coq X, Y : Prop XtoY_is_true : X -> Y X_is_true : X Y X, Y X Y X Y 1 Coq

22 SSReflect

23 From mathcomp 2 Require Import all_ssreflect. 3 4 Set Implicit Arguments. 5 Unset Strict Implicit. 6 Import Prenex Implicits. 1 2 MathComp SSReflect Coq 7 8 Definition myset (M : Type) := M -> Prop. 9 Definition belong {M : Type} (A : myset M) (x : M) : 10 Prop := A x. 11 Notation "x A" := (belong A x) (at level 11). 12 Axiom axiom_myset : forall (M : Type )( A : myset M), 13 forall (x : M), (x A) \/ ~(x A). x Coq/SSReflect M : Type mother set M M M -> Prop myset M myset M M -> Prop Coq Coq Sets.Ensembles Ensemble M A : myset M

24 x : M A A x (A x) belong A x A x : Prop x A belong A x A x : Prop belong { } {M : Type} { } Coq myset (M : Type) := M -> Prop x x A x / A myset T axiom_myset Definition myemptyset {M : Type} : myset M := fun _ => False. 16 Definition mymotherset {M : Type} : myset M := fun _ => True. myemptyset mymotherset x : M (x myemptyset) x : M x mymotherset 5.2 A, B A B x A x B mysub M -> mysub M -> Prop mysub M Prop mysub Definition mysub {M} := fun (A B : myset M) => 19 (forall (x : M), (x A) -> (x B)). 20 Notation "A B" := (mysub A B) (at level 11).

25 Section. 23 Variable M : Type Lemma Sub_Mother (A : myset M) : A mymotherset. 26 Proof. by []. Qed Lemma Sub_Empty (A : myset M) : myemptyset A. 29 Proof. by []. Qed Lemma rfl_sub (A : myset M) : (A A). 32 Proof. by []. Qed Lemma transitive_sub (A B C : myset M): 35 (A B) -> (B C) -> (A C). 36 Proof. by move=> H1 H2 t H3; apply: H2; apply: H1. Qed End. 2 Section M : Type Variable mysub Sub Sub_Mother mysub mymotherset Sub_Empty rfl_sub reflexivity rfl transitive_sub 1 A, B A = B A B B A Coq myset {M : Type} A = B A B B A

26 rewrite rfl_sub Definition eqmyset {M : Type }:= 41 fun (A B : myset M) => (A B /\ B A). 42 Axiom axiom_exteqmyset : forall {M : Type} (A B : myset M), 43 eqmyset A B -> A = B. axiom_exteqmyset Section. 46 Variable Mother : Type Lemma rfl_eqs (A : myset Mother) : A = A. 49 Proof. by []. Qed Lemma sym_eqs (A B : myset Mother) : A = B -> B = A. 52 Proof. move=> H. by rewrite H. Qed End. eq S myset eqs sym symmetry Definition mycomplement {M : Type} (A : myset M) : myset M := 57 fun (x : M) => ~(A x). 58 Notation "A ^c" := ( mycomplement A) (at level 11) Definition mycup {M : Type} (A B : myset M) : myset M := 61 fun (x : M) => (x A) \/ (x B). 62 Notation "A B" := (mycup A B) (at level 11). mycomplement A x A c

27 162 5 mycup \/ A B Section. 65 Variable M : Type Lemma cempty_mother : (@myemptyset M)^c = mymotherset. 68 Proof. 69 apply: axiom_exteqmyset; rewrite / eqmyset. 70 by apply: conj; rewrite / mysub / mycomplement // => x Hfull. 71 Qed Lemma cc_cancel (A : myset M) : (A^c)^c = A. 74 apply: axiom_exteqmyset; rewrite / eqmyset. 75 apply: conj; rewrite / mysub / mycomplement => x H //. 76 by case: ( axiom_myset A x). 77 Qed Lemma cmother_empty : (@mymotherset M)^c = myemptyset. 80 Proof. by rewrite - cempty_mother cc_cancel. Qed. M Coq Error: Cannot infer the implicit parameter M of mycomplement whose type is "Type" in environment: M : Type M myemptyset M M M Coq Lemma mycupa (A B C : myset M) : (A B) C = A (B C). 83 Proof.

28 apply: axiom_exteqmyset. 85 rewrite / eqmyset / mysub. 86 apply: conj => x [H1 H2]. 87 -case: H1=> t. 88 +by apply: or_introl. 89 +by apply: or_intror; apply: or_introl. 90 -by apply: or_intror; apply: or_intror. 91 -by apply: or_introl; apply: or_introl. 92 -case: H2=> t. 93 +by apply: or_introl; apply: or_intror. 94 +by apply: or_intror. 95 Qed Lemma myunioncompmother (A : myset M) : A (A^c) = mymotherset. 98 Proof. 99 apply: axiom_exteqmyset; rewrite / eqmyset / mysub; apply: conj => [x x HM] by case by case: ( axiom_myset A x); [ apply: or_introl apply: or_intror ]. 102 Qed. 103 End. mycupa myunioncompmother or_intror or_introl Definition mymap {M1 M2 : Type} (A : myset M1) (B : myset M2) 106 (f : M1 -> M2) 107 := (forall (x : M1), (x A) -> ((f x) B)). 108 Notation "f Map A \to B" := (mymap A B f) (at level 11).

29 'H 204 Abort 113 About 104 addn 43 addn1 44 addnc 45 Admitted 114 and 57, 76 apply/ 89 apply: 36, 73 apply: => 73 apply=> 73 Axiom 116 by 32 Canonical 120 case 58 case: 60 case => 59 case/ 90 case=> [ ] 78 Check 37, 103 CoInductive 201 Compute 102 coqc 204 Corollary 101 Defined 101 Definition 100 do 201 elim 79 End 32, 64 eq 43 exists 77, 123 Fact 101 field 201 Fixpoint 47, 101 Goal 56 H2 204 have 98 Hypothesis 29, 115 if 47 implicit 46 Inductive 42, 117 left 123 Lemma 101 Locate 110 Ltac 201 match with 43 move=> // 48 move/ 87 move: 31, 70 move: => 71 move=> 36, 69 move/ 55 Nat.add 43 O 42 or 76 Print 42, 105 Proof 31, 101 Proposition 101 Qed 32, 101 R 200 Record 118 Remark 101 Require Import 28, 205 rewrite 44, 82 rewrite /= 83 rewrite ( : = ) 49 rewrite / 54 right 123 S 42 Search 105 Section 28 Shift Ctrl C 44 Shift Ctrl P 41 split 123 suff 98 sum 47 Theorem 30, 101 Variable 114 wlog: 99 bigop 150 eqtype 131 fingroup 184, 192 finset 169 fintype 146, 166 Infotheo 196 Reals 200 seq 138 ssrbool 76, 126 ssrfun 46 ssrnat 41, 134 bool 75, 92 eqtype 131 False 77 list 124 nat 41, 77 Prop 29, 92, 117 seq 138 Set 117, 174 True 77 Type 117.vo AUTOMATH 10 Calculus of Constructions 14 Calculus of Inductive Constructions 14 CompCert 23 Coq 2 Coq/SSReflect/MathComp 2

30 211 CoqIDE 23 Coq 23 Display Notations 42 emacs 23 Gallina 14 itext4capofchans 203 MathComp 4 modus ponens 10 Open Scope 184 SSReflect 2 subgoal 30 System F , , , 42, 74, , 3, , 30 26, , , , , , 31, , 7 2, , , , ,

31 /4 2012/3 Research Scholar 2011/3 2012/ Reynald Affeldt 1976 = = 2000 Ingénieur Civil des Mines Coq/SSReflect/MathComp c FAX Printed in Japan ISBN

「計算と論理」 Software Foundations その4

「計算と論理」 Software Foundations その4 Software Foundations 4 cal17@fos.kuis.kyoto-u.ac.jp http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/cal/ November 7, 2017 ( ) ( 4) November 7, 2017 1 / 51 Poly.v ( ) ( 4) November 7, 2017 2 / 51 : (

Coq/SSReflect/MathComp による定理証明 サンプルページ この本の定価 判型などは, 以下の URL からご覧いただけます. このサンプルページの内容は, 初版 1 刷発行時のものです.

Coq/SSReflect/MathComp による定理証明サンプルページこの本の定価判型などは, 以下の URL からご覧いただけます. このサンプルページの内容は, 初版 1 刷発行時のものです.