The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Hi Chris,

In Coq.Program.Tactics, there is the rapply tactic.  This doesn't 
generate a new hypothesis for the term, but it can be easily modified to 
do so by changing the "(p _ ... _)"'s to "(let H := p _ .. _)" where H 
becomes an addtional arg to the tactic.  If you want the subgoals to not 
be shelved, you can either use simple refine instead of refine, or unshelve.

By the way, note that rapply has a maximum number of args it can 
handle.  I have a way to make it handle any number of args if you need that.

-- Jonathan

On 11/12/2016 10:42 AM, 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. 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