From 611b1746896bbadf459c00cc218fa31cf51b4e08 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 6 Mar 2024 16:11:31 -0800
Subject: [PATCH] fix: `ofScientific` at `simp` (#3628)

closes #2159
---
 src/Lean/Meta/Tactic/Simp/Main.lean | 34 +++++++++++++++++++----------
 tests/lean/run/2159.lean            | 13 +++++++++++
 2 files changed, 36 insertions(+), 11 deletions(-)
 create mode 100644 tests/lean/run/2159.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index ecd1ca67ae..6cf6cb72e5 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -50,6 +50,10 @@ def foldRawNatLit (e : Expr) : SimpM Expr := do
       return toExpr n
   | none   => return e
 
+/-- Return true if `e` is of the form `ofScientific n b m` where `n` and `m` are kernel Nat literals. -/
+def isOfScientificLit (e : Expr) : Bool :=
+  e.isAppOfArity ``OfScientific.ofScientific 5 && (e.getArg! 4).isRawNatLit && (e.getArg! 2).isRawNatLit
+
 private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
   matchConst e.getAppFn (fun _ => pure none) fun cinfo _ => do
     match (← getProjectionFnInfo? cinfo.name) with
@@ -410,27 +414,35 @@ private def dsimpReduce : DSimproc := fun e => do
     eNew ← reduceFVar (← getConfig) (← getSimpTheorems) eNew
   if eNew != e then return .visit eNew else return .done e
 
-/--
-Auliliary `dsimproc` for not visiting `OfNat.ofNat` application subterms.
-This is the `dsimp` equivalent of the approach used at `visitApp`.
-Recall that we fold orphan raw Nat literals.
--/
-private def doNotVisitOfNat : DSimproc := fun e => do
-  if isOfNatNatLit e then
-    if (← readThe Simp.Context).isDeclToUnfold ``OfNat.ofNat then
+/-- Helper `dsimproc` for `doNotVisitOfNat` and `doNotVisitOfScientific` -/
+private def doNotVisit (pred : Expr → Bool) (declName : Name) : DSimproc := fun e => do
+  if pred e then
+    if (← readThe Simp.Context).isDeclToUnfold declName then
       return .continue e
     else
       return .done e
   else
     return .continue e
 
+/--
+Auliliary `dsimproc` for not visiting `OfNat.ofNat` application subterms.
+This is the `dsimp` equivalent of the approach used at `visitApp`.
+Recall that we fold orphan raw Nat literals.
+-/
+private def doNotVisitOfNat : DSimproc := doNotVisit isOfNatNatLit ``OfNat.ofNat
+
+/--
+Auliliary `dsimproc` for not visiting `OfScientific.ofScientific` application subterms.
+-/
+private def doNotVisitOfScientific : DSimproc := doNotVisit isOfScientificLit ``OfScientific.ofScientific
+
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let cfg ← getConfig
   unless cfg.dsimp do
     return e
   let m ← getMethods
-  let pre := m.dpre >> doNotVisitOfNat
+  let pre := m.dpre >> doNotVisitOfNat >> doNotVisitOfScientific
   let post := m.dpost >> dsimpReduce
   transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
@@ -550,8 +562,8 @@ def congr (e : Expr) : SimpM Result := do
     congrDefault e
 
 def simpApp (e : Expr) : SimpM Result := do
-  if isOfNatNatLit e then
-    -- Recall that we expand "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
+  if isOfNatNatLit e || isOfScientificLit e then
+    -- Recall that we fold "orphan" kernel Nat literals `n` into `OfNat.ofNat n`
     return { expr := e }
   else
     congr e
diff --git a/tests/lean/run/2159.lean b/tests/lean/run/2159.lean
new file mode 100644
index 0000000000..ee43bd5afd
--- /dev/null
+++ b/tests/lean/run/2159.lean
@@ -0,0 +1,13 @@
+/--
+warning: declaration uses 'sorry'
+---
+info: ⊢ 1.2 < 2
+---
+info: ⊢ 1.2 < 2
+-/
+#guard_msgs in
+example : 1.2 < 2 := by
+  trace_state
+  fail_if_success simp only
+  trace_state
+  sorry