Documentation

Batteries.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.
Instances For

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

      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 : NatNatNat
        | 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.
      Instances For

        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.