|
From: | Renaud Rioboo |
Subject: | Re: [Axiom-developer] [Proving Axiom Correct] Bootstrapping a library |
Date: | Fri, 10 Feb 2017 11:13:31 +0100 |
User-agent: | Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.6.0 |
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] |