[Agda] Re: primality definition

[Sergei Meshveliani]

On Sun, 2015-03-08 at 02:49 +0530, N. Raghavendra wrote:
> At 2015-03-08T00:44:47+04:00, Sergei Meshveliani wrote:
> 
> >> Have you put your proofs on the Web?
> >
> >
> > Do you mean proofs about generic  IsPrime, Factorization etc. ?
> 
> Yes, but I am also interested in any algebra proofs in Agda.


Then, see

http://www.botik.ru/pub/local/Mechveliani/agdaNotes/EuclideanResidue-dec13-2014.zip

It contains all the theory needed for (partial division) in  E/(b) 
for any Euclidean ring E.
But  IsPrime  and the  Factorization structure  are skipped there (this
part is not ready).

Also I use different definitions for  Semigroup, Monoid, Group, Ring 
than they are in Standard library
(but it is easy to implement the maps  
Semigroup -> Semigroup_standard, ...). 

See README.agda there.

This experience shows that the main obstacle is that providing full
formal proofs takes much effort.

Regards,

------
Sergei