Stream: math-comp analysis

Topic: SciLean


view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 07 2022 at 15:09):

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

view this post on Zulip Alexander Gryzlov (Dec 07 2022 at 15:12):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Dec 07 2022 at 15:19):

I guess you might want to distinguish between:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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