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

[Tim Daly]

Renaud,

I've been looking at FoCal and, in particular, the Zenon program
http://zenon.inria.fr/zenlpar07.pdf

Zenon appears to be able to output OCAML code from proofs.

In your opinion is it reasonable to consider modifying the back end

to output Spad code?

Tim

On Fri, Feb 10, 2017 at 8:39 AM, Tim Daly <address@hidden> wrote:

Renaud,

I'm just getting around to the FoCal information. Obviously you've done a lot of

work on this subject already. I have the papers and the reference manual near

the top of the reading stack. I'm certain to have questions.

Yes, BasicType requires properties for = "" as symmetry which would have

to be proven at the Domain level for each implementation. Of course, = is not

actually implemented directly in NNI but somewhere up the inheritance chain.

For example, the domain ANY has

  x = y ==

    (x.dm = y.dm) and EQUAL(x.ob, y.ob)$Lisp

where dm is a field in the Record implementation of ANY

   Rep := Record(dm: SExpression, ob: None)

which depends on the Lisp definition of EQUAL and SExpression

is one of String, Symbol, Integer, DoubleFloat, OutputForm

Whereas the domain IndexedList implements

  x = y ==

    Qeq(x,y) => true

    while not Qnull x and not Qnull y repeat

      Qfirst x ^=$S Qfirst y => return fase

      x := Qrest x

      y := Qrest y

    Qnull x and Qnull y

where

  Qeq   ==> EQ$Lisp

  Qnull ==> NULL$Lisp

  Qfirst ==> QCAR$Lisp

  Qrest ==> QCDR$Lisp

and

  S : Type

is a dependent argument type. Sigh.

The proofs of = in each domain will involve an appeal to the Lisp

definition of a small number of functions. I'm using ACL2 for Lisp.

This is where the ACL2 and Coq proofs meet.

There is no such thing as a simple job.

Tim

On 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