定理証明支援系Coqにおける手続き的証明から宣言的証明への変換

(1)

1631156 Coq Coq Coq C-zar C-zar Coq Coq C-zar Matita 1 C-zar 1 C-zar

(2)

29 Coq

: 1631156

:

: 2018

3

13

(3)

Coq Coq C-zar C-zar Coq Coq C-zar Matita 1 C-zar 1 C-zar

(4)

1 1 2 Coq 7 2.1 . . . 7 2.2 Coq . . . 10 3 C-zar 13 3.1 . . . 13 3.2 C-zar . . . 14 3.3 . . . 15 4 18 4.1 . . . 18 4.2 . . . 21 4.3 . . . 23 4.4 . . . 24 5 29 5.1 . . . 29 5.2 . . . 30 5.3 . . . 35 6 37 7 38 40 41 : 45

(5)

1

[1] [2] [3] [4] INRIA Coq [5] [6] [7] C [8] LLVM [9] Why3/Frama-C [10] Spoofax [11] Coq Coq Coq 2 Coq ∀x∀y, (x + 1) + y = x + (y + 1) 1.1 Coq 1.1 x 4 x= 0 5 7 x= S x′ (x′+ 1 ) 1.1

4. intros: forall x y:nat, x:nat y:nat

(S x) + y = x + (S y) 5. induction x: x (S 0) + y = x + (S y) (S (S x’)) + y = (S x’) + (S y) 6. reflexivity: x = 0 (S 0) + y = x + (S y) 7. simpl: x = S x’

(6)

1.1 Coq

1 Goal forall x y : nat,

2 S x + y = x + S y. 3 Proof. 4 intros. 5 induction x. 6 reflexivity. 7 simpl. 8 f_equal. 9 apply IHx. 10 Qed. 1.2

1 Goal forall x y : nat, S x + y = x + S y. 2 Proof. 3 intros. 4 induction x as [| _ kinou]. 5 all: swap 1 2. 6 simpl. 7 f_equal. 8 apply kinou. 9 reflexivity. 10 Qed. S (S (x’ + y)) = S (x’ + (S y)) 8. f_equal: S S (x’ + y) = x’ + (S y)

9. apply IHx: (IHx)

S (x’ + y) = x’ + (S y) x S x’ x 0 kinou 1.1 1.2 5 2 6 8 10 4 1.1 Coq 1 Coq Coq induction 1 Coq Coq

(7)

1.3 Coq

1 Goal forall x y : nat, S x + y = x + S y. 2 Proof.

3 intros x y.

4 induction x.

5 - reflexivity. (* x = 0 *)

6 - simpl. f_equal. apply H. (* x = S x’ *) 7 Qed.

1.4 C-zar

1 Goal forall x y : nat, S x + y = x + S y. 2 proof.

3 let x:nat, y:nat.

4 per induction on x.

5 suppose it is O.

6 thus (0 + S y = 0 + S y) by Nat.add using reflexivity.

7 suppose it is (S x’) and IHx:(S x’ + y = x’ + S y).

8 have (S (S (x’ + y)) = S (x’ + S y)) by IHx using f_equal.

9 hence (S (S x’) + y = S x’ + S y) using simpl.

10 end induction. 11 end proof. 12 Qed. 1.1 3 x y 5 6 induction 2 1.2 6

Coq C-zar [12] C-zar

Coq8.1 Coq8.3

Mathemat-ical Proof Language C-zar

C-zar C-zar

1.4 1.1

1.4

(8)

1.5 C-zar

1 Goal forall x y : nat, S x + y = x + S y. 2 proof.

3 let x:nat, y:nat.

4 per induction on x.

5 suppose it is (S x’) and kinou:(S x’ + y = x’ + S y).

6 have (S (S (x’ + y)) = S (x’ + S y)) by kinou using f_equal.

7 hence (S (S x’) + y = S x’ + S y) using simpl.

9 thus (0 + S y = 0 + S y) by Nat.add using reflexivity.

10 end induction.

11 end proof. 12 Qed.

2. proof: C-zar

3. let x:nat, y:nat: forall x y, x:nat y:nat

4. per induction on x: x 5. suppose it is O: x = 0

6. thus by Nat.add using reflexivity: 7. suppose it is (S x’): x = S x’

8. have by IHx using f_equal: S

9. hence using simpl: 10. end induction:

11. end proof: C-zar C-zar C-zar 1.4 1.2 1.5 IHx kinou Whiteside [13] [14] IDE

(9)

1.5

C-zar Coq Coq8.7 C-zar

Coq C-zar [15] [16] [17] C-zar Coq C-zar Coq Matita [18] Coen [19] Coq Matita Coen Coen 1 1 1 Coen

(10)

Coen 2 Coq ( ) Coq 3 C-zar 4 3 5 6 7

(11)

2 Coq

Coq [5] INRIA 1984 [20] Ltac Coq Coq

2.1

Coq [20] Coq forall P, P → P P P P P P P Coq Coq

Coq Gallina Gallina

0 nat nat

Set Gallina 2.1 x

c

fun (x:nat) ⇒ x + 1 fun x ⇒ x + 1 : nat → nat fun x ⇒

x + 1 x nat nat

→ nat

fun x ⇒ (fun y ⇒ ...⇒ t) fun x y ...⇒ t forall x, forall y, ..., t forall x y ..., t

forall A, A → A A

