Removed usage of Fintype and use exclusively EnumType

SciLean/Core/FunctionPropositions/HasAdjDiff.lean

@@ -13,7 +13,7 @@ variable
   {X : Type _} [SemiInnerProductSpace K X]
   {Y : Type _} [SemiInnerProductSpace K Y]
   {Z : Type _} [SemiInnerProductSpace K Z]
-  {ι : Type _} [Fintype ι] [DecidableEq ι]
+  {ι : Type _} [EnumType ι]
   {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)]
 
 def HasAdjDiff (f : X → Y)  : Prop := IsDifferentiable K f ∧ ∀ x, HasSemiAdjoint K (cderiv K f x)
@@ -174,7 +174,7 @@ variable
   {X : Type _} [SemiInnerProductSpace K X]
   {Y : Type _} [SemiInnerProductSpace K Y]
   {Z : Type _} [SemiInnerProductSpace K Z]
-  {ι : Type _} [Fintype ι] [DecidableEq ι]
+  {ι : Type _} [EnumType ι]
   {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)] 
 
 

SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean

@@ -12,7 +12,7 @@ variable
   {X : Type _} [SemiInnerProductSpace K X]
   {Y : Type _} [SemiInnerProductSpace K Y]
   {Z : Type _} [SemiInnerProductSpace K Z]
-  {ι : Type _} [Fintype ι] [DecidableEq ι]
+  {ι : Type _} [EnumType ι]
   {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)] 
 
 def HasAdjDiffAt (f : X → Y) (x : X) : Prop :=

SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean

@@ -12,7 +12,7 @@ variable
   {X : Type _} [SemiInnerProductSpace K X]
   {Y : Type _} [SemiInnerProductSpace K Y]
   {Z : Type _} [SemiInnerProductSpace K Z]
-  {ι : Type _} [Fintype ι] [DecidableEq ι]
+  {ι : Type _} [EnumType ι]
   {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)] 
 
 def HasSemiAdjoint (f : X → Y) : Prop :=
@@ -91,13 +91,12 @@ by
   apply Exists.intro (fun z => semiAdjoint K (fun x => (x, g x)) (semiAdjoint K (fun (xy : X×Y) => f xy.1 xy.2) z)) _
   sorry_proof
 
-open BigOperators in
 theorem pi_rule
   (f : (i : ι) → X → E i)
   (hf : ∀ i, HasSemiAdjoint K (f i))
   : HasSemiAdjoint K (fun x i => f i x) := 
 by 
-  apply Exists.intro (fun g => ∑ i, semiAdjoint K (f i) (g i)) _
+  -- apply Exists.intro (fun g => ∑ i, semiAdjoint K (f i) (g i)) _
   sorry_proof
 
 --------------------------------------------------------------------------------

SciLean/Core/FunctionTransformations/RevCDeriv.lean

@@ -16,7 +16,7 @@ variable
   {X : Type _} [SemiInnerProductSpace K X]
   {Y : Type _} [SemiInnerProductSpace K Y]
   {Z : Type _} [SemiInnerProductSpace K Z]
-  {ι : Type _} [Fintype ι]
+  {ι : Type _} [EnumType ι]
   {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)]
 
 
@@ -91,7 +91,7 @@ by
 variable{X}
 
 variable(E)
-theorem proj_rule [DecidableEq ι] (i : ι)
+theorem proj_rule (i : ι)
   : revCDeriv K (fun (x : (i:ι) → E i) => x i)
     = 
     fun x => 
@@ -141,7 +141,6 @@ by
   funext _; ftrans; ftrans 
 
 
-open BigOperators in
 theorem pi_rule
   (f :  X → (i : ι) → E i) (hf : ∀ i, HasAdjDiff K (f · i))
   : (revCDeriv K fun (x : X) (i : ι) => f x i)
@@ -197,7 +196,6 @@ by
   funext _; simp; sorry_proof
 
 
-open BigOperators in
 theorem pi_rule_at
   (f : X → (i : ι) → E i) (x : X) (hf : ∀ i, HasAdjDiffAt K (f · i) x)
   : (revCDeriv K fun (x : X) (i : ι) => f x i)
@@ -320,7 +318,7 @@ variable
   {Y : Type _} [SemiInnerProductSpace K Y]
   {Z : Type _} [SemiInnerProductSpace K Z]
   {W : Type _} [SemiInnerProductSpace K W]
-  {ι : Type _} [Fintype ι]
+  {ι : Type _} [EnumType ι]
   {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)]
 
 
@@ -658,27 +656,6 @@ by
   unfold revCDeriv; simp; funext dx; ftrans; ftrans; simp[smul_smul]; ring_nf
 
 
