[Agda] ANN: coq-like agda-mode support for databases of lemmas

[Wojciech Jedynak]

Hello Fredrik and everybody!

 Thanks for pointing out that 'open ≡-Reasoning' changes the behavior
 of auto. I realized that I saw it in the docs, but I forgot to try it
 out :)
 On the other hand, (is it | would it be) possible to have this:

 > One remark about your example in Tutorial.lagda is that by
importing the right stuff you can enable some built-in knowledge about
equality reasoning to guide the search. This is preferable to adding
cong, sym  and trans as lemmas, since the equality reasoning
mechanism, although pretty dumb, results in a more efficient search
than if they are included as any lemmas. By including the equality
reasoning stuff (see  example below), auto should solve lem-0x and
lem-suc-n-m with "-c" as only argument. And lem-comm should be proven
just by hinting lem-suc-n-m.

but without having auto generate proofs in the "equality-rewriting"
 style? While I certainly like the look of it when nicely indented, for
 some necessary-but-not-interesting lemmas I find the terse style much
 easier to write.

 This makes me want to ask a general question: is there any support in
 agda-mode for writing proofs that heavily use the ≡-Reasoning
 notations (like \==\< and \qed) by hand? Or, say, for automatically
 indenting proofs written in this style?
 (Sorry for asking about such minor and not really meaningful details,
 but for the time being it's the only subject on which I can contribute
 and if it turns out that there isn't any support for these
 equality-related stuff, I'd give it a go in the next days.)

 > To those who use auto I'd like to tell that the new implementation
will have better performance in general. The current implementation
has a memory leak problem which becomes apparent when running it for
more than about 30 seconds. This problem has been hard to track down
but is gone in the new version. Moreover there will be better support
for equality reasoning, recursion and case splits in subexpressions.

Can't wait to try it!

 --
 Best regards,
Wojciech Jedynak