Sometimes, I find myself with name : Hyp -> Conc in the context, I know I can already prove Hyp, and it turns out easier to do so (forward reasoning) rather than to find a way to apply name and then prove Hyp (backward reasoning). For example, if Conc contains equalities that I want to use automagically with lia.

With the default Coq tactics, I don’t know what to do other than assert (hyp : Hyp). { ... } specialize (name hyp). Is there an easier way without naming hyp? This seems basic, but somehow I can’t find the built-in tactic for it.

Basically, I’m looking for an equivalent of

Ltac fill_hypothesis name :=
match goal with
| [ name : ?Hyp -> ?Conc |- _ ] =>
assert (hypothesis : Hyp); [|specialize (name hypothesis); clear hypothesis]
end.

(I looked for especialize, but it doesn’t seem to exist.)

Another extremely hacky way is unshelve epose proof (name _) as name2; clear name; rename name2 into name.

At least in std++, they were having the same problem, so they added a version of specialize called ospecialize that takes underscores _ and turns them into goals. See tests/tactics.v · master · Iris / stdpp · GitLab for how it’s used. I find these extremely nice and wondered myself why Coq does not have this built in already.

Among others, as part of the Coq platform docs project, we are going a tutorial about foward resonning. In order to do so, last CUDW we had discussions on foward reasonning and e.g. what is done in SSReflect and possible changes. If changes do happen it can be the opportunity to had such a feature at the same time.

You may be looking for lapply. Here is an example:

Lemma plop (A B : Prop) : A -> (A -> B) -> B.
Proof.
intros ha H.
(* At this point, the goal is [B]. *)
lapply H.
- (* proof of B -> B *)
intros hb; exact hb.
- (* proof of A *)
exact ha.
Qed.