[Agda] DoCon-A-0.04 announcement

[Sergei Meshveliani]

A N N O U N C E M E N T

DoCon-A  a Provable Algebraic Domain Constructor
Version 0.04

is available, together with its source program and manual, 
on the Web at the following addresses:

  http://www.botik.ru/pub/local/Mechveliani/docon-A/    (Russian site),
  ftp.botik.ru/pub/local/Mechveliani/docon-A/           (same site),

(see  license.txt).


DoCon-A is
----------
a  Computer Algebra library  written in Agda  and allowing
machine-checked proofs.

DoCon-A applies generic programming. It defines generic notions of the 
algebraic structures: Semigroup, Group, Ring, and so on.
Arithmetic and some other operations are defined under the very
generic assumptions: "over any group", "over any ring", and so on.

Currently the following  Domain Constructors are supported (to a certain
extent): 
  Natural, Integer, Product, Fraction, Euclidean Residue ring.

That is certain set of operations are defined automatically, following
these domain constructors. 

What DoCon-A 0.04 has
---------------------

1. Definitions for 
    DSet (a set with a decidable equality),
    Magma, Semigroup, (Commutative)Semigroup, (Commutative)Monoid,  
    Ringoid, (Commutative)Ring, IntegralRing, GCDRing, Field, 
    module over a ring, vector space,
    FactorizationMonoid, FactorizationRing.

   These structures are accommodated to the methods of the classical
   algorithmic algebra. They differ a bit from the corresponding
definitions of Standard Agda library, they contain certain additional
operations. 

2. Many simple lemmata are proved for these structures.

3. Many simple lemmata are proved for  Natural and Integer
   (in addition to Standard Agda library).
   For Natural\0  it is provided the instance of an Unique factorization
monoid. 
   For Integer  there are provided the instances of an EuclideanRing and
Unique factorization ring.
   Primality is tested there by the sieve method.

4. The constructor EucResidue for the residue ring of any EuclideanRing
is provided with the instance of CommutativeRing in the general case, 
and with the instance of a Field when the base is detected as prime.

5. The sublibrary for processing lists, association lists, multisets
   (call this sublibrary AList).  It is proved the  CommutativeMonoid  
   instance for  Multiset  for the union operation.


So far, DoCon-A-0.04  has been tested under 
-------------------------------------------

        Agda-2.5.2-dc9ffae, MAlonzo, Linux.

We hope to easily port it to the  2.5.2 and 2.6 releases, when they
come.


Reports about possible later ports is in the current notes in the 
distribution:  
              notes/0.04.txt

Documentation
-------------
See           manual.pdf.

Memory requirement 
------------------
For  Agda-2.5.2-dc9ffae,  type-checking the DoCon-A-0.04 library 
requires at least  8 Gb RAM computer.


Remarks are welcome.

------------------------
Dr. Sergei D. Meshveliani,
Program Systems Institute, Pereslavl-Zalessky, Russia.