some improvements to ftrans

SciLean/FTrans/Adjoint/Basic.lean

@@ -34,34 +34,46 @@ instance (f : X →L[K] Y) : SciLean.Dagger f (ContinuousLinearMap.adjoint f : Y
 
 open SciLean
 
+variable (X) (K)
 theorem id_rule 
   : (fun (x : X) =>L[K] x)† = fun x =>L[K] x := 
 by
   have h : (fun (x : X) =>L[K] x) = ContinuousLinearMap.id K X := by rfl
   rw[h]; simp
 
 
+variable (Y)
 theorem const_rule 
   : (fun (x : X) =>L[K] (0 : Y))† = fun x =>L[K] 0 := 
 by
   sorry
+variable {Y}
+
+theorem proj_rule [DecidableEq ι]
+   (i : ι) 
+  : (fun (f : PiLp 2 (fun _ => X)) =>L[K] f i)†
+    = 
+    fun x =>L[K] (fun j => if h : i=j then x else (0 : X))
+  := sorry
+variable {X}
+
 
 theorem prod_rule
-  (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)†
+  (f : X → Y) (g : X → Z) 
+  (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g)
+  : ((fun x =>L[K] (f x, g x)) : X →L[K] Y×₂Z)†
     =
     fun yz : Y×₂Z =>L[K]
-      let x₁ := (fun x =>L[K] g x)† yz.1
-      let x₂ := (fun x =>L[K] f x)† yz.2
+      let x₁ := (fun x =>L[K] f x)† yz.1
+      let x₂ := (fun x =>L[K] g x)† yz.2
       x₁ + x₂ := 
 by 
   sorry
 
 
 theorem comp_rule 
-  (g : X → Y) (hg : IsContinuousLinearMap K g)
-  (f : Y → Z) (hf : IsContinuousLinearMap K f)
+  (f : Y → Z) (g : X → Y) 
+  (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g)
   : (fun x =>L[K] f (g x))†
     =
     fun z =>L[K]
@@ -79,8 +91,8 @@ by
 
 
 theorem let_rule 
-  (g : X → Y)      (hg : IsContinuousLinearMap K g)
-  (f : X → Y → Z) (hf : IsContinuousLinearMap K (fun xy : X×Y => f xy.1 xy.2))
+  (f : X → Y → Z) (g : X → Y)      
+  (hf : IsContinuousLinearMap K (fun xy : X×Y => f xy.1 xy.2)) (hg : IsContinuousLinearMap K g)
   : (fun x =>L[K] let y := g x; f x y)†
     =
     fun z =>L[K]
@@ -96,40 +108,19 @@ by
   have h' : ((fun x =>L[K] (x, g x)) : X →L[K] X×₂Y)† 
             = 
             (fun (xy : X×₂Y) =>L[K] xy.1 + (fun x =>L[K] g x)† xy.2)
-          := by rw[prod_rule (fun x => x) (by fprop) g hg]; simp[id_rule]
+          := by rw[prod_rule K (fun x => x) g (by fprop) hg]; simp[id_rule]
   rw[h']; rfl
 
 
-
-example : CompleteSpace ((i :ι) → E i) := by infer_instance
-
-open BigOperators
-
--- set_option trace.Meta.Tactic.fprop.discharge true in
--- set_option trace.Meta.Tactic.fprop.step true in
+open BigOperators in
 theorem pi_rule
-  (f : (i : ι) → X → E i) (hf : ∀ i, IsContinuousLinearMap K (f i))
-  : ((fun (x : X) =>L[K] fun (i : ι) => f i x) : X →L[K] PiLp 2 E)†
+  (f : X → (i : ι) → E i) (hf : ∀ i, IsContinuousLinearMap K (f · i))
+  : ((fun (x : X) =>L[K] fun (i : ι) => f x i) : X →L[K] PiLp 2 E)†
     = 
-    (fun x' =>L[K] ∑ i, (fun x =>L[K] f i x)† (x' i))
+    (fun x' =>L[K] ∑ i, (fun x =>L[K] f x i)† (x' i))
   := sorry
 
 
