modus ponens in context

Stream: Is there code for X?

[Patrick Thomas]

If I have P -> Q and P in the context, is there a tactic that will add Q to the context?

[Johan Commelin]

I think apply_fun f at x do it, if f : P -> Q and x : P.

[Johan Commelin]

But have := f x or let y := f x also work.

[Patrick Thomas]

Thank you.

[Patrick Thomas]

apply_fun doesn't seem to work, but let does,

[Scott Morrison]

You might need to import tactic.basic for apply_fun.

[Patrick Thomas]

I still get, failed to apply f at x.

[Scott Morrison]

Can you post a #mwe?

[Eric Wieser]

Isn't apply_fun for equalities not implications?

[Yaël Dillies]

Yup, as far as I know all it does is using congr_arg.

[Scott Morrison]

apply_fun X at Y definitely does more than congr_arg!

[Scott Morrison]

But yes, it doesn't do this.

[Yaël Dillies]

I should really know better :sweat_smile:

[Johan Commelin]

Sorry for the apply_fun suggestion. I should have know that it doesn't work here.

[Scott Morrison]

It's so tempting though. We use apply many ways in informal maths.

[Scott Morrison]

I think it's reasonable to have apply_fun's semantics be "please do something sensible with this function (at this location)". So we should support it. :-)

[Scott Morrison]

@Patrick Thomas, often useful in similar situations is tactic#specialize.

[Eric Wieser]

I don't think this is such a case though; apply_fun f means "put f on the right of the colon somewhere". In the case we're talking about, it would mean "use this to construct the term"

[Yaël Dillies]

specialize is indeed what you want.

[Patrick Thomas]

I think Coq might have an apply in tactic?

[Bhavik Mehta]

iirc Coq has apply atfor this, in Lean you can also do replace x := f x to mimic this behaviour, but I generally prefer Johan's original suggestion of have := f x in case I want x : P later

[Eric Wieser]

I think apply at would make sense for lean to support

[Alex J. Best]

No idea if this code still works but there looks to be an implementation here: https://github.com/jldodds/coq-lean-cheatsheet/blob/master/coq-tactic-substitutes.lean, edit: or is apply in different to apply at?