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

[Fredrik Lindblad]

Hi Wojciech and others,

This is certainly a useful feature and it seems to be sufficient to implement around auto as you did. When it comes to user friendliness of auto there is several things that can be improved. In particular the user should have to type less. There has been some rather successful experiments with sorting lemmas in order of generality and most eagerly trying the least general ones. This way it could be tractable to let auto try lemmas (at least in the vicinity of the current position) without explicitly asking it to. But working with databases of lemmas is certainly useful too, and could be combined with the generality analysis. And, importantly, the database feature is already around.
Implementing your feature in the emacs interface is a good idea because the current implementation of auto is outdated. Due to some changes in the core of the search procedure, the implementation will be completely replaced. So one shouldn't spend time improving the current code.
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.

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. And hopefully the user interface will be improved. Feedback from the users of auto is very welcome. Unfortunately, I don't have much time to spend on this now, so we have to stick around with the current version yet a few months.

Example:
The file

\begin{code}
module AdditionCommutative where

open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning
open ≡-Reasoning
open import Data.Nat

lemma : ∀ n m → n + suc m ≡ suc (n + m)
lemma n m = {!-c!}

addcommut : ∀ n m → n + m ≡ m + n
addcommut n m = {!-c -m!}
\end{code}

after running auto on the goals becomes (-m includes the lemmas in the current module as hints)

\begin{code}
module AdditionCommutative where

open import Relation.Binary.PropositionalEquality
import Relation.Binary.EqReasoning
open ≡-Reasoning
open import Data.Nat

lemma : ∀ n m → n + suc m ≡ suc (n + m)
lemma zero m = refl
lemma (suc n) m = cong suc (lemma n m)

addcommut : ∀ n m → n + m ≡ m + n
addcommut zero zero = refl
addcommut zero (suc n) = sym (cong suc (addcommut n zero))
addcommut (suc n) m = begin suc (n + m) ≡⟨ cong suc (addcommut n m) ⟩ suc (m + n) ≡⟨ sym (lemma m n) ⟩ (m + suc n ∎)
\end{code}

Cheers,
 Fredrik

________________________________________
From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] On Behalf Of Wojciech Jedynak [wjedynak at gmail.com]
Sent: Thursday, May 26, 2011 23:50
To: agda at lists.chalmers.se
Subject: [Agda] ANN: coq-like agda-mode support for databases of lemmas [fixed?]

( Sorry for the noise, when I check the archive at
https://lists.chalmers.se/pipermail/agda/2011/thread.html it seems
that the previous message body was truncated, so I'm trying again,
this time without any attachments... )

My original mail:
-----------------------

Hello everybody!

I'm a Coq user that has been recently fascinated by Agda. As I started
to make some simple developments, I realized that being able to extend
the behavior of auto by using databases of user selected lemmas (the
way it works in Coq) would be pretty nice to have. I haven't seen
anything like this on the Agda wiki, so I tried to implement a simple
and straightforward prototype in emacs-lisp by extending the
agda-mode. Basically I just modified the agda2-mode.el file, so I'm
taking the liberty of attaching the extended version to this mail.

This implementation might occur to be a little simplistic to you, but
since I didn't touch the Haskell source files, it's very easy to
install and it's pretty lightweight.
As I'm not very experienced with writing in elisp there may be some
rough edges, but I tried to comment some potential pitfalls. I have
only tested this with Agda 2.2.10.

To see what it's all about please check the Tutorial.lagda file at my
git repository (https://github.com/wjzz/Agda-mode-improvements) and
read it there.
I may have written too many details, but I hope this way it will be
useful even to beginners.

I have some ideas for improvement, but since I don't know if anybody
will be interested at all I decided to release this early version. I
hope you'll find it useful and since it's actually my first go at
contributing to an open-source project please don't hesitate to
comment on anything.

Greetings,
Wojtek Jedynak (wjzz)
_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda