From a4797fb22a4ec7311ec986f2079947ff3e6cfce7 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Tue, 31 Oct 2023 12:48:42 -0400
Subject: [PATCH] fix to lsimp, call reduce instead of full dsimp in post pass,
 fixes #26

---
 .../FunctionPropositions/HasAdjDiffAt.lean    |  2 +-
 SciLean/Tactic/LSimp2/Main.lean               | 57 +++++++++----------
 test/issues/26.lean                           | 13 +----
 3 files changed, 32 insertions(+), 40 deletions(-)

diff --git a/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean b/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean
index 2905e009..16ccb432 100644
--- a/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean
+++ b/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean
@@ -322,7 +322,7 @@ theorem HSMul.hSMul.arg_a1.HasAdjDiffAt_rule
   : HasAdjDiffAt K (fun x => c • g x) x :=
 by 
   have ⟨_,_⟩ := hg
-  constructor; fprop; ftrans; simp; fprop
+  constructor; fprop; ftrans; fprop
 
 
 
diff --git a/SciLean/Tactic/LSimp2/Main.lean b/SciLean/Tactic/LSimp2/Main.lean
index 8b842251..fa236880 100644
--- a/SciLean/Tactic/LSimp2/Main.lean
+++ b/SciLean/Tactic/LSimp2/Main.lean
@@ -249,34 +249,33 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   | none => return e
 
 private partial def dsimp (e : Expr) : M Expr := do
-  return e
-  -- let cfg ← Simp.getConfig
-  -- withTraceNode `ldsimp (fun _ => pure s!"ldsimp {cfg.dsimp}") do
-  -- unless cfg.dsimp do
-  --   return e
-  -- let pre (e : Expr) : M TransformStep := do
-  --   withTraceNode `ldsimp (fun _ => pure "ldsimp pre") do
-  --   if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
-  --     if r.expr != e then
-  --       return .visit r.expr
-  --   return .continue
-  -- let post (e : Expr) : M TransformStep := do
-  --   withTraceNode `ldsimp (fun _ => pure "ldsimp post") do
-  --   -- lsimp modification               
-  --   -- remove unsued let bindings
-  --   let e := 
-  --     if e.isLet && ¬e.letBody!.hasLooseBVars then
-  --       e.letBody!
-  --     else
-  --       e
-  --   if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
-  --     if r.expr != e then
-  --       return .visit r.expr
-  --   let mut eNew ← reduce e
-  --   if cfg.zeta && eNew.isFVar then
-  --     eNew ← reduceFVar cfg eNew
-  --   if eNew != e then return .visit eNew else return .done e
-  -- transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
+  let cfg ← Simp.getConfig
+  withTraceNode `ldsimp (fun _ => pure s!"ldsimp {cfg.dsimp}") do
+  unless cfg.dsimp do
+    return e
+  let pre (e : Expr) : M TransformStep := do
+    withTraceNode `ldsimp (fun _ => pure "ldsimp pre") do
+    if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    return .continue
+  let post (e : Expr) : M TransformStep := do
+    withTraceNode `ldsimp (fun _ => pure "ldsimp post") do
+    -- lsimp modification               
+    -- remove unsued let bindings
+    let e := 
+      if e.isLet && ¬e.letBody!.hasLooseBVars then
+        e.letBody!
+      else
+        e
+    if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
+      if r.expr != e then
+        return .visit r.expr
+    let mut eNew ← reduce e
+    if cfg.zeta && eNew.isFVar then
+      eNew ← reduceFVar cfg eNew
+    if eNew != e then return .visit eNew else return .done e
+  transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
 instance : Inhabited (M α) where
   default := fun _ _ _ => default
@@ -468,7 +467,7 @@ where
           let r ← mkEqTrans r r'
           -- lsimp modification
           -- clean up expressions after rewrites
-          let r ← mkEqTrans r { expr := ← dsimp r.expr }
+          let r ← mkEqTrans r { expr := ← reduce r.expr }
           if cfg.singlePass || init == r.expr then
             cacheResult cfg r
           else
diff --git a/test/issues/26.lean b/test/issues/26.lean
index b1f28b27..8fffd3eb 100644
--- a/test/issues/26.lean
+++ b/test/issues/26.lean
@@ -1,22 +1,15 @@
 import SciLean
 
-
 variable (a : Nat)
 
-/- expected
+/--
 info: let x := a + a;
 a + (a + x) : ℕ
 -/
-
-/--
-info: a +
-  let x := a + a;
-  a + x : ℕ
--/
 #guard_msgs in
 #check 
-  (a + 
-    (a + 
+  (a +
+    (a +
     let x := a + a
     x))
   rewrite_by