## Stream: math-comp analysis

### Topic: SciLean

#### Alexander Gryzlov (Dec 07 2022 at 15:07):

I wonder how hard would it be to implement something like this on top of mathcomp-analysis: https://lecopivo.github.io/SciLean/build/doc/literate/harmonic_oscillator.html

#### Karl Palmskog (Dec 07 2022 at 15:09):

isn't this kinda close? https://github.com/drouhling/LaSalle (if ported to mathcomp-analysis)

#### Alexander Gryzlov (Dec 07 2022 at 15:12):

not sure, does it have some form of ODE solver?

#### Karl Palmskog (Dec 07 2022 at 15:14):

This formalization is a step towards a formal verification of dynamical systems. LaSalle’s invariance principle and its extensions play an important role in the study of control techniques. We plan to use this work to formally verify a control law for the swing-up of an inverted pendulum

#### Karl Palmskog (Dec 07 2022 at 15:15):

if you want ODE solvers, there is at least https://github.com/coq-community/corn/tree/master/ode

#### Karl Palmskog (Dec 07 2022 at 15:19):

I guess you might want to distinguish between:

• defining and reasoning about oscillating/dynamical systems
• "solving" such systems with numerical methods
• illustrating the dynamics of such systems graphically

#### Alexander Gryzlov (Dec 07 2022 at 15:23):

I guess the core question is whether mathcomp-analysis is "computational" enough, or you have to start from something like https://holgerthies.github.io/continuity/ instead

#### Alexander Gryzlov (Dec 07 2022 at 15:24):

I think the first 2 points are crucial, numbers can be converted into pictures in some way always

#### Karl Palmskog (Dec 07 2022 at 15:25):

CoRN has verified plotting (explained here: https://coq.discourse.group/t/interval-4-2-now-with-plotting/1248)

#### Bas Spitters (Dec 08 2022 at 08:50):

Moreover, there's a connection between corn/math-classes and the stdlib. So, one can even compute with classical reals (that happen to be computable). We build the ODE solver to see how far we could come with Bishop's constructive analysis. This does backward computation, that often overshoots, the forward approach is probably faster. (It was also done quite a bit later)

Last updated: Jun 25 2024 at 18:02 UTC