search

LS-Lab / KeYmaeraX-release

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
http://keymaeraX.org/
GNU General Public License v2.0
77 stars 39 forks source link

Vector and Matrix Support #69

Open zstone1 opened 4 years ago

zstone1 commented 4 years ago

Is there any plan for syntactic support for vectors and matrices in KeYmaera?

I've got a non-trivial matlab algorithm that I want to encode in a hybrid program. It uses lots of vector operations (dot products, cross products, read/write to the nth element). I happen to know all the lengths of the vector statically, so I can flatten to a bunch of reals. However, that will make all the proofs rather nasty. Is there a trick here, or do I have to do this the hard way?

Depending on how hard it would be, I might be able to attempt adding such support myself. But that would depend on having a suitable design already agreed on.

rbohrer commented 4 years ago

Vectors and matrices are something we've long wanted to have, but as you've hinted, it's important to get the design right, and we've never yet quite convinced ourselves that we have the right design. For a little background: KeYmaera X's data structures do feature a rudimentary type system that could be extended with other types, but by and large our actual proof algorithms are designed with real numbers in mind. In particular, there's a very clean story for how to automate proofs of first-order formulas that only talk about reals, but automation for arbitrary vectors or matrices would require a very different approach. On the type-system side, vectors and matrices have dimensions, and treating their dimensions correctly often demands at least a rudimentary form of dependency or polymorphism in the type system.

That's not to say it can't or shouldn't be done, this is just to say why we've thought about it for so long without having implemented a solution yet.

If you're working with fixed-length vectors or matrices, you can sometimes make your life a little better by making extensive use of function definitions (here is an example proof where we used definitions a lot: https://github.com/LS-Lab/KeYmaeraX-projects/tree/master/ijrr/robix.kyx). You could define functions like norm, distance, dot product, cross product, etc. KeYmaeraX also allows you to prove a lemma and use it in a proof of another theorem. If you identify some general lemmas for finite vectors or matrices, you could try writing them as lemmas and using them in the proof. (I might caution that the lemma feature has mainly been used by our lab, so if you run into any weird issues or poor error messages while using it, feel free to ask us)

If there are some natural or important lemmas for fixed-size matrices or vectors, one option would be to assemble a library of functions and lemmas which could be shipped with future releases. But for all the reasons discussed above, that would also require a lot of discussion and thought.

By the way, KeYmaera X does have pairs. At least internally, it should be possible to implement fixed-size vectors using nested pairs. However, I have never tried to use them from a .kyx file or from the UI, and do not know if that is currently supported.

On Thu, Sep 24, 2020 at 2:05 PM zstone1 notifications@github.com wrote:

Is there any plan for syntactic support for vectors and matrices in KeYmaera?

I've got a non-trivial matlab algorithm that I want to encode in a hybrid program. It uses lots of vector operations (dot products, cross products, read/write to the nth element). I happen to know all the lengths of the vector statically, so I can flatten to a bunch of reals. However, that will make all the proofs rather nasty. Is there a trick here, or do I have to do this the hard way?

Depending on how hard it would be, I might be able to attempt adding such support myself. But that would depend on having a suitable design already agreed on.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/LS-Lab/KeYmaeraX-release/issues/69, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAO6WYNP5ZE5IJM2IOBA3YLSHOC7HANCNFSM4RYTMHHQ .

zstone1 commented 4 years ago

Yeah, there's no silver bullet as I suspected. I had thought about the dependent typing issues, and it's not nice. Is there even a decision procedure for vector arithmetic? Certainly for statically known lengths it's easy to convert to standard real QE, so at least in my case there is hope.

I'm already making heavy use of function symbols. But to make that feature really nice, being able to import a library of functions (and function symbols + assertions) would be really important. For example, I'm adding sin cos and pi symbols, and then assuming some properties about them. I'd love to do this once, and then import a file. Does anything like this exist?

Tuples are an interesting suggestion that would help a lot with readability. Unfortunately, all of the arithmetic like plus have RBinaryCompositeTerm, which requires its arguments to be Real sort. So I'd also have to add plus1, plus2, plus3, losing the readability benefit. A naive idea is to define a notion for sorts of "recursively real", and assert that both sorts are equal, and recursively real. The Assign class is already does this kind of equality check in its insist block. Extending ODE and Assign with this behavior would be provide a fairly complete tuples feature in the syntax. I have no idea how that would affect the tactics...

To simulate tuples, I was considering "encoding" a vector as a real by adding uninterpreted function symbols length : (encoded R) -> nat, read : (encoded R) -> nat -> R, write : (encoded R) -> nat -> R -> (encoded R) (where nat and (encoded R) are of course just R) then assuming the lens laws. I'd have to add uninterpreted plus, dot, cross, ect forall of these as well. Good news about this approach is assignment magically works out. Bad news is ODEs do not work at all.

For a bit of context, I'm writing a Scala program to translate simulink/matlab models into hyrbid programs, so features without UI should be fine. But I'm a tad unsure how to setup an interactive theorem proving environment for KeYmaera without the UI. I've got lots of experience with Coq using vscoq, but I don't see an analogous feature here. All I really need is something to apply a tactic and pretty print the new context. Is there a doc for this?

rbohrer commented 4 years ago

When we're not working with the UI, we usually write a Scala test case and write proofs using the Scala embedding of our tactic language bellerophon. The wiki has an article on setting up the development environment and running tests.

We do also have a rudimentary REPL, but it's not actively maintained, and I am unsure of its status

