Identifiers in auto-param tactics

Stream: lean4

[Jannis Limperg]

Auto-param tactics currently can't contain identifiers:

def T := True

structure Foo where
  x : T := by simp [T] -- invalid auto tactic, identifier is not allowed

Does anyone know why this is? Perhaps the purpose is to ensure that the tactic doesn't depend on fvars, but then it would suffice to check that all identifiers resolve to global constants.

The issue can be worked around with macros:

def T := True

local macro "simp_with_T" : tactic => `(tactic| simp [T])

structure Foo where
  x : T := by simp_with_T

However, this is a lot of ceremony for one auto-param.

A real example where this came up: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Coxeter.20Groups/near/421120660

[James Gallicchio]

would thumbsup an issue for this :big_smile:

[Kim Morrison]

I think you can thumbs up the draft of a fix by Mario: lean4#3328

[Eric Wieser]

Here's a really nasty workaround in the meantime:

elab "just_let_me_use_the_tactic" s:str : tactic => do
  match Lean.Parser.runParserCategory (← Lean.getEnv) `tactic s.getString with
  | .error e => throwErrorAt s e
  | .ok t => Lean.Elab.Tactic.evalTactic t

structure AlwaysOne'' where
  one : Nat
  one_eq : one = 1 := by just_let_me_use_the_tactic "exact rfl"

[Eric Wieser]

Unfortunately this emits the error message from the exact rfl on the very first line of the file using it!

[Kyle Miller]

Hacks upon hacks, this puts the error at the right position :upside_down:

elab "just_let_me_use_the_tactic" s:str : tactic => do
  let r ← getRef
  let p := if let some pos := r.getPos? then String.replicate pos.byteIdx ' ' else ""
  match Lean.Parser.runParserCategory (← Lean.getEnv) `tactic (p ++ s.getString) with
  | .error e => throwErrorAt s e
  | .ok t => Lean.Elab.Tactic.evalTactic t

[Mario Carneiro]

The subscript parser instead goes over the syntax and adds the right offset to everything