Oak Tutorial

Installation

See here for how to install Oak.

Usage

Oak is a command-line application which takes a proof file as input, and tells you whether or not the proof is correct.

oak [-v] [-c] [-f] [-m] [-w] <filename>
  -v  print the version number of Oak
  -c  check for unneeded citations
  -f  look for a fix
  -m  assume until marker
  -w  wait for validity (does not change proof outcome)

Getting started

Let's get started with Oak. To begin, we'll create a one-line proof. Make a new file called "proof.oak" and open it with a text editor. In the file, put the following line:

x or not x

Save your file, then go to the command line, and from the folder where you created your file, run:

oak proof.oak

You should see the following output:

proof.oak: processing line 1
all lines accepted
proof successful!

This tells you that your one-line "proof" was correct. Since x or not x is a simple tautology, Oak was able to accept it outright, without needing any further justification from you.

Now let's see the output for an incorrect proof. Change proof.oak to the following:

x or y

We get:

proof.oak: processing line 1
line 1: invalid derivation "x or y"

This tells you that your proof is not correct. That's because the statement x or y is not valid (universally true): if x and y are both false, then the statement is false.

`axiom`

Any statement can be accepted by making it an axiom. Change your file to:

axiom for all x, p(x)

The command axiom simply accepts the accompanying statement without proof. Oak reports that the proof is correct, and notes that the proof file contained an axiom.

proof.oak: processing line 1
all lines accepted
1 axiom in proof.oak
proof successful!

`so`

Once a statement is accepted, it goes into something called the buffer. The command so uses the current buffer to prove its accompanying statement. Try the following:

axiom every man is mortal
axiom Socrates is a man
so Socrates is mortal

You get:

proof.oak: processing line 1 2 3
all lines accepted
2 axioms in proof.oak
proof successful!

Above, the first two statements go into the buffer. Then so uses them to prove the third statement. After so proves its accompanying statement, it clears the buffer, and then puts the accompanying statement in it. The buffer after a so therefore contains only the accompanying statement. For example:

axiom x and y
so x
so not not x
so y

gives

proof.oak: processing line 1 2 3 4
line 4: invalid derivation "y"

After the second line, the buffer contains only x. That's enough to prove the third line, after which the buffer contains only not not x. The fourth line then fails.

Until you use so, the buffer accumulates new statements, but is not used in deriving them. Each new statement is derived independently, until so is reached, at which point the buffer is used.

Labels and `by`

It is possible to give a statement a label, and refer to it using by.

axiom A1: x and y
x by A1
y by A1

Note that labeled statements do not enter the buffer. They can only be accessed by their labels.

axiom A1: x and y
so x

proof.oak: processing line 1 2
error at line 2: nothing for "so" to use

Labels can be written either after commands (as above) or before them (as below).

A1: axiom x
A2: axiom y
x and y by A1, A2

proof.oak: processing line 1 2 3
all lines accepted
2 axioms in proof.oak
proof successful!

`now` blocks

A now block creates a new buffer. Statements inside the block use the new buffer. At the end of the block, its buffer is added to the outer buffer.

axiom A: for all x, p(x)
axiom B: for all x, p(x) implies q(x)

p(i) by A
so q(i) by B
now
  p(j) by A
  so q(j) by B
end
so q(i) and q(j)

Here, the so in the now block uses only the inner buffer p(j), and not the outer buffer q(i). However, it can still access labeled statements with by. At the end of the now block, its final buffer q(j) is added to the outer buffer, which then contains both q(i) and q(j).

`suppose`

axiom A1: x or y
suppose not x
  so y by A1
end
so not x implies y

The suppose command creates a new buffer containing the accompanying statement, in this case not x. When a suppose ends, it takes its final buffer, makes it conditional on the supposition that started the suppose, and adds the result to the outer buffer. Here, the inner buffer y is added to the outer buffer as not x implies y. The so in the last line then uses the outer buffer to prove its accompanying statement.

