new classes VecStruct and SemiInnerProductSpaceStruct

SciLean/Core/FunctionTransformations/RevDerivProj.lean

@@ -14,11 +14,13 @@ variable
   {W : Type _} [SemiInnerProductSpace K W]
   {ι : Type _} [EnumType ι]
   {E I : Type _} {EI : I → Type _} 
-  [StructLike E I EI]
+  [StructLike E I EI] [EnumType I]
   [SemiInnerProductSpace K E] [∀ i, SemiInnerProductSpace K (EI i)]
+  [SemiInnerProductSpaceStruct K E I EI]
   {F J : Type _} {FJ : J → Type _} 
-  [StructLike F J FJ]
+  [StructLike F J FJ] [EnumType J]
   [SemiInnerProductSpace K F] [∀ j, SemiInnerProductSpace K (FJ j)]
+  [SemiInnerProductSpaceStruct K F J FJ]
 
 noncomputable
 def revDerivProj
@@ -31,9 +33,8 @@ def revDerivProj
 noncomputable
 def revDerivProjUpdate
   (f : X → E) (x : X) : E×((i : I)→EI i→X→X) :=
-  let ydf' := revDerivUpdate K f x
-  (ydf'.1, fun i de dx => 
-    ydf'.2 (have := Classical.propDecidable; StructLike.make fun i' => if h:i=i' then h▸de else 0) 1 dx)
+  let ydf' := revDerivProj K f x
+  (ydf'.1, fun i de dx => dx + ydf'.2 i de)
 
 
 --------------------------------------------------------------------------------
@@ -61,11 +62,19 @@ theorem revDerivProjUpdate.id_rule
        fun i de dx => 
          StructLike.modify i (fun ei => ei + de) dx) := 
 by
-  simp[revDerivProjUpdate]
-  ftrans
-  sorry_proof
+  funext x
+  simp[revDerivProjUpdate, revDerivProj.id_rule]
+  funext i de dx
+  apply StructLike.ext
+  intro i'
+  if h : i=i' then
+    subst h; simp
+  else
+    simp[StructLike.proj_modify' _ _ _ _ h, h]
+
 variable {E}
 
+
 variable (Y)
 theorem revDerivProj.const_rule (x : E)
   : revDerivProj K (fun _ : Y => x)
@@ -84,8 +93,8 @@ theorem revDerivProjUpdate.const_rule (x : E)
       (x,
        fun i de dx => dx) := 
 by
-  simp[revDerivProjUpdate];
-  ftrans
+  simp[revDerivProjUpdate,revDerivProj.const_rule]
+
 variable {Y}
 
 
@@ -103,7 +112,21 @@ theorem revDerivProj.proj_rule [DecidableEq I] (i : ι)
         else 
           0) := 
 by
-  sorry_proof
+  simp[revDerivProj]
+  ftrans
+  funext x; simp
+  funext j dxj i'
+  apply StructLike.ext
+  intro j'
+  if h:i=i' then
+    subst h; simp
+    if h:j=j' then
+      subst h; simp
+    else
+      simp[h]
+  else
+    simp[h]
+
 
 
 theorem revDerivProjUpdate.proj_rule [DecidableEq I] (i : ι)
@@ -116,7 +139,19 @@ theorem revDerivProjUpdate.proj_rule [DecidableEq I] (i : ι)
         else 
           df i') := 
 by
-  sorry_proof
+  funext x;
+  simp[revDerivProjUpdate, revDerivProj.proj_rule]
+  funext j dxj f i'
+  apply StructLike.ext
+  intro j'
+  if h :i=i' then
+    subst h; simp
+    if h:j=j' then
+      subst h; simp
+    else
+      simp[h]
+  else
+    simp[h]
 
 
 theorem revDerivProj.comp_rule
@@ -131,7 +166,8 @@ theorem revDerivProj.comp_rule
        fun i de => 
          ydg'.2 (zdf'.2 i de)) := 
 by
-  sorry_proof
+  simp[revDerivProj]
+  ftrans
 
 
 theorem revDerivProjUpdate.comp_rule
@@ -146,7 +182,16 @@ theorem revDerivProjUpdate.comp_rule
        fun i de dx => 
          ydg'.2 (zdf'.2 i de) 1 dx) := 
 by
-  sorry_proof
+  funext x
+  simp[revDerivProjUpdate,revDerivProj.comp_rule]
+  constructor
+  . sorry
+  . 
+    funext i de dx
+    if h :i=i' then
+      subst h; simp
+    else
+      simp[h]
 
 
 theorem revDerivProj.let_rule

SciLean/Data/StructLike/Algebra.lean

@@ -8,30 +8,101 @@ namespace SciLean
 
 variable
   (K : Type _) [IsROrC K]
