Writing Faster Proofs

Sometimes proofs take a long time to write/check. This page contains tips for writing proofs that are more efficient.

Solve ODE's before branching

Solving ODEs using diffSolve takes a long time. You can expedite these proofs by solving the ODE before decomposing into control cases. Concretely, suppose you have a controller of the form:

[{a ++ b ++ c}; ODE]P

One way of proving this is by breaking the proof into three cases:

[a][ODE]P    [b][ODE]P    [c][ODE]P
-------------------------------------
       [{a ++ b ++ c}][ODE]P
-------------------------------------
       [{a ++ b ++ c}; ODE]P

But now you have to run diffSolve three times! A much faster proof is to run diffSolve on the inner formula [ODE]P:

[a]Q           [b]Q         [c]Q
-------------------------------------
       [{a ++ b ++ c}]Q
-------------------------------------
       [{a ++ b ++ c}][ODE]P
-------------------------------------
       [{a ++ b ++ c}; ODE]P

where Q is the result of running diffSolve on [ODE]P.

Lazy vs. Eager QE

When all we have left is arithmetic, you might use master or you might use the QE tactic, but these will actually do different things. master will split as many logical connectives as it can and send the (possibly many) resulting subgoals to QE individually, whereas the QE tactic will send the current formula to QE all at once. Sometimes one of these will be much faster than the other. If master produces a very large number of branches, QE might be faster, and if master lets you get rid of some variables, then it could be faster. If your current method is too slow, experiment with the other one - it all depends on the model you're proving.