The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hello, Hani --

What format are you looking for the information to be in? Without doing anything on the Coq implementation side, you can run the ideslvae protocol and parse the results (you might want to issue 'Set Printing All' first so you don't need to worry about notations). I know of several projects that have done something similar to this.

I did a very hacky implementation a while ago:

https://github.com/gmalecha/coq-interact

Val Roberts at UCSD has done something nicer for PeaCoq:

http://goto.ucsd.edu/peacoq/ (probably check out the source code)

On Sat, Mar 26, 2016 at 5:40 PM, Hani Awni <hani.awni AT gmail.com> wrote:

Hello,

What would be the best way to get the current proof state at the point in interactive proving where Coq is expecting the human to suggest the next tactic? For example, I need the information for Proof General's display of the list of goals when it is waiting for the user to input "intros", "trivial", etc.

For background, I am a cognitive scientist and budding computer scientist working in Dr. Hummel's Abstract Relational Reasoning cognitive science lab at UIUC, where we have a python model (called LISA) of how humans solve relational analogies. The idea is, during an attempt at using Coq to prove a human-specified theorem, our model should be able to recognize the abstract, structural similarity of the current goals and proof state to previous examples it has seen, and consequently suggest the appropriate tactic string, including specific mappings like what variable to apply over.

In order for this to happen, I must automatically translate the proof state given by Coq into a series of propositions for LISA to understand. I can design this translation, but the first step in this is getting my hands on Coq's current goals list, whether in OCaml or Lisp or Python.

On the #coq IRC, it was suggested that I implement a new tactic using a Coq plugin in OCaml, because there I could acquire the proof state; however, a tactic specifies the new proof state, whereas our model can only provide the tactic to use. Can I recursively attempt a new tactic in place of my current one?

This seems like a basic need, so I feel like I have overlooked something very basic in my searching; feel free to point out the obvious approaches first.

Thank you,

Hani Awni

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/