422920f643
This PR adds an experimental tactic `mvcgen'` that will soon replace `mvcgen`. It has been reimplemented from the ground up using the new `SymM`-based framework for efficient symbolic evaluation and can outperform `mvcgen` by a factor of >100x for some synthetic benchmarks. `mvcgen'` aspires to be feature-complete with `mvcgen`. Known exceptions currently are join point sharing, introduction of local specs and smaller bugs. The implementation of `mvgen'` used to live in the benchmark suite for rapid prototyping; this commit merely moves it into the Lean toolchain. Doing so results in an build time instruction count increase in seemingly unrelated tests such as `elab/delayed_assign//instructions`; the reason is that the builtin elaborator attribute now pulls in substantially more import code on startup. --------- Co-authored-by: Sebastian Graf <sg@lean-fro.org>
36 lines
897 B
Text
36 lines
897 B
Text
import Lean
|
||
import Std.Tactic.Do
|
||
|
||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||
|
||
namespace AddSubCancelSimp
|
||
|
||
set_option mvcgen.warning false
|
||
|
||
-- Same benchmark as `AddSubCancel` but using simp spec equations instead of triple specs
|
||
-- for `get` and `set`. This exercises the `reduceSimpSpec` + `replaceTargetEq` code path.
|
||
|
||
@[spec high]
|
||
theorem Spec.MonadState_get {m} [Monad m] {σ} :
|
||
get (m := StateT σ m) = fun s => pure (s, s) := by
|
||
rfl
|
||
|
||
@[spec high]
|
||
theorem Spec.MonadStateOf_set {m} [Monad m] {σ} {s : σ} :
|
||
set (m := StateT σ m) s = fun _ => pure (⟨⟩, s) := by
|
||
rfl
|
||
|
||
def step (v : Nat) : StateM Nat Unit := do
|
||
let s ← get
|
||
set (s + v)
|
||
let s ← get
|
||
set (s - v)
|
||
|
||
def loop (n : Nat) : StateM Nat Unit := do
|
||
match n with
|
||
| 0 => pure ()
|
||
| n+1 => step n; loop n
|
||
|
||
def Goal (n : Nat) : Prop := ∀ post, ⦃post⦄ loop n ⦃⇓_ => post⦄
|
||
|
||
end AddSubCancelSimp
|