Implicit and Explicit Proof Management in KeYmaera X

TL;DR

This paper introduces proof management techniques in KeYmaera X that enhance proof flexibility and trustworthiness in hybrid systems theorem proving by controlling formula expansion, lemma application, and proof structuring outside the core prover.

Contribution

It presents novel proof management methods that extend the capabilities of KeYmaera X, enabling more flexible and reliable hybrid systems proofs without compromising core soundness.

Findings

Techniques for controlled formula expansion and lemma application.

Implicit sub-proofs improve proof management reliability.

Enhanced proof features like hiding formulas are implemented successfully.

Abstract

Hybrid systems theorem proving provides strong correctness guarantees about the interacting discrete and continuous dynamics of cyber-physical systems. The trustworthiness of proofs rests on the soundness of the proof calculus and its correct implementation in a theorem prover. Correctness is easier to achieve with a soundness-critical core that is stripped to the bare minimum, but, as a consequence, proof convenience has to be regained outside the soundness-critical core with proof management techniques. We present modeling and proof management techniques that are built on top of the soundness-critical core of KeYmaera X to enable expanding definitions, parametric proofs, lemmas, and other useful proof techniques in hybrid systems proofs. Our techniques steer the uniform substitution implementation of the differential dynamic logic proof calculus in KeYmaera X to allow users choose when and how in a proof abstract formulas, terms, or programs become expanded to their concrete definitions, and when and how lemmas and sub-proofs are combined to a full proof. The same techniques are exploited in implicit sub-proofs (without making such sub-proofs explicit to the user) to provide proof features, such as temporarily hiding formulas, which are notoriously difficult to get right when implemented in the prover core, but become trustworthy as proof management techniques outside the core. We illustrate our approach with several useful proof techniques and discuss their presentation on the KeYmaera X user interface.