[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] Why proving Axiom correct is important
From: |
Martin Baker |
Subject: |
Re: [Axiom-developer] Why proving Axiom correct is important |
Date: |
Sat, 09 May 2015 09:37:15 +0100 |
User-agent: |
Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0 |
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