structure Lean.Elab.Tactic.Do.VCGen.Config : Type

• trivial : Bool

  If true (the default), we will try to prove VCs via mvcgen_trivial, which is extensible via macro_rules.

• leave : Bool

  If true (the default), we will simplify every generated VC after trying mvcgen_trivial by running mleave. (Note that this can be expensive.)

• elimLets : Bool

  If true (the default), we substitute away let-declarations that are used at most once before starting VC generation and will do the same for every VC generated.

• jp : Bool

  If false (the default), then we aggresively split if and match statements and inline join points unconditionally. For some programs this causes exponential blowup of VCs. Set this flag to choose a more conservative (but slightly lossy) encoding that traverses every join point only once and yields a formula the size of which is linear in the number of control flow splits.

• stepLimit : Option Nat

  If set to some n, mvcgen will only do 42 steps of the VC generation procedure. This is helpful for bisecting bugs in mvcgen and tracing its execution.

def Lean.Parser.Attr.spec : ParserDescr

Theorems tagged with the spec attribute are used by the mspec and mvcgen tactics.

• When used on a theorem foo_spec : Triple (foo a b c) P Q, then mspec and mvcgen will use foo_spec as a specification for calls to foo.
• Otherwise, when used on a definition that @[simp] would work on, it is added to the internal simp set of mvcgen that is used within wp⟦·⟧ contexts to simplify match discriminants and applications of constants.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.massumption : ParserDescr

massumption is like assumption, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : Q ⊢ₛ P → Q := by
  mintro _ _
  massumption

Equations

• Lean.Parser.Tactic.massumption = Lean.ParserDescr.node `Lean.Parser.Tactic.massumption 1024 (Lean.ParserDescr.nonReservedSymbol "massumption" false)

def Lean.Parser.Tactic.mclear : ParserDescr

mclear is like clear, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ Q → Q := by
  mintro HP
  mintro HQ
  mclear HP
  mexact HQ

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mconstructor : ParserDescr

mconstructor is like constructor, but operating on a stateful Std.Do.SPred goal.

example (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by
  mintro HQ
  mconstructor <;> mexact HQ

Equations

• Lean.Parser.Tactic.mconstructor = Lean.ParserDescr.node `Lean.Parser.Tactic.mconstructor 1024 (Lean.ParserDescr.nonReservedSymbol "mconstructor" false)

def Lean.Parser.Tactic.mexact : ParserDescr

mexact is like exact, but operating on a stateful Std.Do.SPred goal.

example (Q : SPred σs) : Q ⊢ₛ Q := by
  mstart
  mintro HQ
  mexact HQ

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mexfalso : ParserDescr

mexfalso is like exfalso, but operating on a stateful Std.Do.SPred goal.

