[Axiom-developer] [Proving Axiom Correct] Bootstrapping a library

[Tim Daly]

The game is to prove GCD in NonNegativeInteger (NNI).

We would like to use the 'nat' theorems from the existing library

but extract those theorems automatically from Axiom sources

at build time.

Axiom's NNI inherits from a dozen Category objects, one of which

is BasicType which contains two signatures:

 ?=?: (%,%) -> Boolean       ?~=?: (%,%) -> Boolean

In the ideal case we would decorate BasicType with the existing

definitions of = and ~= so we could create a new library structure

for the logic system. So BasicType would contain

theorem = (a, b : Type) : Boolean := .....

theorem ~= (a, b : Type) : Boolean := ....

These theorems would be imported into NNI when it inherits the

signatures from the BasicType Category. The collection of all of

the theorems in NNI's Category structure would be used (hopefully

exclusively) to prove GCD. In this way, all of the theorems used to

prove Axiom source code would be inheritied from the Category

structure.

Unfortunately it appears the Coq and Lean will not take kindly to

removing the existing libraries and replacing them with a new version

that only contains a limited number of theorems. I'm not yet sure about

FoCaL but I suspect it has the same bootstrap problem.

Jeremy Avigad (Lean) made the suggestion to rename these theorems.

Thus, instead of =, the supporting theorem would be 'spad=' (spad is

the name of Axiom's algebra language).

Initially this would make Axiom depend on the external library structure.

Eventually there should be enough embedded logic to start coding Axiom

theorems by changing external references from = to spad= everywhere.

Axiom proofs would still depend on the external proof system but only

for the correctness engine, not the library structure. This will minimize

the struggle about Axiom's world view (e.g. handling excluded middle).

It will also organize the logic library to more closely mirror abstract algebra.

Comments, suggestions?

Tim