[Agda] ring solver

[Nils Anders Danielsson]

On 2010-03-14 00:22, Ruben Henner Zilibowitz wrote:
> Then agda crashes on lem₂ due to memory allocation failure. So could
> this be caused by a bug somewhere in the ring solver?

The following code type checks on my machine:

  module Test where

  open import Algebra
  import Algebra.RingSolver.AlmostCommutativeRing as ACR
  import Algebra.RingSolver.Simple as Solver
  open import Data.Integer
  open import Relation.Binary.PropositionalEquality

  ℤ-Ring : CommutativeRing _ _
  ℤ-Ring = record
    { Carrier           = ℤ
    ; _≈_               = _≡_
    ; _+_               = _+_
    ; _*_               = _*_
    ; -_                = -_
    ; 0#                = + 0
    ; 1#                = + 1
    ; isCommutativeRing = trustMe
    }
    where postulate trustMe : _

  open Solver (ACR.fromCommutativeRing ℤ-Ring)

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

If you want the ring solver to be more efficient there are at least two
routes two follow:

• Optimise Agda.

• Optimise the ring solver. The paper by Grégoire and Mahboubi contains
  some ideas which may be useful.

--
/NAD