[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |

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 placeDetails 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 |

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.

[ < ] | [ > ] | [ << ] | [ Up ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |

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; |

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

[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |

This document was generated by