# 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.

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:

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

### Menu

#### 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 Q_{0}.

Prooftoys has the same theorems as Q_{0} 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 Q_{0}, but two are generalizations
that in Q_{0} 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 Q_{0} 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 Q_{0} 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)

## No comments:

## Post a Comment