More: if you go to https://wp.software.imdea.org/cbc/ and click on the entry corresponding to the lecture on 13/03/2024, there is a link to a short video where I show possible actions that may work to discharge easily the proof obligations that were not automatically proved.
Best / Saludos,
Manuel
On Thu, 14 Mar 2024 15:57:01 +0100, Manuel Carro manuel.carro@imdea.org wrote:
To add some more information to what happened (or, rather, what did not happen) yesterday during the lectures, I wrote to the developers of Rodin and this is their answer:
We believe that this issue is caused by a bug introduced in Rodin 3.8 related to the handling of rewritten equalities, which are incorrectly being hidden. Therefore, provers like ML do not have access to these equalities and may fail to prove goals that were proved in previous versions. It will be fixed in version 3.9, for which a release candidate will be published soon.
So it aligns with what I suspected.
I cannot evaluate its real impact at this moment, except that some proofs (as we have seen) won't be automatically discharged upon saving the model, but may need some manual intervention. It has been very little so far, so unless I find a more serious bugs, I think it is something we can live with. I will not change the slides, as it does not make a lot of sense to update the slides to adapt to something that is a but and that will, hopefully, disappear in the next version of Rodin.
Best / Saludos,
Manuel
On Thu, 14 Mar 2024 00:43:14 +0100, Manuel Carro manuel.carro@imdea.org wrote:
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,