feat: enable failIfUnchanged by default in simp

RELEASES.md

@@ -1,6 +1,14 @@
 Unreleased
 ---------
 
+* [`dsimp` / `simp` / `simp_all` now fail by default if they make no progress](https://github.com/leanprover/lean4/pull/2336).
+
+  This can be overriden with the `(config := { failIfUnchanged := false })` option.
+  This change was made to ease manual use of `simp` (with complicated goals it can be hard to tell if it was effective)
+  and to allow easier flow control in tactics internally using `simp`.
+  See the [summary discussion](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20fails.20if.20no.20progress/near/380153295)
+  on zulip for more details.
+
 * [`simp_all` now preserves order of hypotheses](https://github.com/leanprover/lean4/pull/2334).
 
   In order to support the `failIfUnchanged` configuration option for `dsimp` / `simp` / `simp_all`

doc/examples/bintree.lean

@@ -282,7 +282,7 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (h : k ≠ k') (v : β)
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    split <;> simp <;> split <;> simp
+    split <;> (try simp) <;> split <;> (try simp)
     have_eq k k'
     contradiction
   | node left key value right ihl ihr =>

src/Init/Data/Nat/Linear.lean

@@ -353,7 +353,7 @@ theorem Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
   | zero => assumption
   | succ fuel ih =>
     simp
-    split <;> simp at h <;> try assumption
+    split <;> try (simp at h; try assumption)
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
     · apply ih; simp [denote_eq] at h |-; assumption
@@ -387,7 +387,7 @@ theorem Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
   | zero => assumption
   | succ fuel ih =>
     simp at h
-    split at h <;> simp <;> try assumption
+    split at h <;> (try simp; assumption)
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
     · have ih := ih (h := h); simp [denote_eq] at ih ⊢; assumption
@@ -413,10 +413,9 @@ theorem Poly.of_denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
             rw [← Nat.add_assoc, ih, Nat.add_assoc]
 
 theorem Poly.denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (m₁, m₂)) : denote_eq ctx (cancel m₁ m₂) := by
-  simp; apply denote_eq_cancelAux; simp [h]
+  apply denote_eq_cancelAux; simp [h]
 
 theorem Poly.of_denote_eq_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_eq ctx (cancel m₁ m₂)) : denote_eq ctx (m₁, m₂) := by
-  simp at h
   have := Poly.of_denote_eq_cancelAux (h := h)
   simp at this
   assumption
@@ -432,7 +431,7 @@ theorem Poly.denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r
   | zero => assumption
   | succ fuel ih =>
     simp
-    split <;> simp at h <;> try assumption
+    split <;> try (simp at h; assumption)
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv]
     · apply ih; simp [denote_le] at h |-; assumption
@@ -466,7 +465,7 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
   | zero => assumption
   | succ fuel ih =>
     simp at h
-    split at h <;> simp <;> try assumption
+    split at h <;> try (simp; assumption)
     rename_i k₁ v₁ m₁ k₂ v₂ m₂
     by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv] at h
     · have ih := ih (h := h); simp [denote_le] at ih ⊢; assumption
@@ -494,10 +493,9 @@ theorem Poly.of_denote_le_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁
             exact this
 
 theorem Poly.denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (m₁, m₂)) : denote_le ctx (cancel m₁ m₂) := by
-  simp; apply denote_le_cancelAux; simp [h]
+  apply denote_le_cancelAux; simp [h]
 
 theorem Poly.of_denote_le_cancel {ctx : Context} {m₁ m₂ : Poly} (h : denote_le ctx (cancel m₁ m₂)) : denote_le ctx (m₁, m₂) := by
-  simp at h
   have := Poly.of_denote_le_cancelAux (h := h)
   simp at this
   assumption

src/Init/Meta.lean

@@ -1229,7 +1229,7 @@ structure Config where
   autoUnfold        : Bool := false
   /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will fail if they do not make progress. -/
-  failIfUnchanged   : Bool := false
+  failIfUnchanged   : Bool := true
   deriving Inhabited, BEq, Repr
 
 end DSimp
@@ -1260,7 +1260,7 @@ structure Config where
   dsimp             : Bool := true
   /-- If `failIfUnchanged := true`, then calls to `simp`, `dsimp`, or `simp_all`
   will fail if they do not make progress. -/
-  failIfUnchanged   : Bool := false
+  failIfUnchanged   : Bool := true
   deriving Inhabited, BEq, Repr
 
 -- Configuration object for `simp_all`

src/Init/WFTactics.lean

@@ -10,8 +10,7 @@ import Init.WF
 /-- Unfold definitions commonly used in well founded relation definitions.
 This is primarily intended for internal use in `decreasing_tactic`. -/
 macro "simp_wf" : tactic =>
