From 0d83abe45cff3fecdcab1f6104ae6abdbfcad187 Mon Sep 17 00:00:00 2001
From: Tim Richter <tim@cs.uni-potsdam.de>
Date: Sat, 1 Feb 2025 21:42:38 +0100
Subject: [PATCH] add ApproxSolution for use in isValid, cleanup

---
 IVP.agda | 82 +++++++++++++++++++++++++++-----------------------------
 1 file changed, 40 insertions(+), 42 deletions(-)

diff --git a/IVP.agda b/IVP.agda
index 0c16839..bfe63e7 100644
--- a/IVP.agda
+++ b/IVP.agda
@@ -15,9 +15,11 @@ module IVP where
 infix 22 _^_
 infix 15 _*R^sR_
 infix 10 _+R^s_
+infix 22 _/â„_
 
 -- We need â„ ^ s to describe a system of s ODE's as one time dependent function
--- (â„ â†’ (â„ ^ s)) that takes the time t : â„ and gives a vector in â„ ^ s where each value corresponds to one ODE.
+-- (â„ â†’ (â„ ^ s)) that takes the time t : â„ and gives a vector in â„ ^ s where each
+-- value corresponds to one ODE.
 
 _^_ : Set â†’ â„• â†’ Set
 A ^ zero  = âŠ¤
@@ -27,23 +29,26 @@ postulate
   -- real numbers  with standard operations
   â„ : Set
   0R : â„
-  â„+ : Set
+  -- â„+ : Set
   _+R_ : â„ â†’ â„ â†’ â„
   _*R_ : â„ â†’ â„ â†’ â„
-  _<R_ :  â„ â†’ â„ â†’ Set
-  _>R_ :  â„ â†’ â„ â†’ Set
+  _<R_ : â„ â†’ â„ â†’ Set
+  _>R_ : â„ â†’ â„ â†’ Set
+  _/â„_ : â„ â†’ â„ â†’ â„
+
+  -- We need a way to add and multiply natural numbers with real numbers, and divide
+  -- real numbers by natural numbers.
+  -- Converting natural numbers to real numbers and using the operations above is an
+  -- easy way to do so.
 
-  -- We need a way to add and multiply natural numbers with real numbers.
-  -- Converting natural numbers to real numbers and using the operations above is an easy way to do so.
   nToR : â„• â†’ â„
 
-  -- derivative
-  -- this is of course problematic: we postulate that any real function is everywhere differentiable
-  -- we might refine later
+  -- Derivative (This is of course problematic: we postulate that any real function
+  -- is everywhere differentiable; might refine later...)
   D : (â„ â†’ â„) â†’ (â„ â†’ â„)
 
--- We define the derivative of vector valued functions by calculating the derivative for each element of the vector â„ ^ s
--- to describe the derivative of ODE systems.
+-- We define the derivative of vector valued functions by calculating the derivative
+-- for each element of the vector â„ ^ s to describe the derivative of ODE systems.
 
 Ds : {s : â„•} â†’ (â„ â†’ (â„ ^ s)) â†’ (â„ â†’ (â„ ^ s))
 Ds {zero}  f x = tt
@@ -108,49 +113,42 @@ EulerMethod {s} ivp U k n = U +R^s k *R^sR (IVP.f ivp) (U , (nToR n) *R k)
 
 -- A solution method only approximates for 1 timestep.
 -- We need a method to calculate approximations for all timesteps beginning with t_0 until t_n.
-SolveIVP : {s : â„• } â†’ (ivp : IVP s) â†’ SolutionMethod ivp â†’ â„• â†’ â„ â†’ â„ ^ s
-SolveIVP {s} ivp m zero k = IVP.Î· ivp
-SolveIVP {s} ivp m (suc n) k = m (SolveIVP ivp m n k) k n
+SolveIVP : {s : â„• } â†’ (ivp : IVP s) â†’ SolutionMethod ivp â†’ â„ â†’ â„• â†’ â„ ^ s
+SolveIVP {s} ivp m k zero    = IVP.Î· ivp
+SolveIVP {s} ivp m k (suc n) = m (SolveIVP ivp m k n) k n
+
+-- Now, for any n âˆˆ â„• and t > 0, we can choose step width to be t / n.
+-- SolveIVP {s} ivp m (t / n) n   will then be an approximation for the
+-- solution of the IVP at t (= n * (t / n)):
+
+ApproxSolution : {s : â„• } â†’ (ivp : IVP s) â†’ SolutionMethod ivp â†’ â„• â†’ â„ â†’ â„ ^ s
+ApproxSolution ivp m n t = SolveIVP ivp m (t /â„ (nToR n)) n
 
 -- We need to adjust the main condition of IVP to allow approximations with precision prec.
 ApproxMainCond : {s : â„•} â†’ (â„ ^ s Ã— â„ â†’ â„ ^ s) â†’ (â„ â†’ â„ ^ s) â†’ â„ â†’ â„ â†’ Set
 ApproxMainCond f u t prec = (distance  (Ds u t) (f (u t , t))) <R prec
 
