Solid Intuition/Screen

From SE Wiki
Jump to: navigation, search

The screen has principally three parts: the current focus expression on top (quite small), while the larger lower part is split in two: One side has expressions to replace the focus with, which are generated by matching laws from theories and context. The other side is a browser for laws and context.

the focus expression

This shows the expression on which we are currently working. Initially it is the statement which we want to prove. After zooming in, it is a sub-expression of that statement and after applying some proof steps it is the current state of the proof.

zoom

We can focus in on a sub-expression by pointing the mouse on one side of the expression's top-most operator and turning the mouse-wheel once. For zooming out, turn the mouse-wheel the other way anywhere. In expression where the top-most operators are associative or continuous (such as "a+b+c" or "a≤b<c"), we have special zooming yet to be specified and a coloured expression background moving with the mouse pointer which always shows what the focus will be if we zoom in at that point.

direction

Direction operators can be:

= : ≤ ⇒

The operators exist only in one direction. Two directions can actually be used by placing the operator to the left or the right side of the focus.

The initial direction of an expression to proof is "⇒ exp" with an implicit "T" that we are aiming for. Whenever we zoom into a monotonic operator, the direction stays the same. When zooming into an anti-monotonic operator, the direction switches sides. When zooming past a direction operator (= : ≤ ⇒) then this operator becomes the new direction (it is inverted if previously our direction was "exp ⇒").

When proving a statement about strictly smaller (or proper subset), the program automatically keeps track of having at least one strictly smaller step in the chain. (Maybe it will display "<" as direction of proof as long as no such step has been executed.)

the "next step" list

The program automatically matches the current focus expression with all the available laws. If one side of a law matches the focus, they are unified and the other side of the law is displayed as a potential next step. For this to happen, the top-most operator of a law has to be equality or correspond to the current direction of proof. Every item in the list is labelled with the name of the law that produced it and with the direction operator that the proof step would be. Selecting an item executes the proof step.

Steps can be selected using the number keys on the keyboard. This way simple steps can be executed without moving the mouse out of the focus area.

the law browser

The law browser has a line of tabs on top which switch between sets of laws to display. The most important tab is the "context" tab which shows all the local laws which are result of focusing deeper into an expression. This view helps the user understand how context laws work by observing them while zooming on different sub-expressions.

The law browser can also be used to find a law that one would have expected to show up on the "next step" list and figure out why they are not there and what preparatory work is needed to make them applicable. Laws can be found by theory, by name and by pattern matching.