Proof assistant demos at ICMS 2006

Exercise

Problem [B2 from IMO 1972]
f and g are real-valued functions defined on the real line. For all x and y,

f(x + y) + f(x - y) = 2 f(x) g(y).

f is not identically zero and |f(x)| ≤ 1 for all x. Prove that |g(x)| ≤ 1 for all x.

Solution
Let k be the least upper bound for |f(x)|. Suppose |g(y)| > 1. Then

2k ≥ |f(x + y)| + |f(x - y)| ≥ |f(x + y) + f(x - y)| = 2 |g(y)||f(x)|,

so |f(x)| ≤ k/|g(y)|. In other words, k/|g(y)| is an upper bound for |f(x)| which is less than k. Contradiction.

• Paper version without the proof: ps.gz pdf dvi tex
• Paper version with the proof (handed out at the demo session): ps.gz pdf dvi tex
• Version with an alternative proof by Tom Hales: ps.gz pdf dvi tex

Demos

1. Isabelle, try-out by Jeremy Avigad

   
   • First cut (formalization time: about 75 minutes; de Bruijn factor: 1.7)
   • Polished version (de Bruijn factor: 1.5)

2. HOL Light, demo by John Harrison

   

   Video of the demo

   • First cut (formalization time: about 20 minutes; de Bruijn factor: 1.3)
   • Polished version (de Bruijn factor: 1.1)
   • Version of Tom Hales' proof (de Bruijn factor 0.9)

3. Mizar, demo by Artur Kornilowicz

   

   Video of the demo

   • Polished version (de Bruijn factor: 2.1)

4. ProofPower, demo by Rob Arthan

   

   Video of the demo

   • Polished version with both the demo proof and Hales' proof: pdf doc (doc does not mean "Word" here, but "ProofPower") (formalization times: about 77 minutes and about 35 minutes; de Bruijn factors: about 2.4 and about 2.0)

5. Coq, demo by Laurent Théry

   

   Video of the demo

   • Polished version (de Bruijn factor: 2.0)
   • Version of Tom Hales' proof (de Bruijn factor: 1.4)
   
   
   • Version of the demo proof and of Tom Hales' proof by Georges Gonthier of the Labo Commun INRIA-Microsoft, using his proof language for Coq (de Bruijn factors: 1.6 and 1.0) and another version based on his own version of the reals
   • Version of the demo proof by Pierre Corbineau using his declarative proof language for Coq (de Bruijn factor: 2.7)

(last modification 2006-09-21)