The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 11/12/2016 04:42 PM, Chris Dams wrote:
> Dear all,
> 
> In a proof I have a long and complicated term (let us call it
> long_and_complicated_term) that is of a type that is of the form A -> B -> C
> where all of A, B, and C are also long and complicated. Because these terms
> are long and complicated I do not want to cut and paste them into my proof
> script. I don't mind having long_and_complicated_term in my proof script
> because it cannot really be avoided but I do want to have it only once. I
> would like to have a tactic that adds C as hypothesis and generates A and B
> as goals of the proof and then allows me to continue with the proof of the
> actual goal with C now a hypothesis that can be used.

There is an "exploit" tactic in CompCert that does pretty much what
you want, I think:

https://github.com/AbsInt/CompCert/blob/master/lib/Coqlib.v#L56

Its Ltac implementation is awful, though.  Don't sue me.

Usage: if "G" is your current goal,

       exploit long_and_complicated_term.

will leave you with 3 goals:

Goal 1:   A
Goal 2:   B
Goal 3:   C -> G

Hope this helps,

- Xavier Leroy