(novice question) Automatic prove does not do anything. about keymaerax-release HOT 1 CLOSED

The feedback from the user interface might be a little surprising here. To understand what is going on, we have to look a little into the proof techniques of KeYmaera X.

For starters, here's a tutorial that introduces common modeling examples gradually. There's also an extensive set of lecture notes with details on the proof techniques.

The master tactic does an automated proof search, which may or may not succeed. When the master tactic stops with open proof goals (tabs), it means either

• There's a loop without @invariant annotation and master did not find a loop invariant on its own -> solution: provide a loop invariant (see below what an invariant annotation tells KeYmaera X, and Lecture Notes)
• There's an unsolvable differential equation without @invariant annotation and master did not find the appropriate differential invariants on its own -> solution: provide a differential invariant (Diff. Inv. and Diff. Cuts)
• The formula is wrong -> solution: click Inspect->Counterexample (only for real arithmetic formulas, i.e., not for formulas of the form [a]p or <a>p), which return values that make the assumptions left of the turnstile |- true but the formulas right of the turnstile false. Or click Inspect->Find Assumptions to get suggestions what KeYmaera X thinks is missing. But carefully scrutinize the suggestions: additional assumptions can result in a vacuous proof, e.g., controlsig=50 & controlsig=4 -> whatever and master will happily prove that for you.

Now let's look into your particular example. The program contains a loop, the annotation @invariant tells the master tactic about a formula that it should try as a loop invariant in an induction proof. Such a proof has three cases:

1. Base case: the invariant must be true in the beginning (in this particular example: controlsig=50 & temp=18 & setpoint=23 -> temp>10)
2. Use case: the invariant must be strong enough to show the safety property (here: temp>10 -> temp>20)
3. Induction step: the invariant must stay true through one run of the loop body (here: temp>10 -> [program]temp>10)

Your tactic ending in <(nil, nil) tells that after running master there are two open goals (tabs). This means, that master was able to prove one of the cases automatically, but not the other two. They are quite likely wrong, because the program looks like it should be handled automatically even though the differential equation does not come with an @invariant annotation. Indeed, temp>10 -> temp>20 doesn't look very true. Try Counterexample on that branch, it'll show something like temp=11. The same is true for the induction step: even when starting at temp>10 (say temp=13) the program can end up at temp<=10, because the differential equation decreases temperature (temp'=-50*0.01), so if we just follow the differential equation long enough the temperature will drop below 10. This means that both the invariant and the program must be changed to guarantee your safety property. Pay particular attention to the use case and the induction step. Usually, the induction step is the hardest to get right, because it requires a combination of finding the right invariant and writing a correct program.

A good way of learning about the different proof techniques by just interacting with KeYmaera X is when you hover the mouse over formulas. Turning a formula background dark on hovering is the KeYmaera X way of telling you that you can do something with that formula. Right-click to see what particular proof tactics apply. If you are willing to spend a little extra time: manual interaction gives you more control over the proof, more insight into your model, and facilitates learning in our experience.

from keymaerax-release.