feat: attribute [simp ←] (#5870)

This adds the ability to add the converse direction of a rewrite rule
not just in simp arguments `simp [← thm]`, but also as a global
attribute

```lean
attribute [simp ←] thm
```

This fixes #5828.

This can be undone with `attribute [-simp]`, although note that
`[-simp]` wins and cannot be undone at the moment (#5868).

Like `simp [← thm]` (see #4290), this will do an implicit `attribute
[-simp] thm` if the other direction is already defined.

src/Init/Tactics.lean

@@ -1490,6 +1490,11 @@ have been simplified by using the modifier `↓`. Here is an example
 @[simp↓] theorem not_and_eq (p q : Prop) : (¬ (p ∧ q)) = (¬p ∨ ¬q) :=
 ```
 
+You can instruct the simplifier to rewrite the lemma from right-to-left:
+```lean
+attribute @[simp ←] and_assoc
+```
+
 When multiple simp theorems are applicable, the simplifier uses the one with highest priority.
 The equational theorems of function are applied at very low priority (100 and below).
 If there are several with the same priority, it is uses the "most recent one". Example:
@@ -1501,7 +1506,7 @@ If there are several with the same priority, it is uses the "most recent one". E
   cases d <;> rfl
 ```
 -/
-syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
+syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
 
 /--
 Theorems tagged with the `grind_norm` attribute are used by the `grind` tactic normalizer/pre-processor.

src/Lean/Meta/Tactic/Simp/Attr.lean

@@ -26,10 +26,13 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension)
         let go : MetaM Unit := do
           let info ← getConstInfo declName
           let post := if stx[1].isNone then true else stx[1][0].getKind == ``Lean.Parser.Tactic.simpPost
-          let prio ← getAttrParamOptPrio stx[2]
+          let inv := !stx[2].isNone
+          let prio ← getAttrParamOptPrio stx[3]
           if (← isProp info.type) then
-            addSimpTheorem ext declName post (inv := false) attrKind prio
+            addSimpTheorem ext declName post (inv := inv) attrKind prio
           else if info.hasValue then
+            if inv then
+              throwError "invalid '←' modifier, '{declName}' is a declaration name to be unfolded"
             if (← SimpTheorems.ignoreEquations declName) then
               ext.add (SimpEntry.toUnfold declName) attrKind
             else if let some eqns ← getEqnsFor? declName then

src/Lean/Meta/Tactic/Simp/RegisterCommand.lean

@@ -21,7 +21,7 @@ macro (name := _root_.Lean.Parser.Command.registerSimpAttr) doc:(docComment)?
   let procDescr := quote s!"simproc set for {procId.getId.toString}"
   -- TODO: better docDomment for simprocs
   `($[$doc:docComment]? initialize ext : SimpExtension ← registerSimpAttr $(quote id.getId) $descr $(quote id.getId)
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? (prio)? : attr
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str (Parser.Tactic.simpPre <|> Parser.Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (prio)? : attr
     /-- Simplification procedure -/
     initialize extProc : SimprocExtension ← registerSimprocAttr $(quote procId.getId) $procDescr none $(quote procId.getId)
     /-- Simplification procedure -/

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -49,6 +49,11 @@ def Origin.key : Origin → Name
   | .stx id _ => id
   | .other name => name
 
+/-- The origin corresponding to the converse direction (`← thm` vs. `thm`) -/
+def Origin.converse : Origin → Option Origin
+  | .decl declName phase inv => some (.decl declName phase (not inv))
+  | _ => none
+
 instance : BEq Origin where
   beq a b := match a, b with
     | .decl declName₁ _ inv₁, .decl declName₂ _ inv₂ =>
@@ -225,9 +230,10 @@ If `e` is a backwards theorem `← thm`, we must ensure the forward theorem is e
 from `d`. See issue #4290
 -/
 private def eraseFwdIfBwd (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems :=
-  match e.origin with
-  | .decl declName post true => eraseIfExists d (.decl declName post false)
-  | _ => d
+  if let some converseOrigin := e.origin.converse then
+    eraseIfExists d converseOrigin
+  else
+    d
 
 def addSimpTheoremEntry (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems :=
   let d := eraseFwdIfBwd d e
@@ -262,13 +268,20 @@ def SimpTheorems.registerDeclToUnfoldThms (d : SimpTheorems) (declName : Name) (
 
 def SimpTheorems.erase [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
     (d : SimpTheorems) (thmId : Origin) : m SimpTheorems := do
-  unless d.isLemma thmId ||
+  if d.isLemma thmId ||
     match thmId with
     | .decl declName .. => d.isDeclToUnfold declName || d.toUnfoldThms.contains declName
     | _ => false
-  do
-    logWarning m!"'{thmId.key}' does not have [simp] attribute"
-  return d.eraseCore thmId
+  then
+    return d.eraseCore thmId
+
+  -- `attribute [-simp] foo` should also undo `attribute [simp ←] foo`.
+  if let some thmId' := thmId.converse then
+    if d.isLemma thmId' then
+      return d.eraseCore thmId'
+
+  logWarning m!"'{thmId.key}' does not have [simp] attribute"
+  return d
 
 private partial def isPerm : Expr → Expr → MetaM Bool
   | .app f₁ a₁, .app f₂ a₂ => isPerm f₁ f₂ <&&> isPerm a₁ a₂

stage0/src/stdlib_flags.h

@@ -6,7 +6,7 @@ options get_default_options() {
     // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications
 #if LEAN_IS_STAGE0 == 1
     // switch to `true` for ABI-breaking changes affecting meta code
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `true` for changing built-in parsers used in quotations
     opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax

tests/lean/run/issue5828.lean

@@ -0,0 +1,97 @@
+axiom a : Nat
+axiom b : Nat
+axiom a_eq_b : a = b
+
+axiom P : Nat → Nat → Prop
+
+-- Warm-up: rewriting in the forward direction
+
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+attribute [simp] a_eq_b
+
+/--
+error: unsolved goals
+⊢ P b b
+-/
+#guard_msgs in example : P a b := by simp
+
+attribute [-simp] a_eq_b
+
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+-- Re-adding an attribute after [-simp] does not work, see
+-- https://github.com/leanprover/lean4/issues/5868
+
+attribute [simp] a_eq_b
+
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+-- so this test use new copies of `a_eq_b` for now
+
+axiom a_eq_b_2 : a = b
+
+attribute [simp ←] a_eq_b_2
+
+/--
+error: unsolved goals
+⊢ P a a
+-/
+#guard_msgs in example : P a b := by simp
+
+-- Removing the attribute works, no matter the direction
+
+attribute [-simp] a_eq_b_2
+
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+-- Setting one should erase the other
+
+axiom a_eq_b_3 : a = b
+
+attribute [simp ←] a_eq_b_3
+attribute [simp] a_eq_b_3
+
+/--
+error: unsolved goals
+⊢ P b b
+-/
+#guard_msgs in example : P a b := by simp
+
+
+-- The erasure is sticky:
+attribute [simp ←] a_eq_b_3
+/-- error: simp made no progress -/
+#guard_msgs in example : P a b := by simp
+
+axiom a_eq_b_4 : a = b
+
+attribute [simp] a_eq_b_4
+attribute [simp ←] a_eq_b_4
+
+/--
+error: unsolved goals
+⊢ P a a
+-/
+#guard_msgs in example : P a b := by simp
+
+
+-- Some more error conditions
+
+axiom P_a : P a a
+
+/-- error: invalid '←' modifier in rewrite rule to 'True' -/
+#guard_msgs in
+attribute [simp ←] P_a
+
+/-- error: invalid 'simp', it is not a proposition nor a definition (to unfold) -/
+#guard_msgs in
+attribute [simp ←] P
+
+/-- error: invalid '←' modifier, 'id' is a declaration name to be unfolded -/
+#guard_msgs in
+attribute [simp ←] id