--- EnumType.sum ----------------------------------------------------------------
--------------------------------------------------------------------------------- 
-
-open BigOperators in
-@[ftrans]
-theorem Finset.sum.arg_f.revCDeriv_rule {ι : Type _} [Fintype ι]
-  (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i))
-  : revCDeriv K (fun x => ∑ i, f x i)
-    =
-    fun x => 
-      let ydf := revCDeriv K (fun x i => f x i) x
-      (∑ i, ydf.1 i, 
-       fun dy => ydf.2 (fun _ => dy)) :=
-by
-  have _ := fun i => (hf i).1
-  have _ := fun i => (hf i).2
-  simp [revCDeriv]
-  funext x; simp
-  ftrans
-  sorry_proof
-
 
 -- EnumType.sum ----------------------------------------------------------------
 -------------------------------------------------------------------------------- 

SciLean/Core/FunctionTransformations/SemiAdjoint.lean

@@ -11,7 +11,7 @@ variable
   {X : Type _} [SemiInnerProductSpace K X]
   {Y : Type _} [SemiInnerProductSpace K Y]
   {Z : Type _} [SemiInnerProductSpace K Z]
-  {ι : Type _} [Fintype ι]
+  {ι : Type _} [EnumType ι]
   {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)]
 
 namespace semiAdjoint
@@ -60,7 +60,6 @@ theorem let_rule
       xy.1 + x' := 
 by sorry_proof
 
-open BigOperators in
 theorem pi_rule
   (f : X → (i : ι) → E i) (hf : ∀ i, HasSemiAdjoint K (f · i))
   : semiAdjoint K (fun (x : X) (i : ι) => f x i)

SciLean/Core/Objects/FinVec.lean

@@ -1,6 +1,6 @@
 import SciLean.Core.Objects.SemiInnerProductSpace
 
-open BigOperators ComplexConjugate
+open ComplexConjugate
 
 namespace SciLean
 
@@ -105,19 +105,19 @@ class OrthonormalBasis (ι K X : Type _) [Semiring K] [Basis ι K X] [Inner K X]
 
 /--
  -/
-class FinVec (ι : outParam $ Type _) (K : Type _) (X : Type _) [outParam $ Fintype ι] [IsROrC K] [DecidableEq ι] extends SemiInnerProductSpace K X, Basis ι K X, DualBasis ι K X, BasisDuality X where
+class FinVec (ι : outParam $ Type _) (K : Type _) (X : Type _) [outParam $ EnumType ι] [IsROrC K] extends SemiInnerProductSpace K X, Basis ι K X, DualBasis ι K X, BasisDuality X where
   is_basis : ∀ x : X, x = ∑ i : ι, ℼ i x • ⅇ[X] i
   duality : ∀ i j, ⟪ⅇ[X] i, ⅇ'[X] j⟫[K] = if i=j then 1 else 0
   to_dual   : toDual   x = ∑ i,  ℼ i x • ⅇ'[X] i
   from_dual : fromDual x = ∑ i, ℼ' i x •  ⅇ[X] i
 
-theorem basis_ext {ι K X} {_ : Fintype ι} [DecidableEq ι] [IsROrC K] [FinVec ι K X] (x y : X)
+theorem basis_ext {ι K X} {_ : EnumType ι} [IsROrC K] [FinVec ι K X] (x y : X)
   : (∀ i, ⟪x, ⅇ i⟫[K] = ⟪y, ⅇ i⟫[K]) → (x = y) := sorry_proof
 
-theorem dualBasis_ext {ι K X} {_ : Fintype ι} [DecidableEq ι] [IsROrC K] [FinVec ι K X] (x y : X)
+theorem dualBasis_ext {ι K X} {_ : EnumType ι}  [IsROrC K] [FinVec ι K X] (x y : X)
   : (∀ i, ⟪x, ⅇ' i⟫[K] = ⟪y, ⅇ' i⟫[K]) → (x = y) := sorry_proof
 
-theorem inner_proj_dualProj {ι K X} {_ : Fintype ι} [DecidableEq ι] [IsROrC K] [FinVec ι K X] (x y : X)
+theorem inner_proj_dualProj {ι K X} {_ : EnumType ι} [IsROrC K] [FinVec ι K X] (x y : X)
   : ⟪x, y⟫[K] = ∑ i, ℼ i x * ℼ' i y :=
 by 
   calc 
