feat: remove bracket-less rw

src/Init/Data/Array/InsertionSort.lean

@@ -23,6 +23,6 @@ where
     | j'+1 =>
       have h' : j' < a.size by subst j; exact Nat.ltTrans (Nat.ltSuccSelf _) h
       if lt (a.get ⟨j, h⟩) (a.get ⟨j', h'⟩) then
-        swapLoop (a.swap ⟨j, h⟩ ⟨j', h'⟩) j' (by rw size_swap; assumption done)
+        swapLoop (a.swap ⟨j, h⟩ ⟨j', h'⟩) j' (by rw [size_swap]; assumption done)
       else
         a

src/Init/Data/Nat/Basic.lean

@@ -192,7 +192,7 @@ theorem succ_sub_succ (n m : Nat) : succ n - succ m = n - m :=
   succ_sub_succ_eq_sub n m
 
 protected theorem sub_self : ∀ (n : Nat), n - n = 0
-  | 0        => by rw Nat.sub_zero
+  | 0        => by rw [Nat.sub_zero]
   | (succ n) => by rw [succ_sub_succ, Nat.sub_self n]
 
 protected theorem ltOfLtOfLe {n m k : Nat} : n < m → m ≤ k → n < k :=

src/Init/Notation.lean

@@ -246,31 +246,19 @@ syntax (name := changeWith) "change " term " with " term (location)? : tactic
 syntax rwRule    := ("←" <|> "<-")? term
 syntax rwRuleSeq := "[" rwRule,+,? "]"
 
-syntax (name := rewrite) "rewrite " rwRule (location)? : tactic
-syntax (name := rewriteSeq) (priority := high) "rewrite " rwRuleSeq (location)? : tactic
-syntax (name := erewrite) "erewrite " rwRule (location)? : tactic
-syntax (name := erewriteSeq) (priority := high) "erewrite " rwRuleSeq (location)? : tactic
+syntax (name := rewriteSeq) "rewrite " rwRuleSeq (location)? : tactic
+syntax (name := erewriteSeq) "erewrite " rwRuleSeq (location)? : tactic
 
-syntax (name := rw) "rw " rwRule (location)? : tactic
-syntax (name := rwSeq) (priority := high) "rw " rwRuleSeq (location)? : tactic
-syntax (name := erw) "erw " rwRule (location)? : tactic
-syntax (name := erwSeq) (priority := high) "erw " rwRuleSeq (location)? : tactic
+syntax (name := rwSeq) "rw " rwRuleSeq (location)? : tactic
+syntax (name := erwSeq) "erw " rwRuleSeq (location)? : tactic
 
 private def withCheapRefl (tac : Syntax) : MacroM Syntax :=
   `(tactic| $tac; try (withReducible rfl))
 
-@[macro rw]
-def expandRw : Macro :=
-  fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.rewrite |>.setArg 0 (mkAtomFrom stx "rewrite"))
-
 @[macro rwSeq]
 def expandRwSeq : Macro :=
   fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.rewriteSeq |>.setArg 0 (mkAtomFrom stx "rewrite"))
 
-@[macro erw]
-def expandERw : Macro :=
-  fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewrite |>.setArg 0 (mkAtomFrom stx "erewrite"))
-
 @[macro erwSeq]
 def expandERwSeq : Macro :=
   fun stx => withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite"))

src/Lean/Elab/Tactic/Rewrite.lean

@@ -11,36 +11,6 @@ import Lean.Elab.Tactic.Location
 namespace Lean.Elab.Tactic
 open Meta
 
-private def expand (kind : SyntaxNodeKind) (stx : Syntax) : Syntax := do
-  let token   := stx[0]
-  let lbrak   := stx[1][0]
-  let rwRules := stx[1][1].getArgs
-  let rbrak   := stx[1][2]
-  let loc     := stx[2]
-  let mut newTacs := #[]
-  let numRules := (rwRules.size + 1) / 2
-  for i in [:numRules] do
-    let rwRule := rwRules[i * 2]
-    let sep    := rwRules.getD (i * 2 + 1) Syntax.missing
-    -- We use `stx` as "position provider" for the first rule
-    -- Without this change, we don't get correct information when we hover over `rw`/`rewrite`/`erewrite` with multiple rewrites
-    let ref :=
-      -- use whole original tactic as "position provider" for last rule so
-      -- we show the final state outside the brackets
-      if i == numRules - 1 then stx
-      -- other rules: include separator
-      else mkNullNode #[rwRule, sep]
-    let newTac := Syntax.node kind #[token, rwRule, loc]
-    let newTac := newTac.copyHeadTailInfoFrom ref
-    newTacs := newTacs.push newTac
-  return mkNullNode newTacs
-
-@[builtinMacro Lean.Parser.Tactic.rewriteSeq] def expandRewriteTactic : Macro := fun stx =>
-  return expand ``Parser.Tactic.rewrite stx
-
-@[builtinMacro Lean.Parser.Tactic.erewriteSeq] def expandERewriteTactic : Macro := fun stx =>
-  return expand ``Parser.Tactic.erewrite stx
-
 def rewriteTarget (stx : Syntax) (symm : Bool) (mode : TransparencyMode) : TacticM Unit := do
   Term.withSynthesize <| withMainContext do
     let e ← elabTerm stx none true
@@ -73,27 +43,37 @@ def rewriteAll (stx : Syntax) (symm : Bool) (mode : TransparencyMode) : TacticM
       throwTacticEx `rewrite mvarId "did not find instance of the pattern in the current goal"
 
 def evalRewriteCore (mode : TransparencyMode) : Tactic := fun stx => do
