[Agda] Tactics in Agda

[gallais]

As far as I know, the biggest effort towards providing a nicer API
to work by reflection is by Paul van der Walt and Wouter Swierstra:
https://github.com/toothbrush/reflection-proofs

Pierre Évariste Dagand has also started a little library to quote
(data)type definitions:
https://github.com/pedagand/agda-datalib/blob/master/DataQuote.agda

On 02/10/14 15:59, Jesper Cockx wrote:
> Dear Agda people,
>
> While experimenting with reflection in Agda, I implemented a version 
> of the 'rewrite' keyword as a tactic (i.e. a function Term -> Term). 
> For example, instead of using the build-in rewrite like this
>
> test : (x y : ℕ) → (x + y) + 0 ≡ y + (x + 0)
> test x y
> rewrite +-right-identity x
> | +-right-identity (x + y)
> | +-comm x y
> = refl
>
> you can use the rewrite' tactic like this:
>
> test′ : (x y : ℕ) → (x + y) + 0 ≡ y + (x + 0)
> test′ x y =
> tactic (rewrite′ (quoteTerm (+-right-identity x)))
> | tactic (rewrite′ (quoteTerm (+-right-identity (x + y))))
> | tactic (rewrite′ (quoteTerm (+-comm x y)))
> | refl
>
> (Full code in the attachment.) The tactic version is somewhat more 
> verbose, but it has the big (IMO) advantage of not relying on any 
> build-in mechanics. In fact, test' normalizes to the following:
>
> λ x y →
> subst (λ z → x + y + 0 ≡ y + z) (sym (+-right-identity x))
> (subst (λ z → z ≡ y + x) (sym (+-right-identity (x + y)))
> (subst (λ z → z ≡ y + x) (sym (+-comm x y)) refl))
>
> I think this is pretty sweet, so a big thank you to the people who've 
> made this possible. I also have some questions for you:
>
> * Are there any other examples of tactics like this in Agda?
> * Is there a library that provides basic reflection functions beyond 
> Reflection.agda in the standard library, for example for shifting and 
> substitution?
> * Also, do you think that tactics are a good style of 
> programming/proving that we should promote in the future?
>
> If the answer to the last question is 'yes', then here are some 
> features that I'd very much like to have in Agda (a way to look at the 
> current context, datatype reflection, ...), but maybe that's better 
> left for a discussion at AIM in two weeks.
>
> Cheers,
> Jesper Cockx
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda