Skip to content

Commit

Permalink
work on adjoint
Browse files Browse the repository at this point in the history
  • Loading branch information
lecopivo committed Jul 27, 2023
1 parent ba1a6bb commit 33276f7
Showing 1 changed file with 125 additions and 1 deletion.
126 changes: 125 additions & 1 deletion SciLean/FTrans/Adjoint/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -30,7 +32,6 @@ variable (g : X → Y) (hg : SciLean.IsContinuousLinearMap K g)

-- Basic lambda calculus rules -------------------------------------------------
--------------------------------------------------------------------------------
namespace ContinuousLinearMap.adjoint

open SciLean

Expand Down Expand Up @@ -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

0 comments on commit 33276f7

Please sign in to comment.