18. The mvcgen tactic🔗

The mvcgen tactic implements a monadic verification condition generator: It breaks down a goal involving a program written using Lean's imperative do notation into a number of pure verification conditions (VCs) that discharge said goal. A verification condition is a sub-goal that does not mention the monad underlying the do block.

In order to use the mvcgen tactic, Std.Tactic.Do must be imported and the namespace Std.Do must be opened.

import Std.Tactic.Do
open Std.Do

1. 18.1. Verifying imperative programs using mvcgen