Lean4
/-- Rewrite `e` using the relation `hrel : x ~ y`, and construct an implication proof
using the `gcongr` tactic to discharge this goal.
if `forwardImp = true`, we prove that `e → eNew`; otherwise `eNew → e`.
If `symm = false`, we rewrite `e` to `eNew := e[x/y]`; otherwise `eNew := e[y/x]`.
The code aligns with `Lean.MVarId.rewrite` as much as possible.
-/
def _root_.Lean.MVarId.grewrite (goal : MVarId) (e : Expr) (hrel : Expr) (forwardImp symm : Bool)
(config : GRewrite.Config) : MetaM GRewriteResult :=
goal.withContext
(do
goal.checkNotAssigned `grewrite
let hrelType ← instantiateMVars (← inferType hrel)
let maxMVars? ←
if config.implicationHyp then
if let arity + 1 := hrelType.getForallArity then
pure (some arity)
else
throwTacticEx `apply_rw goal m! "invalid implication {hrelType}"
else
pure none
let (newMVars, binderInfos, hrelType) ← withReducible <| forallMetaTelescopeReducing hrelType maxMVars?
if (hrelType.isAppOfArity ``Iff 2 || hrelType.isAppOfArity ``Eq 3) && config.useRewrite then
let { eNew, eqProof, mvarIds } ← goal.rewrite e hrel symm config.toConfig
let mp := if forwardImp then ``Eq.mp else ``Eq.mpr
let impProof ← mkAppOptM mp #[e, eNew, eqProof]
return { eNew, impProof, mvarIds }
let hrelIn := hrel
let hrel := mkAppN hrel newMVars
let some (_, lhs, rhs) := GCongr.getRel hrelType |
throwTacticEx `grewrite goal m! "{hrelType} is not a relation"
let (lhs, rhs) := if symm then (rhs, lhs) else (lhs, rhs)
if lhs.getAppFn.isMVar then
throwTacticEx `grewrite goal m!"pattern is a metavariable{(indentExpr lhs)}\nfrom relation{indentExpr hrelType}"
let e ← instantiateMVars e
let eAbst ← withConfig (fun oldConfig => { config, oldConfig with }) <| kabstract e lhs config.occs
unless eAbst.hasLooseBVars do
throwTacticEx `grewrite goal m! "did not find instance of the pattern in the target expression{indentExpr lhs}"
let eNew := eAbst.instantiate1 rhs
let eNew ← instantiateMVars eNew
try
check eNew
catch ex =>
throwTacticEx `grewrite goal
m!"\
rewritten expression is not type correct:{(indentD eNew)}\nError: {ex.toMessageData}\
\n\n\
Possible solutions: use grewrite's 'occs' configuration option to limit which occurrences \
are rewritten, or specify what the rewritten expression should be and use 'gcongr'."
let eNew ←
if rhs.hasBinderNameHint then
eNew.resolveBinderNameHint
else
pure eNew
let hole ← mkFreshExprMVar default
let template := eAbst.instantiate1 hole
let mkImp (e₁ e₂ : Expr) : Expr := .forallE `_a e₁ e₂ .default
let imp := if forwardImp then mkImp e eNew else mkImp eNew e
let gcongrGoal ← mkFreshExprMVar imp
let (_, _, sideGoals) ←
gcongrGoal.mvarId!.gcongr template [] (grewriteHole := hole.mvarId!) (mainGoalDischarger :=
GRewrite.dischargeMain hrel)
-- post-process the metavariables
postprocessAppMVars `grewrite goal newMVars binderInfos (synthAssignedInstances :=
!tactic.skipAssignedInstances.get (← getOptions))
let newMVarIds ← (sideGoals ++ newMVars.map Expr.mvarId!).filterM (not <$> ·.isAssigned)
let otherMVarIds ← getMVarsNoDelayed hrelIn
let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)
let newMVarIds := newMVarIds ++ otherMVarIds
pure { eNew, impProof := ← instantiateMVars gcongrGoal, mvarIds := newMVarIds.toList })
