...

Author: lecopivo

SciLean/Analysis/Calculus/Monad/StateT.lean

@@ -26,15 +26,12 @@ instance (S : Type) [NormedAddCommGroup S] [NormedSpace K S] :
 
   DifferentiableM_bind f g hf hg :=
     by
-      simp; simp at hf; simp at hg
       simp[bind, StateT.bind]
       fun_prop
 
   DifferentiableM_pair f hf :=
     by
-      simp; simp at hf
       simp[bind, StateT.bind, pure, StateT.pure, Functor.map]
-      simp only [StateT.map]
       fun_prop
 
 

SciLean/Analysis/Scalar/Basic.lean

@@ -19,6 +19,7 @@ namespace SciLean
 
 open Classical
 
+
 /-- `K` are real or complex numbers over real numbers `R`
 
 This class allows us to write code independent of particular implementation of real or complex numbers.
@@ -115,7 +116,9 @@ This class allows us to write code independent of particular implementation of r
 
 See `Scalar` for motivation for this class.
 -/
-class RealScalar (R :(Type _)) extends Scalar R R, LinearOrder R where
+class RealScalar (R : Type*) extends Scalar R R where
+  [order : LinearOrder R]
+
   is_real : ∀ x : R, im x = 0
 
   asin (x : R) : R
@@ -127,6 +130,8 @@ class RealScalar (R :(Type _)) extends Scalar R R, LinearOrder R where
   atan (x : R) : R
   atan_def : ∀ x, toReal (atan x) = Real.arctan (toReal x)
 
+instance {R : Type*} [RealScalar R] : LinearOrder R := RealScalar.order
+
 def RealScalar.pi [RealScalar R] : R := RealScalar.acos (-1)
 
 scoped notation "π" => @RealScalar.pi defaultScalar% inferInstance
@@ -282,10 +287,10 @@ noncomputable instance : RealScalar ℝ where
   pow_def := by intros; simp; rfl
 
   abs x := abs x
-  abs_def := by intros; simp; sorry_proof
+  abs_def := by intros; sorry_proof
 
   tgamma x := x.Gamma
-  tgamma_def := by intros; simp; sorry_proof
+  tgamma_def := by intros;sorry_proof
 
   lgamma x := |x.Gamma|.log
   lgamma_def := by intros; simp; sorry_proof
@@ -296,36 +301,7 @@ noncomputable instance : RealScalar ℝ where
   isNaN x := false
   isInf x := false
 
-  le_total := by sorry_proof
-
-  decidableLE x y :=
-    have := Classical.propDecidable
-    if h : x ≤ y then
-      .isTrue h
-    else
-      .isFalse h
-
-  decidableEq x y :=
-    have := Classical.propDecidable
-    if h : x = y then
-      .isTrue h
-    else
-      .isFalse h
-
-  decidableLT x y :=
-    have := Classical.propDecidable
-    if h : x < y then
-      .isTrue h
-    else
-      .isFalse h
-
-  min := fun a b => if a ≤ b then a else b
-  max := fun a b => if a ≤ b then b else a
-  min_def := by sorry_proof
-  max_def := by sorry_proof
-  compare a b := compareOfLessAndEq a b
-  compare_eq_compareOfLessAndEq := by
-    compareOfLessAndEq_rfl
+  order := by infer_instance
 
 
 

SciLean/Analysis/Scalar/FloatAsReal.lean

@@ -213,15 +213,17 @@ instance : RealScalar Float where
   isInf x := x.isInf
   isFinite x := x.isFinite
 
-  le_total := by sorry_proof
-  decidableLE := inferInstance
-  decidableEq := inferInstance
-  decidableLT := inferInstance
-
-  min_def := by sorry_proof
-  max_def := by sorry_proof
-  compare x y := compare x y
-  compare_eq_compareOfLessAndEq := by sorry_proof
+  order := {
+    le_total := by sorry_proof
+    decidableLE := inferInstance
+    decidableEq := inferInstance
+    decidableLT := inferInstance
+
+    min_def := by sorry_proof
+    max_def := by sorry_proof
+    compare x y := compare x y
+    compare_eq_compareOfLessAndEq := by sorry_proof
+  }
 
 
 open ComplexConjugate

SciLean/Data/DataArray/Basis.lean

@@ -13,7 +13,7 @@ instance (priority:=high) : CanonicalBasis I R (R^[I]) where
   dualBasis i := setElem (0 : R^[I]) i 1 .intro
   proj i x := x[i]
   dualProj i x := x[i]
-  basis_complete := by intros; ext i; simp[sum_pull]; sorry_proof
+  basis_complete := by intros; ext i; sorry_proof
   proj_basis := by sorry_proof --classical intro i j; by_cases i = j <;> aesop
   dualProj_dualBasis :=  by sorry_proof --classical intro i j; by_cases i = j <;> aesop
   inner_basis_dualBasis := sorry_proof

SciLean/Data/DataArray/DataArray.lean

