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