# 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`.

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

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.

Instances For

source
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

Instances For

source
structure Mathlib.Tactic.GRewrite.Config extends 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.

Instances For

source
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.

Instances For