projection rule in fprop

SciLean/FTrans/Adjoint/Basic.lean

@@ -100,18 +100,36 @@ by
   rw[h']; rfl
 
 
-#exit
 
 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.discharge true in
+-- set_option trace.Meta.Tactic.fprop.step true in
 theorem pi_rule
-  (x : X)
   (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)†
     = 
     (fun x' =>L[K] ∑ i, (fun x =>L[K] f i x)† (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
+
+
+
+

SciLean/FunctionSpaces/Continuous/Basic.lean

@@ -55,6 +55,11 @@ theorem pi_rule
   : Continuous (fun x i => f i x)
   := by continuity
 
+theorem proj_rule
+  (i : ι)
+  : Continuous (fun x : (i : ι) → E i => x i)
+  := by continuity
+
 
 end SciLean.Continuous
 
@@ -143,6 +148,15 @@ def Continuous.fpropExt : FPropExt where
     }
     FProp.tryTheorem? e thm (fun _ => pure none)
 
+  projRule e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``Continuous.proj_rule 
+      origin := .decl ``Continuous.proj_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
   discharger _ := return none
 
 -- register fderiv

SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean

@@ -103,10 +103,16 @@ theorem pi_rule
   (by simp)
 
 
+theorem proj_rule (i : ι)
+  : IsContinuousLinearMap R fun f : (i : ι) → E i => f i
+:= 
+  by_morphism (ContinuousLinearMap.proj i) (by simp)
+
+
 end SciLean.IsContinuousLinearMap
 
 --------------------------------------------------------------------------------
--- Register Diferentiable ------------------------------------------------------
+-- Register IsContinuousLinearMap ----------------------------------------------
 --------------------------------------------------------------------------------
 
 open Lean Meta SciLean FProp
@@ -194,6 +200,16 @@ def IsContinuousLinearMap.fpropExt : FPropExt where
     }
     FProp.tryTheorem? e thm (fun _ => pure none)
 
+  projRule e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``IsContinuousLinearMap.proj_rule 
+      origin := .decl ``IsContinuousLinearMap.proj_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+
   discharger _ := return none
 
 -- register fderiv
@@ -486,12 +502,16 @@ theorem HDiv.hDul.arg_a4.IsContinuousLinearMap_comp
 -- Finset.sum -------------------------------------------------------------------
 -------------------------------------------------------------------------------- 
 
-
 open BigOperators in
 @[fprop_rule]
 theorem Finset.sum.arg_f.IsContinuousLinearMap_comp
   (f : X → ι → Y) (hf : ∀ i, IsContinuousLinearMap R fun x : X => f x i) (A : Finset ι)
-  : IsContinuousLinearMap R fun x => ∑ i in A, f x i := sorry
+  : IsContinuousLinearMap R fun x => ∑ i in A, f x i := 
+{
+  map_add'  := sorry
+  map_smul' := sorry
+  cont := sorry
+}
 
 -- do we need this one?
 -- open BigOperators in
@@ -500,3 +520,28 @@ theorem Finset.sum.arg_f.IsContinuousLinearMap_comp
 --   (f : ι → X → Y) (hf : ∀ i, IsContinuousLinearMap R (f i)) (A : Finset ι)
 --   : IsContinuousLinearMap R fun (x : X) => ∑ i in A, f i x := sorry
 
+
+-- ite -------------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop_rule]
+theorem ite.arg_te.IsContinuousLinearMap_comp
+  (c : Prop) [dec : Decidable c]
+  (t e : X → Y) (ht : IsContinuousLinearMap R t) (he : IsContinuousLinearMap R e)
+  : IsContinuousLinearMap R fun x => ite c (t x) (e x) := 
+by
+  induction dec
+  case isTrue h  => simp[h]; fprop
+  case isFalse h => simp[h]; fprop
+
+
+@[fprop_rule]
+theorem dite.arg_te.IsContinuousLinearMap_comp
+  (c : Prop) [dec : Decidable c]
+  (t : c  → X → Y) (ht : ∀ p, IsContinuousLinearMap R (t p)) 
+  (e : ¬c → X → Y) (he : ∀ p, IsContinuousLinearMap R (e p))
+  : IsContinuousLinearMap R fun x => dite c (t · x) (e · x) := 
+by
+  induction dec
+  case isTrue h  => simp[h]; apply ht
+  case isFalse h => simp[h]; apply he

SciLean/FunctionSpaces/Differentiable/Basic.lean

@@ -61,6 +61,11 @@ theorem pi_rule
   : Differentiable R (fun x i => f i x)
   := fun x => DifferentiableAt.pi_rule x f (fun i => hf i x)
 
