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

[Wojciech Jedynak]

Hello Nils and everybody!

2011/5/27 Nils Anders Danielsson <nad at chalmers.se> wrote:
> On 2011-05-26 23:42, Wojciech Jedynak wrote:
>>
>> Databases do not have to be declared. All you need to do is to insert
>> a comment of the form:
>> {- BASE name-of-database lemma_1 lemma_2 ... lemma_n -}
>
> Wouldn't it be nicer to use ordinary Agda definitions to define
> databases? In fact, this is already possible:

<cut>

That's an interesting example -- I didn't notice that auto uses record
projections.
I played with this approach for a bit, and there three advantages:

1) we can import databases from modules for free (I haven't
implemented this yet)
2) we can compose databases and even create hierarchies of them (same here)
3) the language prevents us from adding an unproved/unstated lemma to the db

However, there seem to be more cons that pros. I extended your code in
a vicious way,
but I only wanted to see what happens with a slightly more complex db
and having lemmas
used only in some proofs in the db should be a common use case.
-----------------------------------------------------------------------------------------------------------------------------------------------
module DBs where

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

postulate
  right-identity : ∀ n → n + 0 ≡ n
  move-suc       : ∀ m n → suc (m + n) ≡ m + suc n
  left-identity  : ∀ n → 0 + n ≡ n
  plus-one       : ∀ n → 1 + n ≡ n + 1

db = left-identity ,′ plus-one ,′ right-identity ,′ move-suc

-- running

comm' : ∀ m n → m + n ≡ n + m
comm' m n = {!-c db -t 10!}

-- gives us this term

comm : ∀ m n → m + n ≡ n + m
comm zero n = sym (proj₁ (proj₂ (proj₂ db)) n)
comm (suc n) n' = begin suc (n + n') ≡⟨ cong suc (comm n n') ⟩ suc (n'
+ n) ≡⟨ proj₂ (proj₂ (proj₂ db)) n' n ⟩ (n' + suc n ∎)

-- OTOH

{- BASE global left-identity plus-one right-identity move-suc -}

-- running (by firing agda2-solve-with-db using C-u C-c C-a [pre-fix
ver] or C-c C-v [fixed ver])

comm'' : ∀ m n → m + n ≡ n + m
comm'' m n = {!-c !}

-- yields

comm2 : ∀ m n → m + n ≡ n + m
comm2 zero n = sym (right-identity n)
comm2 (suc n) n' = begin suc (n + n') ≡⟨ cong suc (comm2 n n') ⟩ suc
(n' + n) ≡⟨ move-suc n' n ⟩ (n' + suc n ∎)

-----------------------------------------------------------------------------------------------------------------------------------------------

The cons are:
1) the proofs are cluttered with many proj1 and proj2 selectors
2) it take much more time to generate the terms
(the reason for 1 & 2 is auto will have to explicitly unwrap each
lemma from the nested pair structure. The
further a lemma appears in the db, the more unwrapping layers are needed)
3) changing the order of lemmas/deleting|adding a lemma invalidates
ALL proofs that use the db, because db
appears as a part of the proof term
4) it's better to have the name move-suc appear in the term than to
have a proj1 db expression.

Of course, the order of lemmas in the db is deliberate, but it's to
make the disadvantages obvious.

I thought about using heterogeneous lists as an alternative inside db
representation, but I don't see any advantages.
Defining a map-like structure/interface for the db and teaching auto
how to access it's elements could perhaps be
a more promising approach. In my opinion it would be easier to extend
the elisp-based approach to incorporate the
pros, than to eliminate the cons.

There is also a big difference between using an internal and external
database: when using the external version,
there is no trace in the proofs that the user had used any databases
at all! After the development is finished, all
db declarations could be actually deleted with no harm.

Greetings,
Wojciech Jedynak