From 33276f7f50bd5b96882d9b0b00d8b383b077a4e4 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Thu, 27 Jul 2023 12:37:53 -0400
Subject: [PATCH] work on adjoint

---
 SciLean/FTrans/Adjoint/Basic.lean | 126 +++++++++++++++++++++++++++++-
 1 file changed, 125 insertions(+), 1 deletion(-)

diff --git a/SciLean/FTrans/Adjoint/Basic.lean b/SciLean/FTrans/Adjoint/Basic.lean
index 7f961efc..ef0bd375 100644
--- a/SciLean/FTrans/Adjoint/Basic.lean
+++ b/SciLean/FTrans/Adjoint/Basic.lean
@@ -10,6 +10,8 @@ import SciLean.Mathlib.Analysis.InnerProductSpace.Prod
 import SciLean.Profile
 
 
+namespace  ContinuousLinearMap.adjoint
+
 variable 
   {K : Type _} [IsROrC K]
   {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X] [CompleteSpace X]
@@ -30,7 +32,6 @@ variable (g : X → Y) (hg : SciLean.IsContinuousLinearMap K g)
 
 -- Basic lambda calculus rules -------------------------------------------------
 --------------------------------------------------------------------------------
-namespace  ContinuousLinearMap.adjoint
 
 open SciLean
 
@@ -131,5 +132,128 @@ theorem proj_rule [DecidableEq ι]
   := sorry
 
 
+-- Register `adjoint` as function transformation -------------------------------
+--------------------------------------------------------------------------------
+
+open Lean Meta Qq
+
+def discharger (e : Expr) : SimpM (Option Expr) := do
+  withTraceNode `fwdDeriv_discharger (fun _ => return s!"discharge {← ppExpr e}") do
+  let cache := (← get).cache
+  let config : FProp.Config := {}
+  let state  : FProp.State := { cache := cache }
+  let (proof?, state) ← FProp.fprop e |>.run config |>.run state
+  modify (fun simpState => { simpState with cache := state.cache })
+  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?
+
+open Lean Elab Term FTrans
+def ftransExt : FTransExt where
+  ftransName := ``adjoint
+
+  getFTransFun? e := Id.run do
+    let (name, args) := e.getAppFnArgs
+    if name == ``FunLike.coe && args.size = 6 then
+      
+      if ¬(args[4]!.isAppOf ``adjoint) then
+        return none
+
+      let f := args[5]!
+      if f.isAppOf ``ContinuousLinearMap.mk' then
+        if let .some f' := f.getArg? 10 then
+          return f'
+        else
+          return f
+      else
+        return f
+
+    return none
+
+  replaceFTransFun e f := Id.run do
+    let (name, args) := e.getAppFnArgs
+    if name == ``FunLike.coe && args.size = 6 then
+      
+      if ¬(args[4]!.isAppOf ``adjoint) then
+        return e         
+      
+      return e.modifyArg (fun _ => f) 5
+    else
+      return e
+
+  identityRule     := .some <| .thm ``adjoint.id_rule
+  constantRule     := .some <| .thm ``adjoint.const_rule
+  compRule         := .some <| .thm ``adjoint.comp_rule
+  lambdaLetRule    := .some <| .thm ``adjoint.let_rule
+  lambdaLambdaRule := .some <| .thm ``adjoint.pi_rule
+
+  discharger := adjoint.discharger
+
+
+-- register adjoint
+#eval show Lean.CoreM Unit from do
+  modifyEnv (λ env => FTrans.ftransExt.addEntry env (``adjoint, adjoint.ftransExt))
+
+end ContinuousLinearMap.adjoint
+
+
+--------------------------------------------------------------------------------
+-- Function Rules --------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+variable 
+  {K : Type _} [IsROrC K]
+  {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X] [CompleteSpace X]
+  {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y] [CompleteSpace Y]
+  {Z : Type _} [NormedAddCommGroup Z] [InnerProductSpace K Z] [CompleteSpace Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace K (E i)] [∀ i, CompleteSpace (E i)]
+
+open SciLean
+
+-- Prod.mk ---------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
 
 
+example
+  (g : X → Y) (hg : IsContinuousLinearMap K g)
+  (f : X → Z) (hf : IsContinuousLinearMap K f)
+  : IsContinuousLinearMap K
+    fun yz : Y×₂Z =>
+      (fun x =>L[K] g x)† yz.1 + (fun x =>L[K] f x)† yz.2 := by fprop
+
+
+set_option trace.Meta.Tactic.fprop.step true in
+set_option trace.Meta.Tactic.fprop.discharge true in
+@[ftrans_rule]
+theorem Prod.mk.arg_fstsnd.adjoint_comp
+  (g : X → Y) (hg : IsContinuousLinearMap K g)
+  (f : X → Z) (hf : IsContinuousLinearMap K f)
+  : ((fun x =>L[K] (g x, f x)) : X →L[K] Y×₂Z)†
+    =
+    fun yz =>L[K] 
+      -- (fun x =>L[K] g x)† yz.1 + (fun x =>L[K] f x)† yz.2 :=
+      let x₁ := (fun x =>L[K] g x)† yz.1
+      let x₂ := (fun x =>L[K] f x)† yz.2
+      x₁ + x₂ := 
+by sorry
+
+
+
+
+-- set_option trace.Meta.Tactic.ftrans.step true in
+set_option trace.Meta.flattenLet.step true in
+example
+  (g : X → Y) (hg : IsContinuousLinearMap K g)
+  (f : X → Z) (hf : IsContinuousLinearMap K f)
+  : ((fun x =>L[K] (g x, f x)) : X →L[K] Y×₂Z)†
+    =
+    fun yz =>L[K]
+      (fun x =>L[K] g x)† yz.1 + (fun x =>L[K] f x)† yz.2 :=
+by ftrans only
+