Lean4
/-- If `e : te` is a term whose type mentions `x`, `h` (the generalization variables)
or entries in `Δ`/`δ`,
return `h.symm ▸ e : te[p/x, rfl/h, …]`.
Otherwise return `none`. -/
def castBack? (e te x h : Expr) (Δ : Array (FVarId × Expr)) (δ : Std.HashSet FVarId) : MetaM (Option Expr) := do
if !te.hasAnyFVar (fun f => f == x.fvarId! || f == h.fvarId! || Δ.any (·.1 == f) || δ.contains f) then
return none
let e' ← mkEqRec (← motive) e (← mkEqSymm h)
trace[Tactic.depRewrite.cast]"casting (x ↦ p):{indentExpr e'}"
return some e'
where/-- Compute the motive that casts `e` back to `te[p/x, rfl/h, …]`. -/
motive : MetaM Expr := do
withLocalDeclD `x' (← inferType x) fun x' => do
withLocalDeclD `h' (← mkEq x x') fun h' => do
/- The motive computation below operates syntactically, i.e.,
it looks for the fvars `x` and `h`.
This breaks in the presence of `let`-binders:
if we traverse into `b` in `let a := n; b` with `n` as the pattern,
we will have `a := x` in the local context.
If the type-correctness of `b` depends on the defeq `a ≡ n`,
because `b` does not depend on `x` syntactically,
a `replaceFVars` substitution will not suffice to fix `b`.
Thus we unfold the necessary dependent `ldecl`s when computing motives.
If their values depend on `x`,
this will be visible in the syntactic form of `te`. -/
let te ← zetaDelta te δ
let mut fs := #[x, h]
let mut es := #[x', ← mkEqTrans h h']
for (f, M) in Δ do
fs := fs.push (.fvar f)
es := es.push (← mkEqRec M (.fvar f) h')
let te := te.replaceFVars fs es
mkLambdaFVars #[x', h'] te
