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