feat: rewrite tactic

src/Lean/Elab/Tactic.lean

@@ -12,3 +12,4 @@ import Lean.Elab.Tactic.Injection
 import Lean.Elab.Tactic.Match
 import Lean.Elab.Tactic.Binders
 import Lean.Elab.Tactic.Rewrite
+import Lean.Elab.Tactic.Location

src/Lean/Elab/Tactic/Basic.lean

@@ -217,6 +217,12 @@ pure a
 def focus {α} (tactic : TacticM α) : TacticM α :=
 focusAux (do a ← tactic; done; pure a)
 
+def try? {α} (tactic : TacticM α) : TacticM (Option α) :=
+catch (do a ← tactic; pure (some a)) (fun _ => pure none)
+
+def try {α} (tactic : TacticM α) : TacticM Bool :=
+catch (do tactic; pure true) (fun _ => pure false)
+
 /--
   Use `parentTag` to tag untagged goals at `newGoals`.
   If there are multiple new untagged goals, they are named using `<parentTag>.<newSuffix>_<idx>` where `idx > 0`.

src/Lean/Elab/Tactic/Location.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+namespace Lean
+namespace Elab
+namespace Tactic
+
+inductive Location
+| wildcard
+| target
+| localDecls (userNames : Array Name)
+
+/-
+Recall that
+```
+def locationWildcard := parser! "*"
+def locationTarget   := parser! unicodeSymbol "⊢" "|-"
+def locationHyp      := parser! many1 ident
+def location         := parser! "at " >> (locationWildcard <|> locationTarget <|> locationHyp)
+```
+-/
+def expandLocation (stx : Syntax) : Location :=
+let arg := stx.getArg 1;
+if arg.getKind == `Lean.Parser.Tactic.locationWildcard then Location.wildcard
+else if arg.getKind == `Lean.Parser.Tactic.locationTarget then Location.target
+else Location.localDecls $ (arg.getArg 0).getArgs.map fun stx => stx.getId
+
+def expandOptLocation (stx : Syntax) : Location :=
+if stx.isNone then Location.target
+else expandLocation $ stx.getArg 0
+
+end Tactic
+end Elab
+end Lean

src/Lean/Elab/Tactic/Rewrite.lean

@@ -3,23 +3,77 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Meta.Tactic.Rewrite
+import Lean.Meta.Tactic.Replace
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Tactic.Location
 
 namespace Lean
 namespace Elab
 namespace Tactic
 
+open Meta
+
 @[builtinMacro Lean.Parser.Tactic.rewriteSeq] def expandRewriteTactic : Macro :=
 fun stx =>
   let seq := ((stx.getArg 1).getArg 1).getArgs.getSepElems;
   let loc := stx.getArg 2;
-  pure $ mkNullNode $ seq.map fun rwRule => Syntax.node `Lean.Parser.Tactic.rewrite #[stx.getArg 0, rwRule, loc]
+  pure $ mkNullNode $ seq.map fun rwRule => Syntax.node `Lean.Parser.Tactic.rewrite #[mkAtomFrom rwRule "rewrite ", rwRule, loc]
 
