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.

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

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

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

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

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

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

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

def Lean.Parser.Tactic.mdup : ParserDescr

Duplicate a stateful Std.Do.SPred hypothesis.

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

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

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

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

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φ)

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

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'

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Ψ

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Ψ

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.

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.

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

def Lean.Parser.Category.mcasesPat : Category

def Lean.Parser.Tactic.mcasesPatAlts : ParserDescr

def Lean.Parser.Tactic.mcasesPat_ : ParserDescr

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

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

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

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

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

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

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

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

instance Lean.Parser.Tactic.instInhabitedMCasesPat : Inhabited MCasesPat

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

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

def Lean.Parser.Category.mrefinePat : Category

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

def Lean.Parser.Tactic.mrefinePat_ : ParserDescr

def Lean.Parser.Tactic.mrefinePats : ParserDescr

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

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

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

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

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

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

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

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

instance Lean.Parser.Tactic.instInhabitedMRefinePat : Inhabited MRefinePat

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

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⟩

def Lean.Parser.Category.mintroPat : Category

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

def Lean.Parser.Tactic.mintroPat_ : ParserDescr

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

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.

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

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.true_intro_simp_nil, SVal.curry_cons,
                   SVal.uncurry_cons, SVal.getThe_here, SVal.getThe_there]);
   (try mpure_intro; trivial))

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⟧.apply 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 as h.
• Any uninstantiated MVar arising from instantiation of foo_spec becomes a new subgoal.
• If the 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), ⦃⌜n = ‹Nat›ₛ⌝⦄ 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.

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.

def Lean.Parser.Tactic.mvcgenNoTrivial : ParserDescr

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

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.