As you may remember, some proofs that were supposed to be discharged by the automatic theorem provers in Rodin today were not proven. I am not yet sure why, but, barring some mistake in the model that went unnoticed, it may be due to a different version of Rodin with different heuristics in the automatic theorem provers.
For the remaining profs that should be proven, except those concerning invariant 5, what worked for me was:
- Go to the Proving perspective, select one unproven proof obligation, double click on it.
- In the left panel with the proof tree, cut (✀) / slash backtrack the search tree to the root, so that the proof three only contains the root.
- Select "lasso" to bring to the current hypotheses a set of relevant formulas.
In ny Rodin insallation, after this the automatic theorem prover is triggered and it performs a series of inference steps that end up proving the intended goal.
Best,