doc-next-gen

Mathlib.Tactic.SimpRw

Module docstring

{"# 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 ↦ .... "}

Mathlib.Tactic.withSimpRWRulesSeq definition
(token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit
Full source 
/-- A version of `withRWRulesSeq` (in core) that doesn't attempt to find equation lemmas, and simply
  passes the rw rules on to `x`. -/
def withSimpRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax)
    (x : (symm : Bool) → (term : Syntax) → TacticM Unit) : TacticM Unit := do
  let lbrak := rwRulesSeqStx[0]
  let rules := rwRulesSeqStx[1].getArgs
  -- show initial state up to (incl.) `[`
  withTacticInfoContextwithTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
  let numRules := (rules.size + 1) / 2
  for i in [:numRules] do
    let rule := rules[i * 2]!
    let sep  := rules.getD (i * 2 + 1) Syntax.missing
    -- show rule state up to (incl.) next `,`
    withTacticInfoContext (mkNullNode #[rule, sep]) do
      -- show errors on rule
      withRef rule do
        let symm := !rule[0].isNone
        let term := rule[1]
        -- let processId (id : Syntax) : TacticM Unit := do
        x symm term
Processing Rewrite Rules for `simp_rw`
Informal description
The function `withSimpRWRulesSeq` processes a sequence of rewrite rules for the `simp_rw` tactic. It takes a syntax token and a sequence of rewrite rules, then applies each rule in order while maintaining the tactic state context. For each rule, it checks if the rule is symmetric (indicated by the presence of a modifier) and extracts the term to rewrite. The function then applies the rule using the provided continuation function `x` which handles the actual rewriting logic.
Mathlib.Tactic.tacticSimp_rw___ definition
: Lean.ParserDescr✝
Full source 
/--
`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 ↦...`.
Usage:

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

Lemmas passed to `simp_rw` must be expressions that are valid arguments to `simp`.
For example, neither `simp` nor `rw` can solve the following, but `simp_rw` can:

```lean
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]
```
-/
elab s:"simp_rw " cfg:optConfig rws:rwRuleSeq g:(location)? : tactic => focus do
  evalTactic (← `(tactic| simp%$s $[$(getConfigItems cfg)]* (failIfUnchanged := false) only $(g)?))
  withSimpRWRulesSeq s rws fun symm term => do
    evalTactic (← match term with
    | `(term| $e:term) =>
      if symm then
        `(tactic| simp%$e $cfg only [← $e:term] $g ?)
      else
        `(tactic| simp%$e $cfg only [$e:term] $g ?))
`simp_rw` tactic (combined `simp` and `rw`)
Informal description
The `simp_rw` tactic combines the functionality of `simp` and `rw`. It applies each rewrite rule in the given order (like `rw`), but also repeatedly applies these rules and works under binders such as `∀ x, ...`, `∃ x, ...`, and `λ x, ...` (like `simp`). Usage: - `simp_rw [lemma_1, ..., lemma_n]` rewrites the goal by applying the lemmas in order, with `←` indicating reverse application. - `simp_rw [lemma_1, ..., lemma_n] at h₁ ... hₙ` rewrites the specified hypotheses. - `simp_rw [...] at *` rewrites the entire context (all hypotheses and the goal). The lemmas must be valid `simp` arguments. For example, `simp_rw` can solve cases where neither `simp` nor `rw` alone suffices, such as rewriting under nested quantifiers.