opaque Lean.Elab.Tactic.Do.SpecAttr.mvcgenSimpExt : Meta.SimpExtension

This attribute should not be used directly. It is an implementation detail of the mvcgen tactic.

def Lean.Elab.Tactic.Do.SpecAttr.getSpecSimpTheorems : CoreM Meta.SimpTheorems

The simp set accumulated by the @[spec] attribute. (This does not include Hoare triple specs.) It is an implementation detail of the mvcgen tactic.

inductive Lean.Elab.Tactic.Do.SpecAttr.SpecProof : Type

• global (declName : Name) : SpecProof
• local (fvarId : FVarId) : SpecProof
• stx (id : Name) (ref : Syntax) (proof : Expr) : SpecProof

@[instance_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecProof : Inhabited SpecProof

@[instance_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof : BEq SpecProof

def Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecProof.beq : SpecProof → SpecProof → Bool

def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.key : SpecProof → Name

A unique identifier corresponding to the origin.

def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.ofOrigin : Meta.Origin → Option SpecProof

Convert a simp Origin to a SpecProof.

def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.getProof : SpecProof → MetaM (List Name × Expr)

@[instance_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instHashableSpecProof : Hashable SpecProof

def Lean.Elab.Tactic.Do.SpecAttr.SpecProof.instantiate (proof : SpecProof) : MetaM (Array Expr × Array BinderInfo × Expr × Expr)

@[instance_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instToMessageDataSpecProof : ToMessageData SpecProof

structure Lean.Elab.Tactic.Do.SpecAttr.SpecTheorem : Type

• keys : Array Meta.DiscrTree.Key
• prog : Expr

  Expr key tested for matching, in ∀-quantified form. keys = (← mkPath (← forallMetaTelescope prog).2.2).

• proof : SpecProof

  The proof for the theorem.

• etaPotential : Nat

  If etaPotential is non-zero, then the precondition contains meta variables that can be instantiated after applying mintro ∀s etaPotential many times.

• priority : Nat

@[instance_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorem : Inhabited SpecTheorem

def Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem.beq : SpecTheorem → SpecTheorem → Bool

@[instance_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instBEqSpecTheorem : BEq SpecTheorem

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.SpecAttr.SpecEntry : Type

structure Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems : Type

• specs : Meta.DiscrTree SpecTheorem
• erased : PHashSet SpecProof

@[instance_reducible]

instance Lean.Elab.Tactic.Do.SpecAttr.instInhabitedSpecTheorems : Inhabited SpecTheorems

def Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems.insert (d : SpecTheorems) (e : SpecTheorem) : SpecTheorems

def Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems.isErased (d : SpecTheorems) (thmId : SpecProof) : Bool

def Lean.Elab.Tactic.Do.SpecAttr.SpecTheorems.erase (d : SpecTheorems) (thmId : SpecProof) : SpecTheorems

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.SpecAttr.SpecExtension : Type

def Lean.Elab.Tactic.Do.SpecAttr.simpSPredConfig : Meta.ConfigWithKey

def Lean.Elab.Tactic.Do.SpecAttr.computeMVarBetaPotentialForSPred (xs : Array Expr) (σs e : Expr) : MetaM Nat

If σs : List Type, then e : SPred σs. Return the number of times e needs to be applied in order to assign closed solutions to meta variables.

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromConst (declName : Name) (prio : Nat := 1000) : MetaM SpecTheorem

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromLocal (fvar : FVarId) (prio : Nat := 1000) : MetaM SpecTheorem

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecTheoremFromStx (ref : Syntax) (proof : Expr) (prio : Nat := 1000) : MetaM SpecTheorem

def Lean.Elab.Tactic.Do.SpecAttr.SpecExtension.addSpecTheoremFromConst (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) : MetaM Unit

def Lean.Elab.Tactic.Do.SpecAttr.SpecExtension.addSpecTheoremFromLocal (ext : SpecExtension) (fvar : FVarId) (prio : Nat := 1000) : MetaM Unit

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecExt : SimpleScopedEnvExtension.Descr SpecEntry SpecTheorems

opaque Lean.Elab.Tactic.Do.SpecAttr.specAttr : SpecExtension

def Lean.Elab.Tactic.Do.SpecAttr.SpecExtension.getTheorems (ext : SpecExtension) : CoreM SpecTheorems

def Lean.Elab.Tactic.Do.SpecAttr.getSpecTheorems : CoreM SpecTheorems

inductive Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheoremKind : Type

The kind of a spec theorem.

• triple : SpecTheoremKind

  A Hoare triple spec: ⦃P⦄ prog ⦃Q⦄.

• simp (etaArgs : Nat := 0) : SpecTheoremKind

  A simp/equational spec: lhs = rhs. The pattern is the LHS. When matched, the VCGen rewrites the program from lhs to rhs and continues. etaArgs is the number of extra arguments introduced by eta-expanding function-level equations (e.g., class projection unfold lemmas). These args need congrFun at instantiation time.

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.SpecAttr.instInhabitedSpecTheoremKind : Inhabited SpecTheoremKind

inductive Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof : Type

• global (declName : Name) : SpecProof
• local (fvarId : FVarId) : SpecProof
• stx (id : Name) (ref : Syntax) (proof : Expr) : SpecProof

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.SpecAttr.instInhabitedSpecProof : Inhabited SpecProof

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.SpecAttr.instBEqSpecProof : BEq SpecProof

def Lean.Elab.Tactic.Do.Internal.SpecAttr.instBEqSpecProof.beq : SpecProof → SpecProof → Bool

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.key : SpecProof → Name

A unique identifier corresponding to the origin.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.ofOrigin : Meta.Origin → Option SpecProof

Convert a simp Origin to a SpecProof.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.getProof : SpecProof → MetaM (List Name × Expr)

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.SpecAttr.instHashableSpecProof : Hashable SpecProof

def Lean.Elab.Tactic.Do.Internal.SpecAttr.tripleToWpProof? (proof type : Expr) : MetaM (Option (Expr × Expr))

Normalises a specification proof so its conclusion is in pre ⊑ wp … form.

• Returns some for Triple proofs (rewriting via Triple.hwp) and proofs already in pre ⊑ wp … form (passed through unchanged).
• Returns none if type is neither shape; callers should throwError.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.instantiate (proof : SpecProof) : MetaM (Array Expr × Array BinderInfo × Expr × Expr)

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.SpecAttr.instToMessageDataSpecProof : ToMessageData SpecProof

structure Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorem : Type

• pattern : Meta.Sym.Pattern

  Pattern for the program expression. This is the key used in the discrimination tree. If the proof has type ∀ a b c d e, ⦃P⦄ prog ⦃Q⦄ and only a, c and e occur in prog, then the pattern is prog[a:=#2, c:=#1, e:=#0]. For specs stated as pre ⊑ wp prog post epost, the pattern is keyed on prog.

• proof : SpecProof

  The proof for the theorem.

• kind : SpecTheoremKind

  The kind of spec theorem: triple or simp.

• priority : Nat

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.SpecAttr.instInhabitedSpecTheorem : Inhabited SpecTheorem

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.SpecAttr.instBEqSpecTheorem : BEq SpecTheorem

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecEntry : Type

structure Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorems : Type

• specs : Meta.DiscrTree SpecTheorem
• erased : PHashSet SpecProof

@[instance_reducible]

instance Lean.Elab.Tactic.Do.Internal.SpecAttr.instInhabitedSpecTheorems : Inhabited SpecTheorems

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorems.insert (d : SpecTheorems) (e : SpecTheorem) : SpecTheorems

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorems.isErased (d : SpecTheorems) (thmId : SpecProof) : Bool

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorems.erase (d : SpecTheorems) (thmId : SpecProof) : SpecTheorems

@[reducible, inline]

abbrev Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecExtension : Type

def Lean.Elab.Tactic.Do.Internal.SpecAttr.eraseUnusedVarsFromPattern (p : Meta.Sym.Pattern) : Meta.Sym.Pattern

Drops pattern variables that the pattern expression does not depend on.

Sym.mkPatternFromExprWithKey/Sym.mkPatternFromDeclWithKey turn every leading ∀-binder of the source type into a pattern variable, even binders the selected key (e.g. the program of a Triple conclusion) never mentions. During matching those variables only ever become fresh metavariables (see Sym.mkPreResult); for instance binders they additionally trigger spurious trySynthInstance calls. This keeps only the variables that the pattern expression references, together with the transitive closure of variables their types depend on, and renumbers the remaining de Bruijn indices. varInfos? and checkTypeMask? are filtered to the surviving telescope; fnInfos, levelParams, and the discrimination-tree key are unchanged because the pattern expression's structure is untouched (bound variables are wildcards in the key).

Important: only use this when the matched arguments are not reused to rebuild a proof term, as Sym.BackwardRule/Sym.mkValue do — dropping variables would drop arguments those need. It is meant for databases such as vcgen's spec table, where the proof is re-elaborated independently of the pattern.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.progArgIdx? (declName : Name) : MetaM (Option Nat)

The application-argument index of declName's program parameter x, read from its signature.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.selectProg (type : Expr) : MetaM (Option Expr)

Selects the program a spec conclusion is keyed on: the program of a Triple, or the program inside the wp on the RHS of a pre ⊑ wp … entailment. Returns none if type is neither shape — e.g. a bare lhs ⊑ rhs whose RHS is not a wp application (an invariant entailment such as (I n h).inv … ⊑ Q n r.2, which can appear as an ordinary hypothesis but is not a spec). Callers use none to skip such non-spec hypotheses instead of failing.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.mkSpecPatternFromExpr (expr : Expr) (levelParams : List Name := []) : MetaM Meta.Sym.Pattern

Builds a Sym.Pattern keyed on the program selected by selectProg from a spec conclusion. The conclusion is assumed to already be a valid spec shape (checked by the caller via selectProg); a non-spec shape reaching here is a logic error and throws.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.mkSpecTheoremFromConst (declName : Name) (prio : Nat := 1000) : MetaM (Option SpecTheorem)

def Lean.Elab.Tactic.Do.Internal.SpecAttr.mkSpecTheoremFromLocal (fvar : FVarId) (prio : Nat := 1000) : MetaM (Option SpecTheorem)

def Lean.Elab.Tactic.Do.Internal.SpecAttr.mkSpecTheoremFromStx (ref : Syntax) (proof : Expr) (prio : Nat := 1000) : MetaM (Option SpecTheorem)

def Lean.Elab.Tactic.Do.Internal.SpecAttr.mkSpecTheoremFromSimpDecl? (declName : Name) (prio : Nat) : MetaM (Option SpecTheorem)

Create a SpecTheorem from a simp/equational declaration declName : ∀ xs, lhs = rhs, keyed on the LHS. Function-level equations (e.g. class projection unfold lemmas) are eta-expanded so the discrimination-tree key includes all arguments. Returns none for no-op equations whose LHS key is syntactically the RHS.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecExtension.addSimpSpecTheoremsFromConst (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) : MetaM Unit

Register the equational lemmas of a @[spec]-annotated declaration as .simp entries with the given priority. An equational proposition is registered directly; a definition is registered via its equation lemmas (getEqnsFor?). Anything else throws, since it cannot serve as a vcgen spec.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.specEraseProofs (declName : Name) : MetaM (Array SpecProof)

The spec proofs a @[spec] constant contributes to the database: the constant itself for a Triple/⊑ wp spec, the equation itself for an equational spec, or its equation lemmas for a definition registered to unfold. Mirrors addSimpSpecTheoremsFromConst so [-foo] erases exactly the entries that annotating foo inserted.

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecExtension.addSpecTheoremFromConst (ext : SpecExtension) (declName : Name) (prio : Nat) (attrKind : AttributeKind) : MetaM Unit

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecExtension.addSpecTheoremFromLocal (ext : SpecExtension) (fvar : FVarId) (prio : Nat := 1000) : MetaM Unit

def Lean.Elab.Tactic.Do.Internal.SpecAttr.mkSpecExt : SimpleScopedEnvExtension.Descr SpecEntry SpecTheorems

opaque Lean.Elab.Tactic.Do.Internal.SpecAttr.specAttr : SpecExtension

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecExtension.getTheorems (ext : SpecExtension) : CoreM SpecTheorems

def Lean.Elab.Tactic.Do.Internal.SpecAttr.getSpecTheorems : CoreM SpecTheorems

def Lean.Elab.Tactic.Do.SpecAttr.mkSpecAttr : AttributeImpl

opaque Lean.Elab.Tactic.Do.SpecAttr.specInvariantAttr : TagAttribute

Marks a type as an invariant type for the mvcgen tactic. Goals whose type is an application of a tagged type will be classified as invariants rather than verification conditions.

def Lean.Elab.Tactic.Do.SpecAttr.isSpecInvariantType (env : Environment) (ty : Expr) : Bool

Returns true if ty is an application of a type tagged with @[spec_invariant_type].