# Tactic to fill a hypothesis of some term in the context

**URL:** <https://discourse.rocq-prover.org/t/tactic-to-fill-a-hypothesis-of-some-term-in-the-context/2377>\
**Category:** Using Rocq\
**Created:** [July 17, 2024, 4:36pm UTC](https://discourse.rocq-prover.org/t/tactic-to-fill-a-hypothesis-of-some-term-in-the-context/2377 "2024-07-17T16:36:51Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![jeanas](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jeanas/32/762_2.png) [@jeanas](https://discourse.rocq-prover.org/u/jeanas)\
**Post date:** [July 17, 2024, 4:36pm UTC](https://discourse.rocq-prover.org/t/tactic-to-fill-a-hypothesis-of-some-term-in-the-context/2377/1 "2024-07-17T16:36:51Z")

</div>

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

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

---

<div class="post-metadata">

**Author:** ![thomas-lamiaux](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/thomas-lamiaux/32/982_2.png) [@thomas-lamiaux](https://discourse.rocq-prover.org/u/thomas-lamiaux)\
**Post date:** [July 17, 2024, 5:12pm UTC](https://discourse.rocq-prover.org/t/tactic-to-fill-a-hypothesis-of-some-term-in-the-context/2377/2 "2024-07-17T17:12:30Z")

</div>

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

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

```

---

<div class="post-metadata">

**Author:** ![JoJoDeveloping](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jojodeveloping/32/886_2.png) [@JoJoDeveloping](https://discourse.rocq-prover.org/u/JoJoDeveloping)\
**Post date:** [July 17, 2024, 5:24pm UTC](https://discourse.rocq-prover.org/t/tactic-to-fill-a-hypothesis-of-some-term-in-the-context/2377/3 "2024-07-17T17:24:54Z")

</div>

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](https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/tests/tactics.v?ref_type=heads#L196) for how it’s used. I find these extremely nice and wondered myself why Coq does not have this built in already.

---

<div class="post-metadata">

**Author:** ![jeanas](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/jeanas/32/762_2.png) [@jeanas](https://discourse.rocq-prover.org/u/jeanas)\
**Post date:** [July 17, 2024, 5:30pm UTC](https://discourse.rocq-prover.org/t/tactic-to-fill-a-hypothesis-of-some-term-in-the-context/2377/4 "2024-07-17T17:30:18Z")

</div>

OK, thanks. I too am surprised this isn’t built-in; actually I just found [Add an "especialize" tactic · Issue #7412 · coq/coq · GitHub](https://github.com/coq/coq/issues/7412) which looks related.

---

<div class="post-metadata">

**Author:** ![thomas-lamiaux](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/thomas-lamiaux/32/982_2.png) [@thomas-lamiaux](https://discourse.rocq-prover.org/u/thomas-lamiaux)\
**Post date:** [July 17, 2024, 6:25pm UTC](https://discourse.rocq-prover.org/t/tactic-to-fill-a-hypothesis-of-some-term-in-the-context/2377/5 "2024-07-17T18:25:06Z")

</div>

Among others, as part of the [Coq platform docs project](https://github.com/Zimmi48/platform-docs), 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.

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [July 18, 2024, 3:35pm UTC](https://discourse.rocq-prover.org/t/tactic-to-fill-a-hypothesis-of-some-term-in-the-context/2377/6 "2024-07-18T15:35:05Z")

</div>

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

```coq
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.

---

<div class="post-metadata">

**Author:** ![Villetaneuse](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/villetaneuse/32/1011_2.png) [@Villetaneuse](https://discourse.rocq-prover.org/u/Villetaneuse)\
**Post date:** [July 20, 2024, 10:53am UTC](https://discourse.rocq-prover.org/t/tactic-to-fill-a-hypothesis-of-some-term-in-the-context/2377/7 "2024-07-20T10:53:10Z")

</div>

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

```Coq
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.

```