Provable/Lemma management in Web UI

[nrfulton]

It should be possible to extract a subgoal, prove that subgoal in another window, save the proven subgoal as a lemma, and then use the proven lemma in your original proof.

Note that this functionality already exists in the core+tactics language (proveAs/lazyUseAt or simply useAt), but isn't exposed to the web UI. Integrating with HyDRA so that the lemma cache is repopulated on-demand would also be nice.

1. Saving Lemmas

• Add a "Save As Lemma" option in the drop-down menu on the proofs-of-model page, which allows saving the lemma with a name.
• Add a lemmas table that stores the name, conclusion, and proofId of each lemma.
• Add a mechanism for re-proving saved lemmas and then storing them in the lemma database (should do nothing if the lemma already exists in the lemma database and matches the expected conclusion). reProve(lemmaId)
• Run this mechanism on every available lemma on server startup.

2. Using Lemmas

• Add a tactic for using a lemma and expose this to the web ui.
• Add a new REST request for running a lemma. If the lemma does not exist in the lemma database but does exist in the lemmas table, try to reProve(lemmaName).
  • Add an element to the "Propositional" drop-down menu in the web ui. When clicked, search all elements of the lemmas table for something that matches the current subgoal. Prove by a useAt, doing a reProve(lemmaname) if there's a correct conclusion in the database but not in the lemma cache. Display errors otherwise "Current goal does not match conclusion of indicated lemma", or "Indicated lemma does not exist", or "failed to re-prove lemmaname: your proof of poofIdHere was deleted or no longer works in the latest version of KeYmaera X".

[aplatzer]

That'd be a really great mechanism! Much of the lemma use mechanism ought to be able to reuse the useAt mechanism. The only missing bit is the key, which, however, could be marked with the mouse or selected with shift-cursor keys or so from the web UI in the lemma.

[smitsch]

Updated lemma UI: creating and using lemmas is accessible from the Browse menu.