The suppose command can be used for proof by contradiction.

axiom A1: for all x, p(x) implies q(x)
axiom A2: for no x, q(x)

suppose for some x, p(x)
  so q(x) by A1
  so contradiction by A2
end
so for no x, p(x)

Comments

Oak supports both line comments and block comments.

/#
  Here is a block comment at the beginning of the proof.
  ...
#/

x or not x  # this is a tautology

Conditions

Conditions can be placed on quantified variables by using the operator where (or its alias such that).

axiom for all x where p(x), q(x)
axiom for all x such that q(x), r(x)
so for all x, p(x) implies r(x)

In addition to where and such that, there are "shortcut" operators for common conditions. These include in and not in, inequalities (like <), and set relations (like ⊆).

for some A ⊆ B, p(A)
for all i,j > 0, q(i,j)
for some x in S and y in T, r(x,y)
for at most one c ≠ d, s(c)

You can also use arbitrary predicates as conditions. For example, instead of

for all x, whale(x) implies mammal(x)

you can write

for all whale x, mammal(x)

`take`

With a take block, you can prove something about an arbitrary variable meeting some condition, and then generalize the result to all variables meeting that condition.

axiom A1: for all x in S, x is in T
axiom A2: for all x in T, x is in U

take any x in S
  so x is in T by A1
  so x is in U by A2
end
so for all x in S, x is in U

`assume`

While working on your proof, you might want to temporarily leave a "gap" to be filled in later. If you use axiom for these gaps as well as for actual premises of your proof, it could become hard to keep track of which are which. For this reason, Oak has the command assume. It's like axiom, but generates a warning that your proof is incomplete. Thus, you can use it for "gaps", and as long as it is present, Oak will remind you that your proof is not finished.

assume can also be used in places that axiom cannot, e.g. in a suppose block.

suppose x
  assume y  # will prove this later!
end
so x implies y

proof.oak: processing line 1 2 3 4
all lines accepted
proof.oak: assumption on line 2
proof incomplete due to 1 assumption

A series of statements can be assumed with begin assume and end assume.

# just assume these for now
begin assume
1: x
2: y
end assume

x and y by 1,2

`proof` blocks

Instead of using so or by to justify a statement, you can provide a proof block. In the block, you can use thesis as a shortcut for the statement to be proved.

A1: axiom for all x, p(x) implies r(x)
A2: axiom for all x, q(x) implies r(x)
A3: axiom for all x, p(x) or q(x)

theorem 1: for all x, r(x)
proof
  take any x
    if p(x) then r(x) by A1
    if q(x) then r(x) by A2
  end
  so thesis by A3
end

r(a) by theorem 1

proof.oak: processing line 1 2 3 5 7 8 9 10 11 12 14
all lines accepted
3 axioms in proof.oak
proof successful!

Actually, the "theorem" above is simple enough that Oak can prove it directly from the axioms (try it!); the proof block here is just for the sake of the example.

`define`

For your convenience, statements beginning with an existential quantifier bind variables so that they can be used in subsequent lines. Variables bound in this way can later be rebound. Below, x is bound on line 1, then rebound on line 3. Thus, the x on line 2 is a different x than the one on line 4.

assume for some x, p(x)
so p(x)
assume for some x, q(x)
so q(x)

To guarantee that a variable keeps its original binding, use define. Variables bound with define cannot be rebound in the same scope. This ensures that a variable you bind at the beginning of your proof will have the same binding at the end.

assume define x such that p(x)
so p(x)
assume for some x, q(x)  # error

Notice that the define above is preceded by an assume. To define a variable with a condition, you must show that such a variable exists, just as if you had used for some instead of define.

Tie-ins

When you bind a variable, you can give it a tie-in. Tie-ins are statements about variables that "follow them around", meaning you do not have to cite them when you use the variable. The operator with creates a tie-in.