A A 2 fun A (x:A) ⇒ x

Coq

(existential variable)?x

(12)

| fix x0 := t0 with . . . with xi := ti for tj ( )

| cofix x0 := t0 with . . . with xi := ti for tj ( )

✒ ✑ 2.1 Gallina Coq coqtop 2.2 CoqIDE 2.3 2.2 2 2.3 y : nat 1 + y = 0 + S y 1 1 2.2 x, y : nat x:nat y:nat 2 1 2.2 2 subgoal 2 1 ( ) 0 0 1 Coq

(13)

2.2 coqtop 2.3 CoqIDE

H P H ⊢ P

1.1 induction x (fun (x:nat) (y:nat) ⇒

nat_ind (fun x’:nat ⇒ S x’ + y = x’ + S y) ?g1 (fun (x’:nat) (IHx:S x’ + y = x’ + S y) ⇒ ?g2) x)

nat_ind nat 1 2 0 3 S x’ 4 nat_ind ... x S x + y = x + S y ( ) forall x y, S x + y = x + S y ?g1 ?g2 g1 g2 Γ ?g2 ?g1 ?g1 g1 = Γ, x:nat, y:nat ⊢ (S 0) + y = 0 + (S y)

g2 = Γ, x:nat, y:nat, x’:nat, IHx:(S x’ + y = x’ + S y) ⊢ (S (S x’)) + y = (S x’) + (S y)

Γ, x:nat, y:nat ⊢ (S x) + y = x + (S y)

induction x g1 g2 2 Γ,

(14)

2.1 Coq

1 Goal forall x y : nat, S x + y = x + S y. 2 Proof. 3 intros. 4 induction x. 5 reflexivity. 6 simpl. 7 f_equal. 8 apply IHx. 9 Qed.

2.2 Coq

Coq ( ) Coq Coq 1.1 2.1 Coq Goal

Goal Lemma Lemma

Lemma lemma1 (x:nat) : x = x.

x:nat x = x lemma1 Proof Goal Qed intros X → Y forall x:X, Y Y x:X X → Y

(15)

apply H H H X → Y Y X H simpl ⊢ 1 + 1 = 2 simpl ⊢ 2 = 2 2 rewrite H H ⊢ x = y H y = z rewrite H ⊢ x = z f_equal f x = f y f x = y reflexivity x = x destruct x x x n x n induction x x destruct trivial auto firstorder Coq Ltac [21] Ltac 2 ( ) destruct x; auto x

(16)

1.3 5 6 -2 2 1 ( ) Coq Coq Coq

(17)

3 C-zar

C-zar [12] Corbineau Coq

Coq Coq MMode [22]

C-zar C-zar 4 • : • : • : Coq • : Coq C-zar

3.1

Mizar [23] Mizar induction justification (backward proof) C-zar

(forward proof) C-zar

(18)

Isabelle Isar

3.2 C-zar

C-zar proof. proof C-zar Qed proof. end proof.

C-zar C-zar

proof end proof

thus P by ls using tac. hence P by ls using tac.

P by justification tac ls Gallina hence ls tac P firstorder ls tac ls (hence ) tac 1.4 tac ls * P thesis

(19)

have H : P by ls using tac. then H : P by ls using tac.

thus /hence tac P P

P H then hence ls H (hence ) let H : P. H P H ( ) intro H define x as t. t x

claim H : P. end claim.

P H

claim end claim claim

per cases on x. end cases.

per induction on x. end induction.

suppose it is (c t1 ...tn) and H1:P1 and ...and Hm:Pm.

x cases end cases suppose

suppose x c

cases induction suppose

Hi:Pi

3.3

Harrison [26] 2 • • • ( ) •

(20)

Coq coqdoc

coqdoc Coq HTML LA_TEX

[27] coqdoc

Coq Certified Programming with

Dependent Types [28] Software Foundation [29] Coq

C-zar

1 Isabelle IDE jEdit

jEdit 1 ( ) 1 C-zar C-zar C-zar 2 C-zar 1.1 1.4 C-zar 1.5 C-zar 1 3 1 CoqIDE C-zar C-zar

(21)

C-zar

(22)

4

3 Goal Qed 1. 2. ( ) 3. 3 justification 1 C-zar justification C-zar 4.1 1 2 4.2 3 4.3 3 4.2 4.3 4.4 3

4.1

1 3 1.1 1 4.1 4.1 4.2 simpl tac fun x ⇒ ?g1 fun x ⇒ ?g2 x tac ?g1 ?g2 x [g1] [g2] g2 (tac, ?g2 x, [g2]) 3 2

(23)

✓ ✏ [

(intros, fun x y ⇒ ?g1, [g1]), (induction x,

nat_ind (fun x0 ⇒ S x0 + y = x0 + S y) ?g2 (fun x0 IHx ⇒ ?g3) x, [g2, g3]),

(reflexivity, @eq_refl nat (O + S y), []), (simpl, ?g4, [g4]), . . . ] ✒ ✑ 4.1 1 4.2 4.1

T := (hyp, tac, diﬀ , [x1:T1, . . . , xn:Tn])

1 1 1 hyp tac diﬀ subs 4.1 4.3 4.4 4.3 2 1 1 2

(24)

