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 Lean.Parser.Term.do : termdo notation into a number of smaller verification conditions (VCs) that are sufficient to prove the goal. In addition to a reference that describes the use of mvcgen, this chapter includes a tutorial that can be read independently of the reference.

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

1. 18.1. Overview
2. 18.2. Predicate Transformers
3. 18.3. Verification Conditions
4. 18.4. Enabling mvcgen For Monads
5. 18.5. Proof Mode
6. 18.6. Tutorial: Verifying Imperative Programs Using mvcgen