gadget function fpropParam which marks difficult parameters

right now we discharge these parameters with sorry

SciLean/Core/FunctionPropositions/HasAdjDiff.lean

@@ -4,6 +4,8 @@ import SciLean.Core.FunctionPropositions.HasAdjDiffAt
 
 import SciLean.Core.FunctionTransformations.CDeriv
 
+import Lean.Meta.Tactic.Assumption
+
 set_option linter.unusedVariables false
 
 namespace SciLean
@@ -152,8 +154,15 @@ def fpropExt : FPropExt where
     }
     FProp.tryTheorem? e thm (fun _ => pure none)
 
-  discharger e := 
-    FProp.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption") e
+  discharger e := do
+    if let .some prf ← Lean.Meta.findLocalDeclWithType? e then
+      return .some (.fvar prf)
+    else
+      if e.isAppOf ``fpropParam then
+        trace[Meta.Tactic.fprop.unsafe] s!"discharging with sorry: {← ppExpr e}"
+        return .some <| ← mkAppOptM ``sorryProofAxiom #[e.appArg!]
+      else
+        return none
 
 
 -- register fderiv
@@ -338,7 +347,7 @@ by
 @[fprop]
 def HDiv.hDiv.arg_a0a1.HasAdjDiff_rule
   (f : X → K) (g : X → K) 
-  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : fpropParam (∀ x, g x ≠ 0))
   : HasAdjDiff K (fun x => f x / g x) := 
 by 
   have ⟨_,_⟩ := hf

SciLean/Core/FunctionPropositions/IsDifferentiable.lean

@@ -294,18 +294,17 @@ by
 @[fprop]
 def HDiv.hDiv.arg_a0a1.IsDifferentiable_rule
   (f : X → K) (g : X → K)
-  (hf : IsDifferentiable K f) (hg : IsDifferentiable K g) (hx : ∀ x, g x ≠ 0)
+  (hf : IsDifferentiable K f) (hg : IsDifferentiable K g) (hx : fpropParam (∀ x, g x ≠ 0))
   : IsDifferentiable K (fun x => f x / g x)
   := by sorry_proof
 
 @[fprop]
 def HDiv.hDiv.arg_a0.IsDifferentiable_rule
   (f : X → K) (r : K)
-  (hf : IsDifferentiable K f) (hr : r ≠ 0)
+  (hf : IsDifferentiable K f) (hr : fpropParam (r ≠ 0))
   : IsDifferentiable K (fun x => f x / r) := 
 by 
-  apply HDiv.hDiv.arg_a0a1.IsDifferentiable_rule <;> first | assumption | fprop | aesop
-
+  apply HDiv.hDiv.arg_a0a1.IsDifferentiable_rule <;> first | assumption | fprop | simp[hr,fpropParam]
 
 
 -- HPow.hPow -------------------------------------------------------------------

SciLean/Core/FunctionTransformations/CDeriv.lean

@@ -613,7 +613,7 @@ theorem HSMul.hSMul.arg_a0a1.cderiv_rule
 @[ftrans]
 theorem HDiv.hDiv.arg_a0a1.cderiv_rule_at
   (x : X) (f : X → K) (g : X → K) 
-  (hf : IsDifferentiableAt K f x) (hg : IsDifferentiableAt K g x) (hx : g x ≠ 0)
+  (hf : IsDifferentiableAt K f x) (hg : IsDifferentiableAt K g x) (hx : fpropParam (g x ≠ 0))
   : (cderiv K fun x => f x / g x) x
     =
     let k := f x