@@ -126,7 +126,7 @@ by
          _ = ∑ i, ∑ j, (ℼ i x * ℼ' j y) * if i=j then 1 else 0 := by simp [FinVec.duality]
          _ = ∑ i, ℼ i x * ℼ' i y := sorry_proof -- summing over [[i=j]]  
 
-variable {ι K X} {_ : Fintype ι} [DecidableEq ι] [IsROrC K] [FinVec ι K X]
+variable {ι K X} {_ : EnumType ι} [IsROrC K] [FinVec ι K X]
 
 @[simp]
 theorem inner_basis_dualBasis (i j : ι)
@@ -141,11 +141,11 @@ by sorry_proof
 @[simp]
 theorem inner_dualBasis_proj  (i : ι) (x : X)
   : ⟪x, ⅇ' i⟫[K] = ℼ i x :=
-by 
-  calc
-    ⟪x, ⅇ' i⟫[K] = ⟪∑ j, ℼ j x • ⅇ[X] j, ⅇ' i⟫[K] := by sorry_proof -- rw[← (FinVec.is_basis x)]
-            _ = ∑ j, ℼ j x * if j=i then 1 else 0 := by sorry_proof -- inner_basis_dualBasis and some linearity
-            _ = ℼ i x := by sorry_proof
+by sorry_proof
+  -- calc
+  --   ⟪x, ⅇ' i⟫[K] = ⟪∑ j, ℼ j x • ⅇ[X] j, ⅇ' i⟫[K] := by sorry_proof -- rw[← (FinVec.is_basis x)]
+  --           _ = ∑ j, ℼ j x * if j=i then 1 else 0 := by sorry_proof -- inner_basis_dualBasis and some linearity
+  --           _ = ℼ i x := by sorry_proof
 
 @[simp]
 theorem inner_basis_dualProj (i : ι) (x : X)
@@ -163,7 +163,7 @@ theorem dualProj_dualBasis (i j : ι)
 by simp only [←inner_basis_dualProj, inner_dualBasis_basis, eq_comm]; done
 
 instance : FinVec Unit K K where
-  is_basis := by simp[Basis.proj, Basis.basis]
+  is_basis := by simp[Basis.proj, Basis.basis]; sorry_proof
   duality := by simp[Basis.proj, Basis.basis, DualBasis.dualProj, DualBasis.dualBasis, Inner.inner]; done
   to_dual := by sorry_proof
   from_dual := by sorry_proof
@@ -173,7 +173,7 @@ instance : OrthonormalBasis Unit K K where
   is_orthonormal := sorry_proof
 
 -- @[infer_tc_goals_rl]
-instance {ι κ K X Y} {_ : Fintype ι} {_ : Fintype κ} [DecidableEq ι] [DecidableEq κ] [IsROrC K] [FinVec ι K X] [FinVec κ K Y]
+instance {ι κ K X Y} {_ : EnumType ι} {_ : EnumType κ} [IsROrC K] [FinVec ι K X] [FinVec κ K Y]
   : FinVec (ι⊕κ) K (X×Y) where
   is_basis := sorry_proof
   duality := sorry_proof

SciLean/Core/Objects/SemiInnerProductSpace.lean

@@ -7,7 +7,7 @@ import SciLean.Data.EnumType
 
 namespace SciLean
 
-open IsROrC ComplexConjugate BigOperators
+open IsROrC ComplexConjugate
 
 /-- Square of L₂ norm over the field `K` -/
 class Norm2 (K X : Type _) where
@@ -69,14 +69,14 @@ end NotationOverField
 instance (K X Y) [AddCommMonoid K] [Inner K X] [Inner K Y] : Inner K (X × Y) where
   inner := λ (x,y) (x',y') => ⟪x,x'⟫[K] + ⟪y,y'⟫[K]
 
-instance (K X) [AddCommMonoid K] [Inner K X] (ι) [Fintype ι] : Inner K (ι → X) where
-  inner := λ f g => ∑ i, ⟪f i, g i⟫[K]
+-- instance (K X) [AddCommMonoid K] [Inner K X] (ι) [Fintype ι] : Inner K (ι → X) where
+--   inner := λ f g => ∑ i, ⟪f i, g i⟫[K]
 
-instance (K X) [AddCommMonoid K] [Inner K X] (ι) [EnumType ι] : Inner K (ι → X) where
-  inner := λ f g => EnumType.sum fun i => ⟪f i, g i⟫[K]
+-- instance (K X) [AddCommMonoid K] [Inner K X] (ι) [EnumType ι] : Inner K (ι → X) where
+--   inner := λ f g => EnumType.sum fun i => ⟪f i, g i⟫[K]
 
 instance (priority:=low) (K ι) (X : ι → Type) 
-  [AddCommMonoid K] [∀ i, Inner K (X i)] [Fintype ι] 
+  [AddCommMonoid K] [∀ i, Inner K (X i)] [EnumType ι] 
   : Inner K ((i : ι) → X i) where
   inner := λ f g => ∑ i, ⟪f i, g i⟫[K]
 
@@ -99,8 +99,8 @@ export TestFunctions (TestFunction)
 instance (X Y) [TestFunctions X] [TestFunctions Y] : TestFunctions (X×Y) where
   TestFunction xy := TestFunction xy.1 ∧ TestFunction xy.2
 
-instance (X ι : Type _) [TestFunctions X]  : TestFunctions (ι → X) where
-  TestFunction f := ∀ i, TestFunction (f i)
+-- instance (X ι : Type _) [TestFunctions X]  : TestFunctions (ι → X) where
+--   TestFunction f := ∀ i, TestFunction (f i)
 
 instance (priority:=low) (ι : Type _) (X : ι → Type) [∀ i, TestFunctions (X i)]
   : TestFunctions ((i : ι) → X i) where
@@ -223,8 +223,8 @@ abbrev SemiInnerProductSpace.mkSorryProofs {α} [Vec K α] [Inner K α] [TestFun
 
 instance (X Y) [SemiInnerProductSpace K X] [SemiInnerProductSpace K Y] : SemiInnerProductSpace K (X × Y) := SemiInnerProductSpace.mkSorryProofs
 
-instance (X) [SemiInnerProductSpace K X] (ι) [Fintype ι] : SemiInnerProductSpace K (ι → X) := SemiInnerProductSpace.mkSorryProofs
-instance (X) [SemiInnerProductSpace K X] (ι) [EnumType ι] : SemiInnerProductSpace K (ι → X) := SemiInnerProductSpace.mkSorryProofs
-instance (priority:=low) (ι) (X : ι → Type) [∀ i, SemiInnerProductSpace K (X i)] [Fintype ι] : SemiInnerProductSpace K ((i : ι) → X i) 
+-- instance (X) [SemiInnerProductSpace K X] (ι) [Fintype ι] : SemiInnerProductSpace K (ι → X) := SemiInnerProductSpace.mkSorryProofs
+-- instance (X) [SemiInnerProductSpace K X] (ι) [EnumType ι] : SemiInnerProductSpace K (ι → X) := SemiInnerProductSpace.mkSorryProofs
+instance (priority:=low) (ι) (X : ι → Type) [∀ i, SemiInnerProductSpace K (X i)] [EnumType ι] : SemiInnerProductSpace K ((i : ι) → X i) 
   := SemiInnerProductSpace.mkSorryProofs
 

SciLean/Core/Objects/Vec.lean

@@ -111,14 +111,14 @@ section CommonVectorSpaces
   instance [IsROrC K] : Vec K K where
     scalar_wise_smooth := sorry_proof
 
-  instance [inst : Vec K U] : Vec K (α → U) := 
-    -- option 1:
-    -- Vec.mkSorryProofs
-    -- option 2:
-    -- have : Module K U := inst.toModule
-    -- Vec.mk
-    -- option 3:
-    by cases inst; apply Vec.mk (scalar_wise_smooth := sorry_proof)
+  -- instance [inst : Vec K U] : Vec K (α → U) := 
+  --   -- option 1:
+  --   -- Vec.mkSorryProofs
+  --   -- option 2:
+  --   -- have : Module K U := inst.toModule
+  --   -- Vec.mk
+  --   -- option 3:
+  --   by cases inst; apply Vec.mk (scalar_wise_smooth := sorry_proof)
 
 
   instance(priority:=low) (α : Type _) (X : α → Type _) [inst : ∀ a, Vec K (X a)] : Vec K ((a : α) → X a) := 

SciLean/Data/Idx.lean

@@ -1,3 +1,4 @@
+import Mathlib.Data.Fintype.Basic
 import SciLean.Util.SorryProof
 
 namespace SciLean
@@ -66,10 +67,19 @@ instance : OfNat (Idx (no_index (n+1))) i where
 instance : Inhabited (Idx (no_index (n+1))) where
   default := 0
 
+instance : Fintype (Idx n) where
+  elems := {
+      val := Id.run do
+        let mut l : List (Idx n) := []
+        for i in [0:n.toNat] do
+          l := ⟨i.toUSize, sorry_proof⟩ :: l
+        Multiset.ofList l.reverse
+      nodup := sorry_proof
+    }
+  complete := sorry_proof
+
 
 instance (n : Nat) : Nonempty (Idx (no_index (OfNat.ofNat (n+1)))) := sorry_proof
 instance (n : Nat) : OfNat (Idx (no_index (OfNat.ofNat (n+1)))) i := ⟨(i % (n+1)).toUSize, sorry_proof⟩
 
-
-
 -- #check (0 : Idx 10)