# Oak Tutorial

## Installation

Oak is available for download as a .tar.gz file (see the main page). Extract the file somewhere. If you like, add the extracted folder to your system's PATH variable so that you can run Oak from anywhere just by typing `oak`.

Oak requires the Ruby programming language, so if you get an error about Ruby not being installed, go here to find out how to install it.

## 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] [filename]
-v  print the version number of Oak
```

## 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 context. The command `so` uses the current context 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 context. Then `so` uses them to prove the third statement. After `so` proves its accompanying statement, it clears the context, and then puts the accompanying statement in it. The context 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 context contains only `x`. That's enough to prove the third line, after which the context contains only `not not x`. The fourth line then fails.

## 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 labelled statements do not enter the context. 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 context. Statements inside the block use the new context. At the end of the block, its context is added to the outer context.
```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 context `p(j)`, and not the outer context `q(i)`. However, it can still access labelled statements with `by`. At the end of the `now` block, its final context `q(j)` is added to the outer context, 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 context containing the accompanying statement, in this case `not x`. When a `suppose` ends, it takes its final context, makes it conditional on the supposition that started the suppose, and adds the result to the outer context. Here, the inner context `y` is added to the outer context as `(not x) implies y`. The `so` in the last line then uses the outer context 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
end
so there is no x with p(x)```

```/#
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, using the operators `in`, `with`, and `such that`, in the manner below. The operators `with` and `such that` are synonymous.
```axiom for all x in S, p(x)
axiom for all x with p(x), q(x)
axiom for all x such that q(x), r(x)
so for all x in S, r(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 assumptions
```

## `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 q(x)
A2: axiom for all x, q(x) implies p(x)

theorem 1: for all x, p(x) iff q(x)
proof
take any x
p(x) implies q(x) by A1
q(x) implies p(x) by A2
so p(x) iff q(x)
end
so thesis
end

p(a) iff q(a) by theorem 1```
```proof.oak: processing line 1 2 4 6 7 8 9 10 11 12 14
all lines accepted
2 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.

## `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!
```

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

## Any questions?

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

You can also post to the issue tracker on Oak's page at GitHub.