A draft list of the features that need to be implemented for SI Milestone 1.
The most important difference to existing graphical math editors is that there is a set of primitive proof-step generating rules which basically only let us apply axioms and laws which are formulated in the expression language themselves. Every law that we prove therefore extends our portfolio in possible proof steps. Axioms can be added just be typing them in as an expression.
The screen is divided into a part the shows the current proof (attempt) and another part that shows laws (and axioms). Selecting a (sub)expression in the proof will automatically show all the matching laws on the other side of the screen and sort them by closeness of match. The law can then be applied by one single click.
- Data model for Expressions.
- Saving and loading of Expressions from the data model to external files and back.
- Rendering of Expressions on Screen (in M1 with no frills: the output is an unmodified text window).
- Entering of expressions.
- Keeping a collections of theorems (each of them being an expression), stating the type of free variables in the theorems, loading and saving the theorems (probably with a set of laws loaded automatically).
- Transparent Parsing:
- when the cursor (or mouse) is near an operator, the editor will show the implicit parenthesis around that operators sub-expression. Example: 1 + 2/3. Touching + shows as (1 + 2/3), while touching / shows as 1 + (2/3).
- when the cursor (or mouse) is near an associative or continuing operator then the status line will show the word "associative" or "continuing" and highlight all other operators on the same level of associativity or continuation.
- Zoom: any line from a proof can be hidden using the scroll-wheel of the mouse. The hints before and after that line will then be shown together on one line. Optionally we could also zoom out some of the hints, so that only the most interesting hint, or none, is left.
- Unification of expressions with free variables, taking into account associativity and symmetry. (Associativity is trivial and symmetry might take some backtracking, but is still simple enough.)
- Data model for proofs consisting of
- an expression that is the hypothesis (which contains all prerequisites which are not theorems as antecedents of an implication)
- the name of the proof format of which there are two:
- if the hypothesis is of the form X <> Y, where <> is a transitive relation (e.g. equality, implication, greater/smaller than, ...), the proof can have the form X <> ... <> Y. We'll call this Proof by transitivity.
- in all other cases for hypothesis H the proof will have the form H <= ... <= Th, where <= is implication and Th is a theorem. We'll call this Proof by reduction to a theorem.
- note that in our current working hypothesis, we do not need special proof formats like "by case distinction" or "by induction", neither are there special proof rules for this. It is just done by applying the case law (if-expression) and the induction law, which are both ordinary theorems.
- the proof itself as an expression with hints.
- Application of rules. (Every rule can be applied forward or backwards, depending on whether the user selected the expression before or after the "..." in the proof.)
- instantiation of free variables and instantiation of functions (besides equivalence and implication, functions are the only language elements that always need to be hard-wired).
- substitution of equals for equals (this is also covered by the "instance rule" of aPToP). This means
- given a theorem of the form "a=b", obtain a new line in the proof expression, where the previous line has an "a" and the new line has a "b" instead, the lines are connected by "=".
- given any theorem, whose instance appears in the proof expression, replace it with "T" and connect the lines with "=".
- substitution with monotonicity (i.e. weakening/strengthening). Same as above only substitute "==>" for "=". Antimonotonicity automatically changes it to "<==".
- substitution with context (i.e. window inference)
- equality substitution with one of the laws of inclusion, i.e. applying the law a==>b can be used to replace a by "a and b" or to replace b by "b or a". (same for <= and min/max and for : and ,')
- arithmetic, which evaluation of expressions containing only numbers and arithmetic operators (+, -, *, /, power). To simplify expressions with variables, the laws of arithmetic have to be used manually.
- laws can also be applied to expressions in the context (or even in global laws), the resulting new expression is then immediately added as a new context law (this emulates reasoning which is often implicit in calculational proofs, e.g. in discharging antecedents of laws)
Note that substitution is the principal way of applying laws: either the law is an equality or implication, in which case one side of the law is unified with a sub term and replaced by the other side, or the law itself is unified with the sub term and replaced by T.
The following rules could be automatically generated from theorems, but will probably be hard-coded in M1:
- permissible relations to be used in place of <> in a proof by transitivity
- symmetric, associative operators
- monotonicity and antimonotonicity in the generalised substitution rule
- generation of local hypothesis in window inference
Robinson's Ergo Prover also had window-inference hard-coded in the first version and later made it generic.