The Coq mailing list

[Jevgenijs Sallinens <jevgenijs AT dva.lv>]

Quoting Aaron Bohannon 
<bohannon AT cis.upenn.edu>:

> 
> Other than this, are there any other improvement for my axiomatization 
> or any more comments about additional techniques?
> 

I think it is more interesting to include (decidable) equality as one of 
axiomatization elements, so to consider nat as a setoid, not a type.
One of application then could be for lists (with two lists considered
equal if their lengthes are equal, we can provide structure of abstract 
natural 
numbers).  Or we can use axiomatized theory for binary representation of 
natural numbers. 
I already formalized quit large piece of the theory (without multiplication)
assuming equality as an operator nat -> nat -> bool, but have no time
to finalize it to be published or to submit it to Coq contributions.
Old and ugly version with modules usage could be downloaded from 
http://www.mathcoq.dva.lv/downloads/NewNat.zip. Now I prefer to use records ;
(structures) to represent theories, since being first class citizens ( in our 
case, abstract structures of natural numbers could depend on external 
parameters).
If somebody interested in enhancing this approach or its applications, I will 
be glad to provide more details.

Regards,
Jevgenijs Sallinens.


-------------------------------------------------
This mail sent through IMP: http://webmail.dva.lv/