The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If you have all of them in your context, you can do:

repeat match goal with

  | [ H1 : ?A, H2 : ?A -> ?B |- _ ] => specialize (H2 H1)

  end

On Tue, Apr 16, 2019, 20:04 Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de> wrote:

Hi,

I use a technique using `evar` and unification which is described in
Chapter 14.5 of CPDT [1].

Sincerely
Maximilian


[1] http://adam.chlipala.net/cpdt/cpdt.pdf#page=292&zoom=auto,-398,796

On 17/04/2019 00:04, Kaiyu Yang wrote:
> Hi folks,
>
> Is there a tactic in Coq for automatic forward reasoning? Suppose you
> have a lemma *forall (t1 : T1) (t2 : T2) ... (tn : Tn), C. *
> And you have T1, T2, Tk in your local context (k <= n). Is it possible
> to apply some tactic which automatically finds relevant hypotheses in
> the local context and gives you the result of forward
> reasoning: *forall (t_{k+1} : T_{k+1}), ... (tn : Tn), **C* ?   Thanks!
>
> Best,
>
> --
> Kaiyu Yang
> Ph.D. student in computer science at Princeton University
> 35 Olden Street, Room 431
> Princeton, NJ 08540
> +1 (734)389-9696