The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Oh, I noticed that we can use [Hint Rewrite] to manage what I previously 
called general hints, that is we can share databases for autorewrite and for 
general hints.

The only thing needed to change in ML is to add $-references to "rewrite" 
tactic. Or should we create a new tactic specifically for this? I think we'd 
better to extend "rewrite" tactic with $-notation.

09.01.2013, 16:54, "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

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