-  `(tactic| simp [invImage, InvImage, Prod.lex, sizeOfWFRel,
-          measure, Nat.lt_wfRel, WellFoundedRelation.rel])
+  `(tactic| try simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel])
 
 /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case"
 reasoning after applying lexicographic order lemmas.
@@ -22,7 +21,7 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)
 -/
 syntax "decreasing_trivial" : tactic
 
-macro_rules | `(tactic| decreasing_trivial) => `(tactic| simp (config := { arith := true }); done)
+macro_rules | `(tactic| decreasing_trivial) => `(tactic| (simp (config := { arith := true, failIfUnchanged := false })); done)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| assumption)
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.sub_succ_lt_self; assumption) -- a - (i+1) < a - i if i < a
 macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt'; assumption) -- i-1 < i if j < i

tests/lean/973b.lean

@@ -7,5 +7,5 @@ theorem ex {x : Nat} {p : Nat → Prop} (h₁ : p x) (h₂ : q x p = x) : f x =
 
 set_option trace.Meta.Tactic.simp.discharge true
 theorem foo : f (f x) = x := by
-  simp
+  simp (config := { failIfUnchanged := false })
   sorry

tests/lean/dsimpZetaIssue.lean

@@ -1,5 +1,5 @@
 example : let x := 0; x + 5 = 5 := by
-  dsimp (config := { zeta := false })
+  dsimp (config := { zeta := false, failIfUnchanged := false })
   trace_state
   simp
 
@@ -12,7 +12,7 @@ example : let x := 0; x + y = y := by
   rw [Nat.zero_add]
 
 example : let x := 0; x + y = y := by
-  dsimp (config := { zeta := false })
+  dsimp (config := { zeta := false, failIfUnchanged := false })
   trace_state
   conv => zeta
   trace_state

tests/lean/eraseSimp.lean

@@ -12,7 +12,7 @@ section
 attribute [-simp] Nat.zero_add
 
 theorem ex2 {a b : Nat} (h₁ : a = b) : 0 + a = b := by
-  simp -- did not apply `Nat.zero_add`
+  fail_if_success simp -- did not apply `Nat.zero_add`
   rw [Nat.zero_add]
   assumption
 
@@ -24,6 +24,6 @@ theorem ex3 {a b : Nat} (h₁ : a = b) : 0 + a = b := by
   assumption
 
 theorem ex4 {a b : Nat} (h₁ : a = b) : 0 + a = b := by
-  simp [-Nat.zero_add]
+  fail_if_success simp [-Nat.zero_add]
   rw [Nat.zero_add]
   assumption

tests/lean/ppProofs.lean

@@ -2,7 +2,7 @@ set_option pp.analyze.trustSubst true
 set_option pp.proofs false
 example (h : α = β) : h ▸ (a : α) = (b : β) := _
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
-example (h : α = β) : id h ▸ (a : α) = (b : β) := by simp
+example (h : α = β) : id h ▸ (a : α) = (b : β) := by simp (config := { failIfUnchanged := false })
 set_option pp.proofs.withType false
 example (h : α = β) : id h ▸ (a : α) = (b : β) := _
 set_option pp.proofs true

tests/lean/ppProofs.lean.expected.out

@@ -12,7 +12,7 @@ b : β
 a : α
 h : α = β
 ⊢ (_ : α = β) ▸ a = b
-ppProofs.lean:5:50-5:57: error: unsolved goals
+ppProofs.lean:5:50-5:98: error: unsolved goals
 α β : Sort ?u
 b : β
 a : α

tests/lean/root.lean

@@ -87,12 +87,12 @@ example : isEven (x+1+1) = isEven x := by simp -- Ok
 
 end Ex
 
-example : isEven (x+1+1) = isEven x := by simp; done -- Error
+example : isEven (x+1+1) = isEven x := by simp (config := { failIfUnchanged := false }); done -- Error
 
 open Ex in
 example : isEven (x+1+1) = isEven x := by simp -- Ok
 
-example : isEven (x+1+1) = isEven x := by simp; done -- Error
+example : isEven (x+1+1) = isEven x := by simp (config := { failIfUnchanged := false }); done -- Error
 
 namespace Foo
 

tests/lean/root.lean.expected.out

@@ -8,9 +8,9 @@ root.lean:41:7-41:8: error: unknown identifier 'h'
 root.lean:43:7-43:8: error: unknown identifier 'f'
 Bla.f (x : Nat) : Nat
 prv (x : Nat) : Nat