axiom A1: there is an n with p(n)
axiom A2: for all x, p(x) implies q(x)
q(n) by A2  # no need to cite A1

Here, the variable n is given the tie-in p(n). Henceforth, whenever n is used, p(n) is automatically included. Thus, line 3 does not need to cite line 1.

In addition to with, the "shortcut" condition operators (e.g. in) also create tie-ins, when binding a variable. The use of a predicate as a condition (e.g. for all integer n) also creates a tie-in. The condition operator where (and its alias such that) does not create a tie-in.

take any integer n in S such that p(n)
  integer(n)  # succeeds
  n is in S  # succeeds
  p(n)  # fails, needs a citation
end

For performance reasons, tie-ins cannot include quantifiers.

Proof assistance

Oak offers a limited amount of proof assistance. First, it lets you put ? in place of a label in a by clause. Oak will search the labels in your proof for one that can be substituted for ? to make the derivation valid.

axiom 1: x
axiom 2: y

x by ?

proof.oak: processing line 1 2 4
line 4: trying to resolve ?

line 4: resolved ? into:
  1

proof incomplete due to ?

You must remove the ? and cite the resolved label to complete the proof.

-f  look for a fix

There is also a command-line option -f. Whereas ? looks for a single label, -f looks for a set of labels.

axiom 1: x
axiom 2: y
axiom 3: z

x and y and z by 1

proof.oak: processing line 1 2 3 5
line 5: invalid derivation "x and y and z"
line 5: -f option: looking for a fix
line 5: -f option: found a fix, reducing
line 5: -f option: derivation will work if you add:
  2, 3

If citing a single label can fix your derivation:

? will find it, and will list all such labels that suffice.
-f will find a set of one or more labels that jointly suffice.

If citing multiple labels is needed to fix your derivation:

? will not find them.
-f may find them, but it may not: there is no guarantee.

Other command-line options

Besides -f (described above), Oak has some other handy command-line options.

-c  check for unneeded citations

This option notifies you of any citations in your proof that can be reduced. For example, in the last line of the proof below, you only need to cite A1, not A2. Calling Oak with -c will tell you that.

axiom A1: for all x, p(x)
axiom A2: for all x, q(x)
p(c) by A1,A2

line 3: citation can be reduced from:
  A1, A2
to:
  A1

The -c option slows down the proof checker, so don't use it all the time, just when you want to clean up your citations.

-m  assume until marker

The -m option lets you put the word marker anywhere in your proof. Oak will assume everything up to the marker, then begin checking from there.

1: x
2: x implies y

marker

y by 1,2

proof.oak: processing line 1 2 4 6
all lines accepted
proof.oak: assumptions on lines start-4
proof incomplete due to marker

-w  wait for validity (does not change proof outcome)

Sometimes, when checking a proof, Oak will stop at some line and say "could not determine validity of derivation". This means the prover exceeded the "amount of work" allowed for that line, so your proof failed. If you pass -w, Oak will "keep working" to try to determine if the line in question is valid. However, this is only for your edification, and does not change the proof outcome. Even if -w finds that the line is valid, Oak will not accept that line until you fix it (e.g. by breaking it into smaller steps).

`include`

As your proof gets bigger, you may wish to split it into multiple files. You can use include to access one file from another. Create a new file "axioms.oak" with the following content:

axiom A1: for all x, p(x)
axiom A2: for all x, q(x)

Now put the following in your original file proof.oak.

include "axioms.oak"

p(a) by A1
q(a) by A2

proof.oak: processing line 1
axioms.oak: processing line 1 2
proof.oak: processing line 3 4
all lines accepted
2 axioms in axioms.oak
proof successful!

`exit`

The exit command skips the rest of the proof. It outputs a notice that the remaining lines were skipped and marks the proof as incomplete.

axiom for all x, p(x)
so p(c)
exit
# under construction, not ready to be checked yet
q(c)

