Sunday, March 31, 2019

ITP2019

ITP2019

A Proof Assistant for Beginners

Abstract

Prooftoys is a web-based visual proof assistant, written in JavaScript to run in modern web browsers. It reflects the author’s belief that it is time for computer tools to become a welcome improvement pencil and paper in in basic proof-based mathematical problem-solving.

Its purpose is to support non-experts in exploration and self-education in logic and axiomatic mathematical reasoning, using the real numbers as a starting point. The design is driven by an overriding concern for simplicity and a less difficult learning process. It also strives for compatibility with textbook presentations of mathematical concepts.

This paper introduces the system, its logic, implementation, and user interaction. It aims to acquaint a technical audience with aspects of interest, though the system itself is designed for less technical users. The source code repository https://github.com/crisperdue/prooftoys contains the full source code and documentation, and the project Web site http://prooftoys.org/ is updated frequently with recent versions of the working system.

Introduction

To a new user, Prooftoys is a list of steps in a proof, displayed on a Web page. The list might be open for the user to extend and modify, or it might be locked down to be viewed but not changed. It might be on the Prooftoys web site (http://prooftoys.org/proofbuilder.html), or anywhere else on the web. It can operate in all of these modes.

All aspects of the system are under continuing development, so some parts should be expected to evolve in the future.

Prooftoys at work

Proof displays

In the user interface a proof is just a sequence of proof steps, each being an axiom, a definition, a fact already known true, or the result of applying some rule of inference to some input values, which may be proof steps, parts of proof steps, terms in the language, or other values.

Sample proof display A live version is at http://prooftoys.org/proofbuilder.html?fact=SubclassInter&details=true

Each step is numbered, with a statement of the step followed by some description of its derivation. Hovering over the step number highlights key step(s) and/or parts of the steps involved in deriving the step. Assumptions of types, using “ind”.

Assumptions of the form R x (that certain variables are real-valued) are omitted by default from the displays, and repetitive displays in the left side of a step may be reduced to just an ellipsis if they are identical to the previous step.

Proof step details

Almost all proofs use theorems that have already been proved, and most proof steps are really compositions of many smaller steps. Proof displays give the user easy access to proofs of theorems and details of proof steps by clicking within some part of the description of the step that is highlighted in blue.

So in the proof above, clicking on the word “use” in step 2, then digging down to details of details eventually takes us to:

proof display step details

This reveals the final phase of the proof of the key tautology for step 2.

Proof editing

  • “Point and click” selection – of steps and arbitrary terms
  • Simple editing of existing proof, with deletion and inlining of details

Selecting, drilling down. Viewing proofs

Levels of difficulty

Saving and restoring work

Logical concepts

The logic is based on Alonzo Church’s simple type theory as developed by Peter Andrews under the name Q0.

Prooftoys has the same theorems as Q0 and the same rule of inference, which allows replacement of an arbitrary term with one always equal to it. The axioms are like the five axioms of Q0, but two are generalizations that in Q0 are proved as theorems. The definitions of the boolean operators (except boolean equality) are defined by their truth tables by axiomatizing if-then-else. Prooftoys implements Q0 as a Hilbert-style system in the sense that it does not support a concept of hypotheses except as conjunctions of assumptions that form the antecedent of a conditional statement.

The logical core supports simple constant definitions that take the form of equalities with the defined name on the left and its definition on the right, with the usual restrictions on freshness of the name and absence of free variables in the right-hand side.

The real numbers are treated as a subset of the logical base type of individuals, and are axiomatized as a complete ordered field. This approach gives the math in Prooftoys a significantly different feel than other systems based on type theory. In particular, statements about the real numbers must explicitly include assumptions that certain variables have values in ℝ, where in other systems numbers are introduced as new types of the logic itself

Given that the reals are treated as a subset of the individuals, the integers, rationals, and natural numbers naturally become subsets of the reals, and there is much less need for explicit presentation of types of variables. On the other hand, closure of operations must be stated explicitly, and assumptions that an expression has a real value must be proved.

Logical kernel

The inference component of Prooftoys is built as a logical kernel, with additional functionality implemented by additional JavaScript functions that call the kernel functions and each other. JavaScript does not offer guarantees that new code will not bypass the kernel, but this aspect of the design still greatly improves the trustworthiness of the system.

The logical kernel supports assertion of axioms, starting with the logical axioms, and builds proofs withe Q0 primitive inference rule R, which takes a proved statement, a path specifying a term within that statement, and an equation as input. It returns a new proved statement as its result.

An empty path refers to an entire statement, and each component of a path indicates which part of the top-level term to traverse. A function invocation has a function part and an argument part, and a lambda term has a bound variable and a body. A path is a sequence of zero or more of these indications.

The kernel also supports assertion of axioms by an assert function that takes a statement in the logic as its only argument.

New proof steps (“steps”) are built up from axioms, constant definitions, and use of rule R. Each proved statement is linked to the name of the inference function that produced it, and all the arguments passed to that function, so the step can be reproduced.

Additional inference rules are implemented as side-effect-free JavaScript functions that accept arguments and return a proof step.

A step may depend on other steps, or on facts already proved as part of the system. Or it may not depend on other steps, for example being an axiom or theorem, or a step that proves a tautology from its statement.

Additional inference rules are implemented as JavaScript functions that accept arguments such as terms of the language and previously proved statements.

Notation

Identifiers are composed of alphanumerics with an optional numeric subscript indicated by appending _<digits>. Sequences of most other printing (currently ASCII) characters are considered to be operators. There are also integer literals within the limits of exact arithmetic in JavaScript.

Variable names are single-character identifiers, possibly subscripted. Operators and all other identifiers are reserved for constants, and operators can be declared internally as infix with a precedence. At present there is not an explicit syntax for entering an explicit type (such as individual) through the language.

Any expression can be enclosed in parentheses for grouping, a sequence of proof steps.
In this sense, the proof editornd an operator enclosed by itself in parentheses is allowed to represent its designed to support forward reasoning.

[[Move this:]] Backward reasoning from a goal toassociated constant. Notations of the form {<var>. <term>} and [<var>. <term>] indicate lambda expressions. For example {x. p x} its proof is also supported idiomatically by sthe same as λ x. p x in lambda notarting with with a step of the form conditions ⇒ goal, where goal is the conclusion part of the desired theorem. on. Terms with quantifiers use this notation, e.g. forall {x. p x ⇒ q x} ⇒ subclass p q. The syntax with braces is intentionally suggestive of set/class notation, but brackets have the same meaning.

Convenient inference

Tautology checking

The tautology checker is a function that takes a propositional calculus statement as its argument and attempts to prove the statement true. The result is a proved duplicate of the input. Like all proved statements in Prooftoys, the result is connected to the steps from which it was derived.

Rewriting

Rewriting could be considered the characteristic form of reasoning in Prooftoys. When a basic math text describes use of a basic law such as commutativity, it is effectively referring to rewriting.

Prooftoys matches a statement of equality (or logical equivalence) with an occurrence of an arbitrary term in some statement. If it finds a substitution into the equality that makes its left-hand side identical to the term it is matched against, the rewrite applies this substitution to the equality and replaces the occurrence with the right-hand side of the resulting equality.

The equality can be conditional, and if so the replacement step adds the antecedent (after substitution) to any assumptions as it replaces the occurrence of the term.

The system uses rewriting to accomplish other traditional forms of reasoning as well, described below.

Forward and backward reasoning

(goals and subgoals?)

The user interacts with the proof editor primarily by entering one step after another, producing a sequence of proof steps. In this sense, the proof editor is designed to support forward reasoning.

It is also straightforward to reason backward from a goal. For example a proof of a theorem of the form conditions ⇒ conclusion could start with an already-proved fact that has the same form but different conditions, even a tautology such as conclusion ⇒ conclusion.

Other convenient inferences

Simplification

Auto-simplification

Supporting mechanisms

Fact registration and lookup

Matching / substitution finding

Higher-order matching

Assumption management

Some basic and ubiquitous issues related to assumptions are handled internally to some of the rules of inference, such as rewriting rules. Among these are

It deduplication ofes assumptions, removal ofes assumptions trivially known to be true, such as “3 is a real number”, and handling of closure of operations by reducing reduces type assumptions on terms such as R (x + y) to R x & R y, and puts assumptions into a standard order for consistency between steps.

Working with real numbers

Comparison with other tools

Metamath, Mizar, (no tactic proofs)