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
, thenmspec
andmvcgen
will usefoo_spec
as a specification for calls tofoo
. - Otherwise, when used on a definition that
@[simp]
would work on, it is added to the internal simp set ofmvcgen
that is used withinwp⟦·⟧
contexts to simplify match discriminants and applications of constants.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
Instances For
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)
Instances For
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.
Instances For
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)
Instances For
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.
Instances For
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)
Instances For
Duplicate a stateful Std.Do.SPred
hypothesis.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
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)
Instances For
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)
Instances For
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)
Instances For
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.
Instances For
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.
Instances For
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)
Instances For
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)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Parser.Tactic.mcasesPat_ = Lean.ParserDescr.node `Lean.Parser.Tactic.mcasesPat_ 1022 Lean.binderIdent
Instances For
Equations
- Lean.Parser.Tactic.«mcasesPat-» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mcasesPat-» 1024 (Lean.ParserDescr.symbol "-")
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Parser.Tactic.«mcasesPat□_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mcasesPat□_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") Lean.binderIdent)
Instances For
Equations
- Lean.Parser.Tactic.«mcasesPat%_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mcasesPat%_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "%") Lean.binderIdent)
Instances For
Equations
- Lean.Parser.Tactic.«mcasesPat#_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mcasesPat#_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") Lean.binderIdent)
Instances For
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
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'
renamesh
toh'
in the stateful context, regardless of whetherh
is purepat=⌜h'⌝
introducesh' : φ
to the pure local context ifh : ⌜φ⌝
(c.f.Lean.Elab.Tactic.Do.ProofMode.IsPure
)pat=h'
is likepat=⌜h'⌝
ifh
is pure (c.f.Lean.Elab.Tactic.Do.ProofMode.IsPure
), otherwise it is likepat=□h'
.pat=_
renamesh
to an inaccessible namepat=-
discardsh
⟨pat₁, pat₂⟩
matches on conjunctions and existential quantifiers and recurses viapat₁
andpat₂
.⟨pat₁ | pat₂⟩
matches on disjunctions, matching the left alternative viapat₁
and the right alternative viapat₂
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Parser.Tactic.mrefinePat_ = Lean.ParserDescr.node `Lean.Parser.Tactic.mrefinePat_ 1022 Lean.binderIdent
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Parser.Tactic.«mrefinePat□_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mrefinePat□_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") Lean.binderIdent)
Instances For
Equations
- Lean.Parser.Tactic.mrefinePat?_ = Lean.ParserDescr.node `Lean.Parser.Tactic.mrefinePat?_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "?") Lean.binderIdent)
Instances For
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))
Instances For
Equations
- Lean.Parser.Tactic.«mrefinePat#_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mrefinePat#_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#") Lean.binderIdent)
Instances For
- 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
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Parser.Tactic.mintroPat_ = Lean.ParserDescr.node `Lean.Parser.Tactic.mintroPat_ 1022 (Lean.ParserDescr.cat `mcasesPat 0)
Instances For
Equations
- Lean.Parser.Tactic.«mintroPat∀_» = Lean.ParserDescr.node `Lean.Parser.Tactic.«mintroPat∀_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀") Lean.binderIdent)
Instances For
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.
Instances For
mspec_no_simp $spec
first tries to decompose Bind.bind
s 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.
Instances For
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))
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
, thenmspec Specs.bind
is tried first so thatfoo
is matched againstx
instead. Tacticmspec_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 ash
.- Any uninstantiated MVar arising from instantiation of
foo_spec
becomes a new subgoal. - If the goal looks like
fun s => _ ⊢ₛ _
thenmspec
will firstmintro ∀s
. - If
P
has schematic variables that can be instantiated by doingmintro ∀s
, for examplefoo_spec : ∀(n:Nat), ⦃⌜n = ‹Nat›ₛ⌝⦄ foo ⦃Q⦄
, thenmspec
will domintro ∀s
first to instantiaten = s
. - Right before applying the spec, the
mframe
tactic is used, which has the following effect: Any hypothesisHᵢ
in the goalh₁:H₁, h₂:H₂, ..., hₙ:Hₙ ⊢ₛ T
that is pure (i.e., equivalent to some⌜φᵢ⌝
) will be moved into the pure context ashᵢ:φᵢ
.
Additionally, mspec
can be used without arguments or with a term argument:
mspec
without argument will try and look up a spec forx
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.
Instances For
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⦄
tospec
set for a functionfoo
occurring inprog
, - unfold a definition
def bar_def ... := ...
inprog
, - unfold any method of the
instBEqFloat : BEq Float
instance inprog
. - it will no longer substitute away
let
-expressions that occur at most once inP
,Q
orprog
.
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.
Instances For
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.