From 968759637f1a8a1255e7063d9e4228a62a553ebf Mon Sep 17 00:00:00 2001 From: Shrys Date: Thu, 27 Jun 2024 15:05:18 +0000 Subject: [PATCH] chore: Improved nth_rewrite and nth_rw docstrings (#13877) [Zulip thread of discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/docstrings.20of.20.60nth_rewrite.60.20and.20.60nth_rw.60/near/444853793) --- Mathlib/Tactic/NthRewrite.lean | 104 +++++++++++++++++++++++++++++++-- 1 file changed, 99 insertions(+), 5 deletions(-) diff --git a/Mathlib/Tactic/NthRewrite.lean b/Mathlib/Tactic/NthRewrite.lean index 2a64b121d3dfd..3ba52c3db0334 100644 --- a/Mathlib/Tactic/NthRewrite.lean +++ b/Mathlib/Tactic/NthRewrite.lean @@ -17,11 +17,56 @@ namespace Mathlib.Tactic open Lean Elab Tactic Meta Parser.Tactic -/-- `nth_rewrite` is a variant of `rewrite` that only changes the nth occurrence of the expression -to be rewritten. +/-- `nth_rewrite` is a variant of `rewrite` that only changes the `n`ᵗʰ _occurrence_ of the +expression to be rewritten. `nth_rewrite n [eq₁, eq₂,..., eqₘ]` will rewrite the `n`ᵗʰ _occurrence_ +of each of the `m` equalities `eqᵢ`in that order. Occurrences are counted beginning with `1` in +order of precedence. -Note: The occurrences are counted beginning with `1` and not `0`, this is different than in -mathlib3. The translation will be handled by mathport. -/ +For example, +```lean +example (h : a = 1) : a + a + a + a + a = 5 := by + nth_rewrite 2 [h] +/- +a: ℕ +h: a = 1 +⊢ a + 1 + a + a + a = 5 +-/ +``` +Notice that the second occurrence of `a` from the left has been rewritten by `nth_rewrite`. + +To understand the importance of order of precedence, consider the example below +```lean +example (a b c : Nat) : (a + b) + c = (b + a) + c := by + nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c +``` +Here, although the occurrence parameter is `2`, `(a + b)` is rewritten to `(b + a)`. This happens +because in order of precedence, the first occurrence of `_ + _` is the one that adds `a + b` to `c`. +The occurrence in `a + b` counts as the second occurrence. + +If a term `t` is introduced by rewriting with `eqᵢ`, then this instance of `t` will be counted as an +_occurrence_ of `t` for all subsequent rewrites of `t` with `eqⱼ` for `j > i`. This behaviour is +illustrated by the example below +```lean +example (h : a = a + b) : a + a + a + a + a = 0 := by + nth_rewrite 3 [h, h] +/- +a b: ℕ +h: a = a + b +⊢ a + a + (a + b + b) + a + a = 0 +-/ +``` +Here, the first `nth_rewrite` with `h` introduces an additional occurrence of `a` in the goal. +That is, the goal state after the first rewrite looks like below +```lean +/- +a b: ℕ +h: a = a + b +⊢ a + a + (a + b) + a + a = 0 +-/ +``` +This new instance of `a` also turns out to be the third _occurrence_ of `a`. Therefore, +the next `nth_rewrite` with `h` rewrites this `a`. +-/ syntax (name := nthRewriteSeq) "nth_rewrite" (config)? ppSpace num rwRuleSeq (location)? : tactic @[inherit_doc nthRewriteSeq, tactic nthRewriteSeq] def evalNthRewriteSeq : Tactic := fun stx => do @@ -41,7 +86,56 @@ syntax (name := nthRewriteSeq) "nth_rewrite" (config)? ppSpace num rwRuleSeq (lo | _ => throwUnsupportedSyntax /-- -`nth_rw` is like `nth_rewrite`, but also tries to close the goal by trying `rfl` afterwards. +`nth_rw` is a variant of `rw` that only changes the `n`ᵗʰ _occurrence_ of the expression to be +rewritten. Like `rw`, and unlike `nth_rewrite`, it will try to close the goal by trying `rfl` +afterwards. `nth_rw n [eq₁, eq₂,..., eqₘ]` will rewrite the `n`ᵗʰ _occurrence_ of each of the +`m` equalities `eqᵢ`in that order. Occurrences are counted beginning with `1` in +order of precedence. For example, +```lean +example (h : a = 1) : a + a + a + a + a = 5 := by + nth_rw 2 [h] +/- +a: ℕ +h: a = 1 +⊢ a + 1 + a + a + a = 5 +-/ +``` +Notice that the second occurrence of `a` from the left has been rewritten by `nth_rewrite`. + +To understand the importance of order of precedence, consider the example below +```lean +example (a b c : Nat) : (a + b) + c = (b + a) + c := by + nth_rewrite 2 [Nat.add_comm] -- ⊢ (b + a) + c = (b + a) + c +``` +Here, although the occurrence parameter is `2`, `(a + b)` is rewritten to `(b + a)`. This happens +because in order of precedence, the first occurrence of `_ + _` is the one that adds `a + b` to `c`. +The occurrence in `a + b` counts as the second occurrence. + +If a term `t` is introduced by rewriting with `eqᵢ`, then this instance of `t` will be counted as an +_occurrence_ of `t` for all subsequent rewrites of `t` with `eqⱼ` for `j > i`. This behaviour is +illustrated by the example below +```lean +example (h : a = a + b) : a + a + a + a + a = 0 := by + nth_rw 3 [h, h] +/- +a b: ℕ +h: a = a + b +⊢ a + a + (a + b + b) + a + a = 0 +-/ +``` +Here, the first `nth_rw` with `h` introduces an additional occurrence of `a` in the goal. That is, +the goal state after the first rewrite looks like below +```lean +/- +a b: ℕ +h: a = a + b +⊢ a + a + (a + b) + a + a = 0 +-/ +``` +This new instance of `a` also turns out to be the third _occurrence_ of `a`. Therefore, +the next `nth_rw` with `h` rewrites this `a`. + +Further, `nth_rw` will close the remaining goal with `rfl` if possible. -/ macro (name := nthRwSeq) "nth_rw" c:(config)? ppSpace n:num s:rwRuleSeq l:(location)? : tactic => -- Note: This is a direct copy of `nth_rw` from core.