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.

ink

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

ink

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

ink

def Std.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]"
→ 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]"
→ 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.

ink

opaque Std.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))↦ (x ↦ (stx, simps))↦ (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.

ink

def Std.Tactic.dsimpLocation' (ctx : Lean.Meta.Simp.Context) (loc : Lean.Elab.Tactic.Location) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.UsedSimps

Implementation of dsimp.

Equations

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

ink

def Std.Tactic.dsimpLocation'.go (ctx : Lean.Meta.Simp.Context) (fvarIdsToSimp : Array Lean.FVarId) (simplifyTarget : Bool) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.UsedSimps

Implementation of dsimp.

Equations

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