axiom-developer
[Top][All Lists]

## Re: [Axiom-developer] [Proving Axiom Correct] Bootstrapping a library

 From: Jeremy Avigad Subject: Re: [Axiom-developer] [Proving Axiom Correct] Bootstrapping a library Date: Wed, 8 Feb 2017 17:52:48 -0500

Dear Tim,

I don't understand what you mean. For one thing, theorems in both Lean and Coq are marked as opaque, since you generally don't care about the contents. But even if we replace "theorem" by "definition," I don't know what you imagine going into the "...".

I think what you want to do is represent Axiom categories as structures. For example, the declarations below declare a BasicType structure and notation for elements of that structure. You can then prove theorems about arbitrary types α that have a BasicType structure. You can also extend the structure as needed.

(Presumably you will eventually want to add axioms to the structures that say things about what eq and neq do. Otherwise, you are just reasoning about a type with two relations.)

Best wishes,

Jeremy

class BasicType (α : Type) : Type :=
(eq : α → α → bool) (neq : α → α → bool)

infix `?=?`:50  := BasicType.eq
infix `?~=?`:50 := BasicType.neq

section
variables (α : Type) [BasicType α]
variables a b : α

check a ?=? b
check a ?~=? b
end

On Wed, Feb 8, 2017 at 9:29 AM, Tim Daly wrote:
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.