apply at

Stream: new members

[Mike Shulman]

Sorry if this is a dumb question. If I have a hypothesis x : A and a lemma f : A -> B, is there a tactic that will replace my hypothesis x : A by x : B? In Coq I would write apply f in x. In Lean I expected to be able to write apply f at x since that's the syntax used for rewrite, simp, unfold, etc. acting on a hypothesis, but it doesn't work. Is there a standard tactic that does this?

[Adam Topaz]

replace x := f x

[Adam Topaz]

Or tactic#apply_fun

[Adam Topaz]

hmmm actually apply_fun doesn't work.

[Adam Topaz]

but replace will work, of course.

[Adam Topaz]

Sorry, I was stupid -- apply_fun will apply f to things like h : a = b where a b : A, yielding h : f a = f b

[Heather Macbeth]

specialize f x should work, tactic#specialize

[Eric Wieser]

specialize is replace f := f x not replace x := f x

[Eric Wieser]

apply at has been suggested before

[Eric Wieser]

And here, and here

[Mike Shulman]

Ok, thanks. That's disappointing that it doesn't exist.

[Adam Topaz]

Is this a good idea for Mathlib4?

macro "apply" f:term "at" h:ident : tactic => `(replace $h := $f $h)

[Matthew Ballard]

Do you want apply [f] at h or are we rebelling against the []?

[Adam Topaz]

why the [f]?

[Adam Topaz]

This works

import Mathlib
import Lean

open Lean

macro "apply" f:term "at" h:ident : tactic => `(replace $h := $f $h)

example {α β : Type _} {a : α} (f : α → β) : β := by
  apply f at a
  exact a

[Matthew Ballard]

What I expect from rw?

[Adam Topaz]

Oh, do you want to be able to apply multiple functions as well? That's an interesting idea!

[Matthew Ballard]

It would be nice.

[Adam Topaz]

import Mathlib
import Lean

open Lean

elab "apply" "[" fs:term,* "]" "at" h:ident : tactic => do
  for f in fs.getElems do
    Elab.Tactic.evalTactic $ ← `(tactic| replace $h := $f $h)


example {α β γ : Type _} {a : α} (f : α → β) (g : β → γ) : γ := by
  apply [f, g] at a
  exact a

[Adam Topaz]

There's probably a better way to handle the parsing

[Eric Wieser]

From my post here, I'd argue the semantics should be to insert underscores:

Eric Wieser said:

Should the semantics instead be replace h := f _* h? That way apply f _ _ at h is similar to apply f at h in the same way that apply f _ _ is similar to apply f.

[Yaël Dillies]

It would, because as I said above you could end up with a discrete order.

[Kevin Buzzard]

Sorry for necro-ing this thread but I just found it when searching for the apply at thread I started yesterday. The underscores are now being inserted in this version of apply at.