-set_option trace.Meta.Tactic.fprop.discharge true in
--- theorem proj_rule [DecidableEq ι]
---    (i : ι) 
---   : (fun (f : PiLp 2 E) =>L[K] f i)†
---     = 
---     fun y =>L[K] ((fun j => if h : i=j then (h ▸ y) else (0 : E j)) : PiLp 2 E)
---   := sorry
-
-theorem proj_rule [DecidableEq ι]
-   (i : ι) 
-  : (fun (f : PiLp 2 (fun _ => X)) =>L[K] f i)†
-    = 
-    fun x =>L[K] (fun j => if h : i=j then x else (0 : X))
-  := sorry
-
 
 -- Register `adjoint` as function transformation -------------------------------
 --------------------------------------------------------------------------------
@@ -184,13 +175,72 @@ def ftransExt : FTransExt where
     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
+  idRule  e X := do
+    let K := (e.getArg! 1).getArg! 0
+    tryTheorems
+      #[ { proof := ← mkAppM ``id_rule #[K, X], origin := .decl ``id_rule, rfl := false} ]
+      discharger e
+
+  constRule e X y := do
+    let K := (e.getArg! 1).getArg! 0
+    tryTheorems
+      #[ { proof := ← mkAppM ``const_rule #[K, X, (← inferType y)], origin := .decl ``const_rule, rfl := false} ]
+      discharger e
+
+  projRule e X i := do
+    let K := (e.getArg! 1).getArg! 0
+    let X' := X.bindingBody!
+    if X'.hasLooseBVars then
+      trace[Meta.Tactic.ftrans.step] "can't handle this bvar app case, projection rule for dependent function of type {← ppExpr X} is not supported"
+      return none
+    tryTheorems
+      #[ { proof := ← mkAppM ``proj_rule #[K, X', i], origin := .decl ``proj_rule, rfl := false} ]
+      discharger e
+
+  compRule e f g := do
+    let K := (e.getArg! 1).getArg! 0
+
+    let XY ← inferType g
+    let YZ ← inferType f
+
+    let two : Q(ℝ)  := q(2)
+    let fixProduct : Expr → Option Expr :=       
+      (fun e => 
+        if let .app (.app (.const name us) A) B := e then
+          if name == ``Prod then
+            mkApp3 (mkConst ``ProdLp us) two A B
+          else
+            none
+        else
+          none)
 
-  discharger := adjoint.discharger
+    let X := XY.bindingDomain!.replace fixProduct
+    let Y := XY.bindingBody!.replace fixProduct
+    let Z := YZ.bindingBody!.replace fixProduct
+
+    let args : Array (Option Expr) := 
+       #[K, none, X, none, none, none, 
+                  Y, none, none, none, 
+                  Z, none, none, none, f, g]
+
+    tryTheorems
+      #[ { proof := ← withTransparency .all <| 
+             mkAppM ``comp_rule #[K, f, g], origin := .decl ``comp_rule, rfl := false} ]
+      discharger e
+
+  letRule e f g := do
+    let K := (e.getArg! 1).getArg! 0
+    tryTheorems
+      #[ { proof := ← mkAppM ``let_rule #[K, f, g], origin := .decl ``let_rule, rfl := false} ]
+      discharger e
+
+  piRule  e f := do
+    let K := (e.getArg! 1).getArg! 0
+    tryTheorems
+      #[ { proof := ← mkAppM ``pi_rule #[K, f], origin := .decl ``pi_rule, rfl := false} ]
+      discharger e
+
+  discharger := discharger
 
 
 -- register adjoint
@@ -215,7 +265,6 @@ variable
 open SciLean
 
 
-
 -- Prod.mk ---------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
@@ -367,7 +416,6 @@ by
   sorry
 
 
-
 -- Finset.sum ------------------------------------------------------------------
 -------------------------------------------------------------------------------- 
 
@@ -414,11 +462,9 @@ by
   case isFalse h => ext y; simp[h]
 
 
-
 -- Inner -----------------------------------------------------------------------
 -------------------------------------------------------------------------------- 
 
-set_option trace.Meta.Tactic.fprop.discharge true in
 open ComplexConjugate in
 @[ftrans_rule]
 theorem Inner.inner.arg_a0.adjoint_comp

SciLean/FTrans/Adjoint/Test.lean

