The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Dear Chris,

I use the tactic spec_all H (see code below) when H

is an hypothesis of the form A1 -> A2 -> ... -> An -> B

From the goal

...  H : A1 -> ... -> B |- C

It generates n+1 sub-goals

...  H : A1 -> ... -> B |- A1

...  H : A1 -> ... -> B |- A2

....

...  H : A1 -> ... -> B |- An

...  H : B |-  C

Notice that it purposely forgets that you have

proved A1 ... An in the last goal because

to keep them, the user would need to give names

for those news hypotheses. It could be

done of course but it is usually unneeded

to keep them.

You have to tweak the code a bit if you want

C as the first subgoal instead of the last one.

I hope it meets you needs

Dominique

(***************************************)

(* with an Hypothesis H : A -> B, specializes H to H : B after
   having provided a proof of A. A is available under U : A
   afterwards
*)

Ltac spec H U :=
  match goal with [ G : ?h -> _ |- _ ] =>
    match G with H => assert h as U; [ idtac | specialize (H U) ] end end.

(* spec but forgets U : A *)

Ltac specf H := let U := fresh in spec H U; [ idtac | clear U ].

(* and do it as much as you can *)

Ltac spec_all_rec H U :=
  try match goal with [ G : ?h -> _ |- _ ] =>
    match G with H => assert h as U; [ idtac | specialize (H U); clear U; spec_all_rec H U ] end end.
      
Ltac spec_all H := let U := fresh in spec_all_rec H U.

(***************************************)

---

De: "Chris Dams" <chris.dams.nl AT gmail.com>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Samedi 12 Novembre 2016 16:42:38
Objet: [Coq-Club] Is there a tactic to do this in a convenient way?

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