Merge branch 'v4.6-bump'

.dir-locals.el

@@ -0,0 +1,6 @@
+;;; Directory Local Variables
+;;; For more information see (info "(emacs) Directory Variables")
+
+((lean4-mode . ((fill-column . 100)
+                (show-trailing-whitespace . t)
+                (eval . (add-hook 'before-save-hook 'delete-trailing-whitespace nil t)))))

README.org

@@ -26,8 +26,8 @@ lake build
 
 To run examples:
 #+begin_src
-lake build HarmonicOscillator && ./build/bin/HarmonicOscillator
-lake build WaveEquation && ./build/bin/WaveEquation 
+lake build HarmonicOscillator && .lake/build/bin/HarmonicOscillator
+lake build WaveEquation && .lake/build/bin/WaveEquation 
 #+end_src
 Other examples in =examples= directory do not currently work.
 

SciLean.lean

@@ -1,15 +1,11 @@
 import SciLean.Core
-import SciLean.Core.FloatAsReal
+
+import SciLean.Tactic.MathlibCompiledTactics
+import SciLean.Tactic.Autodiff
 
 import SciLean.Data.ArrayType
 import SciLean.Data.DataArray
 
-import SciLean.Modules.DifferentialEquations
--- import SciLean.Modules.ML
-
-import SciLean.Tactic.LSimp2.Elab
-
-import SciLean.Util.Profile
 
 /-!
 
@@ -21,4 +17,3 @@ SciLean
 
 
 -/
-

SciLean/Core.lean

@@ -7,12 +7,12 @@ import SciLean.Core.FunctionPropositions
 import SciLean.Core.FunctionTransformations
 import SciLean.Core.Monads
 import SciLean.Core.Notation
-import SciLean.Core.Simp
-import SciLean.Core.Data
+
+import SciLean.Core.Rand
 
 import SciLean.Core.Approx.Basic
 import SciLean.Core.Approx.ApproxLimit
 
-import SciLean.Core.Meta.GenerateRevDeriv
-import SciLean.Core.Meta.GenerateRevCDeriv
-import SciLean.Core.Meta.GenerateFwdCDeriv
+-- import SciLean.Core.Meta.GenerateRevDeriv
+-- import SciLean.Core.Meta.GenerateRevCDeriv
+-- import SciLean.Core.Meta.GenerateFwdCDeriv

SciLean/Core/Approx/ApproxLimit.lean

@@ -2,6 +2,7 @@ import Lean
 
 import SciLean.Core.Approx.Basic
 import SciLean.Tactic.PullLimitOut
+import SciLean.Lean.Meta.Basic
 
 namespace SciLean
 
@@ -25,25 +26,27 @@ where `<proof>` is a proof that this approximation is indeed valid
 
 Warning: The validity proof is not completely correct right now
 -/
-syntax (name:=approx_limit_tactic) "approx_limit " ident " := " term : tactic 
+syntax (name:=approx_limit_tactic) "approx_limit " ident " := " term : tactic
 
