Feature request: proving TCCs for specific lemma only

[Alberto Ercolani]

Hello Paolo,

I would like to ask you whether it is a problem for you to add an additional functionality to VSCode-PVS.

Recently i found myself proving several lemmata for a project of mine, and notice that my statements generate tens of obbligations: I often have to modify my statements and before I start proving them I must discharge all corresponding TCCs.

In the 99% of the cases they are proved by (subtype-tcc) without any human intervention: my theory currently contains 53 TCCs.

Would it be possible to discharge only TCCs related to a specific lemma?

I think this would allow to speed up proof attempts a lot.

Thanks in advance,

Alberto

[Paolo Masci]

Alberto, yes, this can be done -- thank you for suggesting this feature.

I will implement the functionality in the coming days and share a new pre-release in this thread.

Thanks,

Paolo

[Alberto Ercolani]

Thanks Paolo, can't wait for it to be implemented!

Regards,

Alberto

[Paolo Masci]

Alberto, at the following link you can find a new pre-release 1.0.64-gamma with the requested functionality: https://drive.google.com/file/d/1-i8sSJFmrMu_Q2py0abL5N5TmOBArEqW/view?usp=sharing

This new version provides:

- a new inline command "discharge-tccs" over a formula in the pvs files -- you can use this command to discharge TCCs that match the formula name (i.e., those that are labelled <formulaName>_TCCx)

- a new inline command "discharge-matching-tccs" over a formula in the tcc file -- you can use this to discharge a group of TCCs generated from a same formula or function.

- new menu elements in Workspace Explorer -- when right-clicking over a TCC, you can now select "Discharge Matching TCCs"

Please try it out and let me know in the case you have additional suggestions for improvements.

Thanks,

Paolo

[Alberto Ercolani]

Hey Paolo, I tried the pre-release and found the new feature to be even better than expected!

The only improvement that comes to mind is generating a summary files restricted to matching TCCs just tried; however the tool is already great as it is!

Thanks!

Alberto