How to use Agda's auto proof search effectively?

49
votes

When writing proofs I noticed that Agda's auto proof search frequently wouldn't find solutions that seem obvious to me. Unfortunately coming up with a small example, that illustrates the problem seems to be hard, so I try to describe the most common patterns instead.

  • I forgot to add -m to the hole to make Agda look at the module scope. Can I make that flag the default? What downsides would that have?
  • Often the current hole can be filled by a parameter of the function I am about to implement. Even when adding -m, Agda will not consider function parameters or symbols introduced in let or where clauses though. Is there something wrong with simply trying all of them?
  • When viewing a goal, symbols introduced in let or where clauses are not even displayed. Why?

What other habits can make using auto more effective?

1
agda

1 Answers

1
votes

Agda's auto proof search is hardwired into the compiler. That makes it fast, but limits the amount of customization you can do. One alternative approach would be to implement a similar proof search procedure using Agda's reflection mechanism. With the recent beefed up version of reflection using the TC monad, you no longer need to implement your own unification procedure.

Carlos Tome's been working on reimplementing these ideas (check out his code https://github.com/carlostome/AutoInAgda ). He's been working on several versions that try to use information from the context, print debugging info, etc. Hope this helps!