integrating Coq-style and Mizar-style proof

Freek Wiedijk Radboud University Nijmegen

High Level Languages for Proofs LAMA, Université de Savoie near Chambéry 2005 04 13, 11:30

intro

outline of the talk

1. why not be happy with the proof languages that we already have?

2. ‘formal proof sketches’ formal proofs that can be read like normal mathematical proofs

3. ‘luxury mathmode’ formal proofs that can be written in a mixture of the Coq-way and the Mizar-way requirements for a formal proof language

• (yes, you forgot!) writing proofs

• ‘readable’ reading proofs

• ‘robust’ modifying proofs

• ‘portable’ porting proofs – between different systems

– between different versions of the same system

why more than Mizar?

automatically determining the statements

• intros versus let/assume

theorem even n -> odd n -> False
proof
intros. assume even n;
assume odd n;

• calculating the cases for a proof by induction

• backward chaining and rewriting

apply.
rewrite.

why more than Coq?

informal proof

Theorem 43 (Pythagoras’ theorem). \sqrt{2} is irrational.

The traditional proof ascribed to Pythagoras runs as follows. If \sqrt{2} is rational, then the equation

a^{2} = 2b^{2}  (4.3.1)

is soluble in integers a, b with (a, b) = 1. Hence a^{2} is even, and therefore a is even. If a = 2c, then 4c^{2} = 2b^{2}, 2c^{2} = b^{2}, and b is also even, contrary to the hypothesis that (a, b) = 1. □

‘formal proof sketch’

theorem Th43: sqrt 2 is irrational proof

assume sqrt 2 is rational;

consider a, b such that 4 3 1: aˆ 2 = 2 ∗ bˆ 2 and

a,b are relative prime; aˆ 2 is even; a is even; consider c such that a = 2 ∗ c; 4 ∗ cˆ 2 = 2 ∗ bˆ 2; 2 ∗ cˆ 2 = bˆ 2; b is even; thus contradiction;

end;

theorem Th43: sqrt 2 is irrational :: Pythagoras’ theorem

proof assume sqrt 2 is rational; consider a, b such that

4 3 1:  aˆ 2 = 2 ∗ bˆ 2

and a, b are relative prime; aˆ 2 is even; a is even; consider c such that a = 2 ∗ c; 4 ∗ cˆ 2 = 2 ∗ bˆ 2; 2 ∗ cˆ 2 = bˆ 2; b is even; thus contradiction; end; full formalization

theorem Th43: sqrt 2 is irrational proof

assume sqrt 2 is rational;

then consider a, b such that A1: b ^{<>} 0 and A2: sqrt 2 = a/b and A3: a, b are relative prime by Def1; A4: bˆ 2 ^{<>} 0 by A1, SQUARE 1:73;

2 = (a/b)ˆ 2 by A2, SQUARE 1:def 4

.= aˆ 2/bˆ 2 by SQUARE 1:69; then

4 3 1: aˆ 2 = 2 ∗ bˆ 2 by A4, REAL 1:43; aˆ 2 is even by 4 3 1, ABIAN:def 1; then

A5: a is even by PYTHTRIP:2; :: continue in next column

then consider c such that A6: a = 2 ∗ c by ABIAN:def 1; A7: 4 ∗ cˆ 2 = (2 ∗ 2) ∗ cˆ 2

.= 2ˆ 2 ∗ cˆ 2 by SQUARE 1:def 3

.= 2 ∗ bˆ 2 by A6, 4 3 1, SQUARE 1:68; 2 ∗ (2 ∗ cˆ 2) = (2 ∗ 2) ∗ cˆ 2 by AXIOMS:16

.= 2 ∗ bˆ 2 by A7; then 2 ∗ cˆ 2 = bˆ 2 by REAL 1:9; then bˆ 2 is even by ABIAN:def 1; then b is even by PYTHTRIP:2; then 2 divides a & 2 divides b by A5, Def2; then