-root.lean:90:48-90:52: error: unsolved goals
+root.lean:90:89-90:93: error: unsolved goals
 x : Nat
 ⊢ isEven (x + 1 + 1) = isEven x
-root.lean:95:48-95:52: error: unsolved goals
+root.lean:95:89-95:93: error: unsolved goals
 x : Nat
 ⊢ isEven (x + 1 + 1) = isEven x

tests/lean/run/1711.lean

@@ -20,7 +20,6 @@ theorem MulOneClass.ext {M : Type u} : ∀ ⦃m₁ m₂ : MulOneClass M⦄, m₁
       cases mul₂ with | mk mul₂ =>
         simp
         intro h
-        simp [toMul, Mul.mul] at h -- h : mul₁ = mul₂
         cases h
         have := (one_mul₂ one₁).symm.trans (mul_one₁ one₂) -- TODO: make sure we can apply after congr
         subst this

tests/lean/run/341.lean

@@ -102,7 +102,6 @@ namespace SetModel
            , tm := fun {γ} =>
                      (by
                        simp at fTy xTy; subst fTy xTy; simp at Actx Bctx; subst Actx Bctx
-                       simp [interpTyStep, cast] at *
                        exact (ftm xtm)
                      )
                }

tests/lean/run/387.lean

@@ -8,7 +8,8 @@ example (a : Nat) : p a a := by simp [foo a]
 example : p 0 0 := by simp [foo 0]
 example : p 0 0 := by simp [foo 0 0]
 example : p 0 0 := by
-  simp [foo 1] -- will not simplify
+  fail_if_success
+    simp [foo 1] -- will not simplify
   simp [foo 0]
 example : p 0 0 ∧ p 1 1 := by
   simp [foo 1]

tests/lean/run/constProp.lean

@@ -235,7 +235,7 @@ notation:60 "(" σ ", " s ")"  " ⇓ " σ':60 => Bigstep σ s σ'
 
 /- This proof can be automated using forward reasoning. -/
 theorem Bigstem.det (h₁ : (σ, s) ⇓ σ₁) (h₂ : (σ, s) ⇓ σ₂) : σ₁ = σ₂ := by
-  induction h₁ generalizing σ₂ <;> cases h₂ <;> simp_all
+  induction h₁ generalizing σ₂ <;> cases h₂ <;> try simp_all
   -- The rest of this proof should be automatic with congruence closure and a bit of forward reasoning
   case seq ih₁ ih₂ _ h₁ h₂ =>
     simp [ih₁ h₁] at ih₂
@@ -451,7 +451,7 @@ theorem State.erase_le (σ : State) : σ.erase x ≼ σ := by
   | [] => simp; apply le_refl
   | (y, v) :: σ =>
     simp
-    split <;> simp [*]
+    split <;> try simp [*]
     next => apply erase_le_cons; apply le_refl
     next => apply cons_le_cons; apply erase_le
 

tests/lean/run/declareConfigElabBug.lean

@@ -1,5 +1,5 @@
 set_option trace.Elab true
 theorem ex (h : a = b) : (fun x => x) a = b := by
-  simp (config := { beta := false })
+  simp (config := { beta := false, failIfUnchanged := false })
   trace_state
   simp (config := { beta := true }) [h]

tests/lean/run/discrTreeSimp.lean

