Can't follow "Tutorial: tactic writing in Lean"

Stream: general

[Sorawee Porncharoenwase]

The following code is copied from the tutorial page at https://leanprover-community.github.io/extras/tactic_writing.html. It works perfectly:

open tactic.interactive («have»)
open tactic (get_local infer_type)
open interactive (parse)
open lean.parser (ident)

meta def tactic.interactive.add_eq (h1 : parse ident) (h2 : parse ident) : tactic unit :=
do e1 ← tactic.get_local h1,
   e2 ← tactic.get_local h2,
   «have» none none ``(_root_.congr (congr_arg has_add.add %%e1) %%e2)

example (a b j k : ℤ) (h₁ : a = b) (h₂ : j = k) :
  a + j = b + k :=
begin
  add_eq h₁ h₂,
  exact this,
end

But now, let's add some namespace around the meta definition and the example, then suddenly it doesn't work anymore:

open tactic.interactive («have»)
open tactic (get_local infer_type)
open interactive (parse)
open lean.parser (ident)

namespace foo

meta def tactic.interactive.add_eq (h1 : parse ident) (h2 : parse ident) : tactic unit :=
do e1 ← tactic.get_local h1,
   e2 ← tactic.get_local h2,
   «have» none none ``(_root_.congr (congr_arg has_add.add %%e1) %%e2)

example (a b j k : ℤ) (h₁ : a = b) (h₂ : j = k) :
  a + j = b + k :=
begin
  add_eq h₁ h₂,
  exact this,
end

end foo

outputs:

unknown identifier 'add_eq'
unknown identifier 'h₁'
unknown identifier 'h₂'

I tried adding open tactic.interactive inside the namespace, but that doesn't work too.

Lastly, I tried renaming tactic.interactive.add_eq to add_eq. Now, add_eq is bound, but h₁ and h₂ remain unbound.

What's going on? Thanks!

[Kevin Buzzard]

You're in the foo namespace so are defining foo.tactic.interactive.add_eq, which tactic mode will not pick up.

[Eric Wieser]

What makes the tactic.interactive namespace special? Is it the C++ language implementation, or something bootstrapped in some lean code?

[Sorawee Porncharoenwase]

Ah, that makes sense. The question then is how to workaround the problem? My tactic mentions a lemma defined in the very same namespace, so I can't simply lift the tactic outside of the namespace.

Well, one possibility that works is to split the namespace into two parts, with the tactic defined at the middle. It works but I'm not sure if it's the best solution.

namespace foo
lemma ...
end foo

meta def tactic.interactive... use the lemma here

namespace foo
use the tactic
end foo

[Eric Wieser]

I think the @[interactive] attribute exists for precisely this reason

[Eric Wieser]

Which IIRC, just renames the lemma after its declared so that it behaves as if you'd done the namespace reopening

[Mario Carneiro]

Eric Wieser said:

What makes the tactic.interactive namespace special? Is it the C++ language implementation, or something bootstrapped in some lean code?

The tactic.interactive namespace is special. Anything in it is declared as a top level tactic in begin ... end blocks. More generally, you can define alternate tactic modes in the foo.interactive namespace if you use begin [foo] ... end

[Mario Carneiro]

the name binding is hard coded in the c++

[Eric Wieser]

Does this work for begin [foo.bar] and foo.bar.interactive too?

[Reid Barton]

Yes