formal proof sketches

Freek Wiedijk University of Nijmegen

INRIA, room E003 Sophia-Antipolis

2003 09 17, 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: 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 syntax of 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!)

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; formal proof sketches versus MoWGLI presentations?

• formal proof sketches: much smaller

• formal proof sketches: closer to informal textbook proofs

• formal proof sketches: written in input language

• MoWGLI presentations: can be generated automatically (formal proof sketches will need some human tagging)

improve MoWGLI presentations by studying formal proof sketches?

IMP

formal proof sketches versus Lamport-style proof

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 what can we learn from this?

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

• references are bad for proof readability (at least they are not needed in an informal proof)

and duplicate labels just is a bad idea

• formal proof sketches are surprisingly flexible able to match the structure of all these proofs

adapting IMP technology for generating formal proof sketches?

existing textbook proofs

infinity of primes: original

Theorem There are infinitely many primes: for every number n there exists a prime p > n

Proof [after Euclid] Given n. Consider k = n! + 1, where n! = 1 · 2 · 3 · . . . · n. Let p be a prime that divides k. For this number p we have p > n: otherwise p ≤ n; but then p divides n!, so p cannot divide k = n! + 1, contradicting the choice of p. QED infinity of primes: formal proof sketch

theorem {n : n is prime} is infinite proof for n ex p st p is prime & p > n

proof :: [after Euclid] let n; set k = n! + 1; :: n! = 1 · 2 · 3 · . . . · n consider p such that p is prime & p divides k; take p; thus p is prime; thus p > n proof assume p <= n; then p divides n!; not p divides n! + 1; thus contradiction; end; end; thus thesis; end; image of left unit element: original

Theorem. Let G be a set with a binary operation · and left unit element e. Let H be a set with binary operation ∗ and assume that ϕ is a homomorphism of G onto H. Then H has a left unit element as well.

Proof. Take e′ = ϕ(e). Let h ∈ H. There is g ∈ G such that ϕ(g) = h. Then

e′ ∗ h = ϕ(e) ∗ ϕ(g) = ϕ(e · g) = ϕ(g) = h,

hence e′ is left unit element of H. □ image of left unit element: formal proof sketch

let G, H be non empty HGrStr; let e be Element of G such that e is left unit of G; let phi be map of G, H such that phi is homomorphism G, H and phi is onto; thus ex e′ being Element of H st e′ is left unit of H

proof take e′ = phi.e; now let h be Element of H; consider g being Element of G such that phi.g = h; thus

e′ ∗ h = phi.e ∗ phi.g .= phi.(e ∗ g) .= phi.g .= h;

end; hence e′ is left unit of H; end; the formal proof sketch challenge

claim:

any existing informal proof can be faithfully mimicked as a formal proof sketch

the dream

formalized versions of existing mathematical textbooks = ‘filled in’ formal proof sketch translations

existing informal textbook [figure] [figure] [figure] matching formal proof sketch

full formalization