feat: add failIfUnchanged flag to simp

RELEASES.md

@@ -1,6 +1,20 @@
 Unreleased
 ---------
 
+* [`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`
+  the way `simp_all` replaces hypotheses has changed.
+  In particular it is now more likely to preserve the order of hypotheses.
+  See [`simp_all` reorders hypotheses unnecessarily](https://github.com/leanprover/lean4/pull/2334).
+  (Previously all non-dependent propositional hypotheses were reverted and reintroduced.
+  Now only such hypotheses which were changed, or which come after a changed hypothesis,
+  are reverted and reintroduced.
+  This has the effect of preserving the ordering amongst the non-dependent propositional hypotheses,
+  but now any dependent or non-propositional hypotheses retain their position amongst the unchanged
+  non-dependent propositional hypotheses.)
+  This may affect proofs that use `rename_i`, `case ... =>`, or `next ... =>`.
+
 * [New `have this` implementation](https://github.com/leanprover/lean4/pull/2247).
 
   `this` is now a regular identifier again that is implicitly introduced by anonymous `have :=` for the remainder of the tactic block. It used to be a keyword that was visible in all scopes and led to unexpected behavior when explicitly used as a binder name.

src/Init/Meta.lean

@@ -1227,6 +1227,9 @@ structure Config where
   proj              : Bool := true
   decide            : Bool := false
   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
   deriving Inhabited, BEq, Repr
 
 end DSimp
@@ -1255,6 +1258,9 @@ structure Config where
     `simp` to visit them. If `dsimp := false`, then argument is not visited.
   -/
   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
   deriving Inhabited, BEq, Repr
 
 -- Configuration object for `simp_all`

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

@@ -969,7 +969,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
     (usedSimps : UsedSimps := {}) : MetaM (Option (Array FVarId × MVarId) × UsedSimps) := do
   mvarId.withContext do
     mvarId.checkNotAssigned `simp
-    let mut mvarId := mvarId
+    let mut mvarIdNew := mvarId
     let mut toAssert := #[]
     let mut replaced := #[]
     let mut usedSimps := usedSimps
@@ -980,24 +980,27 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
       let (r, usedSimps') ← simp type ctx discharge? usedSimps
       usedSimps := usedSimps'
       match r.proof? with
-      | some _ => match (← applySimpResultToProp mvarId (mkFVar fvarId) type r) with
+      | some _ => match (← applySimpResultToProp mvarIdNew (mkFVar fvarId) type r) with
         | none => return (none, usedSimps)
         | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
       | none =>
         if r.expr.consumeMData.isConstOf ``False then
-          mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId))
+          mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
           return (none, usedSimps)
         -- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
         -- Reason: it introduces a `mkExpectedTypeHint`
-        mvarId ← mvarId.replaceLocalDeclDefEq fvarId r.expr
+        mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId r.expr
         replaced := replaced.push fvarId
     if simplifyTarget then
-      match (← simpTarget mvarId ctx discharge?) with
+      match (← simpTarget mvarIdNew ctx discharge?) with
       | (none, usedSimps') => return (none, usedSimps')
-      | (some mvarIdNew, usedSimps') => mvarId := mvarIdNew; usedSimps := usedSimps'
-    let (fvarIdsNew, mvarIdNew) ← mvarId.assertHypotheses toAssert
+      | (some mvarIdNew', usedSimps') => mvarIdNew := mvarIdNew'; usedSimps := usedSimps'
+    let (fvarIdsNew, mvarIdNew') ← mvarIdNew.assertHypotheses toAssert
+    mvarIdNew := mvarIdNew'
     let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
-    let mvarIdNew ← mvarIdNew.tryClearMany toClear
+    mvarIdNew ← mvarIdNew.tryClearMany toClear
+    if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
+      throwError "simp made no progress"
     return (some (fvarIdsNew, mvarIdNew), usedSimps)
 
 def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
@@ -1020,31 +1023,33 @@ def dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simplifyTarget : Bool := t
     (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
    mvarId.withContext do
     mvarId.checkNotAssigned `simp
-    let mut mvarId := mvarId
+    let mut mvarIdNew := mvarId
     let mut usedSimps : UsedSimps := usedSimps
     for fvarId in fvarIdsToSimp do
       let type ← instantiateMVars (← fvarId.getType)
       let (typeNew, usedSimps') ← dsimp type ctx
       usedSimps := usedSimps'
       if typeNew.consumeMData.isConstOf ``False then
-        mvarId.assign (← mkFalseElim (← mvarId.getType) (mkFVar fvarId))
+        mvarIdNew.assign (← mkFalseElim (← mvarIdNew.getType) (mkFVar fvarId))
         return (none, usedSimps)
       if typeNew != type then
-        mvarId ← mvarId.replaceLocalDeclDefEq fvarId typeNew
+        mvarIdNew ← mvarIdNew.replaceLocalDeclDefEq fvarId typeNew
     if simplifyTarget then
-      let target ← mvarId.getType
+      let target ← mvarIdNew.getType
       let (targetNew, usedSimps') ← dsimp target ctx usedSimps
       usedSimps := usedSimps'
       if targetNew.consumeMData.isConstOf ``True then
-        mvarId.assign (mkConst ``True.intro)
+        mvarIdNew.assign (mkConst ``True.intro)
         return (none, usedSimps)
       if let some (_, lhs, rhs) := targetNew.eq? then
         if (← withReducible <| isDefEq lhs rhs) then
-          mvarId.assign (← mkEqRefl lhs)
+          mvarIdNew.assign (← mkEqRefl lhs)
           return (none, usedSimps)
       if target != targetNew then
-        mvarId ← mvarId.replaceTargetDefEq targetNew
+        mvarIdNew ← mvarIdNew.replaceTargetDefEq targetNew
       pure () -- FIXME: bug in do notation if this is removed?
-    return (some mvarId, usedSimps)
+    if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
+      throwError "dsimp made no progress"
+    return (some mvarIdNew, usedSimps)
 
 end Lean.Meta

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

@@ -17,6 +17,7 @@ structure Entry where
   fvarId   : FVarId -- original fvarId
   userName : Name
   id       : Origin -- id of the theorem at `SimpTheorems`
+  origType : Expr
   type     : Expr
   proof    : Expr
   deriving Inhabited
@@ -42,7 +43,8 @@ private def initEntries : M Unit := do
       modify fun s => { s with ctx.simpTheorems := simpThms }
       if hsNonDeps.contains h then
         -- We only simplify nondependent hypotheses
-        let entry : Entry := { fvarId := h, userName := localDecl.userName, id := .fvar h, type := (← instantiateMVars localDecl.type), proof := proof }
+        let type ← instantiateMVars localDecl.type
+        let entry : Entry := { fvarId := h, userName := localDecl.userName, id := .fvar h, origType := type, type, proof }
         modify fun s => { s with entries := s.entries.push entry }
 
 private abbrev getSimpTheorems : M SimpTheoremsArray :=
@@ -118,17 +120,32 @@ def main : M (Option MVarId) := do
     return none -- close the goal
   else
     let mvarId := (← get).mvarId
-    let entries := (← get).entries
-    let (_, mvarId) ← mvarId.assertHypotheses <| entries.filterMap fun e =>
-      -- Do not assert `True` hypotheses
-      if e.type.consumeMData.isConstOf ``True then none else some { userName := e.userName, type := e.type, value := e.proof }
-    mvarId.tryClearMany (entries.map fun e => e.fvarId)
+    -- Prior to #2334, the logic here was to re-assert all hypotheses and call `tryClearMany` on them all.
+    -- This had the effect that the order of hypotheses was sometimes modified, whether or not any where simplified.
+    -- Now we only re-assert the first modified hypothesis,
+    -- along with all subsequent hypotheses, so as to preserve the order of hypotheses.
+    let mut toAssert := #[]
+    let mut toClear := #[]
+    let mut modified := false
+    for e in (← get).entries do
+      if e.type.consumeMData.isConstOf ``True then
+        -- Do not assert `True` hypotheses
+        toClear := toClear.push e.fvarId
+      else if modified || e.type != e.origType then
+        toClear := toClear.push e.fvarId
+        toAssert := toAssert.push { userName := e.userName, type := e.type, value := e.proof }
+        modified := true
+    let (_, mvarId) ← mvarId.assertHypotheses toAssert
+    mvarId.tryClearMany toClear
 
 end SimpAll
 
 def simpAll (mvarId : MVarId) (ctx : Simp.Context) (usedSimps : UsedSimps := {}) : MetaM (Option MVarId × UsedSimps) := do
   mvarId.withContext do
     let (r, s) ← SimpAll.main.run { mvarId, ctx, usedSimps }
+    if let .some mvarIdNew := r then
+      if ctx.config.failIfUnchanged && mvarId == mvarIdNew then
+        throwError "simp_all made no progress"
     return (r, s.usedSimps)
 
 end Lean.Meta

tests/lean/run/constProp.lean

@@ -237,7 +237,7 @@ notation:60 "(" σ ", " s ")"  " ⇓ " σ':60 => Bigstep σ s σ'
 theorem Bigstem.det (h₁ : (σ, s) ⇓ σ₁) (h₂ : (σ, s) ⇓ σ₂) : σ₁ = σ₂ := by
   induction h₁ generalizing σ₂ <;> cases h₂ <;> 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₂ =>
+  case seq ih₁ ih₂ _ h₁ h₂ =>
     simp [ih₁ h₁] at ih₂
     simp [ih₂ h₂]
   case ifTrue ih h =>

tests/lean/run/simp_all.lean

@@ -17,3 +17,17 @@ theorem ex4 (h₁ : a = f a) (h₂ : b + 0 = 0) : f b = 0 := by
 
 theorem ex5 (h₁ : a = f a) (h₂ : b + 0 = 0) : f (b + a) = a := by
   simp_all [-h₁, f]
+
+/-!
+Prior to lean4#2334, `simp_all` would unnecessarily reorder hypotheses,
+even when it did not do any simplification.
+See lean4#2402.
+
+This test verifies that the last hypothesis stays in the last position
+through the `simp_all`.
+-/
+example : ∀ {A : Prop} (_ : A) (_ : W), W := by
+  intros
+  simp_all
+  rename_i w
+  exact w

tests/lean/run/simp_failIfUnchanged.lean

@@ -0,0 +1,30 @@
+example (h : False) : False := by
+  fail_if_success
+    simp (config := { failIfUnchanged := true })
+  cases h
+
+example (h : (a :: [b]).length = 3) : False := by
+  fail_if_success
+    simp (config := { failIfUnchanged := true }) only at h
+  simp (config := { failIfUnchanged := false }) only at h
+  simp (config := { failIfUnchanged := true }) at h
+
+example (h : False) : False := by
+  fail_if_success
+    dsimp (config := { failIfUnchanged := true })
+  cases h
+
+example (_h : 37 = 37) (w : Nonempty False) : False ∨ False := by
+  -- removes `_h` and simplifies the goal
+  simp_all (config := { failIfUnchanged := true })
+  -- Now should fail, because it can't do anything.
+  fail_if_success
+    simp_all (config := { failIfUnchanged := true })
+  cases w with
+  | intro w => cases w
+
+example (h : False) : 7 = 8 := by
+  simp (config := { failIfUnchanged := true })
+  cases h
+
+