[Agda] factorization monoid, ring

[Sergei Meshveliani]

On Tue, 2016-06-21 at 13:47 +0530, N. Raghavendra wrote:
> At 2016-06-20T14:36:57+04:00, Sergei Meshveliani wrote:
> 
> > But I do not find:  where there are implemented the general notions of
> > Factorization Monoid or Factorization Ring,
> > a notion of factorization uniqueness for such domains, and some generic
> > lemmata about them?
> > (papers, documentation -- ?)
> >
> > Can somebody point at such?
> 
> In case you are looking for some references on the general theory of
> factorial monoids and rings, here are some possible references.  (They
> don't say anything about implementation.)
> 
> 1. N. Jacobson, Basic Algebra, vol. 1, 2nd ed., section 2.14 (Factorial
>    monoids and rings).
> 
> 2. R. Mines, F. Richman, and W. Ruitenberg, A course in constructive
>    algebra, Chapter IV, section 1 (Divisibility in cancellation
>    monoids).
> 
> 3. N. Bourbaki, Algebra II, Chapter VI, Section 1 (Ordered groups and
>    divisibility).
> 
> 4. Pete L. Clark, Commutative algebra, notes, Section 15
>    (Factorization), http://math.uga.edu/~pete/integral.pdf


Thank you.
No, I meant documentation on implementation of these definitions and
theorems in Coq.

The story is as follows 

1) I was aware only of factorization in an IntegralRing, the notion of 
   FactorialRing (as, for iexample, in S. Lang's book).

2) Then, you have mentioned the case of CC-monoid (cancellative
commutative monoid) and the book by Jacobson.

3) Then I have implemented all the needed things about factorization in
a CC-monoid -- without reading anything. And agreed all this with
factorization in an IntegralRing.
The needed proofs are algebraically trivial, but formal Agda proofs
occur somewhat more complicated technically. A rich library for
multisets is needed.
As Agda has accepted all this, then, I hope, all this "my" theory and
proofs are correct.
4) After this, I still looked into the Jacobson book and observed that
it is all the same. 

Regards,

------
Sergei