[Agda] DoCon-A announcement

[Sergei Meshveliani]

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

DoCon-A  a Provable Algebraic Domain Constructor,
Version 0.03

is available, together with its source program and manual, on the Web
at 
  http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/  
                                                        (Russian site),
  ftp.botik.ru/pub/local/Mechveliani/docon-A/0.03/      (same site).


(Copyright © 2015 Program Systems Institute of RAS
see  license.txt).

Author:  Dr. Sergei D. Meshveliani.


DoCon-A is
a  Computer Algebra library  written in a purely functional, non-strict 
language  Agda  allowing machine-checked proofs.

What it has
-----------

1. Definitions for 
   DSet (a set with a decidable equality),
   Magma, Semigroup, (Commutative)Semigroup, (Commutative)Monoid,  
   Ringoid, (Commutative)Ring, IntegralRing, GCDRing,
   FactorizationRing, EuclideanRing, Field.
   These structures are accommodated to the methods of the classical
   algorithmic algebra. 
   The structures up to CommutativeRing differ a bit from the 
   corresponding definitions of  Standard Agda library, 
   they contain certain additional operations. 
   However there is provided a map to  Semigroup, (Commutative)Monoid,
   and  (Commutative)Ring  of Standard Agda library.

2. Many simple lemmata are proved for these structures.
   The extended GCD method is implemented for an arbitrary Euclidean
   ring.

3. Many simple lemmata are proved for operations with Natural and
   Integer numbers (in addition to Standard Agda library).
   Many lemmata are proved for the binary coded naturals (Bin), 
   in particular the additive isomorphism to Nat,  DecTotalOrder for
   Bin.

4. The library (call it  AList) for processing  lists,  association
   lists, multisets.  It is proved the  CommutativeMonoid  instance for
   Multiset  over any decidable setoid  for the multiset sum operation. 
   The library includes the `merge' sorting of a list over any
   decidable total order domain, with the performance cost of 
   O( n*(log n) ) and with proofs for the result orderedness and for 
   preserving the multiset of a list. 

Everything is supplied with a machine-checked proof.