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

[Andreas Abel]

Neat.  That sort of stuff should accompany the RingSolver code in the 
standard library.

Cheers,
Andreas

On 02.04.12 12:46 AM, Wojciech Jedynak wrote:
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/