Matita HomeMatita HomeDuring an interactive proof, the proof status is made of the set of sequents to prove and the partial proof built so far.
The partial proof can be inspected on demand in the CIC browser. It will be shown in pseudo-natural language produced on the fly from the proof term.
The set of sequents to prove is shown in the notebook of the authoring interface, in the top-right corner of the main window of Matita. Each tab shows a different sequent, named with a question mark followed by a number. The current role of the sequent, according to the following description, is also shown in the tab tag.
Selected sequents (name in boldface, e.g. ?3). The next tactic will be applied to every selected sequent, producing new selected sequents. Tacticals such as branching ("[") or "focus" can be used to change the set of selected sequents.
Sibling sequents (name prefixed by a vertical bar and their position, e.g. |3?2). When the set of selected sequents has more than one element, the user can decide to focus in turn on each of them. The branching tactical ("[") selects the first sequent only, marking every previously selected sequent as a sibling sequent. Each sibling sequent is given a different position. The tactical "2,3:" can be used to select one or more sibling sequents, different from the one proposed, according to their position. Once the user starts to work on the selected sibling sequents it becomes impossible to select a new set of siblings until the ("|") tactical is used to end work on the current one.
Automatically solved sibling sequents (name strokethrough, e.g. |3?2). Sometimes a tactic can close by side effects a sibling sequent the user has not selected yet. The sequent is left in the automatically solved status in order for the user to explicitly accept (using the "skip" tactical) the automatic instantiation in the proof script. This way the correspondence between the number of branches in the proof script and the number of sequents generated in the proof is preserved.