I had actually had something similar in one of OpenAxiom's branch.
On Sat, May 9, 2015 at 3:37 AM, Martin Baker <ax87...@martinb.com> wrote: > On 08/05/15 21:40, d...@axiom-developer.org wrote: > >> There exists a few mathematical axiom statements in the category book >> (Volume 10.2), associated with each category (look at SemiGroup for >> example). The intention is to decorate all of the categories and >> domains with mathematical axioms which can be assumed in the proof. >> >> Much more work needs to be done to just look up the standard axioms >> for the various categories. Feel free to contribute by looking up >> what the group/ring/field/etc axioms should be. They will be added >> to the approprate categories. >> >> The plan is to add an "axioms" category with an "axioms" function >> export so you can query the axioms that something should obey from >> code or the command line. >> > > Tim, > > If you are using COQ then why not just map the COQ library entries into > the Axiom categories? > So if we take part of the base library here: > https://coq.inria.fr/library/Coq.Arith.Mult.html# > > So the appropriate Axiom category could have an entry like: > > Zero property > Lemma mult_0_r : forall n, n * 0 = 0. > Lemma mult_0_l : forall n, 0 * n = 0. > > Of course the COQ libraries have a different structure than the Axiom > libraries so there is no exact mapping between them but it would seem to be > a good idea to have as much compatibility as possible rather than invent > something from scratch? > > Looking at these they are not 'axioms' in that they have redundancy. > > For example there is also the following > Commutativity > Lemma mult_comm : forall n m, n * m = m * n. > > So mult_0_l could have been derived from mult_0_r. > > Do you propose to have a minimal set of axioms or to have a larger set of > lemmas? > > The form you have used in 10.2 is like this (in the human readable LP part > - not part of the category itself): > Axioms: > associative("*":(%,%)->%) (x*y)*z = x*(y*z) > Conditional attributes: > commutative("*":(%,%)->%) x*y = y*x > > Are you proposing to put this into the category itself, not just as a > comment? Do you prefer this syntax over the COQ syntax? > > Isabelle uses a different approach again (in the flavor of Isabelle I have > seen so far) in that it uses 'rules' instead of 'axioms' > > So instead of: > n * 0 = 0 > > We have separate rules for each direction: > n * 0 ==> 0 > 0 ==> n * 0 > > So the first direction can be declared as a simplification rule and can be > applied without any danger of an infinite loop. > > The advantage that I could see, for this in Axiom, is that the > simplification that is applied to equations in the output formatter could > be made explicit, configurable and provable. > > Do you have a view on axioms vs. lemmas vs rules? > Are you proposing to put this into SPAD itself rather than comments or LP? > > Martin > > > > > > > _______________________________________________ > Axiom-developer mailing list > Axiom-developer@nongnu.org > https://lists.nongnu.org/mailman/listinfo/axiom-developer >
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer