Relational Differential Dynamic Logic
203
Consequently, h is the constant function equal to 0, which implies that (ω, ω) ∈
g = g
. By definition, ξ is a solution of δ, so ω 0 −
δ
→ ω. Furthermore, by
Corollary 18, ξ ◦ K
−1 is a solution of δ. Thus ω 0 −
δ
→ ω and
(ω 0 , ω 0 ) −
δ; δ
→ (ω, ω).
The above lemma is a key observation in the current work. It allows us to
turn the relational dynamics δ; δ—expressed as a sequential composition in dL—
into a combined dynamics δ ⊗ (g,g) δ. Moreover, we can do so in a way that
the two dynamics are synchronized in a reparametrized manner, as specified
by (g, g). Such combination of two dynamics is crucial in exploiting the logical
infrastructure of dL and KeYmaera X—we emphasize again that the (DI) rule
does not support invariant reasoning about the relationship between δ and δ,
when the relational dynamics is expressed in the original form δ; δ.
The following is an incarnation of Lemma 23 as a proof rule. We assume that
a postcondition is a conditional form E ⇒ ϕ; E is called an exit condition. By
assuming that E implies g = g, we enforce the second condition (ω, ω) ∈
g = g
in item 1 of Lemma 23. The first three premises are there to ensure that (g, g)
is a synchronizer. Under these premises (the first four), the rule allows one to
transform its conclusion (about δ; δ) into one about the combined dynamics
δ ⊗ (g,g) δ, which is amenable to application of the (DI) rule, for example.
Theorem 24 (synchronization rule). The following inference rule is sound:
Γ [ δ ]L δ g > 0 Γ g = g
Γ [ δ ]L δ g > 0 E g = g Γ [ δ ⊗ (g,g) δ ](E ⇒ ϕ)
Γ [ δ; δ ](E ⇒ ϕ)
(Sync)
Recall the definition of δ ⊗ (g,g) δ (Definition 22), where time stretching for the
second dynamics δ is expressed syntactically by Lie derivatives. We call the four
premises Γ g = g, E g = g, Γ [ δ ]L δ g > 0, and Γ [ δ ]L δ g > 0
the synchronizability conditions. These obligations are usually easy to discharge.
The last premise, which we call the synchronized formula, is typically the core
remaining obligation.
Remark 25 (choice of (g, g)). In applying the (Sync) rule, one still has to
find a suitable synchronizer (g, g). This turns out to be straightforward in many
examples. In all the case studies in Section 6 and in Example 1, the exit condition
E is of the form x = x = C where C is a constant. This suggests the use of g = x,
g = x. Indeed, all our proofs use this choice of (g, g).
5 Implementation
KeYmaera X [17] is an interactive theorem prover based on the sequent calculus
formulation of dL. It is implemented in Scala, replacing its former system KeYmaera [16]. It has a web-based GUI environment, and a support of automated
theorem proving using computer algebra systems such as Mathematica [27].
203
Consequently, h is the constant function equal to 0, which implies that (ω, ω) ∈
g = g
. By definition, ξ is a solution of δ, so ω 0 −
δ
→ ω. Furthermore, by
Corollary 18, ξ ◦ K
−1 is a solution of δ. Thus ω 0 −
δ
→ ω and
(ω 0 , ω 0 ) −
δ; δ
→ (ω, ω).
The above lemma is a key observation in the current work. It allows us to
turn the relational dynamics δ; δ—expressed as a sequential composition in dL—
into a combined dynamics δ ⊗ (g,g) δ. Moreover, we can do so in a way that
the two dynamics are synchronized in a reparametrized manner, as specified
by (g, g). Such combination of two dynamics is crucial in exploiting the logical
infrastructure of dL and KeYmaera X—we emphasize again that the (DI) rule
does not support invariant reasoning about the relationship between δ and δ,
when the relational dynamics is expressed in the original form δ; δ.
The following is an incarnation of Lemma 23 as a proof rule. We assume that
a postcondition is a conditional form E ⇒ ϕ; E is called an exit condition. By
assuming that E implies g = g, we enforce the second condition (ω, ω) ∈
g = g
in item 1 of Lemma 23. The first three premises are there to ensure that (g, g)
is a synchronizer. Under these premises (the first four), the rule allows one to
transform its conclusion (about δ; δ) into one about the combined dynamics
δ ⊗ (g,g) δ, which is amenable to application of the (DI) rule, for example.
Theorem 24 (synchronization rule). The following inference rule is sound:
Γ [ δ ]L δ g > 0 Γ g = g
Γ [ δ ]L δ g > 0 E g = g Γ [ δ ⊗ (g,g) δ ](E ⇒ ϕ)
Γ [ δ; δ ](E ⇒ ϕ)
(Sync)
Recall the definition of δ ⊗ (g,g) δ (Definition 22), where time stretching for the
second dynamics δ is expressed syntactically by Lie derivatives. We call the four
premises Γ g = g, E g = g, Γ [ δ ]L δ g > 0, and Γ [ δ ]L δ g > 0
the synchronizability conditions. These obligations are usually easy to discharge.
The last premise, which we call the synchronized formula, is typically the core
remaining obligation.
Remark 25 (choice of (g, g)). In applying the (Sync) rule, one still has to
find a suitable synchronizer (g, g). This turns out to be straightforward in many
examples. In all the case studies in Section 6 and in Example 1, the exit condition
E is of the form x = x = C where C is a constant. This suggests the use of g = x,
g = x. Indeed, all our proofs use this choice of (g, g).
5 Implementation
KeYmaera X [17] is an interactive theorem prover based on the sequent calculus
formulation of dL. It is implemented in Scala, replacing its former system KeYmaera [16]. It has a web-based GUI environment, and a support of automated
theorem proving using computer algebra systems such as Mathematica [27].