The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

How about using an evar:


Variables (A B C : Type).

Hypothesis long_term : A -> B -> C.

Variable some_goal : Type.

Goal some_goal.
Proof.
evar (Hty : Type).
assert (H : Hty).
- red. (* apply doesn't unfold [Hty := ?Hty] and therefore doesn't 
figure out that it can unify. *)
  apply long_term.
  + admit. (* A *)
  + admit. (* B *)
- subst Hty. (* get rid of Hty := C *)
  admit. (* finish the proof, now with an hypothesis H : C *)
Abort.

As you can see we don't need to refer to A/B/C and long_term only 
appears once.

Gaëtan Gilbert

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