proof.oak: processing line 1 2 3
exit at line 3: skipping remaining lines
all lines accepted prior to exit
1 axiom in proof.oak
proof incomplete due to exit

Parameterized tie-ins

In addition to tie-ins created when binding a variable, there are parameterized tie-ins, created with the tie-in command. These "free-floating" tie-ins apply not just to one variable, but to any term matching a pattern.

axiom A1: for all x, p(x) implies q(x)
tie-in `p(x)` with `p(x) implies q(x)` for all x by A1

suppose p(c)
	so q(c) # no need to cite A1 here
end

Here, a tie-in is created with the pattern p(x) and body p(x) implies q(x), parameterized by x. Afterwards, any occurrence of the pattern will trigger the tie-in, causing the body to be included.

When using tie-in to create a parameterized tie-in, you must prove that the body holds for all values of its parameters. For example, to create the tie-in

tie-in `x+y` with `x+y = y+x` for all x,y

you must prove

for all x,y, x+y = y+x

For performance reasons, parameterized tie-ins cannot instantiate quantified variables.

Axiom schemas

In addition to axiom statements, Oak supports axiom schemas. An axiom schema is a "meta statement" which can be instantiated as multiple statements. An axiom schema must begin with for all meta, a quantifier which ranges over expressions. The body of for all meta must be enclosed in backticks, denoting a statement pattern to be instantiated.

induction: axiom schema for all meta φ,
  `if φ{x:0} and
      for all x, φ implies φ{x:x+1},
   then
      for all x, φ`

assume p(0) or q(0)
assume for all x, p(x) or q(x) implies p(x+1) or q(x+1)
so for all x, p(x) or q(x) by induction

Here, the meta variable φ is instantiated as the expression p(x) or q(x). In the schema, φ{x:0} means "φ with all occurrences of x replaced by 0", and φ{x:x+1} means "φ with all occurrences of x replaced by x+1".

Free variable checks are also possible. Below, free(p,φ) is true iff p occurs free in φ (unbound by a quantifier).

comprehension: axiom schema
  for all meta p,φ such that not free(p,φ),
    `for some p, for all n in N, p(n) iff φ`

# succeeds
for some p, for all n in N, p(n) iff not q(n) by comprehension

# fails
for some p, for all n in N, p(n) iff not p(n) by comprehension

proof.oak: processing line 1 6 9
error at line 9: could not instantiate schema

The first instantiation succeeds, but in the second one, φ is not p(n), so p occurs free in φ, and the instantiation fails.

Next steps

Now that you know Oak, you can download the examples and play around with them. Or you can write a proof of your own!

If you would like to contribute to Oak, e.g. by reporting issues, suggesting features, or expanding the examples, head over to Oak's page at GitHub.

Feel free to contact Tim Smith with any questions or comments.

Installation
Usage
Getting started
axiom
so
Labels and by
now blocks
suppose
Comments
Conditions
take
assume
proof blocks
define
Tie-ins
Proof assistance
Other command-line options
include
exit
Parameterized tie-ins
Axiom schemas
Next steps

Oak Tutorial

Learn Oak!

Installation

Usage

Getting started

`axiom`

`so`

Labels and `by`

`now` blocks

`suppose`

Comments

Conditions

`take`

`assume`

`proof` blocks

`define`

Tie-ins

Proof assistance

Other command-line options

`include`

`exit`

Parameterized tie-ins

Axiom schemas

Next steps

Table of contents

Oak Tutorial

Learn Oak!

Installation

Usage

Getting started

axiom

so

Labels and by

now blocks

suppose

Comments

Conditions

take

assume

proof blocks

define

Tie-ins

Proof assistance

Other command-line options

include

exit

Parameterized tie-ins

Axiom schemas

Next steps

Table of contents

`axiom`

`so`

Labels and `by`

`now` blocks

`suppose`

`take`

`assume`

`proof` blocks

`define`

`include`

`exit`