Alexander Gryzlov (Dec 07 2022 at 15:07): 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:
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: Feb 05 2023 at 13:02 UTC