diff --git a/RELEASES.md b/RELEASES.md index fb17761550..adf080daa3 100644 --- a/RELEASES.md +++ b/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. diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index bc31d1f969..5abb05ca01 100644 --- a/src/Init/Meta.lean +++ b/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` diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index fc6abfd771..5fdc9310d2 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean index b342565df8..915f0c5d05 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean +++ b/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 diff --git a/tests/lean/run/constProp.lean b/tests/lean/run/constProp.lean index 06181a8cca..e9f9c696b4 100644 --- a/tests/lean/run/constProp.lean +++ b/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 => diff --git a/tests/lean/run/simp_all.lean b/tests/lean/run/simp_all.lean index 1ebc79d4a7..7e5b643498 100644 --- a/tests/lean/run/simp_all.lean +++ b/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 diff --git a/tests/lean/run/simp_failIfUnchanged.lean b/tests/lean/run/simp_failIfUnchanged.lean new file mode 100644 index 0000000000..995111a73b --- /dev/null +++ b/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 + +