The Coq mailing list

[Victor Porton <porton AT narod.ru>]

09.01.2013, 16:30, "Victor Porton" 
<porton AT narod.ru>:
> 09.01.2013, 15:52, "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>.
>
> Sorry,
> Remove General Hint <db>: <term-1>...<term-n>.
>
>>  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!
>
> Oh, certainly I THREAT not treat. :-)

We could also do things like

apply $dual_order

but that would not work as desired because apply applies terms in order, so 
that each term should be applied.

We probably need a new tactic for general hint databases... I'm not sure 
about this.

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