Is there a version of `apply t in H`

that doesn't try to instantiate the parameters of `t`

after the one that matches `H`

? I have a certain object with projections and I'd like to apply a lemma along the lines of `forall obj, P obj -> forall i, P (projection i obj)`

to a hypothesis `P obj`

, but the tactic fails saying it can't guess `i`

.

that error could be fixed by `eapply`

, but if you want to get `forall i, ...`

, I'd recommend `pose proof (t _ H)`

instead

(omit `_`

if `obj`

was marked as implicit, as it IMHO should be)

I am already using `pose proof`

. I'd like to get a `forall i, ...`

conclusion while keeping all the usual advantages of `apply t in H`

over `pose proof (t _ _ (* count carefully*) H) as H';clear H';rename H' into H`

.

What about `specialize t with (1 := H) as H'`

?

You will still need the `clear H'; rename H' into H`

dance though because specialize accepts to clear the hypothesis you specialize but not the one you pass as an argument.

I’d recommend Set Implicit Arguments to avoid counting.

I like how that avoids writing `_`

for dependent parameters. But I would also like to know if there is a solution that will make extra subgoals if `t`

has some earlier hypotheses that are not completely filled in by unification. My current lemma and the example I wrote above doesn't demonstrate that, but it's another reason I usually use `apply _ in`

instead of `pose proof`

when I can.

`move: H => /t H`

But that’s still just `specialize`

, it doesn’t create subgoals.

If `pose`

or `specialize`

could make subgoals like `refine`

does that would work, but I don't remember any variants that do that.

I think `apply`

would work if the `forall`

was hidden behind a named definition. I wouldn't want to write a custom definition for every lemma, but maybe there's another way to control where apply decides the arguments end and the conclusion begins?

Brandon Moore said:

If

`pose`

or`specialize`

could make subgoals like`refine`

does that would work, but I don't remember any variants that do that.

epose ?

That's one I had forgotten. To give goals rather than unresolved existentials, `unshelve epose proof`

seems to work.

Last updated: May 24 2024 at 21:01 UTC