Re: [Axiom-developer] Why proving Axiom correct is important

[Gabriel Dos Reis]

I had actually had something similar in one of OpenAxiom's branch.  

On Sat, May 9, 2015 at 3:37 AM, Martin Baker <address@hidden> wrote:

On 08/05/15 21:40, address@hidden 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
address@hidden
https://lists.nongnu.org/mailman/listinfo/axiom-developer