The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Team,

 

I read in the changelog in git for 8.6:

 

- Many new options and new engine based on the proof monad. The

  [typeclasses eauto] tactic is now a multi-goal, multi-success tactic.

 

I wonder if it is now possible to use typeclasses eauto without solving the goal. The use case is to use a hint database for forwarding tactics. I want to be able to write something like:

 

Hint Extern 0 => typeclasses eauto with nocore HdbAutoForward : HdbMain.

 

The effect shall be that all successful tactics in HdbAutoForward, which are generally tactics which inspect hypothesis and see if something can be derived from them, shall be executed. But since these are just forwarding tactics, which add additional derived hypothesis but don’t solve the goal, this currently doesn’t work because eauto eventually fails and everything it did is undone.

 

Of cause I can add each individual forwarding tactic to HdbMain, but the disadvantage is that on backtracking the forwarding tactics are tried in every possible order. The idea of forwarding is that it just adds additional hypothesis and that this should never reduce the solvability of the goal, so that there is no point in trying forwarding tactics in different orders and all forwarding should be done (and undone) in one step in the main eauto. This dramatically reduces branching in the eauto proof search.

 

Currently this is a rather tricky business. I create a dummy goal (current goal \/ True), run eauto on this dummy goal, collect the new hypothesis in a list of Props, assign this list to an evar, solve the \/ True and then expand the list in the evar to hypothesis for the real goal. This works, but it is slow, hard to debug and transporting hypothesis through the evar needs to be done carefully to avoid context dependency issues. I thought about extending eauto with an option for this use case, but maybe someone was faster ;-)

 

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