[Agda] ring solver

[Ruben Henner Zilibowitz]

The example I tried was really simple. It was:

lem₂ : ∀ n → _
lem₂ = solve 1 (λ n → con (+ 1) :+ n  :=  con (+ 1) :+ (n :+ con (+ 0))) refl

Now I have implemented a proof that the integers are a commutative ring, and a proof that they are a commutative semiring. If I use the following code:

import Algebra.RingSolver.Simple as Solver
import Algebra.RingSolver.AlmostCommutativeRing as ACR
module ℤSemiringSolver =
  Solver (ACR.fromCommutativeSemiring commutativeSemiring)
open ℤSemiringSolver

then the function lem₂ above goes through just fine. But if I use:

module ℤRingSolver =
  Solver (ACR.fromCommutativeRing commutativeRing)
open ℤRingSolver

Then agda crashes on lem₂ due to memory allocation failure. So could this be caused by a bug somewhere in the ring solver?

Ruben

On 14/03/2010, at 10:31 AM, Nils Anders Danielsson wrote:

> On 2010-03-13 12:34, Ruben Henner Zilibowitz wrote:
>> I've been trying out the ring solver in Algebra.RingSolver. I've
>> noticed it uses "almost commutative rings" instead of actual rings. Is
>> the code here able to deal with proper rings such as the integers, or
>> only semirings such as the natural numbers?
> 
> The ring solver can handle both commutative rings and commutative
> semirings, see Algebra.RingSolver.AlmostCommutativeRing. The idea to use
> "almost commutative rings" comes from a paper by Grégoire and Mahboubi:
> Proving Equalities in a Commutative Ring Done Right in Coq.
> 
>> I've actually tried it on the full integers and it just eats up all my
>> computer's memory and never produces any answer.
> 
> The ring solver may simply be too inefficient for your example.
> 
> --
> /NAD
>