The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

(Of course, one can get a similar benefit in a laborious way today, by explicitly stating each subgoal as a theorem in a separate .v file, making it easy to prove each theorem with a separate 'coqc' process.  My specific use cases involve hundreds of subgoals generated in a non-obvious way, so it really isn't practical, convenient, etc. to write out separate theorem statements explicitly.)

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.)

-Jason