Stream: Coq users

Topic: Extent of "conclusion" for apply _ in

Brandon Moore (Nov 24 2020 at 16:08):

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.

Paolo Giarrusso (Nov 24 2020 at 16:38):

that error could be fixed by eapply, but if you want to get forall i, ..., I'd recommend pose proof (t _ H) instead

Paolo Giarrusso (Nov 24 2020 at 16:39):

(omit _ if obj was marked as implicit, as it IMHO should be)

Brandon Moore (Nov 24 2020 at 16:55):

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.

Théo Zimmermann (Nov 24 2020 at 17:00):

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

Théo Zimmermann (Nov 24 2020 at 17:01):

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.

Paolo Giarrusso (Nov 24 2020 at 17:07):

I’d recommend Set Implicit Arguments to avoid counting.

Brandon Moore (Nov 24 2020 at 17:07):

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.

Paolo Giarrusso (Nov 24 2020 at 17:09):

move: H => /t H

Paolo Giarrusso (Nov 24 2020 at 17:09):

But that’s still just specialize, it doesn’t create subgoals.

Brandon Moore (Nov 24 2020 at 17:10):

If pose or specialize could make subgoals like refine does that would work, but I don't remember any variants that do that.

Brandon Moore (Nov 24 2020 at 17:12):

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?

Kenji Maillard (Nov 24 2020 at 17:24):

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 ?

Brandon Moore (Nov 24 2020 at 17:33):

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

Last updated: Oct 12 2024 at 11:01 UTC