I had actually had something similar in one of OpenAxiom&#=
39;s branch. =C2=A0

On Sat, May 9, 2015 at 3:37 AM, Martin Baker <ax8=
7438@martinb.com> wrote:

~~On 08/05/15 21:40, daly@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 =3D 0.

Lemma mult_0_l : forall n, 0 * n =3D 0.

Of course the COQ libraries have a different structure than the Axiom libra= ries so there is no exact mapping between them but it would seem to be a go= od idea to have as much compatibility as possible rather than invent someth= ing 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 =3D 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 l= emmas?

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("*":(%,%)->%)=C2=A0 =C2=A0 (x*y)*z =3D x*(y*z)

Conditional attributes:

commutative("*":(%,%)->%)=C2=A0 =C2=A0 x*y =3D y*x

Are you proposing to put this into the category itself, not just as a comme= nt? 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 =3D 0

We have separate rules for each direction:

n * 0 =3D=3D> 0

0 =3D=3D> 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 simplificati= on that is applied to equations in the output formatter could be made expli= cit, 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?<= span class=3D"HOEnZb">

Martin

_______________________________________________

Axiom-developer mailing list

Axiom-devel= oper@nongnu.org

https://lists.nongnu.org/mailman/listinfo/axiom-developer<= br>

--047d7b6d7e483b54670515a4f7f0-- From MAILER-DAEMON Sat May 09 13:17:46 2015 Received: from list by lists.gnu.org with archive (Exim 4.71) id 1Yr8Nm-0005Lm-A7 for mharc-axiom-developer@gnu.org; Sat, 09 May 2015 13:17:46 -0400 Received: from eggs.gnu.org ([2001:4830:134:3::10]:57765) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from