# [Agda] proof by AC-reduction

Serge D. Mechveliani mechvel at botik.ru
Tue Feb 19 15:50:26 CET 2013

```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

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