From 2babb7fae5f3cd0ab17684d07e59e9c35c4b601e Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Wed, 7 Aug 2024 17:09:42 -0400
Subject: [PATCH] improve message when missing lambda theorems for fun_trans

---
 SciLean/Tactic/FunTrans/Core.lean     | 53 +++++++++++++++++----------
 SciLean/Tactic/FunTrans/Theorems.lean |  4 +-
 2 files changed, 35 insertions(+), 22 deletions(-)

diff --git a/SciLean/Tactic/FunTrans/Core.lean b/SciLean/Tactic/FunTrans/Core.lean
index 9e141988..e5b4bd8f 100644
--- a/SciLean/Tactic/FunTrans/Core.lean
+++ b/SciLean/Tactic/FunTrans/Core.lean
@@ -165,9 +165,11 @@ def tryTheorem? (e : Expr) (thmOrigin : FunProp.Origin) : SimpM (Option Simp.Res
 def applyIdRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do
   trace[Meta.Tactic.fun_trans.step] "id case"
 
-  let .some thms ← getLambdaTheorems funTransDecl.funTransName .id e.getAppNumArgs
-    | trace[Meta.Tactic.fun_trans] "missing identity rule to transform `{← ppExpr e}`"
-      return none
+  let thms ← getLambdaTheorems funTransDecl.funTransName .id e.getAppNumArgs
+
+  if thms.size = 0 then
+    trace[Meta.Tactic.fun_trans] "missing identity rule to transform `{← ppExpr e}`"
+    return none
 
   for thm in thms do
     if let .some r ← tryTheorem? e (.decl thm.thmName) then
@@ -176,9 +178,11 @@ def applyIdRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Re
   return none
 
 def applyConstRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do
-  let .some thms ← getLambdaTheorems funTransDecl.funTransName .const e.getAppNumArgs
-    | trace[Meta.Tactic.fun_trans] "missing const rule to transform `{← ppExpr e}`"
-      return none
+  let thms ← getLambdaTheorems funTransDecl.funTransName .const e.getAppNumArgs
+
+  if thms.size = 0 then
+    trace[Meta.Tactic.fun_trans] "missing const rule to transform `{← ppExpr e}`"
+    return none
 
   for thm in thms do
     if let .some r ← tryTheorem? e (.decl thm.thmName) then
@@ -187,9 +191,11 @@ def applyConstRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp
   return none
 
 def applyCompRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Simp.Result) := do
-  let .some thms ← getLambdaTheorems funTransDecl.funTransName .comp e.getAppNumArgs
-    | trace[Meta.Tactic.fun_trans] "missing comp rule to transform `{← ppExpr e}`"
-      return none
+  let thms ← getLambdaTheorems funTransDecl.funTransName .comp e.getAppNumArgs
+
+  if thms.size = 0 then
+    trace[Meta.Tactic.fun_trans] "missing comp rule to transform `{← ppExpr e}`"
+    return none
 
   for thm in thms do
     let .comp id_f id_g := thm.thmArgs | continue
@@ -200,9 +206,11 @@ def applyCompRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option S
   return none
 
 def applyLetRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Simp.Result) := do
-  let .some thms ← getLambdaTheorems funTransDecl.funTransName .letE e.getAppNumArgs
-    | trace[Meta.Tactic.fun_trans] "missing let rule to transform `{← ppExpr e}`"
-      return none
+  let thms ← getLambdaTheorems funTransDecl.funTransName .letE e.getAppNumArgs
+
+  if thms.size = 0 then
+    trace[Meta.Tactic.fun_trans] "missing let rule to transform `{← ppExpr e}`"
+    return none
 
   for thm in thms do
     let .letE id_f id_g := thm.thmArgs | continue
@@ -213,10 +221,13 @@ def applyLetRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Si
   return none
 
 def applyApplyRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do
-  let .some thms ← getLambdaTheorems funTransDecl.funTransName .apply e.getAppNumArgs
-    | trace[Meta.Tactic.fun_trans]
-        "missing projection rule to transform `{← ppExpr e}`"
-      return none
+  let thms ← getLambdaTheorems funTransDecl.funTransName .apply e.getAppNumArgs
+
+  if thms.size = 0 then
+    trace[Meta.Tactic.fun_trans]
+      "missing projection rule to transform `{← ppExpr e}`"
+    return none
+
   for thm in thms do
     if let .some r ← tryTheorem? e (.decl thm.thmName) then
       return r
@@ -224,9 +235,11 @@ def applyApplyRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp
   return none
 
 def applyPiRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do
-  let .some thms ← getLambdaTheorems funTransDecl.funTransName .pi e.getAppNumArgs
-    | trace[Meta.Tactic.fun_trans] "missing pi rule to transform `{← ppExpr e}`"
-      return none
+  let thms ← getLambdaTheorems funTransDecl.funTransName .pi e.getAppNumArgs
+
+  if thms.size = 0 then
+    trace[Meta.Tactic.fun_trans] "missing pi rule to transform `{← ppExpr e}`"
+    return none
 
   for thm in thms do
     if let .some r ← tryTheorem? e (.decl thm.thmName) then
@@ -364,7 +377,7 @@ def tryTheorems (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.Functi
               return r
           | .some (.some (f,g)) =>
             trace[Meta.Tactic.fun_trans.step]
-              s!"decomposing to later use {←ppOrigin' thm.thmOrigin}"
+              s!"decomposing to later use {←ppOrigin' thm.thmOrigin}, {← ppExpr (←fData.toExpr)} = {← ppExpr f}∘{← ppExpr g}"
             if let .some r ← applyCompRule funTransDecl e f g then
               return r
           | _ => continue
diff --git a/SciLean/Tactic/FunTrans/Theorems.lean b/SciLean/Tactic/FunTrans/Theorems.lean
index 92e4b0b3..b5b95a1c 100644
--- a/SciLean/Tactic/FunTrans/Theorems.lean
+++ b/SciLean/Tactic/FunTrans/Theorems.lean
@@ -153,9 +153,9 @@ deriv (fun x' => 1/(1-x')) x
 we prefer the version `deriv (fun x' => f (g x')) x` over `deriv (fun x' => f (g x'))` as the former
 uses `DifferntiableAt` insed of `Differentiable` as preconditions. -/
 def getLambdaTheorems (funTransName : Name) (type : LambdaTheoremType) (nargs : Option Nat):
-    CoreM (Option (Array LambdaTheorem)) := do
+    CoreM (Array LambdaTheorem) := do
   let .some thms := (lambdaTheoremsExt.getState (← getEnv)).theorems.find? (funTransName,type)
-    | return none
+    | return #[]
 
   match nargs with
   | none => return thms