The Coq mailing list

[Victor Porton <porton AT narod.ru>]

The following is my proposal to add a new feature to Coq:

Add and remove hints to a new kind of hints databases which I call "general" 
hints:

Create General Hint <db>.
[Local] General Hint <db>: <term-1>...<term-n>. (* add n terms to the DB *)
[Local] Remove General Hint <db>.

Now for a hint database named "dual_order" it can be used as follows (with $ 
used to refer to general hints DB):

rewrite $dual_order

would be equivalent to

rewrite <term-1>, ..., <term-n>

(if the DB "dual_order" contains <term-1>, ..., <term-n>)

and maybe likewise in other tactics, I haven't yet considered that in details.

We could also mix references to general hints databases with plain IDs like 
this:

rewrite $dual_order, my_rule, $dual_category.

My proposal is not perfect. The following are the deficiencies:

1. I provide no mean to control that all hints inserted in such hints 
databases are setoid equalities.

2. There should be a way to pass "references" to general hint databases, that 
is variables containing a reference to a hint database. This way for example 
code for both order duality and categorical duality can be shared. The best 
thing for this I invented for now is double-dollar notation like:

rewrite $$dbref.

I haven't yet realized what database reference should be. Should these be 
simply strings (with database names)?

Finally, if nobody is willing to implement this, I TREAT you that I will 
learn ML and do it myself!

-- 
Victor Porton - http://portonvictor.org