--- TODO: Better explanation
--- A solution method can be called valid if:
--- a n:â„• exists for all k:â„ and all prec:â„
--- such that it finds approximations until t_n = n * k by using SolveIVP with a maximum precision prec.
+-- A solution method m (for initial value problem ivp) can be called valid if:
+-- for any t > 0 and any precision prec > 0 there exists n âˆˆ â„•
+-- such that at t, ApproxSolution ivp m n  satisfies ApproxMainCond f u t prec
+
 isValid : {s : â„•} â†’ {ivp : IVP s } â†’ SolutionMethod ivp â†’ Set
-isValid {s} {ivp} m = (k : â„) â†’ (prec : â„) â†’ Î£ â„• Î» n â†’ ApproxMainCond (IVP.f ivp) (SolveIVP ivp m n) ((nToR n) *R k) prec
+isValid {s} {ivp} m = (t : â„) â†’ (prec : â„) â†’
+                      Î£ â„• Î» n â†’ ApproxMainCond (IVP.f ivp) (ApproxSolution ivp m n) t prec
 
--- Unter welchen Bedingungen an f ist die EulerMethode valid?
+-- isValid is only concerned with (an approximated variant of) the main condition
+-- for Solutions (MainCond). This is justified by the observation that the
+-- initial data condition is automatically satisfied:
 
 -- (A): Proof that for every solution method SolveIVP fulfills the InitialDataCond.
 
--- Adjust InitialDataCond to work with a discretized time: 
+-- Adjust InitialDataCond to work with a discretized time:
 InitialDataCondâ„• : {s : â„•} â†’ â„ ^ s â†’ (â„• â†’ â„ ^ s) â†’ Set
 InitialDataCondâ„• Î· u = (u zero) â‰¡ Î·
 
--- The proof only works with changing the argument order of SolveIVP.
-SolveIVPâ„• : {s : â„• } â†’ (ivp : IVP s) â†’ SolutionMethod ivp â†’ â„ â†’ â„• â†’ â„ ^ s
-SolveIVPâ„• {s} ivp m k zero = IVP.Î· ivp
-SolveIVPâ„• {s} ivp m k (suc n) = m (SolveIVPâ„• ivp m k n) k n
-
--- Proof for A:
-SolveIVPâ„•hasStartCond : {s : â„•} â†’ (ivp : IVP s) â†’ (m : SolutionMethod ivp) â†’ (k : â„) â†’ InitialDataCondâ„• (IVP.Î· ivp) (SolveIVPâ„• ivp m k)
-SolveIVPâ„•hasStartCond {s} ivp m n = refl
-
--- Konsequenterweise kÃ¶nnte man jetzt auch MainCond und Solution auf die Zeit als n * k anpassen ????
--- Tim: Ja, wahrscheinlich. Denk' noch ein bisschen drÃ¼ber nach, ich tue das auch...
-
---postulate
---  Dâ„• :{s : â„•} â†’ (â„• â†’ â„ ^ s) â†’ (â„• â†’ â„ ^ s)
- -- âˆ˜N :
-
---Dsâ„• : {s : â„•} â†’ (â„• â†’ (â„ ^ s)) â†’ (â„• â†’ (â„ ^ s))
---Dsâ„• {zero}  f x = tt
---Dsâ„• {suc s} f x = (Ds2 (projâ‚ âˆ˜N f) x) , (D2 (projâ‚‚ âˆ˜N f) x)
+-- Proof of A:
+SolveIVPhasStartCond : {s : â„•} â†’ (ivp : IVP s) â†’ (m : SolutionMethod ivp) â†’
+                        (k : â„) â†’ InitialDataCondâ„• (IVP.Î· ivp) (SolveIVP ivp m k)
+SolveIVPhasStartCond {s} ivp m n = refl
 
---MainCondâ„• : {s : â„•} â†’ (â„ ^ s Ã— â„• â†’ â„ ^ s) â†’ (â„• â†’ â„ ^ s) â†’ Set
---MainCondâ„• f u = (n : â„•) â†’ Ds2 u n â‰¡ (f (u n , n))
 
-- 
GitLab