[Agda] Tactics in Agda

[Wouter Swierstra]

Hi Jesper,

> 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

Very cool! I have an MSc student working on something very similar.

> * Are there any other examples of tactics like this in Agda?

I submitted a paper with Pepijn Kokke to ICFP this year:

  http://www.staff.science.uu.nl/~swier004/Publications/AutoInAgda.pdf

We wrote a 'auto' tactic that you provide with a hint database, and
tries to construct a proof term frome these hints. Since then, we've
implemented a quoteContext keyword in Agda that lets you access (some)
local variables (let-bound variables are trickier), which you could
then add to your hint database. We're preparing a new version of the
paper -- any feedback would be most welcome!

> * Is there a library that provides basic reflection functions beyond
> Reflection.agda in the standard library, for example for shifting and
> substitution?

You can check out Pepijn's GitHub repository:

  https://github.com/pepijnkokke/AutoInAgda

In particular, there is a first order unification algorithm, based on
Conor McBride's paper. It should be possible to use that in the
development of rewrite, allowing you to write:

test′ x y =
   tactic (rewrite′ (quote +-right-identity))
   ...

That is, you just quote the lemma you'd like to use; the rewrite
tactic unifies the current goal and conclusion of the lemma, and
figures out how to instantiate the lemma to solve the goal.

> * Also, do you think that tactics are a good style of programming/proving
> that we should promote in the future?

I think this could be very cool. Here are a few problems that we ran
into (off the top of my head). I'm sure Pepijn can mention more:

  - The whole reflection mechanism is non-modular. It's hard to define
abstractions. For example, before the tactic keyword was available,
you'd have to write 'quoteGoal g in unquote (tactic g)' over and over
again. Syntax macros would help here.

  - The reflection mechanism is untyped. Fixing this is really hard.
We can write interesting bits of proof automation without types,
though.

  - The reflection mechanism is unstable. Small changes to the
Reflection module typically have a large impact on any serious use of
Reflection.

All the best,

  Wouter