Stream: Coq users

Topic: Extent of "conclusion" for apply _ in


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 24 2020 at 16:39):

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

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Nov 24 2020 at 17:00):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 24 2020 at 17:07):

I’d recommend Set Implicit Arguments to avoid counting.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Nov 24 2020 at 17:09):

move: H => /t H

view this post on Zulip Paolo Giarrusso (Nov 24 2020 at 17:09):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 ?

view this post on Zulip 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: Jan 31 2023 at 12:01 UTC