A8: 2 divides a gcd b by INT 2:33; a gcd b = 1 by A3, INT 2:def 4; hence contradiction by A8, INT 2:17;

end;

luxury mathmode

Coq-style proof

Lemma Example : forall n, even n -> odd n -> False.
Proof.
induction n.
intros.
inversion H0.
                                   n : nat
                                   IHn : even n -> odd n -> False
                                   ============================
                                    even (S n) -> odd (S n) -> False

intros.
inversion_clear H.
inversion_clear H0.
auto.
Qed.

Mizar-style proof

theorem Example: forall n, even n -> odd n -> False
proof
A1: even 0 -> odd 0 -> False
proof assume that even 0 and H0: odd 0;
 thus False by odd_ind,H0;
end;
now let n be nat;
 assume IHn: even n -> odd n -> False;
 assume that H: even (S n) and H0: odd (S n);
 H1: odd n by even_ind,H;  H2: even n by odd_ind,H0;
 thus False by IHn,H1,H2;
end;
hence thesis by nat_ind,A1;
end;

‘sort | uniq’

 forall n : nat, even n -> odd n -> False

 even 0 -> odd 0 -> False
H : even 0
H0 : odd 0
 False
n : nat
IHn : even n -> odd n -> False
 even (S n) -> odd (S n) -> False
n : nat
IHn : even n -> odd n -> False
H : even (S n)
H0 : odd (S n)
 False

⋮

⟶

                                                                False
                                                                even (S n) -> odd (S n) -> False
                                                                even 0 -> odd 0 -> False
                                                                forall n : nat, even n -> odd n -> False
                                                               H : even (S n)
                                                               H : even 0
                                                               H : even n
                                                               H0 : odd (S n)
                                                               H0 : odd 0
                                                               H1 : odd n
                                                               IHn : even n -> odd n -> False
                                                               n : nat

example

now
A1: now
 assume H: even 0;
 assume H0: odd 0;
 thus False by [     ?4 inversion H0],H,H0;
end;
A2: even 0 -> odd 0 -> False by [intros ?2  ],A1;
A3: now let n be nat;
 assume IHn: even n -> odd n -> False;
 thus even (S n) -> odd (S n) -> False by [  ?3  ],IHn     ;
end;
thus forall n, even n -> odd n -> False
 by [induction n ?1     ],A2,A3;
end;

integration

• proof with goals and tactics

proof = list of tactics
proof state = proof obligation that diminishes until it vanishes

• alternative proposed here

proof = both tactics and statements mixed together
proof state = declarative proof that grows until it is complete

two ways of working on a proof: • manually editing and rechecking the proof (the Mizar way)

• applying a tactic at an unjustified step (the Coq way)

implementation

tiny subset of Mizar

⟨proof⟩ ::= ⟨label⟩ : now
⟨intro⟩^{∗}
⟨proof⟩^{∗}

thus ⟨statement⟩ by ⟨justification⟩ ; end ;

⟨intro⟩ ::= let ⟨variable⟩ be ⟨type⟩ ;
| assume ⟨label⟩ : ⟨statement⟩ ;
⟨justification⟩ ::= { , ⟨label⟩ } ⟨tactic⟩ { , ⟨label⟩ }

simplification of proofs example of one of the proof rewriting rules

now

…  now
now  …
let var ;  consider var such that
assume label : statement_{1};  label : statement_{1} by …;
… ⟶ …
thus statement_{2} by …;  thus statement_{2} by …;
end;  end;

thus statement_{2} by …; end; prototype in HOL Light

demo

let EXAMPLE = prove
 (`!n. ~(EVEN n) <=> ODD n`,
  INDUCT_TAC THEN ASM_REWRITE_TAC[EVEN; ODD]);;

conclusion

desires & doubts desires

• working on formal proof sketch and formalization together

• having the freedom to mix the ways of working in Mizar and Coq

doubts • approach still reasonable when you get large/non-intuitive subgoals?