The simp_rw tactic

This file defines the simp_rw tactic: it functions as a mix of simp and rw. Like rw, it applies each rewrite rule in the given order, but like simp it repeatedly applies these rules and also under binders like ∀ x, ..., ∃ x, ... and fun x ↦ ....

Comparison with simp and rw

rw alone cannot solve the following, but simp_rw can:

example {a : ℕ}
    (h1 : ∀ a b : ℕ, a - 1 ≤ b ↔ a ≤ b + 1)
    (h2 : ∀ a b : ℕ, a ≤ b ↔ ∀ c, c < a → c < b) :
    (∀ b, a - 1 ≤ b) = ∀ b c : ℕ, c < a → c < b + 1 := by
  simp_rw [h1, h2]

simp also solves the goal above, but it does not show the step-by-step transformation of the goal that simp_rw shows. rw alone cannot solve this because it cannot rewrite expressions containing bound variables. With conv and intro, rw can be used:

example {a : ℕ}
    (h1 : ∀ a b : ℕ, a - 1 ≤ b ↔ a ≤ b + 1)
    (h2 : ∀ a b : ℕ, a ≤ b ↔ ∀ c, c < a → c < b) :
    (∀ b, a - 1 ≤ b) = ∀ b c : ℕ, c < a → c < b + 1 := by
  conv_lhs =>
    intro
    rw [h1, h2]

Internally, simp_rw [lemma_1, ..., lemma_n] is equivalent to

simp only [lemma_1]
...
simp only [lemma_n]

Unlike rw, simp_rw cannot introduce new subgoals for conditional rewrite rules. For example, the following works with rw, while simp_rw requires the proofs of the side conditions to be provided upfront, such as simp_rw [h1 h2 h3]:

example (a b c : ℕ) (h1 : a = b → b = c → a = c) (h2 : a = b) (h3 : b = c) : a + 1 = c + 1 := by
  rw [h1]
  -- The rewrite rule `a = c` is applied on the goal, closing it.
  -- The two hypotheses `a = b` and `b = c` of `h1` are created as subgoals.
  · exact h2
  · exact h3

def Mathlib.Tactic.withSimpRWRulesSeq (rwRulesSeqStx : Lean.Syntax) (x : Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

A version of withRWRulesSeq (in core) that doesn't attempt to find equation lemmas, and simply passes the rw rules on to x.

In this case, x passes the rules to simp only, and simp only already finds the equation lemmas, so we don't need to do that here.

Equations

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

def Mathlib.Tactic.tacticSimp_rw___ : Lean.ParserDescr

simp_rw functions as a mix of simp and rw. Like rw, it applies each rewrite rule in the given order, but like simp it repeatedly applies these rules and also under binders like ∀ x, ..., ∃ x, ... and fun x ↦....

See the module docstring for more explanation of the differences between this tactic, simp and rw.

• simp_rw [lemma_1, ..., lemma_n] will rewrite the goal by applying the lemmas in that order. A lemma preceded by ← is applied in the reverse direction. Lemmas passed to simp_rw must be expressions that are valid arguments to simp.
• simp_rw [lemma_1, ..., lemma_n] at h₁ ... hₙ will rewrite the given hypotheses.
• simp_rw [...] at * rewrites in the whole context: all hypotheses and the goal.
• simp_rw (config := cfg) uses cfg as additional configuration options for simp. See the reference manual chapter Configuring Simplification.

Examples:

example {a : ℕ}
    (h1 : ∀ a b : ℕ, a - 1 ≤ b ↔ a ≤ b + 1)
    (h2 : ∀ a b : ℕ, a ≤ b ↔ ∀ c, c < a → c < b) :
    (∀ b, a - 1 ≤ b) = ∀ b c : ℕ, c < a → c < b + 1 := by
  simp_rw [h1, h2]

example (a b c d : ℕ) (h : a = c + d) : b + a = b + c + d := by
  -- The option `+arith` allows `simp` to simplify `b + (c + d)` to `b + c + d` after replacing `a`
  -- with `c + d`.
  simp_rw +arith [h]

Equations

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