The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Dear Michael,

You may be interested in this 2-page article where I explain how to use typeclasses eauto to do forward search in the way that Matthieu suggested:

http://www.theozimmermann.net/TTT2017/abstract/coq-prolog.pdf

Best regards,

Théo

On 12/03/2018 16:24, Soegtrop, Michael wrote:

Dear Matthieu,

 

what I tried with eauto and typeclass eauto is to modify the goal to True /\ old-goal, split the /\ and use eauto (or typeclass eauto) to solve True, remember the new hypothesis created by forwarding and “transport” these to the context of old-goal – a fairly tricky and fragile process. Is this essentially what you propose? The main problem was that it was fairly fragile – sometimes “transporting” the new hypothesis from one goal context to another fails cause of subtle dependencies, and it was terribly complicated to debug this.

 

I abandoned this and now use some “collection” tactics. I add to the tactic be defining a new one which has new functionality and also calls the old collection tactic. Then I define a tactic notation, which is constantly redefined to call the top level collection tactic. The tactic notation I call in an extern hint. There are a few things on top like for each collection I have sub tactics with various priority levels and so on. If I remember right, Jonathan Leivant proposed this approach to me here on the list, and somehow I sticked to it. Knuth definitely would have put it into appendix D.

 

It somehow works, but it is far away from being as flexible or as efficient as I would like to have it. This forward backward split works efficient in the sense that the number of backtracks is on average no more than 3 times the total proof depth of eauto (even if it is 100 or so). So it is linear with search depth, but the individual steps with all the guarding and hacking are fairly slow.

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928