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 aggressively 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.

• errorOnMissingSpec : Bool

  If true (the default), report a hard error when no @[spec] theorem matches the current program head. If false, leave such goals as unsolved VCs for the user to discharge manually. This is the behaviour that mvcgen exhibits implicitly; the new prototypical vcgen opts into it via (errorOnMissingSpec := false).

• debug : Bool

  If true, vcgen checks failed BackwardRule.apply calls by retrying after unfoldReducible-normalizing the goal. If the rule then succeeds, an earlier step forgot a normalization; vcgen raises a hard error pointing at the offending rule and the missing reduction. Off by default; only consulted by vcgen.

• internalize : Bool

  If true (the default in grind mode), vcgen calls Grind.processHypotheses on each emitted VC, internalising local hypotheses into the parent's E-graph so that downstream grind steps share context. The tactic-level entry point disables this when there is no with clause (no grind step will consume the E-graph anyway). Ignored by mvcgen.

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.mclearError : 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

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

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.mexactError : 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

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

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.mexistsError : 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

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

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.mhaveError : 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

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

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.mreplaceError : 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

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

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.mpureError : 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

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

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.mrenameIError : ParserDescr

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

Equations

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

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.mspecializeError : 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

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

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.mspecializePureError : 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

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

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.Tactic.mcasesPat.quot : ParserDescr

Equations

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

def Lean.Parser.Category.mcasesPat : Category

Equations

• Lean.Parser.Category.mcasesPat = { }

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_reducible]

instance Lean.Parser.Tactic.instReprMCasesPat : Repr MCasesPat

Equations

• Lean.Parser.Tactic.instReprMCasesPat = { reprPrec := Lean.Parser.Tactic.instReprMCasesPat.repr }

partial def Lean.Parser.Tactic.instReprMCasesPat.repr : MCasesPat → Nat → Std.Format

@[instance_reducible]

instance Lean.Parser.Tactic.instInhabitedMCasesPat : Inhabited MCasesPat

Equations

• Lean.Parser.Tactic.instInhabitedMCasesPat = { default := Lean.Parser.Tactic.instInhabitedMCasesPat.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.mcasesError : 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

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

def Lean.Parser.Category.mrefinePat : Category

Equations

• Lean.Parser.Category.mrefinePat = { }

def Lean.Parser.Tactic.mrefinePat.quot : 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.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_reducible]

instance Lean.Parser.Tactic.instReprMRefinePat : Repr MRefinePat

Equations

• Lean.Parser.Tactic.instReprMRefinePat = { reprPrec := Lean.Parser.Tactic.instReprMRefinePat.repr }

partial def Lean.Parser.Tactic.instReprMRefinePat.repr : MRefinePat → Nat → Std.Format

@[instance_reducible]

instance Lean.Parser.Tactic.instInhabitedMRefinePat : Inhabited MRefinePat

Equations

• Lean.Parser.Tactic.instInhabitedMRefinePat = { default := Lean.Parser.Tactic.instInhabitedMRefinePat.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.Tactic.mrefineError : 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

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

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

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_ : 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.mintroError : 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

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

def Lean.Parser.Category.mrevertPat : Category

Equations

• Lean.Parser.Category.mrevertPat = { }

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

Equations

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

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.mrevertError : 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

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

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.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.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.vcAlt : ParserDescr

In induction alternative, which can have 1 or more cases on the left and _, ?_, or a tactic sequence after the =>.

Equations

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

def Lean.Parser.Tactic.vcAlts : ParserDescr

After with, there is an optional tactic that runs on all branches, and then a list of alternatives.

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].

mvcgen is deprecated in favor of vcgen.

Verification Conditions and specifications

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].

Features

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.

Config options

+noLetElim is just one config option of many. Check out Lean.Elab.Tactic.Do.VCGen.Config for all options. Of particular note is stepLimit = some 42, which is useful for bisecting bugs in mvcgen and tracing its execution.

Extended syntax

Often, mvcgen will be used like this:

mvcgen [...]
case inv1 => exact I1
case inv2 => exact I2
all_goals (mleave; try grind)

There is special syntax for this:

mvcgen [...] invariants
· I1
· I2
with grind

When I1 and I2 need to refer to inaccessibles (mvcgen will introduce a lot of them for program variables), you can use case label syntax:

mvcgen [...] invariants
| inv1 _ acc _ => I1 acc
| _ => I2
with grind

This is more convenient than the equivalent · by rename_i _ acc _; exact I1 acc.

Invariant suggestions

mvcgen will suggest invariants for you if you use the invariants? keyword.

mvcgen [...] invariants?

This is useful if you do not recall the exact syntax to construct invariants. Furthermore, it will suggest a concrete invariant encoding "this holds at the start of the loop and this must hold at the end of the loop" by looking at the corresponding VCs. Although the suggested invariant is a good starting point, it is too strong and requires users to interpolate it such that the inductive step can be proved. Example:

def mySum (l : List Nat) : Nat := Id.run do
  let mut acc := 0
  for x in l do
    acc := acc + x
  return acc

/--
info: Try this:
  invariants
    · ⇓⟨xs, letMuts⟩ => ⌜xs.prefix = [] ∧ letMuts = 0 ∨ xs.suffix = [] ∧ letMuts = l.sum⌝
-/
#guard_msgs (info) in
theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
  generalize h : mySum l = r
  apply Id.of_wp_run_eq h
  mvcgen invariants?
  all_goals admit

Equations

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

def Lean.Parser.Tactic.mvcgenHint : ParserDescr

A hint tactic that expands to mvcgen invariants?.

Equations

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