Is it possible to have a term like `ltac:(some_tactic)`

where Coq will infer the type but let me prove it as a subgoal? Or, less generally, suppose I want to go from

```
Hpq : P -> Q
============================
True
```

to

```
Hq : Q
============================
True
```

Some options I know of would be

`lapply Hpq.`

, which is akward to do for more than one argument (`lapply H;[clear H; intro H; lapply H|]`

?)`assert P as Hp by admit. specialize (Hpq Hp).`

Here you have to specify the type of`Hp`

`specialize (Hpq ltac:(some_tac)).`

This doesn't give you interactivity

These are all kind of suboptimal and I would really want to specify it as a term and prove it in a subgoal, like a mix of 1 and 3.

I kind of have the feeling that there was some ssreflect feature where you could do something like

```
move/(_ #) in Hpq.
```

which would give a situation like in `lapply Hpq`

but I might have dreamt that one up...

I'd recommend `opose proof (Hpq _)`

from stdpp https://gitlab.mpi-sws.org/iris/stdpp/-/blob/dd93e4c3b23f25b208a6adaabacdb97c73c0059d/stdpp/tactics.v#L593

Or `opose proof* Hpq`

The latter will produce a subgoal for each premise of Hpq; the former will only turn underscore into subgoals, at least if the passed term has a non-dependent function type. (Goals for forall quantifiers are turned into evars that appear in other goals)

`ospecialize (Hpq _)`

is pretty much 100% what I had in mind, thanks a lot!

Would be nice to have this directly in ssreflect as well

Last updated: Jun 13 2024 at 19:02 UTC