[Agda] A frontend for the semiring solver using the reflection API

[Wojciech Jedynak]

Hello everybody,

last week my sanity has been saved by the stdlib's semiring solver. To
make it more convenient to use, and as an exercise in Agda's
reflection API,  I wrote a simple front-end for the solver today.
I guess that this was one of motivating examples for introducing the
API to Agda in the first place, so others must have created similar
modules before - it might be interesting to compare different
approaches, so please share if you can.

The code is available at
https://github.com/wjzz/Agda-reflection-for-semiring-solver
It has been checked with the latest darcs version of Agda & stdlib.

Long story short, instead of

stdlib : ∀ m n → suc (m + n + (m + n)) ≡ m + m + suc (n + n)
stdlib = solve 2 (λ m n → con 1 :+ (m :+ n :+ (m :+ n)) := m :+ m :+
(con 1 :+ (n :+ n))) refl

one can simply say

notbad : ∀ m n → suc (m + n + (m + n)) ≡ m + m + suc (n + n)
notbad = quoteGoal e in ring e refl refl refl refl

The right hand side is the same regardless of the goal, so we can use
it like the ring tactic in Coq.
It would be nice to replace it with a one-word notation, but I don't
know how to do it, so it's either
snippets or copy&paste for now.

The code should be simlifiable, so I would appreciate any comments.

Greetings,
Wojciech

PS. Pattern-matching lambdas in Agda 2.3 are awesome - it's very neat
to use them for trivial inversion properties instead of writing many
one-liners.