Spec-theorem database used by vcgen. The @[spec] attribute already stores Std.Internal.Do specs as pattern-keyed SpecTheorems (see Lean.Elab.Tactic.Do.Attr); this module adds the operations the VC generator needs on top: instantiating a spec to pre ⊑ wp … form, migrating the equational lemmas registered through the mvcgen_simp side of @[spec] into the same database, and looking up the specs matching a program.

def Lean.Meta.Sym.isShared (e : Expr) : SymM Bool

Returns true if e is already internalized into the current SymM share table, in which case shareCommon e returns e unchanged.

Equations

• Lean.Meta.Sym.isShared e = do let __do_lift ← get pure (Lean.PersistentHashSet.contains __do_lift.share.set { expr := e })

def Lean.Meta.Sym.Pattern.shareCommon (p : Pattern) : SymM Pattern

Internalizes the pattern's expressions into the current SymM share table.

A pattern is built in MetaM, outside the SymM thread whose table the targets are internalized into, so its closed subterms (the instance telescope of a wp application, for example) are structurally equal to but distinct from the targets'. Internalizing the pattern once makes those subterms pointer-equal to every target internalized afterwards, so matching them is O(1).

Equations

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

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

Instantiates a spec theorem's proof.

Hoare triple and ⊑ wp specs are normalised to pre ⊑ wp … form via tripleToWpProof?. Simp specs keep the raw lhs = rhs equality, but eta-expand function-level equations: for unfold equations of class projections (e.g., MonadState.modifyGet.eq_1), the equation after forallMetaTelescope may be between functions rather than values: @modifyGet σ m self = self.3 : {α} → (σ → α × σ) → m α This method applies congrFun for each leading forall to reduce the equation to one between values of type m α, introducing fresh metavariables for the extra arguments. The number of extra args is stored in SpecTheoremKind.simp etaArgs.

Equations

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

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorem.global? (specThm : SpecTheorem) : Option Name

The declaration name of a global spec theorem, none for local/syntactic specs.

Equations

• specThm.global? = match specThm.proof with | Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecProof.global decl => some decl | x => none

def Lean.Elab.Tactic.Do.Internal.VCGen.extendWithSimpSpecs (database : SpecAttr.SpecTheorems) (simpThms : Meta.SimpTheorems) : MetaM SpecAttr.SpecTheorems

Extend the @[spec] database with the equational lemmas registered through the mvcgen_simp side of @[spec]:

• simp theorem declarations registered directly as @[spec],
• unfold entries registered with attribute [spec] foo, using stored equation lemmas when available and falling back to Meta.getEqnsFor?.

Hoare triple and ⊑ wp specs are already in database: the attribute stores them pattern-keyed at annotation time.

Equations

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

def Lean.Elab.Tactic.Do.Internal.SpecAttr.SpecTheorems.findSpecs (database : SpecTheorems) (e : Expr) : Meta.Sym.SymM (Except (Array SpecTheorem) SpecTheorem × SpecTheorems)

Look up SpecTheorems in the @[spec] database. Takes all specs that match the given program e and sorts by descending priority.

Equations

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