[Agda] proof by AC-reduction

[Serge D. Mechveliani]

On Wed, Feb 20, 2013 at 05:48:58PM +0100, Nils Anders Danielsson wrote:
> On 2013-02-19 15:50, Serge D. Mechveliani wrote:
> >Agda needs some  proof assistants  provided as additional libraries
> >(some of them may be even in the Standard library).
> 
> Have you seen the ring solver that is part of the standard library?
> 
>   http://www.cse.chalmers.se/~nad/listings/lib/README.Nat.html
>   http://www.cse.chalmers.se/~nad/listings/lib/README.Integer.html
> 
> This solver uses a technique called "proof by reflection", a technique
> that can be used for other solvers as well. For instance, I have written
> one for monoids:
> 
>   http://www.cse.chalmers.se/edu/year/2012/course/afp/lectures/lecture11/html/Proof-by-reflection.html
> 
> I have also written one for equality proofs (intended to be used with
> --without-K):
> 
>   http://www.cse.chalmers.se/~nad/listings/equality/Equality.Tactic.html
> 

Thank you. I have to look into this.

------
Sergei