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>
37 lines
1 KiB
Text
37 lines
1 KiB
Text
import Lean
|
||
import Std.Tactic.Do
|
||
|
||
open Lean Meta Elab Tactic Sym Std Do SpecAttr
|
||
|
||
namespace AddSubCancel
|
||
|
||
set_option mvcgen.warning false
|
||
|
||
-- The following specs partially evaluate the specs for `get` and `set` that otherwise would need
|
||
-- multiple small substeps in the modular lifting framework. This is good practice for performance
|
||
-- sensitive use cases.
|
||
|
||
@[spec high]
|
||
theorem Spec.MonadState_get {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond σ (.arg σ ps)} :
|
||
⦃fun s => Q.fst s s⦄ get (m := StateT σ m) ⦃Q⦄ := by
|
||
mvcgen'
|
||
|
||
@[spec high]
|
||
theorem Spec.MonadStateOf_set {m ps} [Monad m] [WPMonad m ps] {σ} {Q : PostCond PUnit (.arg σ ps)} {s : σ} :
|
||
⦃fun _ => Q.fst ⟨⟩ s⦄ set (m := StateT σ m) s ⦃Q⦄ := by
|
||
mvcgen'
|
||
|
||
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 AddSubCancel
|