Lean4
/-- Derive lemmas specifying the projections of the declaration.
`nm`: name of the lemma
If `todo` is non-empty, it will generate exactly the names in `todo`.
`toApply` is non-empty after a custom projection that is a composition of multiple projections
was just used. In that case we need to apply these projections before we continue changing `lhs`.
`simpLemmas`: names of the simp lemmas added so far.(simpLemmas : Array Name)
-/
partial def addProjections (nm : NameStruct) (type lhs rhs : Expr) (args : Array Expr) (mustBeStr : Bool) (cfg : Config)
(todo : List (String × Syntax)) (toApply : List Nat) : MetaM (Array Name) := do
-- we don't want to unfold non-reducible definitions (like `Set`) to apply more arguments
trace[simps.debug]"Type of the Expression before normalizing: {type}"
withTransparency cfg.typeMd <|
forallTelescopeReducing type fun typeArgs tgt ↦
withDefault
(do
trace[simps.debug]"Type after removing pi's: {tgt}"
let tgt ← whnfD tgt
trace[simps.debug]"Type after reduction: {tgt}"
let newArgs := args ++ typeArgs
let lhsAp := lhs.instantiateLambdasOrApps typeArgs
let rhsAp := rhs.instantiateLambdasOrApps typeArgs
let str := tgt.getAppFn.constName
trace[simps.debug]"todo: {todo }, toApply: {toApply}"
let todoNext := todo.filter (·.1 ≠ "")
let env ← getEnv
let stx? :=
todo.find? (·.1 == "") |>.map
(·.2)
/- The syntax object associated to the projection we're making now (if any).
Note that we use `ref[0]` so that with `simps (config := ...)` we associate it to the word `simps`
instead of the application of the attribute to arguments. -/
let stxProj := stx?.getD ref[0]
let strInfo? := getStructureInfo? env str
if strInfo?.isNone || (todo.isEmpty && str ∈ cfg.notRecursive && !mustBeStr && toApply.isEmpty) then
if mustBeStr then
throwError "Invalid `simps` attribute. Target {str} is not a structure"
if !todoNext.isEmpty && str ∉ cfg.notRecursive then
let firstTodo := todoNext.head!.1
throwError "Invalid simp lemma {nm.update firstTodo false |>.toName}.\nProjection \
{(splitOnNotNumber firstTodo "_")[1]!} doesn't exist, \
because target {str} is not a structure."
if cfg.fullyApplied then
addProjection stxProj univs nm.toName tgt lhsAp rhsAp newArgs cfg
else
addProjection stxProj univs nm.toName type lhs rhs args cfg
return
#[nm.toName]
-- if the type is a structure
let some (.inductInfo { isRec := false, ctors := [ctor], .. }) := env.find? str |
unreachable!
trace[simps.debug]"{str } is a structure with constructor {ctor}."
let rhsEta ← headStructureEtaReduce rhsAp
let addThisProjection := stx?.isSome && toApply.isEmpty
if addThisProjection then
-- we pass the precise argument of simps as syntax argument to `addProjection`
if cfg.fullyApplied then
addProjection stxProj univs nm.toName tgt lhsAp rhsEta newArgs cfg
else
addProjection stxProj univs nm.toName type lhs rhs args cfg
let rhsWhnf ← withTransparency cfg.rhsMd <| whnf rhsEta
trace[simps.debug]"The right-hand-side {(indentExpr rhsAp)}\n reduces to {indentExpr rhsWhnf}"
if !rhsWhnf.getAppFn.isConstOf ctor then
-- if I'm about to run into an error, try to set the transparency for `rhsMd` higher.
if cfg.rhsMd == .reducible && (mustBeStr || !todoNext.isEmpty || !toApply.isEmpty) then
trace[simps.debug]"Using relaxed reducibility."
Linter.logLintIf linter.simpsNoConstructor ref
m! "\
The definition {nm.toName} is not a constructor application. \
Please use `@[simps!]` instead.\n\
\n\
Explanation: `@[simps]` uses the definition to find what the simp lemmas should \
be. If the definition is a constructor, then this is easy, since the values of the \
projections are just the arguments to the constructor. If the definition is not a \
constructor, then `@[simps]` will unfold the right-hand side until it has found a \
constructor application, and uses those values.\n\n\
This might not always result in the simp-lemmas you want, so you are advised to use \
`@[simps?]` to double-check whether `@[simps]` generated satisfactory lemmas.\n\
Note 1: `@[simps!]` also calls the `simp` tactic, and this can be expensive in certain \
cases.\n\
Note 2: `@[simps!]` is equivalent to `@[simps (config := \{rhsMd := .default, \
simpRhs := true})]`. You can also try `@[simps (config := \{rhsMd := .default})]` \
to still unfold the definitions, but avoid calling `simp` on the resulting statement.\n\
Note 3: You need `simps!` if not all fields are given explicitly in this definition, \
even if the definition is a constructor application. For example, if you give a \
`MulEquiv` by giving the corresponding `Equiv` and the proof that it respects \
multiplication, then you need to mark it as `@[simps!]`, since the attribute needs to \
unfold the corresponding `Equiv` to get to the `toFun` field."
let nms ←
addProjections nm type lhs rhs args mustBeStr { cfg with rhsMd := .default, simpRhs := true } todo
toApply
return if addThisProjection then nms.push nm.toName else nms
if !toApply.isEmpty then
throwError "Invalid simp lemma {nm.toName }.\nThe given definition is not a constructor \
application:{indentExpr rhsWhnf}"
if mustBeStr then
throwError "Invalid `simps` attribute. The body is not a constructor application:\
{indentExpr rhsWhnf}"
if !todoNext.isEmpty then
throwError "Invalid simp lemma {nm.update todoNext.head!.1 false |>.toName }.\n\
The given definition is not a constructor application:{indentExpr rhsWhnf}"
if !addThisProjection then
if cfg.fullyApplied then
addProjection stxProj univs nm.toName tgt lhsAp rhsEta newArgs cfg
else
addProjection stxProj univs nm.toName type lhs rhs args cfg
return
#[nm.toName]
-- if the value is a constructor application
trace[simps.debug]"Generating raw projection information..."
let projInfo ← getProjectionExprs ref tgt rhsWhnf cfg
trace[simps.debug]"Raw projection information:{indentD m! "{projInfo}"}"
if let idx :: rest := toApply then
let some ⟨newRhs, _⟩ := projInfo[idx]? |
throwError"unreachable: index of composite projection is out of bounds."
let newType ← inferType newRhs
trace[simps.debug]"Applying a custom composite projection. Todo: {toApply }. Current lhs:\
{indentExpr lhsAp}"
return ← addProjections nm newType lhsAp newRhs newArgs false cfg todo rest
trace[simps.debug]"Not in the middle of applying a custom composite projection"
if todo.length == 1 && todo.head!.1 == "" then
return #[nm.toName]
let projs : Array Name := projInfo.map fun x ↦ x.2.name
let todo := todoNext
trace[simps.debug]"Next todo: {todoNext}"
if let some (x, _) :=
todo.find? fun (x, _) ↦
projs.all fun proj ↦ !isPrefixOfAndNotNumber (proj.lastComponentAsString ++ "_") x then
let simpLemma := nm.update x |>.toName
let neededProj := (splitOnNotNumber x "_")[0]!
throwError "Invalid simp lemma {simpLemma }. \
Structure {str } does not have projection {neededProj}.\n\
The known projections are:\
{(indentD <| toMessageData projs)}\n\
You can also see this information by running\
\n `initialize_simps_projections? {str}`.\n\
Note: these projection names might be customly defined for `simps`, \
and could differ from the projection names of the structure."
let nms ←
projInfo.flatMapM fun ⟨newRhs, proj, projExpr, projNrs, isDefault, isPrefix⟩ ↦ do
let newType ← inferType newRhs
let newTodo :=
todo.filterMap fun (x, stx) ↦
(dropPrefixIfNotNumber? x (proj.lastComponentAsString ++ "_")).map
(·.toString, stx)
-- we only continue with this field if it is default or mentioned in todo
if !(isDefault && todo.isEmpty) && newTodo.isEmpty then
return #[]
let newLhs := projExpr.instantiateLambdasOrApps #[lhsAp]
let newName := nm.update proj.lastComponentAsString isPrefix
trace[simps.debug]"Recursively add projections for:{indentExpr newLhs}"
addProjections newName newType newLhs newRhs newArgs false cfg newTodo projNrs
return if addThisProjection then nms.push nm.toName else nms)