On Fri, Sep 25, 2020, 12:41 PM zstone1 notifications@github.com wrote:

Yeah, there's no silver bullet as I suspected. I had thought about the dependent typing issues, and it's not nice. Is there even a decision procedure for vector arithmetic? Certainly for statically known lengths it's easy to convert to standard real QE, so at least in my case there is hope.

I'm already making heavy use of function symbols. But to make that feature really nice, being able to import a library of functions (and function symbols + assertions) would be really important. For example, I'm adding sin cos and pi symbols, and then assuming some properties about them. I'd love to do this once, and then import a file. Does anything like this exist?

Tuples are an interesting suggestion that would help a lot with readability. Unfortunately, all of the arithmetic like plus have RBinaryCompositeTerm, which requires its arguments to be Real sort. So I'd also have to add plus1, plus2, plus3, losing the readability benefit. A naive idea is to define a notion for sorts of "recursively real", and assert that both sorts are equal, and recursively real. The Assign class is already does this kind of equality check in its insist block. Extending ODE and Assign with this behavior would be provide a fairly complete tuples feature in the syntax. I have no idea how that would affect the tactics...

To simulate tuples, I was considering "encoding" a vector as a real by adding uninterpreted function symbols length : (encoded R) -> nat, read : (encoded R) -> nat -> R, write : (encoded R) -> nat -> R -> (encoded R) (where nat and (encoded R) are of course just R) then assuming the lens laws. I'd have to add uninterpreted plus, dot, cross, ect forall of these as well. Good news about this approach is assignment magically works out. Bad news is ODEs do not work at all.

For a bit of context, I'm writing a Scala program to translate simulink/matlab models into hyrbid programs, so features without UI should be fine. But I'm a tad unsure how to setup an interactive theorem proving environment for KeYmaera without the UI. I've got lots of experience with Coq using vscoq, but I don't see an analogous feature here. All I really need is something to apply a tactic and pretty print the new context. Is there a doc for this?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/LS-Lab/KeYmaeraX-release/issues/69#issuecomment-699032336, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAO6WYKSEXT5BWWWCGWQMH3SHTB2HANCNFSM4RYTMHHQ .

rbohrer commented 4 years ago

I was recently reminded that there is another project which tries to generate KeYmaera X models from Simulink models. I have not used this project myself, and it's possible that their goals or approach differ from yours, but I thought their paper may be helpful in your efforts:

https://link.springer.com/chapter/10.1007/978-3-030-02450-5_6

On Fri, Sep 25, 2020 at 12:45 PM Brandon Bohrer bbohrer@andrew.cmu.edu wrote:

When we're not working with the UI, we usually write a Scala test case and write proofs using the Scala embedding of our tactic language bellerophon. The wiki has an article on setting up the development environment and running tests.

We do also have a rudimentary REPL, but it's not actively maintained, and I am unsure of its status

On Fri, Sep 25, 2020, 12:41 PM zstone1 notifications@github.com wrote:

Yeah, there's no silver bullet as I suspected. I had thought about the dependent typing issues, and it's not nice. Is there even a decision procedure for vector arithmetic? Certainly for statically known lengths it's easy to convert to standard real QE, so at least in my case there is hope.

I'm already making heavy use of function symbols. But to make that feature really nice, being able to import a library of functions (and function symbols + assertions) would be really important. For example, I'm adding sin cos and pi symbols, and then assuming some properties about them. I'd love to do this once, and then import a file. Does anything like this exist?

Tuples are an interesting suggestion that would help a lot with readability. Unfortunately, all of the arithmetic like plus have RBinaryCompositeTerm, which requires its arguments to be Real sort. So I'd also have to add plus1, plus2, plus3, losing the readability benefit. A naive idea is to define a notion for sorts of "recursively real", and assert that both sorts are equal, and recursively real. The Assign class is already does this kind of equality check in its insist block. Extending ODE and Assign with this behavior would be provide a fairly complete tuples feature in the syntax. I have no idea how that would affect the tactics...

To simulate tuples, I was considering "encoding" a vector as a real by adding uninterpreted function symbols length : (encoded R) -> nat, read : (encoded R) -> nat -> R, write : (encoded R) -> nat -> R -> (encoded R) (where nat and (encoded R) are of course just R) then assuming the lens laws. I'd have to add uninterpreted plus, dot, cross, ect forall of these as well. Good news about this approach is assignment magically works out. Bad news is ODEs do not work at all.

For a bit of context, I'm writing a Scala program to translate simulink/matlab models into hyrbid programs, so features without UI should be fine. But I'm a tad unsure how to setup an interactive theorem proving environment for KeYmaera without the UI. I've got lots of experience with Coq using vscoq, but I don't see an analogous feature here. All I really need is something to apply a tactic and pretty print the new context. Is there a doc for this?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/LS-Lab/KeYmaeraX-release/issues/69#issuecomment-699032336, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAO6WYKSEXT5BWWWCGWQMH3SHTB2HANCNFSM4RYTMHHQ .

aplatzer commented 4 years ago

Let me add that these translations can be quite impactful between rigorous verification tools such as KeYmaera X and modeling tools used in engineering practice such as SF/SL. I wish you all the best in your research and encourage you to get in touch with us via email and keep us up to date.

BTW, in theory the relationship of single reals to vectors is perfectly definable by bijection in differential dynamic logic [JAR'08,TOCL'17]. In practice, however, vectors should be done much more pragmatically.