-@[tactic approx_limit_tactic] 
+open Lean Meta in
+@[tactic approx_limit_tactic]
 def approxLimitTactic : Tactic
 | `(tactic| approx_limit $n:ident := $prf:term) => do
   let mainGoal ← getMainGoal
   let goal ← instantiateMVars (← mainGoal.getType)
-  if ¬(goal.isAppOfArity' ``Approx 6) then
+
+  Lean.Meta.letTelescope goal fun xs goal' => do
+  if ¬(goal'.isAppOfArity' ``Approx 6) then
     throwError "the goal is not `Approx _ _`"
 
-  let .app f a := goal | panic! "unreachable code in approxLimitTactic"
+  let .app f a := goal' | panic! "unreachable code in approxLimitTactic"
   let a' ← pullLimitOut a
-  let goal' := f.app a'
+  let goal'' ← mkLambdaFVars xs (f.app a')
   let limitPullProof ← elabTerm (← `($prf)) (← Meta.mkEq a a')
-  let mainGoal ← mainGoal.replaceTargetEq goal' (← Meta.mkAppM ``congr_arg #[f,limitPullProof])
+  let mainGoal ← mainGoal.replaceTargetEq goal'' (← mkLambdaFVars xs (← Meta.mkAppM ``congr_arg #[f,limitPullProof]))
   setGoals [mainGoal]
 
   -- TODO: this probably should be done manually as these holes should not become new goals
   evalTactic (← `(tactic| apply Approx.limit _ _))
   evalTactic (← `(tactic| intros $n))
 | _ => throwUnsupportedSyntax
-

SciLean/Core/Approx/ApproxSolution.lean

@@ -9,7 +9,7 @@ namespace SciLean
 
 open Notation
 
-inductive ApproxSolution {α : Type _} [TopologicalSpace α] [Nonempty α] : {N : Type _} → (lN : Filter N) → (spec : α → Prop) → Type _ 
+inductive ApproxSolution {α : Type _} [TopologicalSpace α] [Nonempty α] : {N : Type _} → (lN : Filter N) → (spec : α → Prop) → Type _
 | exact {spec : α → Prop}
     (impl : α)
     (h : spec impl)
@@ -24,7 +24,7 @@ inductive ApproxSolution {α : Type _} [TopologicalSpace α] [Nonempty α] : {N
     : ApproxSolution (lN.prod lM) spec
 
 
-variable {α} [TopologicalSpace α] [Nonempty α] 
+variable {α} [TopologicalSpace α] [Nonempty α]
 
 @[inline]
 def ApproxSolution.val {N} {lN : Filter N} {spec : α → Prop}
@@ -47,7 +47,7 @@ theorem approx_consistency {N} {lN : Filter N} [T2Space α] {spec : α → Prop}
   : ∀ a, a = (limit n ∈ lN, approx.val n) → spec a :=
 by
   induction approx
-  case exact impl h => 
+  case exact impl h =>
     simp[ApproxSolution.val]
     sorry_proof
     -- intro a h'
@@ -76,10 +76,6 @@ theorem approx_convergence {N} {lN : Filter N} {spec : α → Prop}
 -- by
 --   induction approx
 --   case exact impl h => exact ⟨impl, sorry⟩
---   case approx specₙ lN lM consistent convergence impl hn => 
---     simp[ApproxSolution.val]    
+--   case approx specₙ lN lM consistent convergence impl hn =>
+--     simp[ApproxSolution.val]
 --     sorry
-
-
-
-

SciLean/Core/Approx/Basic.lean

@@ -14,10 +14,10 @@ variable {α} [TopologicalSpace α] [Nonempty α]
 abbrev Approx  {N : outParam $ Type _} (lN : Filter N) (a : α)  := ApproxSolution lN (fun x => a=x)
 
 abbrev Approx.exact {a : α} := ApproxSolution.exact a rfl
-abbrev Approx.limit {N} {lN : Filter N} (M) (lM : Filter M) 
-  {aₙ : N → α} (x : (n : N) → Approx lM (aₙ n)) 
-  : Approx (lN.prod lM) (limit n ∈ lN, aₙ n) := 
-  ApproxSolution.approx _ lN lM 
+abbrev Approx.limit {N} {lN : Filter N} (M) (lM : Filter M)
+  {aₙ : N → α} (x : (n : N) → Approx lM (aₙ n))
+  : Approx (lN.prod lM) (limit n ∈ lN, aₙ n) :=
+  ApproxSolution.approx _ lN lM
     (by intro aₙ' h a h'; simp[h,h'])
     (by sorry_proof)
     x

SciLean/Core/Approx/Test.lean

@@ -1,28 +1,30 @@
 import SciLean.Core.Approx.Basic
 import SciLean.Core.FloatAsReal
 import SciLean.Util.RewriteBy
+import SciLean.Util.Limit
 
 open SciLean
-open LimitNotation
+open Notation
 
 
-def sqrtBabylonian (n : Nat) (x₀ : Float) (y : Float) : Float := 
+def sqrtBabylonian (n : Nat) (x₀ : Float) (y : Float) : Float :=
 match n with
-| 0   => x₀ 
+| 0   => x₀
 | n'+1 => sqrtBabylonian n' ((x₀ + y/x₀)/2) y
 
-theorem sqrtBabylonianLimit (x₀ : Float) 
-  : isomorph `RealToFloat Real.sqrt
-    = 
+
+theorem sqrtBabylonianLimit (x₀ : Float) :
+    isomorph `RealToFloat Real.sqrt
+    =
     limit n → ∞, sqrtBabylonian n x₀
     := sorry
 
+
 approx sqrt_approx := isomorph `RealToFloat Real.sqrt
 by
-  simp
   rw[sqrtBabylonianLimit 1]
   apply Approx.limit; intro n
-  
+
 
 #eval sqrt_approx (0,()) 2
 #eval sqrt_approx (1,()) 2

SciLean/Core/FloatAsReal.lean

@@ -5,13 +5,13 @@ import SciLean.Core.Objects.Scalar
 namespace SciLean
 
 instance : CommRing Float where
-  zero_mul := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; simp
-  mul_zero := by intros; apply isomorph.ext `FloatToReal; simp; ftrans
-  mul_comm := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; rw[mul_comm]
-  left_distrib := by intros;  apply isomorph.ext `FloatToReal; simp; ftrans; simp; ftrans; rw[mul_add]
-  right_distrib := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; simp; ftrans; rw[add_mul]
-  mul_one := by intros; apply isomorph.ext `FloatToReal; simp; ftrans
-  one_mul := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; simp
+  zero_mul := by intros; apply isomorph.ext `FloatToReal; simp; sorry_proof --  fun_trans; simp
+  mul_zero := by intros; apply isomorph.ext `FloatToReal; simp; fun_trans
+  mul_comm := by intros; apply isomorph.ext `FloatToReal; simp; fun_trans; rw[mul_comm]
+  left_distrib := by intros;  apply isomorph.ext `FloatToReal; simp; fun_trans; rw[mul_add]
+  right_distrib := by intros; apply isomorph.ext `FloatToReal; simp; fun_trans; rw[add_mul]
+  mul_one := by intros; apply isomorph.ext `FloatToReal; simp; fun_trans
+  one_mul := by intros; apply isomorph.ext `FloatToReal; simp; fun_trans
   npow n x := x.pow (n.toFloat)  --- TODO: change this implementation
   npow_zero n := sorry_proof
   npow_succ n x := sorry_proof
@@ -25,22 +25,22 @@ instance : CommRing Float where
   nsmul_zero := sorry_proof
   nsmul_succ n x := sorry_proof
   sub_eq_add_neg a b := sorry_proof
-  natCast n := n.toFloat
+  natCast n := n.toUSize.toFloat
   natCast_zero := sorry_proof
   natCast_succ := sorry_proof
-  intCast n := if n ≥ 0 then n.toNat.toFloat else -((-n).toNat).toFloat
+  intCast n := if n ≥ 0 then n.toNat.toUInt64.toFloat else -((-n).toNat.toUInt64).toFloat
   intCast_ofNat := sorry_proof
   intCast_negSucc := sorry_proof
 
 instance : Field Float where
   exists_pair_ne := sorry_proof
-  div_eq_mul_inv := sorry_proof 
+  div_eq_mul_inv := sorry_proof
   mul_inv_cancel := sorry_proof
   inv_zero := sorry_proof
 
-instance : DecidableEq Float := fun x y => 
-  if x ≤ y && y ≤ x 
-  then .isTrue sorry_proof 
+instance : DecidableEq Float := fun x y =>
+  if x ≤ y && y ≤ x
+  then .isTrue sorry_proof
   else .isFalse sorry_proof
 
 instance : LinearOrderedCommRing Float where
@@ -57,7 +57,7 @@ instance : LinearOrderedCommRing Float where
   max := fun a b => if a ≤ b then b else a
   min_def := sorry_proof
   max_def := sorry_proof
-  compare x y :=   
+  compare x y :=
     if x < y then Ordering.lt
     else if x = y then Ordering.eq
     else Ordering.gt
@@ -67,7 +67,7 @@ instance : LinearOrderedCommRing Float where
 instance : LinearOrderedField Float where
   mul_inv_cancel := sorry_proof
   inv_zero := sorry_proof
-  div_eq_mul_inv := sorry_proof 
+  div_eq_mul_inv := sorry_proof
 
 
 instance : SeminormedRing Float where
@@ -82,8 +82,8 @@ instance : SeminormedRing Float where
 
 instance : StarRing Float where
   star := fun x => x
-  star_involutive := by simp[Function.Involutive] 
-  star_mul := by simp[Function.Involutive, mul_comm] 
+  star_involutive := by simp[Function.Involutive]
+  star_mul := by simp[Function.Involutive, mul_comm]
   star_add := by simp[Function.Involutive]
 
 instance : DenselyNormedField Float where
@@ -141,9 +141,11 @@ instance : IsReal Float where
 instance : RealScalar Float where
   toComplex x := ⟨floatToReal x, 0⟩
   toReal x := floatToReal x
+  ofReal x := realToFloat x
+  ofComplex x := realToFloat x.re
 
   is_real := sorry_proof
-  
+
   make x _ := x
   make_def := by intros; simp; sorry_proof
 
@@ -155,7 +157,7 @@ instance : RealScalar Float where
 
   sin x := x.sin
   sin_def := sorry_proof
-  
+
   cos x := x.cos
   cos_def := sorry_proof
 
@@ -164,7 +166,7 @@ instance : RealScalar Float where
 
   asin x := x.asin
   asin_def := sorry_proof
-  
+
   acos x := x.acos
   acos_def := sorry_proof
 
@@ -188,13 +190,13 @@ instance : RealScalar Float where
 
   abs x := x.abs
   abs_def := sorry_proof
-  
+
   le_total := by sorry_proof
   decidableLE := inferInstance
   decidableEq := inferInstance
   decidableLT := inferInstance
 
-  min_def := by sorry_proof 
+  min_def := by sorry_proof
   max_def := by sorry_proof
   compare x y := compare x y
   compare_eq_compareOfLessAndEq := by sorry_proof