The generalized rewriting tactic

This module defines the core of the grw/grewrite tactic.

This file provides two implementations of the tactic:

1. The simple implementation uses kabstract to determine where to rewrite, and then calls MVarId.gcongr to prove that the rewrite is valid. This is used by nth_grw and grw'
2. The more sophisticated implementation has its own congruence loop, applying gcongr lemmas to create the replacement expression, while at the same time proving that this is related to the original expression. This is used by grw and apply_rw.

structure Mathlib.Tactic.GRewrite.GRewriteResult : Type

The result returned by Lean.MVarId.grewrite.

• eNew : Lean.Expr

  The rewritten expression

• impProof : Lean.Expr

  The proof of the implication. The direction depends on the argument forwardImp.

• mvarIds : List Lean.MVarId

  The new side goals

• lctx? : Option Lean.LocalContext

  The outermost local context in which the rewrite makes sense. If the rewrite does not involve bound variables, this is none. This is used for fixing the generated info tree, so that the "Expected Type" is displayed correctly.

structure Mathlib.Tactic.GRewrite.Configextends Lean.Meta.Rewrite.Config : Type

Configures the behavior of the rewrite and rw tactics.

• transparency : TransparencyMode
• offsetCnstrs : Bool
• occs : Occurrences
• newGoals : NewGoals
• useRewrite : Bool

  When useRewrite = true, switch to using the default rewrite tactic when the goal is and equality or iff.

• implicationHyp : Bool

  When implicationHyp = true, interpret the rewrite rule as an implication.

• useKAbstract : Bool

  Whether to use kabstract to find the rewrites locations.

def Lean.MVarId.grewrite (goal : MVarId) (e hrel : Expr) (mvarIds : Array (MVarId × Array LocalDecl)) (forwardImp symm : Bool) (config : Mathlib.Tactic.GRewrite.Config) : MetaM Mathlib.Tactic.GRewrite.GRewriteResult

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.

Equations

• One or more equations did not get rendered due to their size.