Lean4
/-- Generalizes the proofs in the type `e` and runs `k` in a local context with these propositions.
This continuation `k` is passed
1. an array of fvars for the propositions
2. an array of proof terms (extracted from `e`) that prove these propositions
3. the generalized `e`, which refers to these fvars
The `propToFVar` map is updated with the new proposition fvars.
-/
partial def withGeneralizedProofs {α : Type} [Nonempty α] (e : Expr) (ty? : Option Expr)
(k : Array Expr → Array Expr → Expr → MGen α) : MGen α := do
let propToFVar := (← get).propToFVar
trace[Tactic.generalize_proofs]"pre-abstracted{(indentD e)}\npropToFVar: {propToFVar.toArray}"
let (e, generalizations) ← MGen.runMAbs <| abstractProofs e ty?
trace[Tactic.generalize_proofs]"\
post-abstracted{(indentD e)}\nnew generalizations: {generalizations}"
let rec /-- Core loop for `withGeneralizedProofs`, adds generalizations one at a time. -/
go [Nonempty α] (i : Nat) (fvars pfs : Array Expr) (proofToFVar propToFVar : ExprMap Expr) : MGen α := do
if h : i < generalizations.size then
let (ty, pf) := generalizations[i]
let ty := (← instantiateMVars (ty.replace proofToFVar.get?)).cleanupAnnotations
withLocalDeclD (← mkFreshUserName `pf) ty fun fvar => do
go (i + 1) (fvars := fvars.push fvar) (pfs := pfs.push pf) (proofToFVar := proofToFVar.insert pf fvar)
(propToFVar := propToFVar.insert ty fvar)
else
withNewLocalInstances fvars 0
(do
let e' := e.replace proofToFVar.get?
trace[Tactic.generalize_proofs]"after: e' = {e}"
modify fun s => { s with propToFVar }
k fvars pfs e')
go 0 #[] #[] (proofToFVar := { }) (propToFVar := propToFVar)
