The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Hi,

My idea is to use (match .. with ..) and pattern variables to name the long types, and (type of <term>) as the match scrutinee:


Parameters LongA LongB LongC LongD : Type.
Parameter long_term : LongA -> LongB -> LongC.

Goal LongD.
Proof.
  pose (term := long_term).
  match type of term with ?A -> ?B -> ?C => assert C as H; [ apply term | ] end; clear term.
  (* three subgoals:
     |- LongA
     |- LongB
     H:LongC |- LongD
   *)
Admitted.

On Sat, Nov 12, 2016 at 10:42 AM, Chris Dams <chris.dams.nl AT gmail.com> 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