hygiene question?

Stream: lean4

[Scott Morrison]

I'm trying to write a thin wrapper around aesop, that always includes a particular rule set:

declare_aesop_rule_sets [CategoryTheory]

/-- A thin wrapper for `aesop`, which adds the `CategoryTheory` rule set. -/
macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause*: tactic =>
  `(tactic| aesop $c* (rule_sets [CategoryTheory]))

However with set_option trace.Elab.step true, I can see that aesop_cat is expanding to aesop (rule_sets [CategoryTheory✝]), i.e. CategoryTheory is not referring to the "real" one.

How do I refer to the one I've just declared?

[Gabriel Ebner]

That's normal. The CategoryTheory✝ means that it can refer to a local variable bound inside the quotation in addition to the global name.

[Scott Morrison]

#mwe:

import Aesop

declare_aesop_rule_sets [ExtraRules]

/-- A thin wrapper for `aesop`, which adds the `ExtraRules` rule set. -/
macro (name := aesop_extra) "aesop_extra" c:Aesop.tactic_clause*: tactic =>
  `(tactic| aesop $c* (rule_sets [ExtraRules]))

-- We turn on `funext` inside `aesop_extra`.
attribute [aesop safe apply (rule_sets [ExtraRules])] funext

example {f g : α → β} (w : ∀ a, f a = g a) : f = g := by
  -- Check `aesop` can't do it.
  aesop
  sorry

example {f g : α → β} (w : ∀ a, f a = g a) : f = g := by aesop (add safe apply funext)

example {f g : α → β} (w : ∀ a, f a = g a) : f = g := by aesop (rule_sets [ExtraRules])

example {f g : α → β} (w : ∀ a, f a = g a) : f = g := by
  aesop_extra
  -- Should be solved now, but isn't.
  sorry

[Scott Morrison]

set_option hygiene false in works, but I feel dirty. :-)

[Sebastian Ullrich]

If ExtraRules is not an actual declaration name in the environment, Aesop is probably missing an eraseMacroScopes somewhere

[Scott Morrison]

@Jannis Limperg, pinging to see if you know where this might be.

[Jannis Limperg]

I can eraseMacroScopes wherever I handle rule set names, but at least in principle it could be valid to have a hygienic rule set name (e.g. coming from a macro that defines a rule set). Alternatively, you can explicitly circumvent hygiene from within the macro:

macro (name := aesop_extra) "aesop_extra" c:Aesop.tactic_clause*: tactic =>
  `(tactic| aesop $c* (rule_sets [$(Lean.mkIdent `ExtraRules):ident]))

[Sebastian Ullrich]

The hygiene system needs to be aware of scopes to function correctly. The only global scopes it is aware of are the environment and section variables.

[Wojciech Nawrocki]

Jannis Limperg said:

I can eraseMacroScopes wherever I handle rule set names, but at least in principle it could be valid to have a hygienic rule set name (e.g. coming from a macro that defines a rule set). Alternatively, you can explicitly circumvent hygiene from within the macro:

macro (name := aesop_extra) "aesop_extra" c:Aesop.tactic_clause*: tactic =>
  `(tactic| aesop $c* (rule_sets [$(Lean.mkIdent `ExtraRules):ident]))

(Ignore me if this has been resolved, although on newest mathlib4 the hygiene false still seems to be needed.)

What Gabriel is saying above, I think, is that hygienic names such as Foo✝ refer both to Foo and Foo✝. This is so that we can write macros like this one

`(
  def foo := 3
  def bar : Nat := foo)

which will elaborate to

def foo✝ := 3
def bar✝ : Nat✝ := foo✝

where foo✝ will refer to the value introduced by the macro, but Nat✝ will refer to the real Nat. The transformation Name ↦ Name✝ essentially makes all inaccessible names introduced in the current macro scope accessible; but it shouldn't make global names inaccessible. Thus the burden falls on all tactic code to eraseMacroScopes when resolving names..

at least in principle it could be valid to have a hygienic rule set name (e.g. coming from a macro that defines a rule set)

..but this is a valid point. Here is an example to demonstrate the issue.

elab "#resolve" n:ident : command => do
  let nm ← resolveGlobalConstWithInfos n
  logInfo m!"resolve: {nm}"

elab "#resolveEMS" n:ident : command => do
  let nm ← resolveGlobalConstWithInfos (mkIdentFrom n n.getId.eraseMacroScopes)
  logInfo m!"resolveEMS: {nm}"

elab "#test" : command => do
  let stx ← `(
    def foo := 3
    def bar : Nat := foo
    #resolve bar
    #resolveEMS bar)
  elabCommand stx

/- resolve: [bar._@.Mathlib.CategoryTheory.Category.Basic._hyg.661] -/
/- (from resolveEMS) unknown constant 'bar' -/
#test

Does this means that tactics should always try to resolve both n and n.eraseMacroScopes? I am not sure if there is a canonical way to do it. (CC @Sebastian Ullrich)

[Sebastian Ullrich]

Wojciech Nawrocki said:

What Gabriel is saying above, I think, is that hygienic names such as Foo✝ refer both to Foo and Foo✝

Whether that is true depends on the exact scopes stored in the identifier. If Foo was in the global scope at the point of the syntax quotation, any identifier Foo inside of the quotation will get a corresponding global scope tag and can resolve to it. If Foo was not in the scope at the point of declaration, then any reference will not and should not refer to it, no. So a tactic should use eraseMacroScopes iff an identifier is not meant to be a Lean declaration reference.

The capture of scopes in quoted identifiers is a non-extensible part of the quotation elaborator, though we recently moved a little towards extensibility by acknowledging that different kinds of scopes exist.

[Sebastian Ullrich]

Long story short, the simplest way to ensure that rule set references are hygienic would be to make rule sets actual Lean declarations. That doesn't necessarily mean that their information must be stored in the declarations too, they could simply be stubs.