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

[Ramana Kumar]

2012/4/2 Altenkirch Thorsten <psztxa at exmail.nottingham.ac.uk>

> Hi Wojciech,
>
> you are correct this was one of the motivating examples but as far as I
> know nobody  has yet implemented such an interface. Thank you very much!
>

There is in fact another implementation for comparison here:
https://github.com/xplat/agda-tactics/blob/master/Tactics/Nat/Semiring.agda


>
> Thorsten
>
> On 01/04/2012 23:46, "Wojciech Jedynak" <wjedynak at gmail.com> 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
>
> This message and any attachment are intended solely for the addressee and
> may contain confidential information. If you have received this message in
> error, please send it back to me, and immediately delete it.   Please do
> not use, copy or disclose the information contained in this message or in
> any attachment.  Any views or opinions expressed by the author of this
> email do not necessarily reflect the views of the University of Nottingham.
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses which could damage your computer system:
> you are advised to perform your own checks. Email communications with the
> University of Nottingham may be monitored as permitted by UK
> legislation._______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120402/6e4dc350/attachment.html