- eNew : Lean.Expr
- eqProof : Lean.Expr
- mvarIds : List Lean.MVarId
def
Lean.Meta.rewrite
(mvarId : Lean.MVarId)
(e : Lean.Expr)
(heq : Lean.Expr)
(symm : optParam Bool false)
(occs : optParam Lean.Occurrences Lean.Occurrences.all)
(config : optParam Lean.Meta.Rewrite.Config { transparency := Lean.Meta.TransparencyMode.reducible, offsetCnstrs := true })
:
Equations
- Lean.Meta.rewrite mvarId e heq symm occs config = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `rewrite let a ← Lean.Meta.inferType heq let heqType ← Lean.Meta.instantiateMVars a let discr ← Lean.Meta.forallMetaTelescopeReducing heqType none Lean.MetavarKind.natural let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (newMVars, binderInfos, heqType) => let heq := Lean.mkAppN heq newMVars; let cont := fun heq heqType => do let a ← Lean.Meta.matchEq? heqType match a with | none => Lean.Meta.throwTacticEx `rewrite mvarId (Lean.toMessageData "equality or iff proof expected" ++ Lean.toMessageData (Lean.indentExpr heqType) ++ Lean.toMessageData "") Lean.Syntax.missing | some (α, lhs, rhs) => let cont := fun heq heqType lhs rhs => let _do_jp := fun y => do let e ← Lean.Meta.instantiateMVars e let eAbst ← Lean.Meta.withConfig (fun oldConfig => { foApprox := oldConfig.foApprox, ctxApprox := oldConfig.ctxApprox, quasiPatternApprox := oldConfig.quasiPatternApprox, constApprox := oldConfig.constApprox, isDefEqStuckEx := oldConfig.isDefEqStuckEx, transparency := config.transparency, zetaNonDep := oldConfig.zetaNonDep, trackZeta := oldConfig.trackZeta, unificationHints := oldConfig.unificationHints, proofIrrelevance := oldConfig.proofIrrelevance, assignSyntheticOpaque := oldConfig.assignSyntheticOpaque, ignoreLevelMVarDepth := oldConfig.ignoreLevelMVarDepth, offsetCnstrs := config.offsetCnstrs, etaStruct := oldConfig.etaStruct }) (Lean.Meta.kabstract e lhs occs) let _do_jp : PUnit → Lean.MetaM Lean.Meta.RewriteResult := fun y => let eNew := Lean.Expr.instantiate1 eAbst rhs; do let eNew ← Lean.Meta.instantiateMVars eNew let eEqE ← Lean.Meta.mkEq e e let eEqEAbst : Lean.Expr := Lean.mkApp (Lean.Expr.appFn! eEqE) eAbst let motive : Lean.Expr := Lean.mkLambda `_a Lean.BinderInfo.default α eEqEAbst let a ← Lean.Meta.isTypeCorrect motive let _do_jp : PUnit → Lean.MetaM Lean.Meta.RewriteResult := fun y => do let eqRefl ← Lean.Meta.mkEqRefl e let eqPrf ← Lean.Meta.mkEqNDRec motive eqRefl heq Lean.Meta.postprocessAppMVars `rewrite mvarId newMVars binderInfos let newMVarIds ← Array.filterM (fun a => not <$> Lean.Meta.isExprMVarAssigned a) (Array.map Lean.Expr.mvarId! newMVars) 0 (Array.size (Array.map Lean.Expr.mvarId! newMVars)) let otherMVarIds ← Lean.Meta.getMVarsNoDelayed eqPrf let otherMVarIds : Array Lean.MVarId := Array.filter (fun a => !Array.contains newMVarIds a) otherMVarIds 0 (Array.size otherMVarIds) let newMVarIds : Array Lean.MVarId := newMVarIds ++ otherMVarIds pure { eNew := eNew, eqProof := eqPrf, mvarIds := Array.toList newMVarIds } if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwTacticEx `rewrite mvarId (Function.comp Lean.MessageData.ofFormat Lean.format "motive is not type correct") Lean.Syntax.missing _do_jp y if Lean.Expr.hasLooseBVars eAbst = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwTacticEx `rewrite mvarId (Lean.toMessageData "did not find instance of the pattern in the target expression" ++ Lean.toMessageData (Lean.indentExpr lhs) ++ Lean.toMessageData "") Lean.Syntax.missing _do_jp y; if Lean.Expr.isMVar (Lean.Expr.getAppFn lhs) = true then do let y ← Lean.Meta.throwTacticEx `rewrite mvarId (Lean.toMessageData "pattern is a metavariable" ++ Lean.toMessageData (Lean.indentExpr lhs) ++ Lean.toMessageData "\nfrom equation" ++ Lean.toMessageData (Lean.indentExpr heqType) ++ Lean.toMessageData "") Lean.Syntax.missing _do_jp y else do let y ← pure PUnit.unit _do_jp y; match symm with | false => cont heq heqType lhs rhs | true => do let heq ← Lean.Meta.mkEqSymm heq let heqType ← Lean.Meta.mkEq rhs lhs cont heq heqType rhs lhs; match Lean.Expr.iff? heqType with | some (lhs, rhs) => do let heqType ← Lean.Meta.mkEq lhs rhs let heq : Lean.Expr := Lean.mkApp3 (Lean.mkConst `propext) lhs rhs heq cont heq heqType | none => cont heq heqType