@@ -622,11 +622,10 @@ theorem HDiv.hDiv.arg_a0a1.cderiv_rule_at
       ((cderiv K f x dx) * k' - k * (cderiv K g x dx)) / k'^2 := 
 by sorry_proof
 
-
 @[ftrans]
 theorem HDiv.hDiv.arg_a0a1.cderiv_rule
   (f : X → K) (g : X → K) 
-  (hf : IsDifferentiable K f) (hg : IsDifferentiable K g) (hx : ∀ x, g x ≠ 0)
+  (hf : IsDifferentiable K f) (hg : IsDifferentiable K g) (hx : fpropParam (∀ x, g x ≠ 0))
   : (cderiv K fun x => f x / g x)
     =
     fun x => 

SciLean/Core/FunctionTransformations/RevDeriv.lean

@@ -516,10 +516,14 @@ def discharger (e : Expr) : SimpM (Option Expr) := do
   if proof?.isSome then
     return proof?
   else
-    -- if `fprop` fails try assumption
-    let tac := FTrans.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption")
-    let proof? ← tac e
-    return proof?
+    if let .some prf ← Lean.Meta.findLocalDeclWithType? e then
+      return .some (.fvar prf)
+    else
+      if e.isAppOf ``fpropParam then
+        trace[Meta.Tactic.fprop.unsafe] s!"discharging with sorry: {← ppExpr e}"
+        return .some <| ← mkAppOptM ``sorryProofAxiom #[e.appArg!]
+      else
+        return none
 
 
 open Lean Meta FTrans in
@@ -608,10 +612,14 @@ def discharger (e : Expr) : SimpM (Option Expr) := do
   if proof?.isSome then
     return proof?
   else
-    -- if `fprop` fails try assumption
-    let tac := FTrans.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption")
-    let proof? ← tac e
-    return proof?
+    if let .some prf ← Lean.Meta.findLocalDeclWithType? e then
+      return .some (.fvar prf)
+    else
+      if e.isAppOf ``fpropParam then
+        trace[Meta.Tactic.fprop.unsafe] s!"discharging with sorry: {← ppExpr e}"
+        return .some <| ← mkAppOptM ``sorryProofAxiom #[e.appArg!]
+      else
+        return none
 
 
 open Lean Meta FTrans in
@@ -698,10 +706,14 @@ def discharger (e : Expr) : SimpM (Option Expr) := do
   if proof?.isSome then
     return proof?
   else
-    -- if `fprop` fails try assumption
-    let tac := FTrans.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption")
-    let proof? ← tac e
-    return proof?
+    if let .some prf ← Lean.Meta.findLocalDeclWithType? e then
+      return .some (.fvar prf)
+    else
+      if e.isAppOf ``fpropParam then
+        trace[Meta.Tactic.fprop.unsafe] s!"discharging with sorry: {← ppExpr e}"
+        return .some <| ← mkAppOptM ``sorryProofAxiom #[e.appArg!]
+      else
+        return none
 
 
 open Lean Meta FTrans in
@@ -794,10 +806,14 @@ def discharger (e : Expr) : SimpM (Option Expr) := do
   if proof?.isSome then
     return proof?
   else
-    -- if `fprop` fails try assumption
-    let tac := FTrans.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption")
-    let proof? ← tac e
-    return proof?
+    if let .some prf ← Lean.Meta.findLocalDeclWithType? e then
+      return .some (.fvar prf)
+    else
+      if e.isAppOf ``fpropParam then
+        trace[Meta.Tactic.fprop.unsafe] s!"discharging with sorry: {← ppExpr e}"
+        return .some <| ← mkAppOptM ``sorryProofAxiom #[e.appArg!]
+      else
+        return none
 
 
 open Lean Meta FTrans in
@@ -1469,7 +1485,7 @@ by
 @[ftrans]
 theorem HDiv.hDiv.arg_a0a1.revDeriv_rule
   (f g : X → K)
-  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : fpropParam (∀ x, g x ≠ 0))
   : (revDeriv K fun x => f x / g x)
     =
     fun x => 
@@ -1486,7 +1502,7 @@ by
 @[ftrans]
 theorem HDiv.hDiv.arg_a0a1.revDerivUpdate_rule
   (f g : X → K)
-  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : fpropParam (∀ x, g x ≠ 0))
   : (revDerivUpdate K fun x => f x / g x)
     =
     fun x => 
@@ -1506,7 +1522,7 @@ by
 @[ftrans]
 theorem HDiv.hDiv.arg_a0a1.revDerivProj_rule
   (f g : X → K)
-  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : fpropParam (∀ x, g x ≠ 0))
   : (revDerivProj K Unit fun x => f x / g x)
     =
     fun x => 
@@ -1521,7 +1537,7 @@ by
 @[ftrans]
 theorem HDiv.hDiv.arg_a0a1.revDerivProjUpdate_rule
   (f g : X → K)
-  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : fpropParam (∀ x, g x ≠ 0))
   : (revDerivProjUpdate K Unit fun x => f x / g x)
     =
     fun x => 

SciLean/Tactic/FProp/Init.lean

@@ -12,7 +12,17 @@ import SciLean.Tactic.AnalyzeConstLambda
 
 open Lean Meta.Simp Qq
 
-namespace SciLean.FProp
+namespace SciLean
+
+/-- Gadget for marking parameters for `fprop` and `ftrans` tactics.
+
+Parameters marked like this are usually hard to prove. Right now, they are 
+usually discharged with sorry.
+-/
+@[reducible] def fpropParam (α : Sort u) : Sort u := α
+
+
+namespace FProp
 
 
 -- Tracing --
@@ -26,11 +36,13 @@ initialize registerTraceClass `Meta.Tactic.fprop.rewrite
 initialize registerTraceClass `Meta.Tactic.fprop.discharge
 initialize registerTraceClass `Meta.Tactic.fprop.unify
 initialize registerTraceClass `Meta.Tactic.fprop.apply
+initialize registerTraceClass `Meta.Tactic.fprop.unsafe
 -- initialize registerTraceClass `Meta.Tactic.fprop.lambda_special_cases
 
 initialize registerOption `linter.fpropDeclName { defValue := true, descr := "suggests declaration name for fprop rule" }
 
 
+
 open Meta