@@ -90,9 +90,9 @@ def DataArray.capacity (arr : DataArray α) : Squash Nat := Quot.mk _ (pd.capaci
   --     arr' := arr'.set ⟨i.1,sorry_proof⟩ (arr.get i)
   --   arr'
 
-def DataArray.mkEmpty (capacity : Nat) : DataArray α := Id.run do
+def DataArray.emptyWithCapacity (capacity : Nat) : DataArray α := Id.run do
   let newBytes := pd.bytes capacity
-  { byteData := .mkEmpty newBytes
+  { byteData := .emptyWithCapacity newBytes
     h_size := by sorry_proof }
 
 def DataArray.mkZero (n : Nat) : DataArray α := Id.run do
@@ -288,7 +288,7 @@ instance {ι α : Type*} {n} [IndexType ι n] [pd : PlainDataType α] :
 
     fromByteArray := λ b i h =>
       let N := pd.bytes n
-      let bi := b.copySlice (i.toNat) (ByteArray.mkEmpty N) 0 N
+      let bi := b.copySlice (i.toNat) (ByteArray.emptyWithCapacity N) 0 N
       ⟨⟨bi,sorry_proof⟩,sorry_proof⟩
     toByteArray   := λ b i h c => Id.run do
       let N := pd.bytes n
@@ -382,7 +382,7 @@ def DataArrayN.row (x : X^[I,J]) (i : I) := x.curry[i]
 
 def DataArrayN.col (x : X^[I,J]) (j : J) : X^[I] := Id.run do
   let xdata := x.1.1
-  let mut data := ByteArray.mkEmpty (pd.bytes nI)
+  let mut data := ByteArray.emptyWithCapacity (pd.bytes nI)
   let offset := (toIdx j).1
   let width := (pd.bytes 1).toUSize
   let stride := (pd.bytes nJ).toUSize

SciLean/Data/DataArray/TensorOperations.lean

@@ -43,20 +43,20 @@ def sumMiddleR (x : R^[I,J,K]) : R^[I,K] := Id.run do
 
 variable (I) in
 def replicateRowR (r : R^[J]) : R^[I,J] :=
-  let data : DataArray R := DataArray.mkEmpty (nI*nJ)
+  let data : DataArray R := DataArray.emptyWithCapacity (nI*nJ)
   ⟨data.pushArray r.1 nI, sorry_proof⟩
 
 
 variable (J) in
 def replicateColR (r : R^[I]) : R^[I,J] := Id.run do
-  let mut data : DataArray R := DataArray.mkEmpty (nI*nJ)
+  let mut data : DataArray R := DataArray.emptyWithCapacity (nI*nJ)
   for i in fullRange I do
     data := data.push r[i] nJ
   ⟨data, sorry_proof⟩
 
 variable (J) in
 def replicateMiddleR (x : R^[I,K]) : R^[I,J,K] := Id.run do
-  let mut data : DataArray R := DataArray.mkEmpty (nI*nJ*nK)
+  let mut data : DataArray R := DataArray.emptyWithCapacity (nI*nJ*nK)
   for i in fullRange I do
     -- TODO: fix this! it is slow! we make copies of `x`'s rows
     data := data.pushArray (x.curry[i]).1 nJ

SciLean/Data/StructType/Basic.lean

@@ -123,7 +123,7 @@ instance (priority:=low+1) instStrucTypePiSimple
   right_inv := by simp[Function.RightInverse, LeftInverse]
   structProj_structModify := by simp
   structProj_structModify' := by
-    intro i i'; intros _ _ H; simp
+    intro i i'; intros _ _ H
     if h: i' = i then
       simp [h] at H
     else
@@ -162,7 +162,7 @@ instance instStrucTypeArrowSimple
   right_inv := by simp[Function.RightInverse, LeftInverse]
   structProj_structModify := by simp
   structProj_structModify' := by
-    intro j j' f x H; simp
+    intro j j' f x H
     if h: j' = j then
       simp [h] at H
     else

SciLean/Data/Vector.lean

@@ -45,7 +45,7 @@ instance [Add X] : Add (Vector X n) := ⟨fun x y => x.mapFinIdx fun i xi _ => x
 instance [Sub X] : Sub (Vector X n) := ⟨fun x y => x.mapFinIdx fun i xi _ => xi - y[i]⟩
 instance [Neg X] : Neg (Vector X n) := ⟨fun x => x.map fun xi => -xi⟩
 instance [SMul R X] : SMul R (Vector X n) := ⟨fun r x => x.map fun xi => r • xi⟩
-instance [Zero X] : Zero (Vector X n) := ⟨⟨Array.mkArray n (0:X), by simp⟩⟩
+instance [Zero X] : Zero (Vector X n) := ⟨⟨Array.replicate n (0:X), by simp⟩⟩
 
 @[simp, simp_core]
 theorem Vector.getElem_add [Add X] (x y : Vector X n) (i : ℕ) (h : i < n) : (x + y)[i] = x[i] + y[i] := by

SciLean/Lean/Meta/Basic.lean

@@ -144,7 +144,7 @@ def mkAppNoTrailingM (constName : Name) (xs : Array Expr) : MetaM Expr := do
   -- number of arguments to apply
   let argCount := explicitArgIds[xs.size]? |>.getD n
 
-  let mut args : Array (Option Expr) := Array.mkArray argCount none
+  let mut args : Array (Option Expr) := Array.replicate argCount none
   for i in [0:xs.size] do
     args := args.set! explicitArgIds[i]! (.some xs[i]!)
 
@@ -203,7 +203,7 @@ def mkProdProj (x : Expr) (i : Nat) (n : Nat) (fst := ``Prod.fst) (snd := ``Prod
 
 
 def mkProdSplitElem (xs : Expr) (n : Nat) (fst := ``Prod.fst) (snd := ``Prod.snd) : MetaM (Array Expr) :=
-  (Array.mkArray n 0)
+  (Array.replicate n 0)
     |>.mapIdx (λ i _ => i)
     |>.mapM (λ i => mkProdProj xs i n fst snd)
 

SciLean/Modules/DDG/SurfaceMesh.lean

@@ -8,7 +8,6 @@ https://github.com/GeometryCollective/geometry-processing-js/blob/c7ea47ae808979
 -/
 
 import SciLean.Data.DataArray.FloatN
-import Lean.Data.HashMap
 
 open Lean Data