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-develo...@nongnu.org
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
