Subject: GUI

Keywords: ::proof

Title: proof editor concepts

--------------------------------------------------

Proof editor manages three levels of proof representation:
  - lib proof : proof as stored in library
  - edit proof : proof as modified in editor
  - view proof : proof as modifed in window

The lib proof is a PRF object. A PRF object is primarily an inf_tree.
An inf_tree is a tree of INF objects. An INF object is primarily a refinement.
A refinement is a goal, tac, partial extract, references, and subgoals.
A goal is a sequent and a list of annotations. 
See also How proofs are stored in the libary.

The edit proof is a tree of proof nodes. A proof node is initially
derived from an INF object when a proof is viewed.

The view proof shows a segment of the edit proof. User interaction
can modify the view proof. The view proof is saved back to the edit proof
when required.

Refine: the only way to modify a lib proof is via refinement.
When a step is refined a new INF object is created. A new inf_tree
is created from the new INF object keeping old subtrees that still
match the new subgoals. Then new inf_tree is then cut into the old inf_tree
at the appropriate address and saved into the PRF object.

When a refinement occurs the new edit_proof_node is broadcast to the editors
and the proof data is pushed up the chain of proof representations to the view.
Unsaved edit or view changes will be lost if in scope of tree changed.

Invoking refinement from proof editor will save the view proof to the edit proof
and then do the refinement using the tactic from the edit proof and the sequent
from the lib proof.

Changing the tree segment viewed in the view proof will save view proof
changes to the edit proof.

Each node keeps variants of the tree, this is a little used but 
important feature that needs better accessibility/documentation.
 
There is a edit/view variant which chunkifies and hides the hyps to 
make proof display more tractable with long hyp lists.  

⋅
--------------------------------------------------

Authors: RICH:t

Contributors: :t

⋅

Home