The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Maybe.  Partly that just feels like an ugly way to attack the problem, and I'm hoping there's a pretty basic patch possible to Coq to go about it in a less ugly way.

On 03/09/2013 02:54 PM, Jason Gross wrote: Are the terms sufficiently big that [Set Printing All.] or [Unset Printing Notations.] (possibly together with [Set Printing Implicit.]) would be prohibitively costly?

On Sat, Mar 9, 2013 at 2:27 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

This would almost work, except that Coq's term parsing and printing are not inverses of each other.  I believe almost all of my subgoals would fail to parse back into Coq terms.

On 03/09/2013 02:20 PM, Jason Gross wrote:

I'm not sure if you already thought of this, but you could probably script this process, either by an OCaml plugin or a shell script: you could probably use a tactic like

Ltac display_and_solve_by_tac_or_display_db_and_admit tac x y db :=

    idtac "Tactic: " tac " . Solve Tactic: " y " . Database: " db;

    x; (solve [ tac ]

        || repeat match goal with

                   | [ H : _ |- _ ] => revert H

                   | [ H : _ |- _ ] => fail 2 "cannot revert hypothesis:" H

                   | [ |- ?G ] => idtac "Theorem foo : " G "." y ". Qed. Hint Immediate foo : " db "."; admit

                 end).

                   

and call it with something like [ltac:(auto with my_db)] as [tac], some tactic as [x], some string representing a tactic as [y], and ["my_db"] as [db], and then write a script to parse the output of coqc, place the theorems in separate files, run coqc on them, and construct a single file which imports all of the relevant files, and import that file into your original file.  (Admittedly, this is a terrible hack, and probably not something you'd want to keep around in a project.)