example (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by
  mintro HP
  mexfalso
  mexact HP

Equations

• Lean.Parser.Tactic.mexfalso = Lean.ParserDescr.node `Lean.Parser.Tactic.mexfalso 1024 (Lean.ParserDescr.nonReservedSymbol "mexfalso" false)

def Lean.Parser.Tactic.mexists : ParserDescr

mexists is like exists, but operating on a stateful Std.Do.SPred goal.

example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mexists 42

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mframe : ParserDescr

mframe infers which hypotheses from the stateful context can be moved into the pure context. This is useful because pure hypotheses "survive" the next application of modus ponens (Std.Do.SPred.mp) and transitivity (Std.Do.SPred.entails.trans).

It is used as part of the mspec tactic.

example (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
  mintro _
  mframe
  /- `h : p ∧ q ∧ r ∧ s ∧ t` in the pure context -/
  mcases h with hP
  mexact h

Equations

• Lean.Parser.Tactic.mframe = Lean.ParserDescr.node `Lean.Parser.Tactic.mframe 1024 (Lean.ParserDescr.nonReservedSymbol "mframe" false)

def Lean.Parser.Tactic.mdup : ParserDescr

Duplicate a stateful Std.Do.SPred hypothesis.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mhave : ParserDescr

mhave is like have, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HQ

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mreplace : ParserDescr

mreplace is like replace, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ
  mexact HPQ

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mright : ParserDescr

mright is like right, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ Q ∨ P := by
  mintro HP
  mright
  mexact HP

Equations

• Lean.Parser.Tactic.mright = Lean.ParserDescr.node `Lean.Parser.Tactic.mright 1024 (Lean.ParserDescr.nonReservedSymbol "mright" false)

def Lean.Parser.Tactic.mleft : ParserDescr

mleft is like left, but operating on a stateful Std.Do.SPred goal.

example (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by
  mintro HP
  mleft
  mexact HP

Equations

• Lean.Parser.Tactic.mleft = Lean.ParserDescr.node `Lean.Parser.Tactic.mleft 1024 (Lean.ParserDescr.nonReservedSymbol "mleft" false)

def Lean.Parser.Tactic.mpure : ParserDescr

mpure moves a pure hypothesis from the stateful context into the pure context.

example (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
  mintro Hφ
  mpure Hφ
  mexact (ψ Hφ)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mpureIntro : ParserDescr

mpure_intro operates on a stateful Std.Do.SPred goal of the form P ⊢ₛ ⌜φ⌝. It leaves the stateful proof mode (thereby discarding P), leaving the regular goal φ.

theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by
  mpure_intro
  exact True.intro

Equations

• Lean.Parser.Tactic.mpureIntro = Lean.ParserDescr.node `Lean.Parser.Tactic.mpureIntro 1024 (Lean.ParserDescr.nonReservedSymbol "mpure_intro" false)

def Lean.Parser.Tactic.mrenameI : ParserDescr

mrename_i is like rename_i, but names inaccessible stateful hypotheses in a Std.Do.SPred goal.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mspecialize : ParserDescr

mspecialize is like specialize, but operating on a stateful Std.Do.SPred goal. It specializes a hypothesis from the stateful context with hypotheses from either the pure or stateful context or pure terms.

example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
  mintro HP HPQ
  mspecialize HPQ HP
  mexact HPQ

example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
  mintro HQ HΨ
  mspecialize HΨ (y + 1) hP HQ
  mexact HΨ

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mspecializePure : ParserDescr

mspecialize_pure is like mspecialize, but it specializes a hypothesis from the pure context with hypotheses from either the pure or stateful context or pure terms.

example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by
  mintro HQ
  mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ
  mexact HΨ

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mstart : ParserDescr

Start the stateful proof mode of Std.Do.SPred. This will transform a stateful goal of the form H ⊢ₛ T into ⊢ₛ H → T upon which mintro can be used to re-introduce H and give it a name. It is often more convenient to use mintro directly, which will try mstart automatically if necessary.

Equations

• Lean.Parser.Tactic.mstart = Lean.ParserDescr.node `Lean.Parser.Tactic.mstart 1024 (Lean.ParserDescr.nonReservedSymbol "mstart" false)

def Lean.Parser.Tactic.mstop : ParserDescr

Stops the stateful proof mode of Std.Do.SPred. This will simply forget all the names given to stateful hypotheses and pretty-print a bit differently.

Equations

• Lean.Parser.Tactic.mstop = Lean.ParserDescr.node `Lean.Parser.Tactic.mstop 1024 (Lean.ParserDescr.nonReservedSymbol "mstop" false)

def Lean.Parser.Tactic.mleave : ParserDescr

Leaves the stateful proof mode of Std.Do.SPred, tries to eta-expand through all definitions related to the logic of the Std.Do.SPred and gently simplifies the resulting pure Lean proposition. This is often the right thing to do after mvcgen in order for automation to prove the goal.

Equations

• Lean.Parser.Tactic.mleave = Lean.ParserDescr.node `Lean.Parser.Tactic.mleave 1024 (Lean.ParserDescr.nonReservedSymbol "mleave" false)

def Lean.Parser.Category.mcasesPat : Category

Equations

• Lean.Parser.Category.mcasesPat = { }

def Lean.Parser.Tactic.mcasesPat.quot : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mcasesPatAlts : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mcasesPat_ : ParserDescr

Equations

• Lean.Parser.Tactic.mcasesPat_ = Lean.ParserDescr.node `Lean.Parser.Tactic.mcasesPat_ 1022 Lean.binderIdent

def Lean.Parser.Tactic.«mcasesPat-» : ParserDescr

Equations

• Lean.Parser.Tactic.«mcasesPat-» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mcasesPat-» 1024 (Lean.ParserDescr.symbol "-")

def Lean.Parser.Tactic.«mcasesPat⟨_⟩» : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.«mcasesPat(_)» : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.«mcasesPat⌜_⌝» : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.«mcasesPat□_» : ParserDescr

Equations

• Lean.Parser.Tactic.«mcasesPat□_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mcasesPat□_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") Lean.binderIdent)

def Lean.Parser.Tactic.«mcasesPat%_» : ParserDescr

Equations

• Lean.Parser.Tactic.«mcasesPat%_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mcasesPat%_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "%") Lean.binderIdent)

def Lean.Parser.Tactic.«mcasesPat#_» : ParserDescr

Equations

• Lean.Parser.Tactic.«mcasesPat#_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mcasesPat#_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") Lean.binderIdent)

inductive Lean.Parser.Tactic.MCasesPat : Type

• one (name : TSyntax `Lean.binderIdent) : MCasesPat
• clear : MCasesPat
• tuple (args : List MCasesPat) : MCasesPat
• alts (args : List MCasesPat) : MCasesPat
• pure (h : TSyntax `Lean.binderIdent) : MCasesPat
• stateful (h : TSyntax `Lean.binderIdent) : MCasesPat

instance Lean.Parser.Tactic.instReprMCasesPat : Repr MCasesPat

Equations

• Lean.Parser.Tactic.instReprMCasesPat = { reprPrec := Lean.Parser.Tactic.reprMCasesPat✝ }

instance Lean.Parser.Tactic.instInhabitedMCasesPat : Inhabited MCasesPat

Equations

• Lean.Parser.Tactic.instInhabitedMCasesPat = { default := Lean.Parser.Tactic.MCasesPat.one default }

def Lean.Parser.Tactic.MCasesPat.parse (pat : TSyntax `mcasesPat) : MacroM MCasesPat

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Parser.Tactic.MCasesPat.parse.go : TSyntax `mcasesPat → Option MCasesPat

partial def Lean.Parser.Tactic.MCasesPat.parse.goAlts : TSyntax `Lean.Parser.Tactic.mcasesPatAlts → Option MCasesPat

def Lean.Parser.Tactic.mcases : ParserDescr

Like rcases, but operating on stateful Std.Do.SPred goals. Example: Given a goal h : (P ∧ (Q ∨ R) ∧ (Q → R)) ⊢ₛ R, mcases h with ⟨-, ⟨hq | hr⟩, hqr⟩ will yield two goals: (hq : Q, hqr : Q → R) ⊢ₛ R and (hr : R) ⊢ₛ R.

That is, mcases h with pat has the following semantics, based on pat:

• pat=□h' renames h to h' in the stateful context, regardless of whether h is pure
• pat=⌜h'⌝ introduces h' : φ to the pure local context if h : ⌜φ⌝ (c.f. Lean.Elab.Tactic.Do.ProofMode.IsPure)
• pat=h' is like pat=⌜h'⌝ if h is pure (c.f. Lean.Elab.Tactic.Do.ProofMode.IsPure), otherwise it is like pat=□h'.
• pat=_ renames h to an inaccessible name
• pat=- discards h
• ⟨pat₁, pat₂⟩ matches on conjunctions and existential quantifiers and recurses via pat₁ and pat₂.
• ⟨pat₁ | pat₂⟩ matches on disjunctions, matching the left alternative via pat₁ and the right alternative via pat₂.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mrefinePat.quot : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.mrefinePat : Category

Equations

• Lean.Parser.Category.mrefinePat = { }

def Lean.Parser.Tactic.mrefinePat_ : ParserDescr

Equations

• Lean.Parser.Tactic.mrefinePat_ = Lean.ParserDescr.node `Lean.Parser.Tactic.mrefinePat_ 1022 Lean.binderIdent

def Lean.Parser.Tactic.mrefinePats : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.«mrefinePat⟨_⟩» : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.«mrefinePat(_)» : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.«mrefinePat⌜_⌝» : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.«mrefinePat□_» : ParserDescr

Equations

• Lean.Parser.Tactic.«mrefinePat□_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mrefinePat□_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") Lean.binderIdent)

def Lean.Parser.Tactic.mrefinePat?_ : ParserDescr

Equations

• Lean.Parser.Tactic.mrefinePat?_ = Lean.ParserDescr.node `Lean.Parser.Tactic.mrefinePat?_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "?") Lean.binderIdent)

def Lean.Parser.Tactic.«mrefinePat%_» : ParserDescr

Equations

• Lean.Parser.Tactic.«mrefinePat%_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mrefinePat%_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "%") (Lean.ParserDescr.cat `term 0))

