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
Details about this ambiguity in the syntax you find in the reference. We are safe if we always put parentheses around equations in all declarations. (Within the proof this is not required!)
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.
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
Go to the first, previous, next, last section, table of contents.