feat: add option tactic.skipAssignedInstances := true for backward compatibility

When using `set_option tactic.skipAssignedInstances false`, `simp` and
`rw` will synthesize instance implicit arguments even if they have
assigned by unification. If the synthesized argument does not match
the assigned one the rewrite is not performed. This option has been
added for backward compatibility.

src/Lean/Meta/Tactic/Rewrite.lean

@@ -8,6 +8,7 @@ import Lean.Meta.AppBuilder
 import Lean.Meta.MatchUtil
 import Lean.Meta.KAbstract
 import Lean.Meta.Check
+import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Apply
 
 namespace Lean.Meta
@@ -52,7 +53,8 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           let u1 ← getLevel α
           let u2 ← getLevel eType
           let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
-          postprocessAppMVars `rewrite mvarId newMVars binderInfos (synthAssignedInstances := false)
+          postprocessAppMVars `rewrite mvarId newMVars binderInfos
+            (synthAssignedInstances := !tactic.skipAssignedInstances.get (← getOptions))
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
           let otherMVarIds ← getMVarsNoDelayed eqPrf
           let otherMVarIds := otherMVarIds.filter (!newMVarIds.contains ·)

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

@@ -476,7 +476,7 @@ def processCongrHypothesis (h : Expr) : SimpM Bool := do
 def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do
   trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
   let thm ← mkConstWithFreshMVarLevels c.theoremName
-  let (xs, _, type) ← forallMetaTelescopeReducing (← inferType thm)
+  let (xs, bis, type) ← forallMetaTelescopeReducing (← inferType thm)
   if c.hypothesesPos.any (· ≥ xs.size) then
     return none
   let isIff := type.isAppOf ``Iff
@@ -504,7 +504,7 @@ def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Resul
     unless modified do
       trace[Meta.Tactic.simp.congr] "{c.theoremName} not modified"
       return none
-    unless (← synthesizeArgs (.decl c.theoremName) xs) do
+    unless (← synthesizeArgs (.decl c.theoremName) bis xs) do
       trace[Meta.Tactic.simp.congr] "{c.theoremName} synthesizeArgs failed"
       return none
     let eNew ← instantiateMVars rhs

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

@@ -8,6 +8,7 @@ import Lean.Meta.ACLt
 import Lean.Meta.Match.MatchEqsExt
 import Lean.Meta.AppBuilder
 import Lean.Meta.SynthInstance
+import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.UnifyEq
 import Lean.Meta.Tactic.Simp.Types
 import Lean.Meta.Tactic.LinearArith.Simp
@@ -55,9 +56,15 @@ def discharge?' (thmId : Origin) (x : Expr) (type : Expr) : SimpM Bool := do
         return .notProved
   return r = .proved
 
-def synthesizeArgs (thmId : Origin) (xs : Array Expr) : SimpM Bool := do
-  for x in xs do
+def synthesizeArgs (thmId : Origin) (bis : Array BinderInfo) (xs : Array Expr) : SimpM Bool := do
+  let skipAssignedInstances := tactic.skipAssignedInstances.get (← getOptions)
+  for x in xs, bi in bis do
     let type ← inferType x
+    -- We use the flag `tactic.skipAssignedInstances` for backward compatibility.
+    -- See comment below.
+    if !skipAssignedInstances && bi.isInstImplicit then
+      unless (← synthesizeInstance x type) do
+        return false
     /-
     We used to invoke `synthesizeInstance` for every instance implicit argument,
     to ensure the synthesized instance was definitionally equal to the one in
@@ -100,10 +107,10 @@ where
       trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}"
       return false
 
-private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
+private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
-      unless (← synthesizeArgs thm.origin xs) do
+      unless (← synthesizeArgs thm.origin bis xs) do
         return none
       let proof? ← if thm.rfl then
         pure none
@@ -154,25 +161,25 @@ def tryTheoremWithExtraArgs? (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat)
   withNewMCtxDepth do
     let val  ← thm.getValue
     let type ← inferType val
-    let (xs, _, type) ← forallMetaTelescopeReducing type
+    let (xs, bis, type) ← forallMetaTelescopeReducing type
     let type ← whnf (← instantiateMVars type)
     let lhs := type.appFn!.appArg!
-    tryTheoremCore lhs xs val type e thm numExtraArgs
+    tryTheoremCore lhs xs bis val type e thm numExtraArgs
 
 def tryTheorem? (e : Expr) (thm : SimpTheorem) : SimpM (Option Result) := do
   withNewMCtxDepth do
     let val  ← thm.getValue
     let type ← inferType val
-    let (xs, _, type) ← forallMetaTelescopeReducing type
+    let (xs, bis, type) ← forallMetaTelescopeReducing type
     let type ← whnf (← instantiateMVars type)
     let lhs := type.appFn!.appArg!
-    match (← tryTheoremCore lhs xs val type e thm 0) with
+    match (← tryTheoremCore lhs xs bis val type e thm 0) with
     | some result => return some result
     | none =>
       let lhsNumArgs := lhs.getAppNumArgs
       let eNumArgs   := e.getAppNumArgs
       if eNumArgs > lhsNumArgs then
