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.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.