formal proof sketches and MoWGLI

Freek Wiedijk University of Nijmegen

Proof Tools Day 2003 CWI Amsterdam

2003 04 25, 14:30

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: use axioms liberally

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 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!)

MoWGLI

‘Mathematics on the Web, Get it by Logic and Interfaces’

project goal: more intelligent math documents

formalizations → more than tar file of scripts publishing → not only for print/screen

• formalizations (Coq) Bologna: HELM project Sophia/Paris: INRIA, Trusted Logic Nijmegen: FTA project

• math/physics publishing Berlin: Living Reviews in Relativity, Zentrallblatt Saarbrücken: ActiveMath example

proof: 5 lines of Coq

Definition ge [n,m:nat] : Prop := (EX x:nat | n = (plus m x)).

Lemma ge trans : (n,m,p:nat)(ge n m)→(ge m p)→(ge n p). Proof. Unfold ge. Intros n m p H H0. Elim H. Clear H. Intros x H1. Elim H0. Clear H0. Intros x0 H2. Exists (plus x0 x). Rewrite plus assoc l. Rewrite ← H2. Auto. Qed.

MoWGLI presentation

proof: 24 lines of HTML (almost 5 times as many lines)

assume n: nat assume m: nat assume p: nat suppose H: (n≥m) suppose H 0 : (m≥p) consider H we proved (n≥m) that is equivalent to ∃z:nat.(n=(m+z)) there exists x: nat such that ( H 1 ) (n=(m+x)) consider H 0 we proved (m≥p) that is equivalent to ∃z:nat.(m=(p+z)) there exists x 0 : nat such that ( H 2 ) (m=(p+ x 0 )) consider H 1 rewrite m with (p+ x 0 ) by H 2 we proved (n=((p+ x 0 )+x)) rewrite ((p+ x 0 )+x) with (p+( x 0 +x)) by (plus assoc l…) we proved (n=(p+( x 0 +x))) by (ex intro … previous) we proved ∃z:nat.(n=(p+z)) that is equivalent to (n≥p) we proved ∀n: nat .∀m: nat .∀p: nat .∀H: (n≥m) .∀ H 0 : (m≥p) .(n≥p)

formal proof sketch

proof: 5 lines of Mizar

definition let n,m;

pred n >= m means ex x st n = m + x; end;

theorem n >= m & m >= p implies n >= p proof

assume n >= m & m >= p; consider x such that n = m + x; consider x0 such that m = p + x0; n = p + (x + x0); thus n >= p;

end; differences between formal proof sketches and MoWGLI presentations?

+ formal proof sketches: much smaller + formal proof sketches: closer to informal textbook proofs + formal proof sketches: written in input language − formal proof sketches: can’t be generated automatically

(will need some human tagging) improving MoWGLI presentations through studying formal proof sketches