-        tryTheoremCore lhs xs val type e thm (eNumArgs - lhsNumArgs)
+        tryTheoremCore lhs xs bis val type e thm (eNumArgs - lhsNumArgs)
       else
         return none
 

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

@@ -256,6 +256,7 @@ def simprocArrayCore (post : Bool) (ss : SimprocsArray) (e : Expr) : SimpM Step
 
 register_builtin_option simprocs : Bool := {
   defValue := true
+  group    := "backward compatibility"
   descr    := "Enable/disable `simproc`s (simplification procedures)."
 }
 

src/Lean/Meta/Tactic/Util.lean

@@ -178,4 +178,10 @@ def _root_.Lean.MVarId.isSubsingleton (g : MVarId) : MetaM Bool := do
   catch _ =>
     return false
 
+register_builtin_option tactic.skipAssignedInstances : Bool := {
+  defValue := true
+  group    := "backward compatibility"
+  descr    := "in the `rw` and `simp` tactics, if an instance implicit argument is assigned, do not try to synthesize instance."
+}
+
 end Lean.Meta

tests/lean/run/skipAssignedInstances.lean

@@ -0,0 +1,82 @@
+@[reducible]
+def swap {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y := fun y x => f x y
+
+theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y := ⟨swap, swap⟩
+
+@[simp]
+theorem nonempty_Prop {p : Prop} : Nonempty p ↔ p :=
+  Iff.intro (fun ⟨h⟩ ↦ h) fun h ↦ ⟨h⟩
+
+class IsEmpty (α : Sort _) : Prop where
+  protected false : α → False
+
+@[elab_as_elim]
+def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=
+  (IsEmpty.false a).elim
+
+@[elab_as_elim]
+protected def IsEmpty.elim {α : Sort u} (_ : IsEmpty α) {p : α → Sort _} (a : α) : p a :=
+  (IsEmpty.false a).elim
+
+@[simp]
+theorem not_nonempty_iff : ¬Nonempty α ↔ IsEmpty α :=
+  ⟨fun h ↦ ⟨fun x ↦ h ⟨x⟩⟩, fun h1 h2 ↦ h2.elim h1.elim⟩
+
+@[simp]
+theorem isEmpty_Prop {p : Prop} : IsEmpty p ↔ ¬p := by
+  simp only [← not_nonempty_iff, nonempty_Prop]
+
+class Preorder (α : Type u) extends LE α where
+  le_refl : ∀ a : α, a ≤ a
+
+theorem le_refl [Preorder α] : ∀ a : α, a ≤ a :=
+  Preorder.le_refl
+
+theorem le_of_eq [Preorder α] {a b : α} : a = b → a ≤ b := fun h => h ▸ le_refl a
+
+abbrev Eq.le := @le_of_eq
+
+@[simp] theorem le_of_subsingleton [Preorder α] [Subsingleton α] {a b : α} : a ≤ b := (Subsingleton.elim a b).le
+
+theorem iff_of_true' (ha : a) (hb : b) : a ↔ b := Iff.intro (fun _ => hb) (fun _ => ha)
+theorem iff_true_intro' (h : a) : a ↔ True := iff_of_true' h trivial
+
+@[simp]
+theorem IsEmpty.forall_iff [IsEmpty α] {p : α → Prop} : (∀ a, p a) ↔ True :=
+  iff_true_intro' isEmptyElim
+
+@[simp] theorem and_imp' : (a ∧ b → c) ↔ (a → b → c) := ⟨fun h ha hb => h ⟨ha, hb⟩, fun h ⟨ha, hb⟩ => h ha hb⟩
+@[simp] theorem not_and'' : ¬(a ∧ b) ↔ (a → ¬b) := and_imp'
+
+set_option tactic.skipAssignedInstances false in
+/--
+error: simp made no progress
+-/
+#guard_msgs in
+example [Preorder α] {a : α} {p : α → Prop} : ∀ (a_1 : α), a ≤ a_1 ∧ p a_1 → a ≤ a_1 := by
+  simp only [isEmpty_Prop, not_and'',  forall_swap, le_of_subsingleton, IsEmpty.forall_iff] -- should not loop
+
+theorem dec_and (p q : Prop) [Decidable (p ∧ q)] [Decidable p] [Decidable q] : decide (p ∧ q) = (p && q) := by
+  by_cases p <;> by_cases q <;> simp [*]
+
+theorem dec_not (p : Prop) [Decidable (¬p)] [Decidable p] : decide (¬p) = !p := by
+  by_cases p <;> simp [*]
+
+example [Decidable u] [Decidable v] : decide (u ∧ (v → False)) = (decide u && !decide v) := by
+  simp only [imp_false]
+  rw [dec_and]
+  rw [dec_not]
+
+set_option tactic.skipAssignedInstances false in
+/--
+error: tactic 'rewrite' failed, failed to assign synthesized instance
+u v : Prop
+inst✝¹ : Decidable u
+inst✝ : Decidable v
+⊢ decide (u ∧ ¬v) = (decide u && !decide v)
+-/
+#guard_msgs in
+example [Decidable u] [Decidable v] : decide (u ∧ (v → False)) = (decide u && !decide v) := by
+  simp only [imp_false]
+  rw [dec_and]
+  rw [dec_not]