@@ -8,7 +8,7 @@ theorem map_map (f : α → β) (g : β → γ) (xs : List α) : (xs.map f |>.ma
   sorry
 
 theorem ex1 (f : Nat → Nat) (xs : List Nat) : (xs.map f |>.map f) = xs.map (f ∘ f) := by
-  simp
+  fail_if_success simp
   simp [map_map]
   done
 

tests/lean/run/eqnsAtSimp2.lean

@@ -29,11 +29,11 @@ theorem f_succ (x : Nat) : f (x+1) = f x * 2 := by
   simp
 
 theorem f_succ₂ (x : Nat) : f (x+1) = f x * 2 := by
-  simp [-f]
+  fail_if_success simp [-f]
   simp
 
 attribute [-simp] f
 
 theorem f_succ₃ (x : Nat) : f (x+1) = f x * 2 := by
-  simp
+  fail_if_success simp
   simp [f]

tests/lean/run/exfalsoBug.lean

@@ -72,15 +72,15 @@ theorem f_eq (n : Nat) :
   split
   next r h =>
     revert h
-    split <;> simp [f']
+    split <;> try simp [f']
     next => intro h; subst h; simp
     next hne =>
       cases n <;> simp [f']
       next => contradiction
       next n _ =>
        have : Nat.succ n - 1 = n := rfl
        rw [this]
-       split <;> simp
+       split <;> try simp
        next r hrn h₁ =>
          split <;> simp
          next => intro he; subst he; simp [*]

tests/lean/run/openInScopeBug.lean

@@ -9,17 +9,22 @@ namespace Foo
 end Foo
 
 theorem ex1 : f (g (g (g x))) = x := by
-  simp -- does not use ax1 and ax2
+  fail_if_success simp -- does not use ax1 and ax2
   simp [Foo.ax1, Foo.ax2]
 
 theorem ex2 : f (g (g (g x))) = x :=
-  have h₁ : f (g (g (g x))) = f (g x) := by simp; /- try again with `Foo` scoped lemmas -/ open Foo in simp
-  have h₂ : f (g x) = x               := by simp; open Foo in simp
+  have h₁ : f (g (g (g x))) = f (g x) := by
+    fail_if_success simp
+    /- try again with `Foo` scoped lemmas -/
+    open Foo in simp
+  have h₂ : f (g x) = x               := by
+    fail_if_success simp
+    open Foo in simp
   Eq.trans h₁ h₂
   -- open Foo in simp -- works
 
 theorem ex3 : f (g (g (g x))) = x := by
-  simp
+  fail_if_success simp
   simp [Foo.ax1, Foo.ax2]
 
 open Foo in
@@ -28,5 +33,7 @@ theorem ex4 : f (g (g (g x))) = x := by
 
 theorem ex5 : f (g (g (g x))) = x ∧ f (g x) = x := by
   apply And.intro
-  { simp; open Foo in simp }
-  { simp; open Foo in simp }
+  { fail_if_success simp
+    open Foo in simp }
+  { fail_if_success simp
+    open Foo in simp }

tests/lean/run/simp4.lean

@@ -49,7 +49,7 @@ theorem ex8 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
   simp (config := { contextual := true })
 
 theorem ex9 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
-  simp
+  fail_if_success simp
   intro h₁ h₂
   simp [h₁] at h₂
   simp [h₂]

tests/lean/run/simp6.lean

@@ -21,7 +21,7 @@ theorem ex6 : (if "hello" = "world" then 1 else 2) = 2 :=
 #print ex6
 
 theorem ex7 : (if "hello" = "world" then 1 else 2) = 2 := by
-  simp (config := { decide := false })
+  fail_if_success simp (config := { decide := false })
   simp
 
 theorem ex8 : (10 + 2000 = 20) = False :=

tests/lean/run/simpDischargeLoop.lean

@@ -40,6 +40,6 @@ theorem double.inj'' : double n = double m → n = m := by
       apply ih h
 
 theorem double.inj''' : double n = double m → n = m := by
-  simp (config := { maxDischargeDepth := 2 })
-  simp (config := { maxSteps := 2000000 })
+  fail_if_success simp (config := { maxDischargeDepth := 2 })
+  fail_if_success simp (config := { maxSteps := 2000000 })
   admit

tests/lean/run/simpStar.lean

@@ -2,7 +2,7 @@ opaque f (x y : Nat) : Nat
 opaque g (x : Nat) : Nat
 
 theorem ex1 (x : Nat) (h₁ : f x x = g x) (h₂ : g x = x) : f x (f x x) = x := by
-  simp
+  fail_if_success simp
   simp [*]
 
 theorem ex2 (x : Nat) (h₁ : f x x = g x) (h₂ : g x = x) : f x (f x x) = x := by

tests/lean/run/simp_all.lean

@@ -28,6 +28,6 @@ through the `simp_all`.
 -/
 example : ∀ {A : Prop} (_ : A) (_ : W), W := by
   intros
-  simp_all
+  simp_all (config := { failIfUnchanged := false })
   rename_i w
   exact w

tests/lean/simpZetaFalse.lean

@@ -16,7 +16,7 @@ theorem ex2 (x z : Nat) (h : f (f x) = x) (h' : z = x) : (let y := f (f x); y) =
 #print ex2 -- uses let_val_congr
 
 theorem ex3 (x z : Nat) : (let α := Nat; (fun x : α => 0 + x)) = id := by
-  simp (config := { zeta := false })
+  simp (config := { zeta := false, failIfUnchanged := false })
   trace_state -- should not simplify let body since `fun α : Nat => fun x : α => 0 + x` is not type correct
   simp [id]
 

tests/lean/simp_dsimp.lean

@@ -7,6 +7,6 @@ example (x : Nat) (a : A (x + 0)) : f (x + 0) a = x := by
   sorry
 
 example (x : Nat) (a : A (x + 0)) : f (x + 0) a = x := by
-  simp (config := { dsimp := false })
+  simp (config := { dsimp := false, failIfUnchanged := false })
   trace_state -- ⊢ f (x + 0) a = x
   sorry