
From:  Tim Daly 
Subject:  Re: [Axiomdeveloper] [Proving Axiom Correct] Bootstrapping a library 
Date:  Tue, 14 Feb 2017 23:24:18 0500 
TimThere is no such thing as a simple job.This is where the ACL2 and Coq proofs meet.definition of a small number of functions. I'm using ACL2 for Lisp.The proofs of = in each domain will involve an appeal to the Lispis a dependent argument type. Sigh.S : TypeandQrest ==> QCDR$LispwhereQnull x and Qnull yy := Qrest yx := Qrest xQfirst x ^=$S Qfirst y => return fasewhile not Qnull x and not Qnull y repeatQeq(x,y) => truex = y ==(x.dm = y.dm) and EQUAL(x.ob, y.ob)$Lispx = y ==For example, the domain ANY hasactually implemented directly in NNI but somewhere up the inheritance chain.to be proven at the Domain level for each implementation. Of course, = is notwork on this subject already. I have the papers and the reference manual nearRenaud,I'm just getting around to the FoCal information. Obviously you've done a lot ofthe top of the reading stack. I'm certain to have questions.Yes, BasicType requires properties for = "" as symmetry which would havewhere dm is a field in the Record implementation of ANYRep := Record(dm: SExpression, ob: None)which depends on the Lisp definition of EQUAL and SExpressionis one of String, Symbol, Integer, DoubleFloat, OutputForm
Whereas the domain IndexedList implementsQeq ==> EQ$LispQnull ==> NULL$LispQfirst ==> QCAR$LispOn Fri, Feb 10, 2017 at 5:13 AM, Renaud Rioboo <address@hidden> wrote: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
[Prev in Thread]  Current Thread  [Next in Thread] 