progress on data_synth

SciLean/Analysis/Calculus/FwdFDeriv.lean

@@ -305,8 +305,8 @@ theorem HMul.hMul.arg_a0a1.fwdFDeriv_rule_at (x : X) (f g : X → K)
       let y := ydy.1; let dy := ydy.2
       let zdz := (fwdFDeriv K g x dx)
       let z := zdz.1; let dz := zdz.2
-      (y * z, dz * y + dy * z) := by
-  funext dx; unfold fwdFDeriv; fun_trans; simp[mul_comm]
+      (y * z, y * dz + dy * z) := by
+  funext dx; unfold fwdFDeriv; fun_trans
 
 
 -- HSMul.hSMul -----------------------------------------------------------------

SciLean/Tactic/DataSynth/Elab.lean

@@ -44,7 +44,7 @@ syntax (name:=data_synth_conv) "data_synth" optConfig : conv
     if ← isDefEq e e' then
       Conv.changeLhs e'
     else
-      throwError "faield to assign data"
+      throwError "faield to assign data {e'}"
   | none =>
     throwError "`data_synth` failed"
 | _ => throwUnsupportedSyntax

SciLean/Tactic/DataSynth/HasFDerivAt.lean

@@ -0,0 +1,58 @@
+import SciLean.Analysis.Calculus.FDeriv
+import SciLean.Tactic.DataSynth.Attr
+import SciLean.Tactic.DataSynth.Elab
+
+section Missing
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
+variable {f g : E → F} {f' g' : E →L[𝕜] F} {x : E} {s : Set E} {L : Filter E}
+
+theorem HasFDerivAt.letE {g : F → E → G} {g'}
+    (hf : HasFDerivAt f f' x)
+    (hg : HasFDerivAt (fun yx : F×E => g yx.1 yx.2) g' (f x, x)) :
+    HasFDerivAt
+      (fun x => let y := f x; g y x)
+      (g'.comp (f'.prod (.id 𝕜 E))) x := sorry_proof
+
+end Missing
+
+attribute [data_synth out f' in f] HasFDerivAt
+
+attribute [data_synth]
+  hasFDerivAt_id
+  hasFDerivAt_const
+  hasFDerivAt_apply
+  hasFDerivAt_pi''
+  -- HasFDerivAt.comp
+  -- HasFDerivAt.letE
+
+  HasFDerivAt.prod
+  HasFDerivAt.fst
+  HasFDerivAt.snd
+
+  HasFDerivAt.add
+  HasFDerivAt.sub
+  HasFDerivAt.neg
+  HasFDerivAt.mul
+  HasFDerivAt.smul
+
+
+
+variable {𝕜 : Type} [NontriviallyNormedField 𝕜] (x : 𝕜)
+
+set_option profiler true in
+set_option trace.Meta.Tactic.data_synth true in
+set_option trace.Meta.Tactic.data_synth.normalize true in
+#check (HasFDerivAt (𝕜:=𝕜) (fun x : 𝕜 => x * x * x) _ x)
+  rewrite_by
+    data_synth +simp
+
+
+
+set_option profiler true in
+#check (HasFDerivAt (𝕜:=𝕜) (fun yx : 𝕜×𝕜 => yx.1 * yx.2* yx.2* yx.2* yx.2* yx.2* yx.2* yx.2* yx.2* yx.2* yx.2* yx.2* yx.2* yx.2) _ (x, x))
+  rewrite_by
+    data_synth +simp

SciLean/Tactic/DataSynth/HasFwdFDeriv.lean

@@ -1,13 +1,14 @@
 import SciLean.Analysis.Calculus.FwdFDeriv
 import SciLean.Tactic.DataSynth.Attr
 import SciLean.Tactic.DataSynth.Elab
+import SciLean.Tactic.LSimp.Elab
 
 namespace SciLean
 
-variable {R} [RCLike R]
-  {X} [NormedAddCommGroup X] [NormedSpace R X]
-  {Y} [NormedAddCommGroup Y] [NormedSpace R Y]
-  {Z} [NormedAddCommGroup Z] [NormedSpace R Z]
+variable {R : Type} [RCLike R]
+  {X : Type} [NormedAddCommGroup X] [NormedSpace R X]
+  {Y : Type} [NormedAddCommGroup Y] [NormedSpace R Y]
+  {Z : Type} [NormedAddCommGroup Z] [NormedSpace R Z]
 
 variable (R)
 @[data_synth out f' in f]
@@ -32,7 +33,6 @@ theorem const_rule (x : X) (y : Y) :  HasFwdFDerivAt R (fun x : X => y) (fun x d
   · fun_trans
   · fun_prop
 
-@[data_synth]
 theorem comp_rule (f : Y → Z) (g : X → Y) (x : X) (f' g')
     (hf : HasFwdFDerivAt R f f' (g x)) (hg : HasFwdFDerivAt R g g' x) :
     HasFwdFDerivAt R
@@ -46,9 +46,9 @@ theorem comp_rule (f : Y → Z) (g : X → Y) (x : X) (f' g')
   · intro dx; fun_trans only; simp_all
   · fun_prop
 
-@[data_synth]
-theorem let_rule (f : Y → X → Z) (g : X → Y) (x : X) (f' g')
-    (hf : HasFwdFDerivAt R (↿f) f' (g x, x)) (hg : HasFwdFDerivAt R g g' x) :
+theorem let_rule (g : X → Y) (f : Y → X → Z) {x : X} {f' g'}
+    (hg : HasFwdFDerivAt R g g' x)
+    (hf : HasFwdFDerivAt R (fun yx : Y×X => f yx.1 yx.2) f' (g x, x))  :
     HasFwdFDerivAt R
       (fun x : X => let y := g x; f y x)
       (fun x dx =>
@@ -63,7 +63,7 @@ theorem let_rule (f : Y → X → Z) (g : X → Y) (x : X) (f' g')
 
 end HasFwdFDerivAt
 
-
+@[data_synth]
 theorem Prod.mk.arg_a0a1.HasFwdFDerivAt_rule
   (f : X → Y) (g : X → Z) (x) (f' g')
   (hf : HasFwdFDerivAt R f f' x) (hg : HasFwdFDerivAt R g g' x) :
@@ -79,7 +79,7 @@ theorem Prod.mk.arg_a0a1.HasFwdFDerivAt_rule
   · intro dx; fun_trans only; simp_all
   · fun_prop
 
-
+@[data_synth]
 theorem Prod.fst.arg_self.HasFwdFDerivAt_rule
   (f : X → Y×Z) (x) (f')
   (hf : HasFwdFDerivAt R f f' x) :
@@ -93,6 +93,7 @@ theorem Prod.fst.arg_self.HasFwdFDerivAt_rule
   · intro dx; fun_trans only; simp_all
   · fun_prop
 
+@[data_synth]
 theorem Prod.snd.arg_self.HasFwdFDerivAt_rule
   (f : X → Y×Z) (x) (f')
   (hf : HasFwdFDerivAt R f f' x) :
@@ -105,3 +106,116 @@ theorem Prod.snd.arg_self.HasFwdFDerivAt_rule
   constructor
   · intro dx; fun_trans only; simp_all
   · fun_prop
+
+
+@[data_synth]
+theorem HAdd.hAdd.arg_a0a1.HasFwdFDerivAt_rule
+    (f g : X → Y) (x) (f' g')
+    (hf : HasFwdFDerivAt R f f' x) (hg : HasFwdFDerivAt R g g' x) :
+    HasFwdFDerivAt R (fun x => f x + g x)
+      (fun x dx =>
+        let ydy := f' x dx
+        let zdz := g' x dx
+        (ydy.1 + zdz.1, ydy.2 + zdz.2)) x := by
+  cases hf; cases hg
+  constructor
+  · intro dx; fun_trans only; simp_all
+  · fun_prop
+
+
+@[data_synth]
+theorem HSub.hSub.arg_a0a1.HasFwdFDerivAt_rule
+    (f g : X → Y) (x) (f' g')
+    (hf : HasFwdFDerivAt R f f' x) (hg : HasFwdFDerivAt R g g' x) :
+    HasFwdFDerivAt R (fun x => f x - g x)
+      (fun x dx =>
+        let ydy := f' x dx
+        let zdz := g' x dx
+        (ydy.1 - zdz.1, ydy.2 - zdz.2)) x := by
+  cases hf; cases hg
+  constructor
+  · intro dx; fun_trans only; simp_all
+  · fun_prop
+
+
+@[data_synth]
+theorem HMul.hMul.arg_a0a1.HasFwdFDerivAt_rule
+    (f g : X → R) (x) (f' g')
+    (hf : HasFwdFDerivAt R f f' x) (hg : HasFwdFDerivAt R g g' x) :
+    HasFwdFDerivAt R (fun x => f x * g x)
+      (fun x dx =>
+        let ydy := f' x dx
+        let zdz := g' x dx
+        (ydy.1 * zdz.1, ydy.1 * zdz.2 + ydy.2 * zdz.1)) x := by
+  cases hf; cases hg
+  constructor
+  · intro dx; fun_trans only; simp_all
+  · fun_prop
+
+
+theorem HasFwdFDerivAt.fwdFDeriv {f : X → Y} {x} {f'} (hf : HasFwdFDerivAt R f f' x) :
+    fwdFDeriv R f x = f' x := by
+  funext dx; cases hf
+  unfold SciLean.fwdFDeriv
+  simp_all
+
+open SciLean Lean Meta in
+simproc [] dataSynthFwdFDeriv (fwdFDeriv _ _ _) := fun e => do
+
+  let .mkApp2 _ f x := e | return .continue
+  let R := e.getArg! 0
+
+  let h ← mkAppM ``HasFwdFDerivAt #[R,f]
+  let (xs,_) ← forallMetaTelescope (← inferType h)
+  let h := h.beta #[xs[0]!, x]
+
+  let some goal ← Tactic.DataSynth.isDataSynthGoal? h
+    | return .continue
+
+  let (some r,_) ← Tactic.DataSynth.dataSynth goal |>.run {} |>.run {}
+    | return .continue
+
+  let e' := r.xs[0]!.beta #[x]
+
+  return .visit { expr := e', proof? := ← mkAppM ``HasFwdFDerivAt.fwdFDeriv #[r.proof] }
+
+
+set_option trace.Meta.Tactic.data_synth true in
+set_option trace.Meta.Tactic.data_synth.input true in
+
+example : (fwdFDeriv R (fun x : R => x * x * x) 2)
+          =
+          fun dx => (2 * 2 * 2, 2 * 2 * dx + (2 * dx + dx * 2) * 2) := by
+  conv =>
+    lhs
+    simp -zeta [dataSynthFwdFDeriv]
+
+
+
+set_option trace.Meta.Tactic.data_synth true in
+set_option trace.Meta.Tactic.data_synth.input true in
+example : (fwdFDeriv R (fun x : R => let y := x * x; y * x) 2)
+          =
+          fun dx => (2 * 2 * 2, 2 * 2 * dx + (2 * dx + dx * 2) * 2) := by
+  conv =>
+    lhs
+    simp -zeta [dataSynthFwdFDeriv]
+
+
+#check (HasFwdFDerivAt R (fun x : R => let y := x * x; y * x) _ 2)
+  rewrite_by
+    data_synth
+
+
+
+set_option trace.Meta.Tactic.simp.rewrite true in
+#check (fwdFDeriv R (fun x : R => let x₁ := x * x; let x₂ := x*x₁; let x₃ := x*x₁*x₂; x*x₁*x₂*x₃) 2)
+  rewrite_by
+    simp -zeta only [dataSynthFwdFDeriv]
+
+
+set_option profiler true in
+
+#check (HasFwdFDerivAt R (fun x : R×R =>) _ 2)
+  rewrite_by
+    data_synth +lsimp -zeta