-  {X : Type _} [SemiInnerProductSpace K X]
-  {Y : Type _} [SemiInnerProductSpace K Y]
-  {Z : Type _} [SemiInnerProductSpace K Z]
-  {W : Type _} [SemiInnerProductSpace K W]
   {ι κ : Type _} [EnumType ι] [EnumType κ]
   {E I : Type _} {EI : I → Type _}
   [StructLike E I EI]
   {F J : Type _} {FJ : J → Type _}
   [StructLike F J FJ]
 
 
+open StructLike in
+class VecStruct (K X I XI) [StructLike X I XI] [IsROrC K] [Vec K X] [∀ i, Vec K (XI i)] : Prop where
+  proj_add : ∀ i (x x' : X), proj (x + x') i = proj x i + proj x' i
+  proj_smul : ∀ i (k : K) (x : X), proj (k • x) i = k • proj x i
+  proj_zero : ∀ i, proj (0 : X) i = 0
+  proj_continuous : Continuous (fun (x : X) i =>  proj x i)
+  make_continuous : Continuous (fun f => make (X:=X) f)
+
+attribute [simp] VecStruct.proj_add VecStruct.proj_smul VecStruct.proj_zero
+
+open StructLike in
+class SemiInnerProductSpaceStruct (K X I XI) [StructLike X I XI] [IsROrC K] [EnumType I] [SemiInnerProductSpace K X] [∀ i, SemiInnerProductSpace K (XI i)] extends VecStruct K X I XI : Prop where
+  inner_proj : ∀ (x x' : X), ⟪x,x'⟫[K] = ∑ (i : I), ⟪proj x i, proj x' i⟫[K]
+  testFun_proj : ∀ (x : X), TestFunction x ↔ (∀ i, TestFunction (proj x i))
+
+
+@[reducible]
 instance [∀ i, Vec K (EI i)] [∀ j, Vec K (FJ j)] (i : I ⊕ J) : Vec K (Prod.TypeFun EI FJ i) := 
   match i with
   | .inl _ => by infer_instance
   | .inr _ => by infer_instance
 
+
+instance [Vec K E] [Vec K F] [∀ i, Vec K (EI i)] [∀ j, Vec K (FJ j)] 
+  [VecStruct K E I EI] [VecStruct K F J FJ]
+  : VecStruct K (E×F) (I⊕J) (Prod.TypeFun EI FJ) where
+  proj_add := by simp[StructLike.proj]
+  proj_smul := by simp[StructLike.proj]
+  proj_zero := by simp[StructLike.proj]
+  proj_continuous := sorry_proof
+  make_continuous := sorry_proof
+
+
 instance [∀ i, SemiInnerProductSpace K (EI i)] [∀ j, SemiInnerProductSpace K (FJ j)] (i : I ⊕ J) 
-  : SemiInnerProductSpace K (Prod.TypeFun EI FJ i) := 
+  : SemiInnerProductSpace K (Prod.TypeFun EI FJ i) :=
   match i with
   | .inl _ => by infer_instance
   | .inr _ => by infer_instance
 
+
+instance 
+  [SemiInnerProductSpace K E] [SemiInnerProductSpace K F] 
+  [∀ i, SemiInnerProductSpace K (EI i)] [∀ j, SemiInnerProductSpace K (FJ j)] 
+  [EnumType I] [EnumType J]
+  [SemiInnerProductSpaceStruct K E I EI] [SemiInnerProductSpaceStruct K F J FJ]
+  : SemiInnerProductSpaceStruct K (E×F) (I⊕J) (Prod.TypeFun EI FJ) := sorry_proof
+  -- inner_proj := sorry_proof
+  -- testFun_proj := sorry_proof
+
+
 instance [∀ i, FinVec ι K (EI i)] [∀ j, FinVec ι K (FJ j)] (i : I ⊕ J) 
   : FinVec ι K (Prod.TypeFun EI FJ i) := 
   match i with
   | .inl _ => by infer_instance
   | .inr _ => by infer_instance
+
+
+open StructLike
+
+
+variable 
+  {X XI} [StructLike X I XI] [Vec K X] [∀ i, Vec K (XI i)] [VecStruct K X I XI]
+
+@[simp]
+theorem make_zero
+  : make (X:=X) (fun _ => 0)
+    =
+    0 :=
+by
+  apply StructLike.ext
+  simp[VecStruct.proj_zero]
+
+
+@[simp]
+theorem make_add (f g : (i : I) →  XI i)
+  : make (X:=X) f + make g 
+    =
+    make (fun i => f i + g i) :=
+by
+  apply StructLike.ext
+  simp[VecStruct.proj_add]
+
+
+@[simp]
+theorem make_smul (k : K) (f : (i : I) →  XI i)
+  : k • make (X:=X) f 
+    =
+    make (fun i => k • f i) :=
+by
+  apply StructLike.ext
+  simp[VecStruct.proj_smul]

SciLean/Data/StructLike/Basic.lean

@@ -6,13 +6,34 @@ namespace SciLean
 
 open Function
 
-class StructLike (E : Sort _) (I : outParam (Sort _)) (EI : outParam <| I → Sort _) where
-  proj : E → (i : I) → (EI i)
-  make : ((i : I) → (EI i)) → E
-  modify : (i : I) → (EI i → EI i) → (E → E)
-  left_inv : LeftInverse proj intro
-  right_inv : RightInverse proj intro
-  -- TODO: theorem about modify
+class StructLike (X : Sort _) (I : outParam (Sort _)) (XI : outParam <| I → Sort _) where
+  proj (x : X) (i : I) : (XI i)
+  make (f : (i : I) → (XI i)) : X
+  modify (i : I) (f : XI i → XI i) (x : X) : X
+  left_inv : LeftInverse proj make
+  right_inv : RightInverse proj make
+  proj_modify : ∀ i f x, 
+    proj (modify i f x) i = f (proj x i)
+  proj_modify' : ∀ i j f x, 
+    i ≠ j → proj (modify i f x) j = proj x j
+
+namespace StructLike
+
+variable {X I XI} [StructLike X I XI]
+
+attribute [simp] proj_modify proj_modify'
+
+@[simp]
+theorem proj_make (f : (i : I) → XI i) (i : I)
+  : proj (X:=X) (make f) i = f i := by apply congr_fun; apply left_inv
+
+@[simp]
+theorem make_proj (x : X)
+  : make (X:=X) (fun i => proj x i) = x := by apply right_inv
+
+theorem ext (x x' : X) : (∀ i, proj x i = proj x' i) → x = x' := 
+by
+  intro h; rw[← make_proj x]; rw[← make_proj x']; simp[h]
 
 
 /-- Every type is `StructLike` with `Unit` as index set.
@@ -21,14 +42,16 @@ instance (priority:=low) : StructLike α Unit (fun _ => α) where
   proj := fun x _ => x
   make := fun f => f ()
   modify := fun _ f x => f x
-  left_inv := sorry_proof
-  right_inv := sorry_proof
+  left_inv := by simp[LeftInverse]
+  right_inv := by simp[Function.RightInverse, LeftInverse]
+  proj_modify := by simp
+  proj_modify' := by simp
 
 --------------------------------------------------------------------------------
 -- Pi --------------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
-instance (priority:=low) 
+instance (priority:=low+1) 
   (I : Type _) (E : I → Type _)
   (J : I → Type _) (EJ : (i : I) → (J i) → Type _)
   [∀ (i : I), StructLike (E i) (J i) (EJ i)] [DecidableEq I]
@@ -40,8 +63,10 @@ instance (priority:=low)
       StructLike.modify (h▸j) (h▸f) (x i')
     else
       (x i')
-  left_inv := sorry_proof
-  right_inv := sorry_proof
+  left_inv := by simp[LeftInverse]
+  right_inv := by simp[Function.RightInverse, LeftInverse]
+  proj_modify := by simp
+  proj_modify' := by sorry_proof
 
 instance
   (E I J : Type _) (EI : I → Type _)
@@ -50,13 +75,14 @@ instance
   proj := fun f (j,i) => StructLike.proj (f j) i
   make := fun f j => StructLike.make fun i => f (j,i)
   modify := fun (j,i) f x j' =>   
-    if h : j=j' then
+    if j=j' then
       StructLike.modify i f (x j)
     else
       (x j')
-
-  left_inv := sorry_proof
-  right_inv := sorry_proof
+  left_inv := by simp[LeftInverse]
+  right_inv := by simp[Function.RightInverse, LeftInverse]
+  proj_modify := by simp
+  proj_modify' := by intro (j,i) (j',i') f x _h; simp; sorry_proof
 
 
 --------------------------------------------------------------------------------
@@ -80,31 +106,16 @@ instance [StructLike E I EI] [StructLike F J FJ]
     match i with
     | .inl a => (StructLike.modify a f x, y)
     | .inr b => (x, StructLike.modify b f y)
-  left_inv := sorry_proof
-  right_inv := sorry_proof
+  left_inv := by intro x; funext i; induction i <;> simp[LeftInverse]
+  right_inv := by simp[Function.RightInverse, LeftInverse]
+  proj_modify := by simp
+  proj_modify' := by intro i j f x h; induction j <;> induction i <;> (simp at h; simp (disch:=assumption))
 
 
 
 --------------------------------------------------------------------------------
 -- TODO: Add some lawfulness w.r.t. to +,•,0
 
-@[simp]
-theorem StruckLike.make_zero
-  {X I : Type}  {XI : I → Type} [StructLike X I XI] 
-  [Zero X] [∀ i, Zero (XI i)]
-  : StructLike.make (E:=X) (fun _ => 0)
-    =
-    0 :=
-by
-  sorry
 
+
 
-@[simp]
-theorem StruckLike.make_add
-  {X I : Type}  {XI : I → Type} [StructLike X I XI] 
-  [Zero X] [∀ i, Zero (XI i)]
-  : StructLike.make (E:=X) (fun _ => 0)
-    =
-    0 :=
-by
-  sorry