An Example

We will use a solution to the following question, taken from the 1995 Finnish High-School Matriculation Mathematics Exam, to illustrate the use of structured calculation proof on a real problem.

The figure below contains a graph of a polynomial of degree three. Find the expression of the polynomial and compute the coordinates of its extrema.

Let us call the function described by this graph f. From our knowledge of what it means for an expression to be a `polynomial of degree three', we know the general form of fx to be a·x3 + b·x2 + c·x + d, for some a, b and c. We can also read some values for fx for certain xs off the graph; namely f 0 = 0, f 1 = 1, f 2 = 0 and f 3 = 3. Using these facts, we can find a concrete expression for f.

        (EXISTS a b c d. FORALL x. fx = a·x3 + b·x2 + c·x + d) /\
f 0 = 0 /\ f 1 = 1 /\ f 2 = 0 /\ f 3 = 3
      = {Extend the scope of the existential quantification.}
        EXISTS a b c d.
  (FORALL x. fx = a·x3 + b·x2 + c·x + d) /\ f 0 = 0 /\ f 1 = 1 /\ f 2 = 0 /\ f 3 = 3
      = {Simplify using the definition of f.}
              <FORALL x. fx = a·x3 + b·x2 + c·x + d>
                f 0 = 0 /\ f 1 = 1 /\ f 2 = 0 /\ f 3 = 3
              = {Replace each instance of fx using the assumption.}
                (a·03 + b·02 + c·0 + d = 0) /\
(a·13 + b·12 + c·1 + d = 1) /\
(a·23 + b·22 + c·2 + d = 0) /\
(a·33 + b·32 + c·3 + d = 3)
              = {Arithmetic simplification.}
                (d = 0) /\
(a + b + c + d = 1) /\
  (8·a + 4·b + 2·c + d = 0) /\
  (27·a + 9·b + 3·c + d = 3)
              = {Simplify using d = 0.}
                      <d = 0>
                        (a + b + c + d = 1) /\
(8·a + 4·b + 2·c + d = 0) /\
(27·a + 9·b + 3·c + d = 3)
                      = {Replace d with 0 using the assumption.}
                        (a + b + c + 0 = 1) /\
(8·a + 4·b +2·c + 0 = 0) /\
(27·a + 9·b +3·c + 0 = 3)
                      = {Arithmetic simplification.}
                        (a + b + c = 1) /\
(8·a + 4·b + 2·c = 0) /\
  (27·a + 9·b + 3·c = 3)
                      = {Simplify using a + b + c = 1.}
                              <a + b + c = 1>
                                (8·a + 4·b + 2·c = 0) /\ (27·a + 9·b + 3·c = 3)
                              = {Divide the equations by 2 and 3 respectively.}
                                (4·a + 2·b + c = 0) /\ (9·a + 3·b + c = 1)
                              = {Rearrange both equations.}
                                (3·a + b + (a + b + c) = 0) /\ (8·a + 2·b + (a + b + c) = 1)
                              = {Using the assumption replace a + b + c by 1.}
                                (3·a + b + 1 = 0) /\ (8·a + 2·b + 1 = 1)
                              = {Subtract 1 from each equation.}
                                (3·a + b = -1) /\ (8·a + 2·b = 0)
                              = {Simplify using 3·a + b = -1.}
                                      <3·a + b = -1>
                                        8·a + 2·b = 0
                                      = {Divide both sides of the equation by 2.}
                                        4·a + b = 0
                                      = {Rearrange the equation.}
                                        a + (3·a + b) = 0
                                      = {Replace 3·a + b by -1 using the assumption.}
                                        a + -1 = 0
                                      = {Add 1 to both sides of the equation.}
                                        a = 1
                                (3·a + b = -1) /\ (a = 1)
                              = {Simplify the rest using a = 1.}
                                (b = -4) /\ (a = 1)
                        (a + b + c = 1) /\ (b = -4) /\ (a = 1)
                      = {Simplify using (b = -4) /\ (a = 1).}
                              <b = -4, a = 1>
                                a + b + c = 1
                              = {Replace using the assumptions.}
                                1 + -4 + c = 1
                              = {Simplify.}
                                c = 4
                        (c = 4) /\ (b = -4) /\ (a = 1)
                (d = 0) /\ (c = 4) /\ (b = -4) /\ (a = 1)
        EXISTS a b c d.
  (FORALL x. fx = a·x3 + b·x2 + c·x + d ) /\ (d = 0) /\ (c = 4) /\ (b = -4) /\ (a = 1)
      = {Simplify using the values for a, b, c and d.}
        EXISTS a b c d.
  (FORALL x. fx = x3 - 4·x2 + 4·x ) /\ (d = 0) /\ (c = 4) /\ (b = -4) /\ (a = 1)
      = {Reduce the scope of the existential quantification.}
        (FORALL x. fx = x3 - 4·x2 + 4·x) /\
(EXISTS a b c d. (d = 0) /\ (c = 4) /\ (b = -4) /\ (a = 1))
      = {The existential quantification is trivially true.}
        (FORALL x. fx = x3 - 4·x2 + 4·x) /\ T
      = {Boolean simplification.}
        FORALL x. fx = x3 - 4·x2 + 4·x

A Browsable Format for Proof Presentation: An Example / Jim Grundy