Lean4
/-- Main loop for `Lean.MVarId.generalizeProofs`.
The `fvars` array is the array of fvars to generalize proofs for,
and `rfvars` is the array of fvars that have been reverted.
The `g` metavariable has all of these fvars reverted.
-/
partial def generalizeProofsCore (g : MVarId) (fvars rfvars : Array FVarId) (target : Bool) :
MGen (Array Expr × MVarId) :=
go g 0 #[]
where/-- Loop for `generalizeProofsCore`. -/
go (g : MVarId) (i : Nat) (hs : Array Expr) : MGen (Array Expr × MVarId) :=
g.withContext
(do
let tag ← g.getTag
if h : i < rfvars.size then
trace[Tactic.generalize_proofs]"generalizeProofsCore {i }{g}\n{(← get).propToFVar.toArray}"
let fvar := rfvars[i]
if fvars.contains fvar then
-- This is one of the hypotheses that was intentionally reverted.
let tgt ← instantiateMVars <| ← g.getType
let ty := (if tgt.isLet then tgt.letType! else tgt.bindingDomain!).cleanupAnnotations
if ← pure tgt.isLet <&&> Meta.isProp ty then
-- Clear the proof value (using proof irrelevance) and `go` again
let tgt' := Expr.forallE tgt.letName! ty tgt.letBody! .default
let g' ← mkFreshExprSyntheticOpaqueMVar tgt' tag
g.assign <| .app g' tgt.letValue!
return ← go g'.mvarId! i hs
if let some pf := (← get).propToFVar[ty]? then
-- Eliminate this local hypothesis using the pre-existing proof, using proof irrelevance
let tgt' := tgt.bindingBody!.instantiate1 pf
let g' ← mkFreshExprSyntheticOpaqueMVar tgt' tag
g.assign <| .lam tgt.bindingName! tgt.bindingDomain! g' tgt.bindingInfo!
return ← go g'.mvarId! (i + 1) hs
match tgt with
| .forallE n t b bi =>
let prop ← Meta.isProp t
withGeneralizedProofs t none fun hs' pfs' t' => do
let t' := t'.cleanupAnnotations
let tgt' := Expr.forallE n t' b bi
let g' ← mkFreshExprSyntheticOpaqueMVar tgt' tag
g.assign <| mkAppN (← mkLambdaFVars hs' g') pfs'
let (fvar', g') ← g'.mvarId!.intro1P
g'.withContext do
Elab.pushInfoLeaf <|
.ofFVarAliasInfo { id := fvar', baseId := fvar, userName := ← fvar'.getUserName }
if prop then
-- Make this prop available as a proof
MGen.insertFVar t' (.fvar fvar')
go g' (i + 1) (hs ++ hs')
| .letE n t v b nondep =>
withGeneralizedProofs t none fun hs' pfs' t' => do
withGeneralizedProofs v t' fun hs'' pfs'' v' => do
let tgt' := Expr.letE n t' v' b nondep
let g' ← mkFreshExprSyntheticOpaqueMVar tgt' tag
g.assign <| mkAppN (← mkLambdaFVars (hs' ++ hs'') g') (pfs' ++ pfs'')
let (fvar', g') ← g'.mvarId!.intro1P
g'.withContext do
Elab.pushInfoLeaf <|
.ofFVarAliasInfo { id := fvar', baseId := fvar, userName := ← fvar'.getUserName }
go g' (i + 1) (hs ++ hs' ++ hs'')
| _ =>
unreachable!
else
-- This is one of the hypotheses that was incidentally reverted.
let (fvar', g') ← g.intro1P
g'.withContext do
Elab.pushInfoLeaf <| .ofFVarAliasInfo { id := fvar', baseId := fvar, userName := ← fvar'.getUserName }
go g' (i + 1) hs
else if target then
trace[Tactic.generalize_proofs]"\
generalizeProofsCore target{g}\n{(← get).propToFVar.toArray}"
withGeneralizedProofs (← g.getType) none fun hs' pfs' ty' => do
let g' ← mkFreshExprSyntheticOpaqueMVar ty' tag
g.assign <| mkAppN (← mkLambdaFVars hs' g') pfs'
return (hs ++ hs', g'.mvarId!)
else
return (hs, g))