-  let rule := stx[1]
-  let symm := !rule[0].isNone
-  let term := rule[1]
-  let loc  := expandOptLocation stx[2]
-  match loc with
-  | Location.targets hyps type =>
-     hyps.forM (rewriteLocalDecl term symm · mode)
-     if type then
-      rewriteTarget term symm mode
-  | Location.wildcard => rewriteAll term symm mode
+  let token := stx[0]
+  let lbrak := stx[1][0]
+  let rules := stx[1][1].getArgs
+  let rbrak := stx[1][2]
+  let loc   := expandOptLocation stx[2]
+  -- show initial state up to (incl.) `[`
+  withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ())
+  let mut newTacs := #[]
+  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]
+        match loc with
+        | Location.targets hyps type =>
+          hyps.forM (rewriteLocalDecl term symm · mode)
+          if type then
+            rewriteTarget term symm mode
+        | Location.wildcard => rewriteAll term symm mode
+  -- show final state on `]`
+  withTacticInfoContext rbrak (pure ())
 
-/-
-```
-def rwRule    := leading_parser optional (unicodeSymbol "←" "<-") >> termParser
-def «rewrite» := leading_parser "rewrite" >> rwRule >> optional location
-```
--/
-@[builtinTactic Lean.Parser.Tactic.rewrite] def evalRewrite : Tactic :=
+@[builtinTactic Lean.Parser.Tactic.rewriteSeq] def evalRewriteSeq : Tactic :=
   evalRewriteCore TransparencyMode.instances
 
-@[builtinTactic Lean.Parser.Tactic.erewrite] def evalERewrite : Tactic :=
+@[builtinTactic Lean.Parser.Tactic.erewriteSeq] def evalERewriteSeq : Tactic :=
   evalRewriteCore TransparencyMode.default
 
 end Lean.Elab.Tactic

tests/lean/interactive/plainGoal.lean.expected.out

@@ -38,8 +38,8 @@
  "goals": ["α : Sort ?u\na : α\n⊢ α"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 25, "character": 3}}
-{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = 0\n```",
- "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = 0"]}
+{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n\n```",
+ "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 25, "character": 9}}
 {"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m\n```",

tests/lean/rewrite.lean

@@ -5,7 +5,7 @@ axiom reverseEq {α} (as : List α) : as.reverse.reverse = as
 theorem ex1 {α} (as bs : List α) : as.reverse.reverse ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs) := by
   rw [appendNil, appendNil, reverseEq];
   traceState;
-  rw ←appendAssoc;
+  rw [←appendAssoc];
 
 
 theorem ex2 {α} (as bs : List α) : as.reverse.reverse ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs) := by
@@ -15,33 +15,33 @@ done
 axiom zeroAdd (x : Nat) : 0 + x = x
 
 theorem ex2 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
-rewrite zeroAdd at h₁ h₂;
+rewrite [zeroAdd] at h₁ h₂;
 traceState;
 subst x;
 subst y;
 exact rfl
 
 theorem ex3 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
-rewrite zeroAdd at *;
+rewrite [zeroAdd] at *;
 subst x;
 subst y;
 exact rfl
 
 theorem ex4 (x y z) (h₁ : 0 + x = y) (h₂ : 0 + y = z) : x = z := by
-rewrite appendAssoc at *; -- Error
+rewrite [appendAssoc] at *; -- Error
 done
 
 theorem ex5 (m n k : Nat) (h : 0 + n = m) (h : k = m) : k = n := by
-rw zeroAdd at *;
+rw [zeroAdd] at *;
 traceState; -- `h` is still a name for `h : k = m`
 refine Eq.trans h ?hole;
 apply Eq.symm;
 assumption
 
 theorem ex6 (p q r : Prop) (h₁ : q → r) (h₂ : p ↔ q) (h₃ : p) : r := by
-rw ←h₂ at h₁;
+rw [←h₂] at h₁;
 exact h₁ h₃
 
 theorem ex7 (p q r : Prop) (h₁ : q → r) (h₂ : p ↔ q) (h₃ : p) : r := by
-rw h₂ at h₃;
+rw [h₂] at h₃;
 exact h₁ h₃

tests/lean/rewrite.lean.expected.out

@@ -1,7 +1,7 @@
 α : Type u_1
 as bs : List α
 ⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
-rewrite.lean:12:0-12:38: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
+rewrite.lean:12:20-12:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
   List.reverse (List.reverse ?as)
 α : Type u_1
 as bs : List α
@@ -10,7 +10,7 @@ x y z : Nat
 h₁ : x = y
 h₂ : y = z
 ⊢ x = z
-rewrite.lean:31:0-31:24: error: tactic 'rewrite' failed, did not find instance of the pattern in the current goal
+rewrite.lean:31:9-31:20: error: tactic 'rewrite' failed, did not find instance of the pattern in the current goal
 x y z : Nat
 h₁ : 0 + x = y
 h₂ : 0 + y = z