-@[builtinTactic «rewrite»] def evalRewrite : Tactic :=
-fun stx =>  do
-  logInfo $ "WIP " ++ stx;
-  pure ()
+def rewriteTarget (stx : Syntax) (symm : Bool) : TacticM Unit := do
+(g, gs) ← getMainGoal;
+withMVarContext g do
+  e ← elabTerm stx none true;
+  gDecl ← getMVarDecl g;
+  target ← instantiateMVars gDecl.type;
+  r ← liftMetaM $ rewrite g target e symm;
+  g' ← liftMetaM $ replaceTargetEq g r.eNew r.eqProof;
+  setGoals (g' :: r.mvarIds ++ gs)
+
+def rewriteLocalDeclFVarId (stx : Syntax) (symm : Bool) (fvarId : FVarId) : TacticM Unit := do
+(g, gs) ← getMainGoal;
+withMVarContext g do
+  e ← elabTerm stx none true;
+  localDecl ← getLocalDecl fvarId;
+  rwResult ← liftMetaM $ rewrite g localDecl.type e symm;
+  replaceResult ← liftMetaM $ replaceLocalDecl g fvarId rwResult.eNew rwResult.eqProof;
+  setGoals (replaceResult.mvarId :: rwResult.mvarIds ++ gs)
+
+def rewriteLocalDecl (stx : Syntax) (symm : Bool) (userName : Name) : TacticM Unit := do
+withMainMVarContext do
+  localDecl ← getLocalDeclFromUserName userName;
+  rewriteLocalDeclFVarId stx symm localDecl.fvarId
+
+def rewriteAll (stx : Syntax) (symm : Bool) : TacticM Unit := do
+worked ← try $ rewriteTarget stx symm;
+withMainMVarContext do
+  lctx ← getLCtx;
+  worked ← lctx.getFVarIds.foldrM -- We must traverse backwards because `replaceLocalDecl` uses the revert/intro idiom
+    (fun fvarId worked => do
+      worked' ← try $ rewriteLocalDeclFVarId stx symm fvarId;
+      pure $ worked || worked')
+    worked;
+  unless worked do
+    (mvarId, _) ← getMainGoal;
+    liftMetaM $ throwTacticEx `rewrite mvarId ("did not find instance of the pattern in the current goal")
+
+/-
+```
+def rwRule    := parser! optional (unicodeSymbol "←" "<-") >> termParser
+def «rewrite» := parser! "rewrite" >> rwRule >> optional location
+```
+-/
+@[builtinTactic Lean.Parser.Tactic.rewrite] def evalRewrite : Tactic :=
+fun stx => do
+  let rule := stx.getArg 1;
+  let symm := !(rule.getArg 0).isNone;
+  let term := rule.getArg 1;
+  let loc  := expandOptLocation $ stx.getArg 2;
+  match loc with
+  | Location.target => rewriteTarget term symm
+  | Location.localDecls userNames => userNames.forM (rewriteLocalDecl term symm)
+  | Location.wildcard => rewriteAll term symm
 
 end Tactic
 end Elab

src/Lean/Meta/Basic.lean

@@ -353,6 +353,12 @@ match lctx.find? fvarId with
 def getFVarLocalDecl (fvar : Expr) : m LocalDecl := liftMetaM do
 getLocalDecl fvar.fvarId!
 
+def getLocalDeclFromUserName (userName : Name) : m LocalDecl := liftMetaM do
+lctx ← getLCtx;
+match lctx.findFromUserName? userName with
+| some d => pure d
+| none   => throwError ("unknown local declaration '" ++ userName ++ "'")
+
 def instantiateMVars (e : Expr) : m Expr := liftMetaM do
 if e.hasMVar then
   modifyGet $ fun s =>

tests/lean/rewrite.lean

@@ -0,0 +1,49 @@
+new_frontend
+
+axiom appendNil {α} (as : List α) : as ++ [] = as
+axiom appendAssoc {α} (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs)
+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;
+exact rfl
+
+theorem ex2 {α} (as bs : List α) : as.reverse.reverse ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs) := by
+rewrite [reverseEq, reverseEq]; -- Error on second reverseEq
+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₂;
+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 *;
+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
+done
+
+theorem ex5 (m n k : Nat) (h : 0 + n = m) (h : k = m) : k = n := by
+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₁;
+exact h₁ h₃
+
+theorem ex7 (p q r : Prop) (h₁ : q → r) (h₂ : p ↔ q) (h₃ : p) : r := by
+rw h₂ at h₃;
+exact h₁ h₃

tests/lean/rewrite.lean.expected.out

@@ -0,0 +1,20 @@
+α : Type _
+as bs : List α
+⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
+rewrite.lean:14:20: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
+α : Type _
+as bs : List α
+⊢ as ++ List.nil ++ List.nil ++ bs ++ bs = as ++ (bs ++ bs)
+x y z : Nat
+h₁ : x = y
+h₂ : y = z
+⊢ x = z
+rewrite.lean:33:0: 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
+⊢ x = z
+m n k : Nat
+h✝ : n = m
+h : k = m
+⊢ k = n

tests/lean/run/matchtac.lean

@@ -78,4 +78,4 @@ match xs, h:last xs with
 theorem tst9 {α} [Inhabited α] (xs : List α) : xs ≠ [] → xs = popBack xs ++ [back xs] := by
 match xs, h:last xs with
 | _, ListLast.empty         => intro h; exact absurd rfl h
-| _, ListLast.nonEmpty ys y => intro; exact  sorry
+| _, ListLast.nonEmpty ys y => intro; rw [popBackEq, backEq]; exact rfl