Tactic to fill a hypothesis of some term in the context

Using Coq
1

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.)

2

I do not know any tactic to do this directly, but from what I understand of the issue, you could do the following in order not to copy paste types

  Goal forall {A B} (f : A -> B), B.
    intros A B f.
    eassert (foo : _); [ apply f |] ; clear f.
    1: { admit. }
    (* Rest of the proof *)
3

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.

4

OK, thanks. I too am surprised this isn’t built-in; actually I just found Add an "especialize" tactic · Issue #7412 · coq/coq · GitHub which looks related.

5

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.

1 Like
6

With the SSReflect tactic language, you can write something like the following:

apply: _ (name _) => [{}name|].

(possibly followed by ; first last depending on what you want to prove first).

Not sure if there is a simple way to avoid having to write name twice.

7

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.