+theorem proj_rule
+  (i : ι)
+  : Differentiable R (fun x : (i : ι) → E i => x i):= 
+by 
+  apply DifferentiableAt.proj_rule
 
 
 end SciLean.Differentiable
@@ -155,6 +160,16 @@ def Differentiable.fpropExt : FPropExt where
     }
     FProp.tryTheorem? e thm (fun _ => pure none)
 
+  projRule e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``DifferentiableAt.proj_rule 
+      origin := .decl ``DifferentiableAt.proj_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+
   discharger _ := return none
 
 -- register fderiv

SciLean/FunctionSpaces/DifferentiableAt/Basic.lean

@@ -9,6 +9,7 @@ import Mathlib.Analysis.Calculus.Deriv.Inv
 import SciLean.Tactic.FProp.Basic
 import SciLean.Tactic.FProp.Notation
 
+import SciLean.FunctionSpaces.ContinuousLinearMap.Notation
 
 namespace SciLean
 
@@ -65,6 +66,14 @@ theorem pi_rule
   := by apply differentiableAt_pi.2 hf
 
 
+theorem proj_rule
+  (i : ι) (x)
+  : DifferentiableAt R (fun x : (i : ι) → E i => x i) x := 
+by 
+  apply IsBoundedLinearMap.differentiableAt
+  apply ContinuousLinearMap.isBoundedLinearMap (fun (x : (i : ι) → E i) =>L[R] x i)
+
+
 end SciLean.DifferentiableAt
 
 
@@ -162,6 +171,15 @@ def DifferentiableAt.fpropExt : FPropExt where
     }
     FProp.tryTheorem? e thm (fun _ => pure none)
 
+  projRule e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``DifferentiableAt.proj_rule 
+      origin := .decl ``DifferentiableAt.proj_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
   discharger e := 
     FProp.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption") e
 

SciLean/Tactic/FProp/Basic.lean

@@ -28,6 +28,31 @@ def tacticToDischarge (tacticCode : Syntax) : Expr → MetaM (Option Expr) := fu
 
     return result?
 
+def applyBVarApp (e : Expr) : FPropM (Option Expr) := do
+  let .some (fpropName, ext, F) ← getFProp? e
+    | return none
+
+  let .lam n t (.app f x) bi := F
+    | trace[Meta.Tactic.fprop.step] "bvar app step can't handle functions like {← ppExpr F}"
+      return none
+
+  if x.hasLooseBVars then
+    trace[Meta.Tactic.fprop.step] "bvar app step can't handle functions like {← ppExpr F}"
+    return none
+
+
+  if f == .bvar 0 then
+    ext.projRule e
+  else
+    let g := .lam n t f bi
+    let gType ← inferType g
+    let fType := gType.getForallBody
+    if fType.hasLooseBVars then
+      trace[Meta.Tactic.fprop.step] "bvar app step can't handle dependent functions of type {← ppExpr fType} appearing in {← ppExpr F}"
+      return none
+
+    let h := .lam n fType  ((Expr.bvar 0).app x) bi
+    ext.compRule e h g
 
 /-- Takes lambda function `fun x => b` and splits it into composition of two functions. 
 
@@ -163,6 +188,9 @@ mutual
       else if b.getAppFn.isFVar then
         trace[Meta.Tactic.fprop.step] "case fvar app\n{← ppExpr e}"
         applyFVarApp e ext.discharger
+      else if b.getAppFn.isBVar then
+        trace[Meta.Tactic.fprop.step] "case bvar app\n{← ppExpr e}"
+        applyBVarApp e
       else
         trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}\n"
         applyTheorems e (ext.discharger)
@@ -212,8 +240,7 @@ mutual
       if let some proof ← tryTheorem? e thm discharge? then
         return proof
 
-    return none -- ext.lambdaLetRule e
-    -- return none
+    return none 
 
   partial def synthesizeInstance (thmId : Origin) (x type : Expr) : MetaM Bool := do
     match (← trySynthInstance type) with

SciLean/Tactic/FProp/Init.lean

@@ -54,6 +54,8 @@ structure _root_.SciLean.FPropExt where
   identityRule     (expr : Expr) : FPropM (Option Expr)
   /-- Custom rule for proving property of `fun x => y -/
   constantRule     (expr : Expr) : FPropM (Option Expr)
+  /-- Custom rule for proving property of `fun x => x i -/
+  projRule          (expr : Expr) : FPropM (Option Expr)
   /-- Custom rule for proving property of `fun x => f (g x)` or `fun x => let y := g x; f y` -/
   compRule         (expr f g : Expr) : FPropM (Option Expr)
   /-- Custom rule for proving property of `fun x => let y := g x; f x y -/