@@ -0,0 +1,117 @@
+import SciLean.FTrans.Adjoint.Basic
+
+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]
+  {Y₁ : Type _} [NormedAddCommGroup Y₁] [InnerProductSpace K Y₁] [CompleteSpace Y₁]
+  {Y₂ : Type _} [NormedAddCommGroup Y₂] [InnerProductSpace K Y₂] [CompleteSpace Y₂]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace K (E i)] [∀ i, CompleteSpace (E i)]
+
+open SciLean
+
+example
+  : (fun (x : X) =>L[K] x)† = fun x =>L[K] x := by ftrans
+
+example
+  : (fun (x : X) =>L[K] (0 : Y))† = fun x =>L[K] 0 := by ftrans
+
+
+set_option trace.Meta.Tactic.ftrans.step true in
+example [DecidableEq ι] (i : ι) 
+  : (fun (f : PiLp 2 (fun _ => X)) =>L[K] f i)†
+    = 
+    fun x =>L[K] (fun j => if h : i=j then x else (0 : X))
+  := by ftrans
+
+
+example
+  (f : X → Y) (g : X → Z) 
+  (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g)
+  : ((fun x =>L[K] (f x, g x)) : X →L[K] Y×₂Z)†
+    =
+    fun yz : Y×₂Z =>L[K]
+      let x₁ := (fun x =>L[K] f x)† yz.1
+      let x₂ := (fun x =>L[K] g x)† yz.2
+      x₁ + x₂ := by ftrans
+
+
+example
+  (f : Y → Z) (g : X → Y) 
+  (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g)
+  : (fun x =>L[K] f (g x))†
+    =
+    fun z =>L[K]
+      let y := (fun y =>L[K] f y)† z
+      let x := (fun x =>L[K] g x)† y
+      x := by ftrans
+
+
+
+example
+  (f : X → Y → Z) (g : X → Y)      
+  (hf : IsContinuousLinearMap K (fun xy : X×Y => f xy.1 xy.2)) (hg : IsContinuousLinearMap K g)
+  : (fun x =>L[K] let y := g x; f x y)†
+    =
+    fun z =>L[K]
+      let xy := ((fun xy : X×₂Y =>L[K] f xy.1 xy.2)†) z
+      let x' := ((fun x =>L[K] g x)†) xy.2
+      xy.1 + x' := by ftrans
+
+open BigOperators in
+example
+  (f : X → (i : ι) → E i) (hf : ∀ i, IsContinuousLinearMap K (f · i))
+  : ((fun (x : X) =>L[K] fun (i : ι) => f x i) : X →L[K] PiLp 2 E)†
+    = 
+    (fun x' =>L[K] ∑ i, (fun x =>L[K] f x i)† (x' i))
+  := by ftrans
+
+
+-- instance introducing diamond!!!
+@[reducible]
+noncomputable
+instance instNormedAddCommGroupProdL2
+  {K : Type _} [IsROrC K]
+  {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X]
+  {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y]
+  : NormedAddCommGroup (X × Y) := by rw[show (X×Y) = (ProdLp 2 X Y) by rfl]; infer_instance
+
+@[reducible]
+noncomputable
+instance instInnerProductSpaceProdL2
+  {K : Type _} [IsROrC K]
+  {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X]
+  {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y]
+  : @InnerProductSpace K (X × Y) _ (@instNormedAddCommGroupProdL2 K _ X _ _ Y _ _) := 
+ show InnerProductSpace K (ProdLp 2 X Y) by infer_instance
+
+
+
+-- set_option trace.Meta.Tactic.simp.discharge true in
+set_option trace.Meta.Tactic.ftrans.discharge true in
+set_option trace.Meta.Tactic.ftrans.step true in
+set_option trace.Meta.Tactic.simp.unify true in
+example
+  (f : Y₁ → Y₂ → Z) (g₁ : X → Y₁) (g₂ : X → Y₂)
+  (hf : IsContinuousLinearMap K (fun yy : Y₁×Y₂ => f yy.1 yy.2)) 
+  (hg₁ : IsContinuousLinearMap K g₁)
+  (hg₂ : IsContinuousLinearMap K g₂)
+  : (fun x =>L[K] f (g₁ x) (g₂ x))†
+    =
+    0
+  :=
+by
+  ftrans only
+
+
+
+
+
+instance   
+  {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X] [CompleteSpace X]
+  {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y] [CompleteSpace Y]
+  : InnerProductSpace K (X × Y) := by rw[show (X×Y) = (ProdLp 2 X Y) by rfl];
+
+