Direct `changeLocalDecl'`

Stream: metaprogramming / tactics

[Leni Aniva]

In Mathlib4, the changeLocalDecl' function is this:

def _root_.Lean.MVarId.changeLocalDecl' (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr)
    (checkDefEq := true) : MetaM MVarId := do
  mvarId.checkNotAssigned `changeLocalDecl
  let lctx := (← mvarId.getDecl).lctx
  let some decl := lctx.find? fvarId | throwTacticEx `changeLocalDecl mvarId m!"\
    local variable {Expr.fvar fvarId} is not present in local context{mvarId}"
  let toRevert := lctx.foldl (init := #[]) fun arr decl' =>
    if decl.index ≤ decl'.index then arr.push decl'.fvarId else arr
  let (_, mvarId) ← mvarId.withReverted toRevert fun mvarId fvars => mvarId.withContext do
    let check (typeOld : Expr) : MetaM Unit := do
      if checkDefEq then
        unless ← isDefEq typeNew typeOld do
          throwTacticEx `changeLocalDecl mvarId
            m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
    let finalize (targetNew : Expr) := do
      return ((), fvars.map .some, ← mvarId.replaceTargetDefEq targetNew)
    match ← mvarId.getType with
    | .forallE n d b bi => do check d; finalize (.forallE n typeNew b bi)
    | .letE n t v b ndep => do check t; finalize (.letE n typeNew v b ndep)
    | _ => throwTacticEx `changeLocalDecl mvarId "unexpected auxiliary target"
  return mvarId

why does this have to be so complicated? Can we just directly modify the lctx of the mvar in question, and change the type in each fvar declaration?

[Kyle Miller]

This is a way to guarantee that the local variable and everything that depends on it get new fvarids.

The reason for wanting new fvarids is caching. There's an inferType cache for example, and if you keep the same fvarId, then inferType (.fvar fvarId) may give a different result from fvarId.getType.

There are exceptions, if you have an understanding of how your metaprogram tolerates diverging caches, or if you reset the cache, but this function is intending to definitely be safe (it would be nice if it didn't reorder fvars though...)

After all, dsimp updates locals while preserving fvarids and it's not obvious that anything breaks... Surely you could cook up some examples where the local instance cache isn't updated and that impacts elaboration somehow.

[Leni Aniva]

Kyle Miller said:

This is a way to guarantee that the local variable and everything that depends on it get new fvarids.

The reason for wanting new fvarids is caching. There's an inferType cache for example, and if you keep the same fvarId, then inferType (.fvar fvarId) may give a different result from fvarId.getType.

There are exceptions, if you have an understanding of how your metaprogram tolerates diverging caches, or if you reset the cache, but this function is intending to definitely be safe (it would be nice if it didn't reorder fvars though...)

After all, dsimp updates locals while preserving fvarids and it's not obvious that anything breaks... Surely you could cook up some examples where the local instance cache isn't updated and that impacts elaboration somehow.

Is there a way to extract information about which fvar got remapped to which?

After reading the source code further I think the only way is to create my own withRevert

[Kyle Miller]

It would be worth having a version that returns the remapping

[Jannis Limperg]

Tracking fvar renamings is generally difficult because the Lean APIs don't consistently support it. So if you can think of a way to implement your features without such tracking, you should probably try that first.