The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

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. If A, B, and C were not so long and complicated I would have done 'assert (H: C)' and 'apply long_and_complicated_term' and be happily on my way. If C actually were of the form (D /\ E) it would also have been pretty simple. I would have done 'destruct long_and_complicated_term as [H1 H2]' because that actually generates A and B as proof obligations. I am not aware of a tactic that makes this convenient. What I am looking for is kind of a combination of pose and refine. Is it possible?

Many thanks!

Chris