Lean4
/-- This function takes an array of expressions `t`, all of which are assumed to be `RingHom`s,
and searches through the local context to find any additional properties of these `RingHoms`, after
which it tries to add the corresponding `Algebra` properties to the context. It only looks for
properties that have been tagged with the `algebraize` attribute, and uses this tag to find the
corresponding `Algebra` property. -/
def addProperties (t : Array Expr) : TacticM Unit :=
withMainContext do
let ctx ← getLCtx
ctx.forM fun decl => do
if decl.isImplementationDetail then
return
let (nm, args) := (← instantiateMVars decl.type).getAppFnArgs
match Attr.algebraizeAttr.getParam? (← getEnv) nm with
-- If it has, `p` will either be the name of the corresponding `Algebra` property, or a
-- lemma/constructor.
| some p =>
let cinfo ←
try
getConstInfo p
catch _ =>
logWarning
m! "Hypothesis {decl.toExpr} has type{(indentD decl.type)}.\n\
Its head symbol {(.ofConstName nm)} is (effectively) tagged with `@[algebraize {p }]`, \
but no constant{indentD p}\nhas been found.\n\
Check for missing imports, missing namespaces or typos."
return
let p' ← mkConstWithFreshMVarLevels p
let (pargs, _, _) ← forallMetaTelescope (← inferType p')
let tp' := mkAppN p' pargs
let getValType : MetaM (Option (Expr × Expr)) := do
/- If the attribute points to the corresponding `Algebra` property itself, we assume that it
is definitionally the same as the `RingHom` property. Then, we just need to construct its
type and the local declaration will already give a valid term. -/
if cinfo.isInductive then
pargs[0]!.mvarId!.assignIfDefEq args[0]!
pargs[1]!.mvarId!.assignIfDefEq
args[1]!
-- This should be the type `Algebra.Property A B`
let tp ← instantiateMVars tp'
if ← isDefEqGuarded decl.type tp then
return (decl.toExpr, tp)
else
return none
else
try
pargs.back!.mvarId!.assignIfDefEq decl.toExpr
catch _ =>
return none
let val ← instantiateMVars tp'
let tp ← inferType val
return (val, tp)
let some (val, tp) ← getValType |
return
/- Find all arguments to `Algebra.Property A B` or `Module.Property A B` which are
of the form `RingHom.toAlgebra f`, `RingHom.toModule f`
or `Algebra.toModule (RingHom.toAlgebra f)`. -/
let ringHom_args ←
tp.getAppArgs.filterMapM <| fun x =>
liftMetaM
(do
let y := (← whnfUntil x ``Algebra.toModule) >>= (·.getAppArgs.back?)
return
((← whnfUntil (y.getD x) ``RingHom.toAlgebra) <|> (← whnfUntil x ``RingHom.toModule)) >>=
(·.getAppArgs.back?))
unless
(← synthInstance? tp).isSome ||
!(← ringHom_args.allM (fun z => t.anyM (withoutModifyingMCtx <| isDefEq z ·))) do
liftMetaTactic fun mvarid => do
let nm ← mkFreshBinderNameForTactic `algebraizeInst
let (_, mvar) ← mvarid.note nm val tp
return [mvar]
| none =>
return
