computer algebra inside a proof assistant

Freek Wiedijk Radboud University Nijmegen

TYPES workshop Constructive analysis, types and exact real numbers Radboud University Nijmegen 2005 10 03, 15:30

computer algebra versus proof assistants

when things get tedious (the problem with proof assistants) problems from a small Mizar formalization:

x = i/n , n = m + 1 ⊢ n! · x = i · m!
\frac{k}{n} ≥ 0 ⊢ |\frac{n − k}{n} − 1| = \frac{k}{n}
n ≥ 2 , x = \frac{1}{n + 1} ⊢ \frac{x}{1 − x} < 1

Jeremy Avigad, Isabelle:

0 ≤ n ≤ (\frac{K}{2} ) x , C > 0 , 0 < ε < 1 ⊢ (1 + \frac{ε}{3(C + 3)}) n < Kx

calculating ∫_{0}^{∞} \frac{e^{−(x−1)^{2}}}{\sqrt{x}} dx (the problem with computer algebra)

> int(exp(-(x-t)^2)/sqrt(x), x=0..infinity);

\frac{1}{2} \frac{e^{−t^{2}}(−^{\frac{3(t^{2})^{\frac{1}{4}} π^{\frac{1}{2}} 2^{\frac{1}{2}} e^{\frac{t^{2}}{2}} K_{\frac{3}{4}} ( \frac{t^{2}}{2} )}{t^{2}}} + (t^{2})^{\frac{1}{4}} π^{\frac{1}{2}} 2^{\frac{1}{2}} e^{\frac{t^{2}}{2}} K_{\frac{7}{4}} (\frac{t^{2}}{2} ))}{π^{\frac{1}{2}}}

> subs(t=1,%);

\frac{1}{2} \frac{e^{−1}(−3π^{\frac{1}{2}} 2^{\frac{1}{2}} e^{\frac{1}{2}} K_{\frac{3}{4}} (\frac{1}{2}) + π^{\frac{1}{2}} 2^{\frac{1}{2}} e^{\frac{1}{2}} K_{\frac{7}{4}} (\frac{1}{2}))}{π^{\frac{1}{2}}}

> evalf(%);

0.4118623312

> evalf(int(exp(-(x-1)^2)/sqrt(x), x=0..infinity));

1.973732150 simplification and assumptions

> sqrt(x^2);

if we know x ≥ 0 then \sqrt{x^{2}} ⟶ ⟶ x
if we know x ≤ 0 then \sqrt{x^{2}} ⟶ ⟶ −x
nothing known about x then \sqrt{x^{2}} ⟶ ⟶ …

leave it unchanged? ask the user for the sign of x? rewrite it to sign(x) · x? do something else?

‘read-eval-print’ versus decision procedures

• what computer algebra gives ‘answer’ unknown in advance, but just one answer always a trivial answer possible bad administration of assumptions

‘simplify’  Γ  ⊢ t = ?
‘solve’  Γ , ? = ? ⊢ t = u

• what proof assistants need many possible ‘answers’ should be handled problems often too difficult to solve precise administration of assumptions

‘decide’  Γ  ⊢^{?} t = u

MathXpert

system for teaching high school mathematics

computer algebra system, Michael Beeson, 1997

• just high school mathematics ‘algebra’, trig, limits, integrals not as powerful as Maple or Mathematica

• everything very much looks like in high school textbooks

• system explains step by step how it got its results

• designed by a logician, so much more correct than other systems

started out as a research project to show feasibility of idea ⇒ sold to a commercial company ⇒ company went bankrupt ⇒ now privately marketed through the web MathXpert demo

‘ simplify (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} ’

operations Mathpert is operated by repeatedly going through:

• select a sub-expression

• select an ‘operation’ to apply to it (with ‘ShowStep’ or ‘AutoStep’ the system selects the step)

• very occasionally you have to supply an argument to the operation

169 menus
1852 menu items
1702 operations

C source code of a MathXpert operation

MEXPORT_ALGEBRA int EXPORT
    rootexp(term t, term arg, term *next, char *reason)
/*   ^{n}√x = x^(1/n)   */
{ term n,x;
if(FUNCTOR(t) != ROOT)
   return 1;
n = ARG(0,t);
x = ARG(1,t);
*next = make_power(x,make_fraction(one,n));
HIGHLIGHT(*next);
strcpy(reason,"$^{n}√x = x^(1/n)$");
return 0;
}

the ‘prove-refute-assume’ paradigm

calculation has a list of current assumptions built-in ‘prover’ to deduce statements from these assumptions

if conditions need to be satisfied for an operation then if MathXpert …

• can prove the condition, it performs the operation

• can refute the condition, it refuses the operation

• cannot prove nor refute the condition, then it adds it to the assumptions and performs the operation

prover uses non-standard analysis non-standard analysis not visible to the user!

the MathXpert architecture inside the HOL world HOL Light proof assistant, John Harrison, 1998

• reimplementation of the venerable HOL system

• ‘the most perfect program ever written’ (Tom Hales)

• smallest ‘de Bruijn criterion’ kernel that I know of

• largest number formalized from a list of 100 well-known theorems

  http://www.cs.ru.nl/^{∼}freek/100/

currently 54 theorems

Coq has 27, Mizar has 30, all systems together 63

• used to formalize floating point hardware at Intel operations versus lemmas

let ROOTEXP = prove
(`&0 < x /\ 0 < n ==> root(n) x = x^(&1/ &n)`,
STRIP_TAC THEN
SUBGOAL_THEN `?m. n = SUC m`
  (CHOOSE_THEN (fun th -> REWRITE_TAC[th])) THENL
[ASM_MESON_TAC[num_CASES; LT_REFL]; ALL_TAC] THEN
ASM_SIMP_TAC[POWER; ROOT_LN; REAL_MUL_LID; real_div]);;

ML type for MathXpert operations

C

int operationname(term t, term arg, term *next, char *reason)

ML

type operation =
       term option -> term list -> term -> thm list * thm;;
let (operationname:operation) = fun arg ass t -> . . . ;;

returns theorems:

                     ass′ ⊢ ass
                     ass′ ⊢ t = next

C: returnvalue ≠ 0 ⟶ ML: throws an exception ‘reason’ not supported ‘MathXpert in HOL’ demo

‘ show that (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = 2 ’

unimplemented MathXpert features

• 99.8% of the operations

• ‘AutoStep’

  let (one_step: term list -> term -> ↓^{β−expansion} term* operation) =

…;;

• interesting operations for the current focus

• dependence of the behavior of the operations on the user model

features that are rather alien to the HOL Light world: • point & click interface

• graphs MathXpert operations versus HOL conversions conversions

type conv      =               term ->            thm;;

t ↦ ⊢ t = t′

operations

type operation =
           . . . -> term list -> term -> thm list * thm;;

with an empty assumption list this becomes:

ε t ↦ ε , Γ ⊢ t = t′

conclusion

the real puzzle of how to put computer algebra in proof assistants

how to fit quite different interfaces into a nice coherent whole?

• proof assistants goal that is changed by applying tactics successive states are steps in a proof

• computer algebra systems read-eval-print successive states can be completely unrelated

apart from this interaction issue: (semantically correct) computer algebra fits cleanly inside a proof assistant