[Agda] proof by AC-reduction

[Serge D. Mechveliani]

Dear Agda users and developers,

I find that programming proofs in Agda is rather difficult.
Most simple `human' proof usually need a great effort to encode them in 
Agda. This also pollutes the source code with lengthy proofs which in 
reality could be written somewhat 50 times shorter by calling some 
library function.

Am I missing something?
Do other Agda programmers suffer of composing manually proofs which are 
intuitively trivial?

I see the following main reason of why many simple proofs are complex to 
build for Agda. 
For example, such laws (for Group) as 
                       unityLaw : \forall x  (e * x) ~~ x
                       invLaw   : \forall x  (x * (inv x)) ~~ e 
                          
(I write here ~~ for \~~)
(if they present in a program) are not applied automatically in the
type normalization.
The same is for possible laws of  ~~sym, ~~trans, *cong, *assoc, *comm.

Indeed, in the generic case, they  need not  to apply automatically.

But for many special cases they are desirable to apply automatically,
only by a certain special strategy.
In such cases one probably needs to apply such a tool as
        Equational prover based on Many-sorted Term Rewriting
        (unification, matching, reduction, AC-unification, 
         AC-reduction, completion ...). 

(AC stands for ``Associative and Commutative'').

Agda needs some  proof assistants  provided as additional libraries
(some of them may be even in the Standard library).

(1) The simplest variant is  Equality proof  by Term Rewriting
                                            (and without induction),
    in particular, by AC-unification, AC-reduction.

(2) A support for inductive proofs is desirable.

I expect that  Coq  has something essential for (2), and may be, for (1).

What Agda has for (1), (2) ?

The letter

    http://botik.ru/pub/local/Mechveliani/agdaNotes/assistant.agda.zip 

(about 180 lines) 
1) provides a short proof example of a messy proof, 
2) describes a certain naive project of how to automatically build proofs
   (in appropriate special cases) by applying AC-reduction. 
"Apply AC reduction, obtain its trace and convert the trace to the 
sequence of  ~~sym, ~~trans, *assoc, *comm,   and some others".
There exists a certain Many-sorted Equational reasoning library written 
in Haskell which can do AC reduction (and completion too) with returnig 
the trace. And the current Agda implemantation is somewhat compatible 
with Haskell.   

May such a construction have sense for Agda?
Can you, please, look into the letter on the web and issue your notes?

Thanks,

------
Sergei