Division of Informatics, Edinburgh University ProveEasy A proof assistant for teaching logic Rod Burstall rb@dcs.ed.ac.uk Section 1 The proof assistant Introduction and motivation ProveEasy is a tool for teaching students to use logic, in a Natural Deduction style. It has a point and click user interface which minimises typing. It produces a readable proof rather then just a script for creating a proof as in HOL or Coq. The proof style is goal directed as opposed to the traditional style starting from premises at the top and finishing with the conclusion at the bottom of the page. In this respect it is similar to Coq and to the Edinburgh Lego system which partly inspired it. The original motivation was teaching a course on operational semantics of programming languages to computer science undergraduates. Logic The system is logic independent. The logic is specified by the "teacher", who also specifies problems in the form of propositions to be proved. The proof is carried out interactively by the "student". The logic is specified using a meta-language, the rule definition language, which uses first order matching and substitution respecting bound variables. Currently the language is untyped, relying on the teacher to input correctly typed expressions. Occasionally the student also has to take responsibility for type correctness (e.g. when instantiating a variable). A future version may include type checking. Problems and commands The interface starts up with a default file of problems. The problem names are shown in a choice list. The student proceeds to develop a proof for that problem as follows: * Choose a problem. The problem is displayed in the proof area. * Press Commands. This displays a choice list of commands. * Develop the proof by clicking a line in the proof and choosing appropriate commands. * Press Problems to redisplay the choice list of problems. Choose another problem. Press Save to save the proof at any point. It is only saved as text, it cannot be restarted. Press More Problems to input a load another file of problems. The proof window can also be used for inspecting and editing text files using Open and Save, for example problem, command or proof files. The text can be edited with the usual edit keys. After working with other files, press Continue Proof to go on with the current proof. Font cycles through fonts. Restart reloads and restarts the program. Quit quits. Sequents and problems A sequent consists of some Given propositions (possibly none) and a Show proposition (called the Givens and the Show for short). A sub-sequent of a sequent has the same Show and a subset of its Givens. We write a sequent Given P1 ... Given Pn Show R Or more compactly Given P ... Given Pn Show R. Example: Given Q Show R is a subsequent of Given P Given Q Show R. A problem is a sequent. We need to prove the Show from the Givens. A proof command generates a set of subproblems from a problem; each subproblem may add some more Givens and has a new Show. T solve the problem it is sufficient to solve the subproblems Example: The command "givenOr" on the problem Given S Given P or Q Given T Show Q or P generates the problems Given S Given P or Q Given T Given P Show Q or P Given S Given P or Q Given T Given Q Show Q or P Example: The command " Show And" on the problem Given S Given T Given U Show P and Q generates the subproblems Given S Given T Given U Show P Given S Given T Given U Show Q Example: The command "Given And" on the problem Given S Given P and Q Given T Show P generates the problems Given S Given P and Q Given T Given P Given Q Show P Proofs The proof is a tree whose nodes are sequents. The nodes are numbered and indented to denote the tree structure. Each node defines a context, namely the sequence of Givens on all the nodes in the path to that node (the path the node itself). The problem at a node is the context at the node together with the Show at the node. Rules A rule has a parent sequent pattern and may have some child sequent patterns. A sequent pattern is similar to a sequent but its propositions may contain rule variables. . The rule may also have some parameter variables. There are two (main) kinds of rule: * A Show rule has a problem pattern with no Givens. * A Given rule has a problem pattern with at least one Given. A rule is applied to a sequent and possibly some parameter values to produce some sequents (possibly none) as follows: * The parameter variables are replaced by the their values in the parent and children. * The parent sequent pattern is matched against the problem sequent to obtain values for the rule variables. * These values are used in the child sequent patterns to produce the child sequents. Commands A rule name together with possibly some parameter values forms a proof command. A command is applied to a node. The sequence of Givens the must be a Givens of the context at the node, thus determining a sub-sequent of the problem. Now the rule in the command is applied to this sub-sequent and the parameter values to produce some new sequents. These sequents are inserted below the node as new nodes. The Given command This command is special. It looks through the Givens in the current context. If one of them is identical to the Show it stops with no subproblems. Rewriting rules The special commands rewriteShow and rewriteGiven apply rewrite rules to the Show and Given propositions respectively. The available rewrite rules are tried in turn. Applying the commands again may result in further rewrites. Editing text files The text window may be used to edit files, for example problem or command files. Use the Open and Save buttons. Editing keys are available: ctrl-z (undo), ctrl-x (cut), ctrl-c (copy), and ctrl-v (paste). Use the Continue Proof button to resume work on the current proof. The Rule notation Defining a rule. The syntax for a rule is (where k, m, n are greater or equal to 0) RuleDefinition ::= proc rulename {parameter-1 ... param-k} { sequentPattern-0 sequentPattern-1 ... sequentPattern-m } Sequent-pattern ::= Given pattern-1 ... Given pattern-n1 Show pattern The syntax is based on the tcl language which requires spaces between symbols and a space between "}" and "{". A simple lexical check is carried out to see that these rules are obeyed. Patterns are terms of the object language term ::= ident | {term ... term} | term WITH term FOR ident | term REPLACING term BY term Here the ident may be a rule variable. The WITH substitutes the term for the identifier. The substitution respects bound variables in the sense that it does not take effect inside a binding of the identifier. The REPLACING construction replaces one term by another. Variables We must distinguish four kinds of variable * Rule variables. These appear only on the definition of rules. They are declared in a command file by RuleVars v-1 ... v-n * Bound variables. These appear in the problems and proofs. They are introduced by appearing after a binder, e.g. all or exists. Binders are declared in a command file Binders b-1 ... b-n * Local variables. A bound variable in the problem may become a local variable in a subproblem. To show " all k. P" we may show P for an arbitrary k. It is declared as a Given using var. In order to distinguish the local variable we call it n_ (or n_1, or n_2, and so on, to avoid clashes with the names of other local variables). However this marking is done automatically when the rule is applied. It is not written in the rule. * Parameters. These are additional arguments in a command. They are named at the beginning of the rule definition, and in the body of the rule they are preceded by a $ sign. Consider for example the induction rule for numbers Show all n . P Show P 0 Given var n Given P Show P WITH {suc n} FOR n The problem Show all k .{{suc k} > 0} produces the subproblems Show {suc 0} > 0 and Given var k_ Given {suc k} > 0 Show {suc {suc k}} > 0 Here n is a rule variable, k is a bound variable and k_ is a local variable. Parameters, on the other hand, enable us to direct a proof by specifying how to apply a command to decompose the problem at a node. In the case of a command with a "Show rule", either the Show of its parent sequent subsumes the Show at the node or else the rule does not apply; however, to match the associated rule of a more complex command with a sub-sequent of the problem at the node, we are required to detail (by node number) which of the Givens in the context we expect to provide each in turn of the Givens in our rule's parent sequent pattern. At present, the command syntax also requires parameters to be located in the context by a Path statement, but this may not be necessary in future versions of the system: Rule givenImpFwd {g1 g2} { Path $g1 $g2 Given PP -> QQ Given PP Show RR ###### Given QQ Show RR } Command files Logics, for example predicate logic, and particular theories, for example the theory of natural numbers or the theory of a programming language, are described by command files. A command file contains * Declarations of rule variables: RuleVars ... * Declarations of binders: Binders ... * Definitions of rules: proc ... * Definitions of rewrite rules Rewrite ... Problem files Problem files contain * Lists of the names of command file to be loaded: Commands ... * Problem definitions: Problem ... A problem definition is of the form Problem problemName { Given term ... Given term Show term } 5 5 5 5