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 <axiom...@gmail.com> 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 = such 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 <renaud.rio...@ensiie.fr> > 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 >> > >
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
