formal proof sketches & Lamport-style proofs

Freek Wiedijk University of Nijmegen

TYPES 2003 Torino

2003 05 03, 11:00

formal proof sketches

problem 1: what to do with formal proofs? end product of a formalization project: tar file of scripts what people look at: the statements of the lemmas proof scripts are ‘write only’ many projects: presenting formal proofs in natural language MoWGLI project (Bologna, INRIA, Saarbrücken, Berlin, Nijmegen) Coq script ⟶^{Coq} Coq XML ⟶^{XSLT} OMDoc XML ⟶^{XSLT} English HTML generated text should become better currently: rather verbose problem 2: only formalization of the interesting parts?

Peter Aczel (at TYPES 2002 meeting): getting mathematicians interested in formalization

light weight formalization don’t prove everything: support reasoning with gaps

Leslie Lamport: How to Write a Proof (1993) recursive clarification process: hierarchical proofs not formal

IMP project (Paul Cairns & Jeremy Gow, London): implementation interactive course notes: Elements of Euclidean and Metric Topology

experience: structure not easily understood an informal proof

Hardy & Wright, An Introduction to the Theory of Numbers

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’

exactly same reasoning, using Mizar syntax

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

filling out the formal proof sketch to a checkable Mizar text

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;

incomplete but completable proofs

formal proof sketch: only ‘inference errors’ completable into a checkable proof by adding:

• steps

• labels/references

formal proof sketches correctness: semi-decidable

no proofs  full proofs formal proof sketch spectrum full proofs ‘human level’ formal proof sketches

declarative proof style formal proof sketches (in this talk): Mizar system some reinventions of Mizar proof style:

• Markus Wenzel’s Isar language for the Isabelle system

• Henk Barendregt’s ‘math mode’ plans for the Coq system forward reasoning ⟨label⟩: ⟨statement⟩ by ⟨references⟩; natural deduction

→-introduction → assume ⟨proposition⟩;
∃-elimination  → consider ⟨variable⟩ such that ⟨proposition⟩;

etc. formal proof sketch grammar

statement = proposition justification
proposition = [ label : ] formula
justification = [ by label {, label}]
| proof {step ;} [ cases ] end
step = [ then ] statement
| assume proposition
| let variable {, variable}
| (thus | hence) statement
| [ then ] consider variable {, variable}

such that proposition justification

| take term {, term}
cases = per cases justification ;

{suppose proposition ; {step ;}} generating formal proof sketches? full Mizar formalization ⟶ formal proof sketch systematic procedure (works surprisingly well)

• remove all labels/references

• remove ‘in-between’ steps but how to locate the important steps in a proof?

• user tagging no support for this in the Mizar language (yet)

• heuristics but: no good heuristics known to me so formal proof sketches can’t be generated automatically (yet) the proof development cycle

[figure: informal text; formal proof sketch; formal proof sketch; full formalization]

comparing sizes:

formal proof sketch ≪ full formalization ≪ generated language human attention span is important presentation should be much smaller than the formalization (folding sub-proofs: doesn’t help!) formal proof sketches from IMP web pages

informal proof

14 lines

formal proof sketch

18 lines

full formalization

113 lines

[figure: Lamport-style proof 3 … 70 lines; formal proof sketch 32 lines; in Mizar syntax 111 lines; ‘optimized’ formalization 106 lines; full formalization 284 lines] informal proof

Theorem Open intervals are connected

Proof The proof proceeds by contradiction. Suppose that (a, b) were not connected. Then there would be a pair of non-empty disjoint proper open subsets, U, V say, of (a, b) whose union would be (a, b). This implies a ‘gap’ so we use the completeness of the real line to show that there can’t be a gap. To do this, find a supremum of some interval which must be contained in U. Note that there is a small open ball about the supremum which because U and V are open must be contained wholly within one or other of them. However, in both cases, this leads to a contradiction: if the ball is in U then the ball contains points in U exceeding the supremum; if the ball is in V then there are points in the ball also in U by definition of the supremum. formal proof sketch

theorem (.a,b.) is connected proof

assume (.a,b.) is not connected; consider U,V being non empty open Subset of REAL, u,v such that

U ^{/\} V = {} & U ^{\/} V = (.a,b.) & u in U & v in V & u < v; reconsider X = { x : (.u,x.) c= U } as Subset of REAL; set s = sup X; per cases; suppose s in U;

consider e such that e > 0 & Ball(s,e) c= U;

ex x st x in Ball(s,e) & x > s;

thus contradiction; suppose s in V;

consider e such that e > 0 & Ball(s,e) c= V;

ex x st x in Ball(s,e) & x in U;

thus contradiction; end;

Lamport-style proof IMP web page in Mozilla the morals

• sub-proofs are a bad idea it destroys the natural ‘linear structure’ of the proof

• references are a bad idea (at least they are not needed in an informal proof)

and duplicate labels are definitely a bad idea

• formal proof sketches are a good idea able to match the structure of all these proofs

adapting IMP technology for generating formal proof sketches?