[Agda] Tactics in Agda

[Jesper Cockx]

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

[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

Post by Jesper Cockx
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
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
λ 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
* 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
https://lists.chalmers.se/mailman/listinfo/agda

...

[Wouter Swierstra]

Hi Jesper,

Post by Jesper Cockx
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.

Post by Jesper Cockx
* 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!

Post by Jesper Cockx
* 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.

Post by Jesper Cockx
* 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