Documentation

Std.Tactic.SqueezeScope

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.

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.

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.

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.

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.

Implementation of dsimp.

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

Implementation of dsimp.

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