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

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

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

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

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

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

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

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

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

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: Feb 05 2023 at 13:02 UTC