The generalized rewriting tactic

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

TODO:

The algorithm used to implement grw uses the same method as rw to determine where to rewrite. This means that we can get ill-typed results. Moreover, it doesn't detect which occurrences can be rewritten by gcongr and which can't. It also means we cannot rewrite bound variables.

A better algorithm would be similar to simp only, where we recursively enter the subexpression using gcongr lemmas. This is tricky due to the many different gcongr for each pattern.

With the current implementation, we can instead use nth_grw.

def Mathlib.Tactic.GRewrite.dischargeMain (hrel : Lean.Expr) (goal : Lean.MVarId) : Lean.MetaM Unit

Given a proof of a ~ b, close a goal of the form a ~' b or b ~' a for some possibly different relation ~'.

Equations

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

structure Mathlib.Tactic.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

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.

def Lean.MVarId.grewrite (goal : MVarId) (e hrel : Expr) (forwardImp symm : Bool) (config : Mathlib.Tactic.GRewrite.Config) : MetaM Mathlib.Tactic.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.