✓ ✏ (true, intros, fun x y ⇒ ?g1, [

?g1:(true, induction x,

nat_ind (fun x0 ⇒ S x0 + y = x0 + S y) ?g2 (fun x0 IHx ⇒ ?g3) x)), [

g2:(false, reflexivity, @eq_refl nat (O + S y), []), g3:(false, simpl, ?g4, [g4: . . . ]) ]) ]) ✒ ✑ 4.3 4.4 4.3 1 B 4.5 Check(diff ) diff diff true/false x::l l x πi i i i+ 1 B′ B 1 π1 B′ B′

(25)

✓ ✏

B(l ) := π1(B′(l ))

B′((tac, diﬀ , [])::l ) := ((false, tac, diﬀ , []), l )

B′((tac, diff , [g])::l ) := ((Check(diff ), tac, diff , [g:π1(B′(l ))]), π2(B′(l )))

B′((tac, diﬀ , [g1,. . . ,gn])::l ) :=

(Check(diﬀ ), tac, diﬀ ,

[g1:π1(B′(l )), g2:π1(B′(π2(B′(l )))), . . . , gn:π1(B′(π2(B′(. . . π2(B′ ! "# $ n−1 (l )). . . ))))], π2(B′(. . . π2(B′ ! "# $ n (l )). . . ))) ✒ ✑ 4.5 2 4.1

1 Goal forall x y z:Prop,

2 (x → y) → (y → z) → (x → z). 3 Proof. 4 intros. 5 apply H0. 6 apply H. 7 apply H1. 8 Qed. 4.2

1 Goal forall x y z : Prop, 2 (x → y) → (y → z) → x → z. 3 proof.

4 let x:Prop, y:Prop, z:Prop,

5 H:(x → y), H0:(y → z), H1:x.

6 have x by H1 using (apply H1).

7 then y by H using (apply H).

8 hence z by H0 using (apply H0).

9 end proof. 10 Qed.

4.2

3 C-zar 4.1 4.2 4.2 4 5 8 7 6 4.1 4 5 6 7

(26)

✓ ✏

F(t ) := proof. F′(t, true) end proof.

F′((false, tac, diff , []), true) := thus Typeof(diff ) by Vars(diff ) using tac. F′((false, tac, diff , []), false) := have Typeof(diff ) by Vars(diff ) using tac. F′((false, tac, diff , [g:x]), true) :=

F′(x, false) hence Typeof(diff ) by Vars(diff ) using tac. F′((false, tac, diff , [g:x]), false) :=

F′(x, false) then Typeof(diﬀ ) by Vars(diﬀ ) using tac.

F′((false, tac, diﬀ , [g1:(t1, d1, sg1), . . . , gn:(tn, dn, sgn)]), true) := (n ≥ 2)

claim H1:Typeof(d1). F′((t1, d1, sg1), true) end claim.

. . .

claim Hn:Typeof(dn). F′((tn, dn, sgn), true) end claim.

thus Typeof(diﬀ ) by Vars(diﬀ ), H1, . . . , Hn using tac.

F′((false, tac, diﬀ , [g1:(t1, d1, sg1), . . . , gn:(tn, dn, sgn)]), false) := (n ≥ 2)

claim H1:Typeof(d1). F′((t1, d1, sg1), true) end claim.

. . .

claim Hn:Typeof(dn). F′((tn, dn, sgn), true) end claim.

have Typeof(diﬀ ) by Vars(diﬀ ), H1, . . . , Hn using tac.

F′((true, tac, diﬀ , subs ), goal ) := F′′(diﬀ , subs, goal )

✒ ✑ 4.6 F F proof end proof F′ F F′ 4.6 Typeof(t ) t Vars(t ) t Hi F′′ 4.3 F′ 2 (

(27)

hyp 2 hyp

F′ subs 2 6 hyp

F′′ tac

(hyp, tac, diﬀ , subs ) subs

H1, . . . , Hn P

thus P by H1, . . . , Hn using tac P tac

H1, . . . , Hn

thus have

then hence claim /end claim

H1, . . . , Hn 1 ( ) subs ( ) 1 1 2 2 ∗ ( ) + 1

4.3

C-zar 1 1 F′′ diﬀ C-zar F′′ 4.7 Select(subs,?x ) subs ?x F′′ have justification by C-zar x let let goal false claim define t

(28)

C-zar

4.4

F

5

4.4.1 claim

have

1 Goal forall A B:Prop, A → B → A∧B. 2 intros. split. apply H. apply H0. 3 Qed.

F

1 Goal forall A B:Prop, A → B → A∧B. proof. 2 let A:Prop. let B:Prop. let H:A. let H0:B.

3 claim H1:A. thus A by H using apply A. end claim.

4 claim H2:B. thus B by H0 using apply B. end claim.

5 thus A∧B by H1, H2 using split.

6 end proof. Qed.

3 4 claim have claim 1 have (split) (apply) claim F′ F′′ claim subs claim have claim have

3 have H1:A by H using apply A.

4 have H2:B by H0 using apply B.

5 _{thus A∧B by H1, H2 using split.} 6 end proof. Qed.

(29)

✓ ✏

F′′(?x, subs, goal ) := F′(Select(subs, ?x ), goal ) F′′(x, subs, true) := thus Typeof(x ) by x. F′′(x, subs, false) := have Typeof(x ) by x. F′′(t0 . . . tn, subs, true) :=

claim H0:Typeof(t0). F′′((t0, true) end claim.

. . .

claim Hn:Typeof(tn). F′′((tn, true) end claim.

thus Typeof(diﬀ ) by H0 . . . Hn.

F′′(t0 . . . tn, subs, false) :=

claim H0:Typeof(t0). F′′((t0, true) end claim.

. . .

claim Hn:Typeof(tn). F′′((tn, true) end claim.

have Typeof(diﬀ ) by H0 . . . Hn.

F′′(let x := t0 in t1, subs, goal ) :=

claim x:Typeof(t0). F′′(t0, subs, true) end claim. F′′(t1, subs, goal )

F′′(fun x ⇒ t, subs, true) := let x:Typeof(x ). F′′(t, subs, true) F′′(fun x ⇒ t, subs, false) :=

claim Typeof(fun x ⇒ t ). F′′(fun x ⇒ t, subs, true) end claim.

F′′(t1 → t2, subs, true) := thus thesis by (t1 → t2).

F′′(t1 → t2, subs, false) := define H as (t1 → t2).

F′′((forall x, t ), subs, true) := thus thesis by (forall x, t ). F′′((forall x, t ), subs, false) := define H as (forall x, t ).

(30)

✓ ✏

F′′(match t with c₁ _t₁₁ . . . t_1j _{⇒ t}₁ _{| . . . | c}_i _t_i₁ . . . t_ik _{⇒ t}_i _{end, subs, true) :=}

per cases on t.

suppose it is t11 . . . t1j. F′′(t1, subs, true)

. . .

suppose it is ti1 . . . tik. F′′(ti, subs, true)

end cases.

F′′(match t with c1 t11 . . . t1j ⇒ t1 | . . . | ci ti1 . . . tik ⇒ ti end, subs, false) :=

claim Typeof(t1).

F′′(match t with c1 t11 . . . t1j ⇒ t1 | . . . | ci ti1 . . . tik ⇒ ti end, subs, true)

end claim. ✒ ✑ 4.7

4.4.2

claim have H1 H2 H H0 H1 H

3 thus A∧B by H, H0 using split.

4 end proof. Qed.

2

diﬀ

4.4.3

F′′(x+2,[],false) _F′′

1 claim H:nat.

2 have H0:nat by S 0. thus nat by S H0.

3 end claim.

(31)

define define H as x + 2

4.4.4 justification

Vars(diﬀ ) Coq by 1.1 8 f_equal Vars(diﬀ ) 6 *

4.4.5 induction

Coq induction induction

induction

1 Lemma example_ind x:nat, x = x. 2 induction x. auto. auto. 3 Qed.

x x 0 S x0 auto

1 have H1: 0 = 0 using auto.

2 have H2: forall x0, x0 = x0 → (S x0) = (S x0) using auto. 3 thus x = x by (@nat_ind (fun x0 ⇒ x0 = x0 ) H1 H2 x).

C-zar induction

1 per induction on x. 2 suppose it is O.

3 thus 0 = 0 using auto.

4 suppose it is (S x0) and IHx:(x0 = x0). 5 thus (S x0) = (S x0) using auto.

(32)

induction nat_ind induction

(33)

5

Coq Coq

5.1

Coq DProof DEnd 2

5.1 Require

DEnd DProof DEnd

C-zar 5.1 5.1 2 DProof DEnd DEnd DProof DEnd 5.2 7 9 5.3 5.1

1 Require Import dp.DProof. 2 Goal forall x y : nat,

3 S x + y = x + S y. 4 DProof. 5 intros. 6 induction x. 7 reflexivity. 8 simpl. 9 f_equal. 10 apply IHx. 11 DEnd. 12 Qed. 5.1 DEnd

(34)

5.2

1 Require Import dp.DProof. 2 Goal forall x y : nat,

3 S x + y = x + S y. 4 Proof. 5 intros. 6 DProof. 7 induction x. 8 reflexivity. 9 simpl. 10 DEnd. 11 f_equal. 12 apply IHx. 13 Qed. 5.3 5.2

1 Goal forall x y:nat, S x + y = x + S y. 2 proof. 3 let x:nat. 4 let y:nat. 5 per induction on x. 6 suppose it is O. 7 thus (0 + S y = 0 + S y) by Nat.add, y 8 using reflexivity. 9 suppose it is (S x0)

10 and IHx:(S x0 + y = x0 + S y).

11 (* write your proof *)

12 thus (S (S x0) + y = S x0 + S y) using simpl.

13 end induction. 14 end proof. 15 Qed. 2 C-zar Goal Qed DProof ( ) x:T forall x:T let x:T DProof Coq CoqIDE DEnd DProof 4 1 2 3 C-zar

5.2

Coen

(35)

5.1 530 13,899 676 A 2,235 56,357 1,600 B 14,641 512,789 7,431 Coen F′′ (F ) A B [16] Coq Arith 264

proof end proof

265 5.1 A B 264 A 5.2 B 5.3 F 1 1 5.2 2 Lemma A 1 10 B 1 5.3 1 631 B C-zar 1

(36)

5.2 (A) _5.3 _(B) 5.4 1 Lemma add_assoc n m p : n + (m + p) = n + m + p. 2 destruct n. 3 - trivial. 4 - apply add_assoc_pos.

5 - apply opp_inj. rewrite !opp_add_distr. simpl. apply add_assoc_pos. 6 Qed. 5.4 5.5 5.6 5.4 5.5 A 5.6 B ∀n, (2 ∗ n)/2 = n 5.4 induction n n 0 trivial n S n0 5.5 n 0 5.6 10 21 12 ( )18 12 f_equal f_equal

(37)

5.5 A

1 Goal forall (n:nat), div2 (2 * n) = n. 2 proof.

3 let n:nat.

4 per induction on n.

6 thus (0 = 0) by (@Logic.eq_refl nat 0).

7 suppose it is (S n0) and IHn:(div2 (2 * n0) = n0).

8 have (S (div2 (n0 + (n0 + 0))) = S n0) by IHn, n0 using now f_equal.

9 then (div2 (S (S (n0 + (n0 + 0)))) = S n0) using (simpl).

10 then (div2 (S (n0 + S (n0 + 0))) = S n0) by n0 using (rewrite add_succ_r).

11 hence (div2 (2 * S n0) = S n0) using (simpl mul).

13 end proof. 14 Qed.

5.6 B

1 Goal forall (n:nat), div2 (2 * n) = n. 2 proof.

3 let n:nat.

4 per induction on n.

6 thus (0 = 0) by (@Logic.eq_refl nat 0).

7 suppose it is (S n0) and IHn:(div2 (2 * n0) = n0).

8 claim HLo:(S (Init.Nat.div2 (n0 + (n0 + 0))) = S n0).

9 have H: (div2 (n0 + (n0 + 0)) = n0) by IHn.

10 claim (S (Init.Nat.div2 (n0 + (n0 + 0))) = S n0).

11 claim HLo1:(S (Init.Nat.div2 (n0 + (n0 + 0))) =

12 S (Init.Nat.div2 (n0 + (n0 + 0)))).

13 have HLo3:(S = S) by (@Logic.eq_refl (nat → nat) S).

14 hence (S (Init.Nat.div2 (n0 + (n0 + 0))) =

15 S (Init.Nat.div2 (n0 + (n0 + 0)))) by (f_equal

16 (fun f : nat → nat ⇒ f (Init.Nat.div2 (n0 + (n0 + 0)))) HLo3).

17 end claim.

18 have HLo2:(S (Init.Nat.div2 (n0 + (n0 + 0))) = S n0) by (f_equal S H).

19 hence (S (Init.Nat.div2 (n0 + (n0 + 0))) = S n0) by (Logic.eq_trans HLo1 HLo2).

20 end claim.

21 hence thesis.

22 end claim.

23 have HLo0:(n0 + S (n0 + 0) = S (n0 + (n0 + 0))) by (add_succ_r n0

24 (n0 + 0)).

25 thus (div2 (S (n0 + S (n0 + 0))) = S n0) by (eq_ind_r

26 (fun n : nat ⇒ div2 (S n) = S n0) HLo HLo0).

28 end proof. 29 Qed.

(38)

5.7 1

1 Lemma even_plus_aux n m :

2 (odd (n + m) ↔ odd n ∧ even m ∨ even n ∧ odd m) ∧ 3 (even (n + m) ↔ even n ∧ even m ∨ odd n ∧ odd m). 4 Proof.

5 rewrite ?even_equiv, ?odd_equiv, <- ?Nat.even_spec, <- ?Nat.odd_spec; 6 rewrite ?Nat.even_add, ?Nat.odd_add, ?Nat.even_mul, ?Nat.odd_mul; 7 unfold Nat.odd; do 2 destruct Nat.even; simpl; tauto.

8 Qed. f x = g y f x = g x g x = g y f g S B 5.3 10 1 Arith 264 156 1 1 Arith 1 5.7 1 5.7 1 1 5.7 B 429 C-zar A 1 2 1 1 C-zar Arith 92 5.2 2 Qed Arith Qed Defined 5.1 A A B 5.4

(39)

5.2 295 8,381 427 A 1,425 37,396 1,060 B 2,841 72,641 2,107 5.4 B A A B

5.3

Arith 265 C-zar 25 13

x 0 nat 1 bool true

(40)

1 match x as x0

2 return match x0 with O ⇒ nat | _ ⇒ bool end

3 with 4 | O ⇒ 1 5 | _ ⇒ true 6 end claim 2 9 C-zar 1 C-zar auto C-zar C-zar 1

(41)

6

Coq Matita

B

Coq

ProofWeb [30] Fitch [31] coqdoc HTML

Proviola [32]

Coqatoo [33]

Coqatoo

Coq

miz3 [16] HOL Light

Coq [15]

Isabelle/Isar Sledgehammer

(42)

7

Coq C-zar • C-zar C-zar induction • C-zar thus P _{∧ Q} P claim • intros auto 1 intros; auto • by thus by diﬀ • have Coq8.7 8.7 C-zar API Coq Coq8.7 C-zar C-zar

(43)

C-zar C-zar IDE Whiteside [14] Coq C-zar C-zar escape C-zar 2

(44)

(45)

[1] Thomas Hales et al. “A Formal Proof of the Kepler Conjecture”. In: Forum of

Math-ematics, Pi 5 (2017). doi: 10.1017/fmp.2017.1.

[2] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations

of Mathematics. Institute for Advanced Study: https://homotopytypetheory.org/

book, 2013.

[3] seL4. url: https://sel4.systems/ (visited on 01/01/2018). [4] CakeML. url: https://cakeml.org/ (visited on 01/01/2018).

[5] The Coq Proof Assistant. url: https://coq.inria.fr/ (visited on 01/01/2018). [6] Georges Gonthier. “Formal proof—the four-color theorem”. In: Notices Amer. Math.

Soc. 55.11 (2008), pp. 1382–1393. issn: 0002-9920.

[7] Georges Gonthier et al. “A Machine-Checked Proof of the Odd Order Theorem”. In:

ITP 2013, 4th Conference on Interactive Theorem Proving. Ed. by Sandrine Blazy,

Christine Paulin, and David Pichardie. Vol. 7998. LNCS. Rennes, France: Springer, July 2013, pp. 163–179. doi: 10.1007/978-3-642-39634-2_14.

[8] CompCert. url: http://compcert.inria.fr/ (visited on 01/01/2018).

[9] VellVM: Verified LLVM. url: http : / / www . cis . upenn . edu / ~stevez / vellvm/ (visited on 01/01/2018).

[10] Frama-C. url: https://frama-c.com/ (visited on 01/01/2018).

[11] Eelco Visser et al. “A Language Designer’s Workbench: A One-Stop-Shop for Imple-mentation and Verification of Language Designs”. In: Proceedings of the 2014 ACM

International Symposium on New Ideas, New Paradigms, and Reflections on Program-ming & Software. Onward! 2014. Portland, Oregon, USA: ACM, 2014, pp. 95–111.

isbn: 978-1-4503-3210-1. doi: 10.1145/2661136.2661149. url: http://doi.acm. org/10.1145/2661136.2661149.

[12] Pierre Corbineau. “A Declarative Language for the Coq Proof Assistant”. In: Types

for Proofs and Programs: International Conference, TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007 Revised Selected Papers. Ed. by Marino Miculan, Ivan Scagnetto,

and Furio Honsell. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 69–84. isbn: 978-3-540-68103-8. doi: 10.1007/978-3-540-68103-8_5. url: https://doi. org/10.1007/978-3-540-68103-8_5.

[13] Iain Whiteside et al. “Towards Formal Proof Script Refactoring”. In: Intelligent

(46)

Con-ference, MKM 2011, Bertinoro, Italy, July 18-23, 2011. Proceedings. Ed. by James

H. Davenport et al. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 260– 275. isbn: 978-3-642-22673-1. doi: 10.1007/978-3-642-22673-1_18. url: https: //doi.org/10.1007/978-3-642-22673-1_18.

[14] Dominik Dietrich, Iain Whiteside, and David Aspinall. “Polar: A Framework for Proof Refactoring”. In: Logic for Programming, Artificial Intelligence, and

Reasoning: 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. Ed. by Ken McMillan, Aart Middeldorp, and

Andrei Voronkov. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013, pp. 776– 791. isbn: 978-3-642-45221-5. doi: 10 . 1007 / 978 - 3 - 642 - 45221 - 5 _ 52. url: https://doi.org/10.1007/978-3-642-45221-5_52.

[15] Serge Autexier and Dominik Dietrich. “A Tactic Language for Declarative Proofs”. In: Proceedings of the First International Conference on Interactive Theorem Proving. ITP’10. Edinburgh, UK: Springer-Verlag, 2010, pp. 99–114. isbn: 3-642-14051-3, 978-3-642-14051-8. doi: 10.1007/978-3-642-14052-5_9. url: http://dx.doi.org/10. 1007/978-3-642-14052-5_9.

[16] Freek Wiedijk. “A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving”. In: Logical Methods in Computer Science 8.1 (2012). doi: 10. 2168/LMCS-8(1:30)2012. url: https://doi.org/10.2168/LMCS-8(1:30)2012. [17] Sascha Böhme and Tobias Nipkow. “Sledgehammer: Judgement Day”. In: Automated

Reasoning: 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings. Ed. by Jürgen Giesl and Reiner Hähnle. Berlin, Heidelberg:

Springer Berlin Heidelberg, 2010, pp. 107–121. isbn: 978-3-642-14203-1. doi: 10.1007/ 978-3-642-14203-1_9. url: https://doi.org/10.1007/978-3-642-14203-1_9. [18] Matita. url: http://matita.cs.unibo.it/ (visited on 01/01/2018).

[19] Claudio Sacerdoti Coen. “Declarative Representation of Proof Terms”. In: Journal of

Automated Reasoning 44.1 (June 2009), p. 25. issn: 1573-0670. doi:

10.1007/s10817-009-9136-7. url: https://doi.org/10.1007/s10817-10.1007/s10817-009-9136-7.

[20] William A. Howard. “The formulas-as-types notion of construction”. In: To H. B.

Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Ed. by J. P.

Seldin and J. R. Hindley. Academic Press, 1980, pp. 479–490.

[21] David Delahaye. “A Tactic Language for the System Coq”. In: Logic for

Program-ming and Automated Reasoning: 7th International Conference, LPAR 2000 Reunion Island, France, November 6–10, 2000 Proceedings. Ed. by Michel Parigot and Andrei

(47)

978-3-540-44404-6. doi: 10.1007/3-540-44404-1_7. url: https://doi.org/10.1007/3-540-44404-1_7.

[22] M Giero, F Wiedijk, and Mariusz Giero. “MMode, a Mizar Mode for the proof assistant Coq”. In: Technical Report NIII-R0333 (Jan. 2003).

[23] Mizar. url: http://www.mizar.org/ (visited on 01/01/2018).

[24] Isabelle. url: https://www.cl.cam.ac.uk/research/hvg/Isabelle/ (visited on 01/01/2018).

[25] Markus Wenzel. “Isar — A Generic Interpretative Approach to Readable Formal Proof Documents”. In: Theorem Proving in Higher Order Logics: 12th International

Con-ference, TPHOLs’ 99 Nice, France, September 14–17, 1999 Proceedings. Ed. by Yves

Bertot et al. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 167–183. isbn: 978-3-540-48256-7. doi: 10.1007/3-540-48256-3_12. url: https://doi.org/10. 1007/3-540-48256-3_12.

[26] John Harrison. “Proof Style”. In: Types for Proofs and Programs: International

Work-shop TYPES’96. Ed. by Eduardo Giménex and Christine Pausin-Mohring. Vol. 1512.

Lecture Notes in Computer Science. Aussois, France: Springer-Verlag, 1996, pp. 154– 172.

[27] Donald E. Knuth. “Literate Programming”. In: Comput. J. 27.2 (May 1984), pp. 97– 111. issn: 0010-4620. doi: 10.1093/comjnl/27.2.97. url: http://dx.doi.org/10. 1093/comjnl/27.2.97.

[28] Adam Chlipala. Certified Programming with Dependent Types: A Pragmatic

In-troduction to the Coq Proof Assistant. The MIT Press, 2013. isbn: 0262026651,

9780262026659.

[29] Benjamin C. Pierce et al. Software Foundations. Electronic textbook, 2017. url: http: //www.cis.upenn.edu/~bcpierce/sf.

[30] ProofWeb. url: http://proofweb.cs.ru.nl/ (visited on 01/01/2018).

[31] Cezary Kaliszyk and Freek Wiedijk. “Merging Procedural and Declarative Proof”. In: Types for Proofs and Programs: International Conference, TYPES 2008 Torino,

Italy, March 26-29, 2008 Revised Selected Papers. Ed. by Stefano Berardi, Ferruccio

Damiani, and Ugo de’Liguoro. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, pp. 203–219. isbn: 978-3-642-02444-3. doi: 10.1007/978-3-642-02444-3_13. url: https://doi.org/10.1007/978-3-642-02444-3_13.

[32] Carst Tankink et al. “Proviola: A Tool for Proof Re-animation”. In: Intelligent

Com-puter Mathematics: 10th International Conference, AISC 2010, 17th Symposium, Cal-culemus 2010, and 9th International Conference, MKM 2010, Paris, France, July 5-10, 2010. Proceedings. Ed. by Serge Autexier et al. Berlin, Heidelberg: Springer Berlin

(48)

Heidelberg, 2010, pp. 440–454. isbn: 978-3-642-14128-7. doi: 10.1007/978-3-642-14128-7_37. url: https://doi.org/10.1007/978-3-642-10.1007/978-3-642-14128-7_37.

[33] Andrew Bedford. Coqatoo: Generating Natural Language Versions of Coq Proofs. 4th International Workshop on Coq for Programming Languages (CoqPL 2018). 2018. url: https://arxiv.org/pdf/1712.03894.pdf.

(49)

:

F′ F′′ name _

IsProof(x ) x true

false

Pattern(var, thesis, n) x n suppose

x n x thesis x and Pattern(x, x = x, 2) S x’ and H:S x’ = S x’ None • Typeof(t) : t • Vars(t) : t ( *) • Select(subs, ?x) : subs ?x

F′((false, tac, diﬀ , []), false, _) F′((false, tac, diﬀ , []), false, name )

( )

F(t ) := proof. F′(t, true, _) end proof.

F′((false, tac, diff , []), true, name ) := thus Typeof(diff ) by Vars(diff ) using tac. F′((false, tac, diff , []), false, _) := have Typeof(diff ) by Vars(diff ) using tac.

F′((false, tac, diff , []), false, name ) := have name:Typeof(diff ) by Vars(diff ) using tac.

(IsProof(d) = true)

F′((false, tac, diﬀ , [g:x]), true, name ) :=

F′(x, false, _) hence Typeof(diff ) by Vars(diff ) using tac. F′((false, tac, diff , [g:x]), false, _) :=

(50)

F′(x, false, _) have Typeof(diff ) by Vars(diff ) using tac. F′((false, tac, diff , [g:x]), false, name ) :=

F′(x, false, _) then name:Typeof(diﬀ ) by Vars(diﬀ ) using tac.

(IsProof(d) = false)

F′((false, tac, diﬀ , [g:(h,(t,d,s ),r,n )]), true, name ) :=

thus Typeof(diﬀ ) by Vars(diﬀ ), d using tac.

F′((false, tac, diﬀ , [g:(h,(t,d,s ),r,n )]), false, _) :=

have Typeof(diﬀ ) by Vars(diﬀ ), d using tac.

F′((false, tac, diﬀ , [g:(h,(t,d,s ),r,n )]), false, name ) :=

have name:Typeof(diﬀ ) by Vars(diﬀ ), d using tac.

P V(t, p) := p (IsProof(t ) = true)

P V(t, p) := None (IsProof(t ) = false)

JV(t, n ) := n (IsProof(t ) = true)

JV(t, n ) := t (IsProof(t ) = false)

F′((false, tac, diﬀ , [g1:(t1, d1, sg1), . . . gn:(tn, dn, sgn)]), true, name ) :=

P V(d1, F′((t1, d1, sg1), true, H1))

. . .

P V(dn, F′((tn, dn, sgn), true, Hn))

thus Typeof(diﬀ ) by Vars(diﬀ ), JV (d1, H1), . . . , JV (dn, Hn) using tac.

F′((false, tac, diﬀ , [g1:(t1, d1, sg1), . . . gn:(tn, dn, sgn)]), false, _) :=

P V(d1, F′((t1, d1, sg1), true, H1))

. . .

(51)

F′((false, tac, diﬀ , [g1:(t1, d1, sg1), . . . gn:(tn, dn, sgn)]), true, name ) :=

P V(d1, F′((t1, d1, sg1), true, H1))

. . .

have name:Typeof(diﬀ ) by Vars(diﬀ ), JV (d1, H1), . . . , JV (dn, Hn) using tac.

F′((true, tac, diﬀ , subs ), goal, name ) := F′′(diﬀ , subs, goal, name )

F′′(diff , subs, goal, name ) := define H as diff . (IsProof(diff ) = false)

(IsProof(diﬀ ) = true)

F′′(?x, subs, goal, name) := F′(Select(subs, x ), goal, name )

F′′(x, subs, true, name ) := thus Typeof(x ) by x. F′′(x, subs, false, _) := have Typeof(x ) by x,

F′′(x, subs, false, name ) := have name:Typeof(x ) by x,

(IsInd(t0) = true)

F′′((true, tac, t0 . . . x, [g1:(t1, d1, sg1), . . . gn:(tn, dn, sgn)]), true, name) :=

per induction on x.

suppose it is Pattern(x, Typeof(diﬀ ), 1).

F′((t₁, d₁, sg₁), true)

. . .

suppose it is Pattern(x, Typeof(diﬀ ), ( n)).

F′((t_n, d_n, sg_n), true)

end induction.

F′′((true, tac, t0 . . . x, [g1:(t1, d1, sg1), . . . gn:(tn, dn, sgn)]), false, name) :=

claim Typeof(diﬀ ). per induction on x.

suppose it is Pattern(x, Typeof(diﬀ ), 1).

(52)

. . .

suppose it is Pattern(x, Typeof(diﬀ ), ( n)).

F′((tn, dn, sgn), true)

end induction. end claim.

(IsInd(t0) = false)

F′′(t₀ . . . t_n, subs, true, name ) :=

P V(t1, F′′(t0, subs, true, H0)) . . . P V(tn, F′′(tn, subs, true, Hn)) thus Typeof(diﬀ ) by JV (t1, H1), . . . , JV (tn, Hn). F′′(t0 . . . tn, subs, false, _) := P V(t1, F′′(t0, subs, true, H0)) . . . P V(tn, F′′(tn, subs, true, Hn)) have Typeof(diﬀ ) by JV (t1, H1), . . . , JV (tn, Hn).

F′′(t0 . . . tn, subs, false, name ) :=

P V(t1, F′′(t0, subs, true, H0))

. . .

P V(tn, F′′(tn, subs, true, Hn))

have name:Typeof(diﬀ ) by JV (t1, H1), . . . , JV (tn, Hn).

F′′(let x := t0 in t1, subs, true, name ) := F′′(t0, subs, true, x ) F′′(t1, subs, goal, name )

F′′(let x := t0 in t1, subs, false, _) := claim Typeoft0. F′′(let x := t0 in t1, subs, true,

_) end claim.

F′′(let x := t0 in t1, subs, false, name ) := claim name:Typeoft0. F′′(let x := t0 in t1,

subs, true, _) end claim.

(53)

F′′(fun x ⇒ t, subs, false, name) :=

claim name:Typeof(fun x ⇒ t ). F′′_{(fun x ⇒ t, subs, true, _) end claim.}

F′′(t1 → t2, subs, true, name ) := thus thesis by (t1 → t2).

F′′(t1 → t2, subs, false, _) := None

F′′(t1 → t2, subs, false, name ) := define name as (t1 → t2).

F′′((forall x, t ), subs, true, name) := thus thesis by (forall x, t ).

F′′((forall x, t ), subs, false, _) := define H as (forall x, t ).

F′′((forall x, t ), subs, false, name) := define name as (forall x, t ).

F′′(match t with c1 t11 . . . t1j ⇒ t1 | . . . | ci ti1 . . . tik ⇒ ti end, subs, true, name ) :=

per cases on t.

suppose it is c1 t11 . . . t1j. F′′(t1, subs, true)

. . .

suppose it is ci ti1 . . . tik. F′′(ti, subs, true)

end cases.

F′′(match t with c1 t11 . . . t1j ⇒ t1 | . . . | ci ti1 . . . tik ⇒ ti end, subs, false, _) :=

claim Typeof(t1).

F′′(match t with c₁ _t₁₁ . . . t_1j _{⇒ t}₁ _{| . . . | c}_i t_i₁ . . . t_ik _{⇒ t}_i _{end, subs, true)}

end claim.

F′′(match t with c1 t11 . . . t1j ⇒ t1 | . . . | ci ti1 . . . tik ⇒ ti end, subs, false, name ) :=

claim name, Typeof(t1).

F′′(match t with c1 t11 . . . t1j ⇒ t1 | . . . | ci ti1 . . . tik ⇒ ti end, subs, true)