7. Arithmetic

Arithmetic is the first-order theory of natural numbers. This means that to prove properties of propositions and functions over natural numbers, we reason in first-order logic plus induction and the rules for equality on natural numbers. Furthermore we have a relation "less than" on natural numbers. To prove an assertion A(x) for an arbitrary x:nat, we can make use of the fact that x is a natural number and eliminate it with rule natE, what is commonly called induction. This only works if we have a proof of A(0) and -- under the hypotheses x':nat and A(x') -- a proof of A(s x'). Example:

proof reflEq : !x:nat. (x = x) = begin [ x: nat; 0 = 0; [ x': nat, x' = x'; s x' = s x' ]; x = x ]; !x:nat. x = x; end;

We use parentheses around the `x = x' in the declaration to make clear that the `=' does not mean the end of the proposition and the start of the proof block. If we left them out, we would get an error message:

Category mismatch: x is a variable, but a proposition is expected in this place

Tutch reconstructs the justifications as follows:

Proving symEq: !x:nat. x = x ... 1 [ x: nat; 2 0 = 0; by =NI0 3 [ x': nat, x' = x'; 4 s x' = s x' ]; by =NIS 3 5 x = x ]; by NatE 1 2 4 6 !x:nat. x = x by ForallI 5 QED

Here we clearly see the use of induction in tutch. To prove our goal !x:nat. x = x we assume an arbitrary x: nat and prove x = x for this arbitrary x. First we prove the case x = 0, which is done in line 2. Then we prove the case x = s x' (line 4), where we assume that the proposition is proven for x' (line 3). Using these two subproofs, we can apply induction on x: nat and thus prove x = x for that arbitrary x.

As second example we will define the predecessor function for natural numbers and prove it correct.

val pred : nat -> nat = fn x => rec x of f(0) => 0 | f(s(x')) => x' end;

We prove that the successor of the predecessor of a positive number x is equal to x. The annotated proof reads like this:

Proving verifyPred: !x:nat. ~x = 0 => s (pred x) = x ... 1 [ x: nat; 2 [ ~0 = 0; 3 0 = 0; by =NI0 4 F; by ImpE 2 3 5 s (pred 0) = 0 ]; by FalseE 4 6 ~0 = 0 => s (pred 0) = 0; by ImpI 5 7 [ x': nat, ~x' = 0 => s (pred x') = x'; 8 [ ~s x' = 0; 9 !z:nat. z = z; by Lemma reflEq 10 s x' : nat; 11 s (pred (s x')) = s x' ]; by ForallE 9 10 12 ~s x' = 0 => s (pred (s x')) = s x' ]; by ImpI 11 13 ~x = 0 => s (pred x) = x ]; by NatE 1 6 12 14 !x:nat. ~x = 0 => s (pred x) = x by ForallI 13 QED

Again we prove by induction over x:nat. At line 6 we have completed the proof for the base case x = 0. For the step case x = s x' (lines 7--12) we use the reflexivity lemma that we have proven before. Since we know that s (pred (s x')) evaluates to s x' by definition of pred, we instantiate our lemma with s x'. To do so, we need to explicitely have the judgment s x' : nat available. Since it is not a hypothesis, we state it in line 10. No proof is required here, the type-checker ensures that we can only give valid judgments of this form.

7.1 Proof terms

We illustrate how to prove propositions by induction with proof terms by these examples:

term refl : !x:nat. (x = x) = fn x => rec x of f 0 => eq0 | f (s x') => eqS (f x') end;

A proof by induction is isomorphic to a primitive recursive function. In this case the corresponding function takes a natural number x and returns a proof the x equals x. In the base case, eq0 is the proof for 0=0. In the step case by induction hypothesis f x' is a proof of x' = x'. If we then apply eqS we get the desired proof of s x' = s x'.

As a second example we proof transitivity of equality on natural numbers, which shows the proper use of the elimination rules for equality.

term trans : !x:nat. !y:nat. !z:nat. (x = y) => (y = z) => (x = z) = fn x => rec x of f 0 => fn y => rec y of g 0 => fn z => fn p => fn q => q | g (s y') => fn z => fn p => fn q => eqE0S p end | f (s x') => fn y => rec y of g 0 => fn z => fn p => fn q => eqES0 p | g (s y') => fn z => rec z of h 0 => fn p => fn q => eqES0 q | h (s z') => fn p => fn q => eqS (f x' y' z' (eqESS p) (eqESS q)) end end end;

UNDER CONSTRUCTION