squeeze_scope tactic

The squeeze_scope tactic allows aggregating multiple calls to simp coming from the same syntax but in different branches of execution, such as in cases x <;> simp. The reported simp call covers all simp lemmas used by this syntax.

def Batteries.Tactic.squeezeScopeIn : Lean.ParserDescr

squeeze_scope a => tacs is part of the implementation of squeeze_scope. Inside tacs, invocations of simp wrapped with squeeze_wrap a _ => ... will contribute to the accounting associated to scope a.

Equations

• One or more equations did not get rendered due to their size.

def Batteries.Tactic.squeezeWrap : Lean.ParserDescr

squeeze_wrap a x => tac is part of the implementation of squeeze_scope. Here tac will be a simp or dsimp syntax, and squeeze_wrap will run the tactic and contribute the generated usedSimps to the squeezeScopes[a][x] variable.

Equations

• One or more equations did not get rendered due to their size.

def Batteries.Tactic.squeezeScope : Lean.ParserDescr

The squeeze_scope tactic allows aggregating multiple calls to simp coming from the same syntax but in different branches of execution, such as in cases x <;> simp. The reported simp call covers all simp lemmas used by this syntax.

@[simp] def bar (z : Nat) := 1 + z
@[simp] def baz (z : Nat) := 1 + z

@[simp] def foo : Nat → Nat → Nat
  | 0, z => bar z
  | _+1, z => baz z

example : foo x y = 1 + y := by
  cases x <;> simp? -- two printouts:
  -- "Try this: simp only [foo, bar]"
  -- "Try this: simp only [foo, baz]"

example : foo x y = 1 + y := by
  squeeze_scope
    cases x <;> simp -- only one printout: "Try this: simp only [foo, baz, bar]"

Equations

• One or more equations did not get rendered due to their size.

opaque Batteries.Tactic.squeezeScopes : IO.Ref (Lean.NameMap (Lean.NameMap (Lean.Syntax × List Lean.Meta.Simp.UsedSimps)))

We implement squeeze_scope using a global variable that tracks all squeeze_scope invocations in flight. It is a map a => (x => (stx, simps)) where a is a unique identifier for the squeeze_scope invocation which is shared with all contained simps, and x is a unique identifier for a particular piece of simp syntax (which can be called multiple times). Within that, stx is the simp syntax itself, and simps is the aggregated list of simps used so far.