Re: [Proving Axiom Correct] Bootstrapping a library

Dear Axiom gurus,

> 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 := ....

Since BasicType is not an implementation you need to write a 
specification for equal and different. These specifictions should be 
inherited and proved at the domain level. You can see the standard 
library of FoCaLiZe for details.

In practice you need a language for writing logical statements and a 
language to prove these statements. Again see the FoCaLiZe library (for 
instance lattices) to see how a statement can be used in a proof.

> 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.

Inheritance is managed by the FoCaLiZe compiler together with 
dependencies which enables to have statements and proofs in a coherent way.


-- 
Renaud Rioboo