[Agda] Re: examples of tactics via reflection

[Dan Licata]

Hi Andrej,

The draft "A Universe of Binding and Computation" (pdf and agda code
here: http://www.cs.cmu.edu/~drl/pubs.html) contains some simple
tactics, of a sort.

This paper is about constructing a universe of types with variable
binding.  Structural properties (such as weakening, substitution, etc.)
do not hold for all types in the universe, but we have identified some
conditions under which these properties hold.  You could think of these
conditions as being specified by judgements (e.g. a judgement "CanWeaken
A B" meaning that an A can be weakened with a B).  However, we don't
want programmers to have to write out the proofs of these judgements
(the whole point is to get the structural properties for free from the
logical framework), so we define Agda code that computes a boolean
telling whether "A is weakenable with B", and then use the type
Check(canWeaken A B) as the precondition for the code that implements
weakening.  When A is weakenable with B, the type Check(canWeaken A B)
computes definitionally to Unit, so there is no proof obligation.  

It seems like this should be an instance of a more general tactics
framework: I wrote Agda code to automatically discharge goals that look
like "CanWeaken A B", "CanSubst A B", etc.  But I'm not sure what that
tactic framework would look like.

-Dan

> Dear Agdaists,

> I am new to Agda and I am looking for examples of how to implement and
> use in Agda something similar to Coq's tactics. As I understand it,
> the idea is to use reflection and universes. Where can I see some
> examples, such as computing the normal form of a polynomial, or
> checking the truth of a boolean proposition by truth-tables? What
> about "tactics" that may fail or succeed, are there libraries to
> combine those?

> Thanks,

> Andrej