def Lean.Parser.Tactic.«mrefinePat#_» : ParserDescr

Equations

• Lean.Parser.Tactic.«mrefinePat#_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mrefinePat#_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") Lean.binderIdent)

inductive Lean.Parser.Tactic.MRefinePat : Type

• one (name : TSyntax `Lean.binderIdent) : MRefinePat
• tuple (args : List MRefinePat) : MRefinePat
• pure (h : TSyntax `term) : MRefinePat
• stateful (h : TSyntax `Lean.binderIdent) : MRefinePat
• hole (name : TSyntax `Lean.binderIdent) : MRefinePat

instance Lean.Parser.Tactic.instReprMRefinePat : Repr MRefinePat

Equations

• Lean.Parser.Tactic.instReprMRefinePat = { reprPrec := Lean.Parser.Tactic.reprMRefinePat✝ }

instance Lean.Parser.Tactic.instInhabitedMRefinePat : Inhabited MRefinePat

Equations

• Lean.Parser.Tactic.instInhabitedMRefinePat = { default := Lean.Parser.Tactic.MRefinePat.one default }

def Lean.Parser.Tactic.MRefinePat.parse (pat : TSyntax `mrefinePat) : MacroM MRefinePat

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.Parser.Tactic.MRefinePat.parse.go : TSyntax `mrefinePat → Option MRefinePat

def Lean.Parser.Tactic.mrefine : ParserDescr

Like refine, but operating on stateful Std.Do.SPred goals.

example (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by
  mintro ⟨HP, HQ, HR⟩
  mrefine ⟨HP, HR⟩

example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mrefine ⟨⌜42⌝, H⟩

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.mintroPat : Category

Equations

• Lean.Parser.Category.mintroPat = { }

def Lean.Parser.Tactic.mintroPat.quot : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mintroPat_ : ParserDescr

Equations

• Lean.Parser.Tactic.mintroPat_ = Lean.ParserDescr.node `Lean.Parser.Tactic.mintroPat_ 1022 (Lean.ParserDescr.cat `mcasesPat 0)

def Lean.Parser.Tactic.«mintroPat∀_» : ParserDescr

Equations

• Lean.Parser.Tactic.«mintroPat∀_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mintroPat∀_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀") Lean.binderIdent)

def Lean.Parser.Tactic.mintro : ParserDescr

Like intro, but introducing stateful hypotheses into the stateful context of the Std.Do.SPred proof mode. That is, given a stateful goal (hᵢ : Hᵢ)* ⊢ₛ P → T, mintro h transforms into (hᵢ : Hᵢ)*, (h : P) ⊢ₛ T.

Furthermore, mintro ∀s is like intro s, but preserves the stateful goal. That is, mintro ∀s brings the topmost state variable s:σ in scope and transforms (hᵢ : Hᵢ)* ⊢ₛ T (where the entailment is in Std.Do.SPred (σ::σs)) into (hᵢ : Hᵢ s)* ⊢ₛ T s (where the entailment is in Std.Do.SPred σs).

Beyond that, mintro supports the full syntax of mcases patterns (mintro pat = (mintro h; mcases h with pat), and can perform multiple introductions in sequence.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mrevertPat.quot : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.mrevertPat : Category

Equations

• Lean.Parser.Category.mrevertPat = { }

def Lean.Parser.Tactic.mrevertPat_ : ParserDescr

Equations

• Lean.Parser.Tactic.mrevertPat_ = Lean.ParserDescr.node `Lean.Parser.Tactic.mrevertPat_ 1022 (Lean.ParserDescr.const `ident)

def Lean.Parser.Tactic.«mrevertPat∀_» : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mrevert : ParserDescr

mrevert is like revert, but operating on a stateful Std.Do.SPred goal.

example (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ P → R := by
  mintro ⟨HP, HQ, HR⟩
  mrevert HR
  mrevert HP
  mintro HP'
  mintro HR'
  mexact HR'

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mspecNoBind : ParserDescr

mspec_no_simp $spec first tries to decompose Bind.binds before applying $spec. This variant of mspec_no_simp does not; mspec_no_bind $spec is defined as

try with_reducible mspec_no_bind Std.Do.Spec.bind
mspec_no_bind $spec

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mspecNoSimp : ParserDescr

Like mspec, but does not attempt slight simplification and closing of trivial sub-goals. mspec $spec is roughly (the set of simp lemmas below might not be up to date)

mspec_no_simp $spec
all_goals
  ((try simp only [SPred.true_intro_simp, SPred.apply_pure]);
   (try mpure_intro; trivial))

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.tacticMvcgen_trivial_extensible : ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.tacticMvcgen_trivial : ParserDescr

mvcgen_trivial is the tactic automatically called by mvcgen to discharge VCs. It tries to discharge the VC by applying (try mpure_intro); trivial and otherwise delegates to mvcgen_trivial_extensible. Users are encouraged to extend mvcgen_trivial_extensible instead of this tactic in order not to override the default (try mpure_intro); trivial behavior.

Equations

• Lean.Parser.Tactic.tacticMvcgen_trivial = Lean.ParserDescr.node `Lean.Parser.Tactic.tacticMvcgen_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "mvcgen_trivial" false)

def Lean.Parser.Tactic.mspec : ParserDescr

mspec is an apply-like tactic that applies a Hoare triple specification to the target of the stateful goal.

Given a stateful goal H ⊢ₛ wp⟦prog⟧ Q', mspec foo_spec will instantiate foo_spec : ... → ⦃P⦄ foo ⦃Q⦄, match foo against prog and produce subgoals for the verification conditions ?pre : H ⊢ₛ P and ?post : Q ⊢ₚ Q'.

• If prog = x >>= f, then mspec Specs.bind is tried first so that foo is matched against x instead. Tactic mspec_no_bind does not attempt to do this decomposition.
• If ?pre or ?post follow by .rfl, then they are discharged automatically.
• ?post is automatically simplified into constituent ⊢ₛ entailments on success and failure continuations.
• ?pre and ?post.* goals introduce their stateful hypothesis under an inaccessible name. You can give it a name with the mrename_i tactic.
• Any uninstantiated MVar arising from instantiation of foo_spec becomes a new subgoal.
• If the target of the stateful goal looks like fun s => _ then mspec will first mintro ∀s.
• If P has schematic variables that can be instantiated by doing mintro ∀s, for example foo_spec : ∀(n:Nat), ⦃fun s => ⌜n = s⌝⦄ foo ⦃Q⦄, then mspec will do mintro ∀s first to instantiate n = s.
• Right before applying the spec, the mframe tactic is used, which has the following effect: Any hypothesis Hᵢ in the goal h₁:H₁, h₂:H₂, ..., hₙ:Hₙ ⊢ₛ T that is pure (i.e., equivalent to some ⌜φᵢ⌝) will be moved into the pure context as hᵢ:φᵢ.

Additionally, mspec can be used without arguments or with a term argument:

• mspec without argument will try and look up a spec for x registered with @[spec].
• mspec (foo_spec blah ?bleh) will elaborate its argument as a term with expected type ⦃?P⦄ x ⦃?Q⦄ and introduce ?bleh as a subgoal. This is useful to pass an invariant to e.g., Specs.forIn_list and leave the inductive step as a hole.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mvcgen : ParserDescr

mvcgen will break down a Hoare triple proof goal like ⦃P⦄ prog ⦃Q⦄ into verification conditions, provided that all functions used in prog have specifications registered with @[spec].

A verification condition is an entailment in the stateful logic of Std.Do.SPred in which the original program prog no longer occurs. Verification conditions are introduced by the mspec tactic; see the mspec tactic for what they look like. When there's no applicable mspec spec, mvcgen will try and rewrite an application prog = f a b c with the simp set registered via @[spec].

When used like mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat], mvcgen will additionally

• add a Hoare triple specification foo_spec : ... → ⦃P⦄ foo ... ⦃Q⦄ to spec set for a function foo occurring in prog,
• unfold a definition def bar_def ... := ... in prog,
• unfold any method of the instBEqFloat : BEq Float instance in prog.
• it will no longer substitute away let-expressions that occur at most once in P, Q or prog.

Furthermore, mvcgen tries to close trivial verification conditions by SPred.entails.rfl or the tactic sequence try (mpure_intro; trivial). The variant mvcgen_no_trivial does not do this.

For debugging purposes there is also mvcgen_step 42 which will do at most 42 VC generation steps. This is useful for bisecting issues with the generated VCs.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mvcgenNoTrivial : ParserDescr

Like mvcgen, but does not attempt to prove trivial VCs via mpure_intro; trivial.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Tactic.mvcgenStep : ParserDescr

Like mvcgen_no_trivial, but mvcgen_step 42 will only do 42 steps of the VC generation procedure. This is helpful for bisecting bugs in mvcgen and tracing its execution.

Equations

• One or more equations did not get rendered due to their size.