Lean4
/-- Add a lemma with `nm` stating that `lhs = rhs`. `type` is the type of both `lhs` and `rhs`,
`args` is the list of local constants occurring, and `univs` is the list of universe variables. -/
def addProjection (declName : Name) (type lhs rhs : Expr) (args : Array Expr) (cfg : Config) : MetaM Unit := do
trace[simps.debug]"Planning to add the equality{indentD m! "{lhs } = ({rhs } : {type})"}"
let env ← getEnv
let lvl ← getLevel type
let mut (rhs, prf) := (rhs, mkAppN (mkConst `Eq.refl [lvl]) #[type, lhs])
if cfg.simpRhs then
let ctx ← mkSimpContext
let (rhs2, _) ← dsimp rhs ctx
if rhs != rhs2 then
trace[simps.debug]"`dsimp` simplified rhs to{indentExpr rhs2}"
else
trace[simps.debug]"`dsimp` failed to simplify rhs"
let (result, _) ← simp rhs2 ctx
if rhs2 != result.expr then
trace[simps.debug]"`simp` simplified rhs to{indentExpr result.expr}"
else
trace[simps.debug]"`simp` failed to simplify rhs"
rhs := result.expr
prf := result.proof?.getD prf
let eqAp := mkApp3 (mkConst `Eq [lvl]) type lhs rhs
let declType ← mkForallFVars args eqAp
let declValue ← mkLambdaFVars args prf
if (env.find? declName).isSome then -- diverging behavior from Lean 3
throwError "simps tried to add lemma{indentD m!"{(.ofConstName declName)} : {declType}"}\n\
to the environment, but it already exists."
trace[simps.verbose]"adding projection {declName }:{indentExpr declType}"
prependError "Failed to add projection lemma {declName}:" do
addDecl <|
.thmDecl
{ name := declName
levelParams := univs
type := declType
value := declValue }
inferDefEqAttr declName
addDeclarationRangesFromSyntax declName (← getRef) ref
TermElabM.run' do
_ ← addTermInfo (isBinder := true) ref <| ← mkConstWithLevelParams declName
if cfg.isSimp then
addSimpTheorem simpExtension declName true false .global <| eval_prio default
let attrs ← elabAttrs cfg.attrs
Elab.Term.applyAttributes declName attrs
