From d1d6e764c3031bbe8ded95ade53d0bf60b17241a Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Fri, 6 Sep 2024 05:18:57 +0200
Subject: [PATCH] better handling of free variables in fun_trans

---
 SciLean/Tactic/FunTrans/Core.lean | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/SciLean/Tactic/FunTrans/Core.lean b/SciLean/Tactic/FunTrans/Core.lean
index e7f60b88..dd19b6ff 100644
--- a/SciLean/Tactic/FunTrans/Core.lean
+++ b/SciLean/Tactic/FunTrans/Core.lean
@@ -472,6 +472,14 @@ def fvarAppCase (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.Functi
     if let .some r ← tryTheorems funTransDecl e fData thms then
       return r
 
+    -- unfold let fvar and add new let fvar with its transformation
+    if let .some f ← fData.unfoldHeadFVar? then
+      trace[Meta.Tactic.fun_trans] "unfolding local function {Expr.fvar fvarId} ==> {f}"
+      let r' ← Simp.simp (e.setArg funTransDecl.funArgId f)
+      let fname' := (← fvarId.getUserName).appendAfter "'"
+      let e' := Expr.letE fname' (← inferType r'.expr) r'.expr (.bvar 0) false
+      return .some { expr := e', proof? := r'.proof? }
+
     if let .some r ← applyMorTheorems funTransDecl e fData then
       return r
 
@@ -567,7 +575,7 @@ partial def funTrans (e : Expr) : SimpM Simp.Step := do
     else
       return .continue
 
-  match ← FunProp.getFunctionData? f FunProp.defaultUnfoldPred {zeta:=false} with
+  match ← FunProp.getFunctionData? f FunProp.defaultUnfoldPred {zeta:=false,zetaDelta:=false} with
   | .letE f =>
     trace[Meta.Tactic.fun_trans.step] "let case on {← ppExpr f}"
     let e := e.setArg funTransDecl.funArgId f -- update e with reduced f