[Agda] ring solver

[Ruben Henner Zilibowitz]

That code works on my machine too. But if I replace trustMe with the proof that I have written (in another file), then this locks up my whole computer.

My  proof that the integers are a ring is here:
http://patch-tag.com/r/rhz/Zililand/snapshot/current/content/raw/IntegerRing.agda

It would be nice if there were some other example of rings around that I could easily test the ring solver with. It's fairly surprising how much of a difference it makes to change trustMe for my proof. Then again I haven't looked at the internals of the ring solver much so far.

It would be nice to work on optimising Agda too of course, if I get around to that.

Ruben

On 15/03/2010, at 1:45 PM, Nils Anders Danielsson wrote:

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