The generalized rewriting tactic

This file defines the tactics that use the backend defined in Mathlib.Tactic.GRewrite.Core:

• grewrite
• grw
• apply_rw
• nth_grewrite
• nth_grw

def Mathlib.Tactic.grewriteTarget (stx : Lean.Syntax) (symm : Bool) (config : GRewrite.Config) : Lean.Elab.Tactic.TacticM Unit

Apply the grewrite tactic to the current goal.

def Mathlib.Tactic.grewriteLocalDecl (stx : Lean.Syntax) (symm : Bool) (fvarId : Lean.FVarId) (config : GRewrite.Config) : Lean.Elab.Tactic.TacticM Unit

Apply the grewrite tactic to a local hypothesis.

def Mathlib.Tactic.elabGRewriteConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM GRewrite.Config

Function elaborating GRewrite.Config.

def Mathlib.Tactic.grewriteSeq : Lean.ParserDescr

grewrite [e] is like grw [e], but it doesn't try to close the goal with rfl. This is analogous to rw and rewrite, where rewrite doesn't try to close the goal with rfl.

def Mathlib.Tactic.evalGRewriteSeq : Lean.Elab.Tactic.Tactic

grewrite [e] is like grw [e], but it doesn't try to close the goal with rfl. This is analogous to rw and rewrite, where rewrite doesn't try to close the goal with rfl.

def Mathlib.Tactic.grwSeq : Lean.ParserDescr

grw [e] works just like rw [e], but e can be a relation other than = or ↔.

For example:

variable {a b c d n : ℤ}

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [h₁, h₂]

example (h : a ≡ b [ZMOD n]) : a ^ 2 ≡ b ^ 2 [ZMOD n] := by
  grw [h]

example (h₁ : a ∣ b) (h₂ : b ∣ a ^ 2 * c) : a ∣ b ^ 2 * c := by
  grw [h₁] at *
  exact h₂

To replace the RHS with the LHS of the given relation, use the ← notation (just like in rw):

example (h₁ : a < b) (h₂ : b ≤ c) : a + d ≤ c + d := by
  grw [← h₂, ← h₁]

The strict inequality a < b is turned into the non-strict inequality a ≤ b to rewrite with it. A future version of grw may get special support for making better use of strict inequalities.

To rewrite only in the n-th position, use nth_grw n. This is useful when grw tries to rewrite in a position that is not valid for the given relation.

To be able to use grw, the relevant lemmas need to be tagged with @[gcongr]. To rewrite inside a transitive relation, you can also give it an IsTrans instance.

To let grw unfold more aggressively, as in erw, use grw (transparency := default).

def Mathlib.Tactic.tacticApply_rewrite___ : Lean.ParserDescr

apply_rewrite [rules] is a shorthand for grewrite +implicationHyp [rules].

def Mathlib.Tactic.applyRwSeq : Lean.ParserDescr

apply_rw [rules] is a shorthand for grw +implicationHyp [rules].

def Mathlib.Tactic.tacticNth_grewrite_____ : Lean.ParserDescr

nth_grewrite is just like nth_rewrite, but for grewrite.

def Mathlib.Tactic.tacticNth_grw_____ : Lean.ParserDescr

nth_grw is just like nth_rw, but for grw.