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
that error could be fixed by
eapply, but if you want to get
forall i, ..., I'd recommend
pose proof (t _ H) instead
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.
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.
specialize could make subgoals like
refine does that would work, but I don't remember any variants that do that.
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:
specializecould make subgoals like
refinedoes that would work, but I don't remember any variants that do that.
That's one I had forgotten. To give goals rather than unresolved existentials,
unshelve epose proof seems to work.
Last updated: Sep 26 2023 at 11:01 UTC