
From:  Jeremy Avigad 
Subject:  Re: [Axiomdeveloper] [Proving Axiom Correct] Bootstrapping a library 
Date:  Wed, 8 Feb 2017 17:52:48 0500 
Timtheorems by changing external references from = to spad= everywhere.Eventually there should be enough embedded logic to start coding AxiomInitially this would make Axiom depend on the external library structure.the name of Axiom's algebra language).Thus, instead of =, the supporting theorem would be 'spad=' (spad isJeremy Avigad (Lean) made the suggestion to rename these theorems.FoCaL but I suspect it has the same bootstrap problem.that only contains a limited number of theorems. I'm not yet sure aboutremoving the existing libraries and replacing them with a new versionfor the logic system. So BasicType would containdefinitions of = and ~= so we could create a new library structureIn the ideal case we would decorate BasicType with the existing?=?: (%,%) > Boolean ?~=?: (%,%) > Booleanis BasicType which contains two signatures:but extract those theorems automatically from Axiom sourcesThe game is to prove GCD in NonNegativeInteger (NNI).We would like to use the 'nat' theorems from the existing libraryat build time.Axiom's NNI inherits from a dozen Category objects, one of whichtheorem = (a, b : Type) : Boolean := .....theorem ~= (a, b : Type) : Boolean := ....These theorems would be imported into NNI when it inherits thesignatures from the BasicType Category. The collection of all ofthe theorems in NNI's Category structure would be used (hopefullyexclusively) to prove GCD. In this way, all of the theorems used toprove Axiom source code would be inheritied from the Categorystructure.Unfortunately it appears the Coq and Lean will not take kindly toAxiom proofs would still depend on the external proof system but onlyfor the correctness engine, not the library structure. This will minimizethe 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?
[Prev in Thread]  Current Thread  [Next in Thread] 