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.