Library Arith
Section Arith.
Guiseppe Peano defined the natural numbers as given by 0 : nat
and if n is a natural number then S n : nat is a natural number
called the successor of n. Given this we can construct all the
natural numbers, e.g.
- 1 = S 0
- 2 = S 1 = S (S 0)
- 3 = S 2 = S (S (S 0))
- Axiom 7 : 0 is not the successor of any number. forall n:nat, S n <> 0
- Axiom 8 : If two numbers have the same successor, then they are equal. forall m n:nat, S m = S n -> m = n
- Axiom 9 : If any property holds for 0, and is closed under successor, then it holds for all natural numbers (principle of induction). forall P : nat -> Prop, P 0 -> forall( m : nat, P m -> P (S m)) -> forall n : nat, P n
Lemma peano7 : forall n:nat, S n <> 0.
intro n.
intro h.
This is basically the same problem as proving true <> false, we
could apply the same technique here. To avoid repetetion we just
use the discriminate tactic.
discriminate h.
Qed.
To prove the next axiom, it is useful to define the inverse to
S, the predecessor function pred. We arbitrarily decide that the
predecessor of 0 is 0.
Definition pred (n : nat) : nat :=
match n with
| 0 => 0
| S n => n
end.
Lemma peano8 : forall m n:nat, S m = S n -> m = n.
intros m n h.
By folding with pred we can change the current goal so that we can
apply our hypothesis.
fold (pred (S m)).
rewrite h.
And now we just have to unfold. simpl would have done the job too.
unfold pred.
reflexivity.
Qed.
The 8th axiom says that the successor function is injective.
Can we prove the other direction too?
forall m n:nat, m = n -> S m = S n
Does this tell us anything new
about the successor function?
The proof of the induction axiom is rather boring. It just uses a tactic
which is called induction...
Lemma peano9 : forall P : nat -> Prop, P 0
-> (forall m : nat, P m -> P (S m))
-> forall n : nat, P n.
intros P h0 hS n.
induction n.
exact h0.
apply hS.
exact IHn.
Qed.
Peano defined the operations addition and multiplication.
These are actually examples of functions defined by primitive
recursion a general scheme which can be used to define many
other functions. A function is definable by primitive recursion
if we can give a case for 0 and reduce the computation for the
value at S n to the value at n. In Coq we have to use the
keyword fixpoint instead of definition and we have to indicate
on which argument we want to do primitive recursion.
The idea is that we can define addition like this:
- to add 0 to a number is just this number,
- to add one more that n to a number is one more than adding n to the number.
Fixpoint add (m n : nat) {struct m} : nat :=
match m with
| 0 => n
| S m => S (add m n)
end.
Eval compute in (add 2 3).
In the Coq library addition is defined using the usual infix
notation +.
To define multiplication we use primitive recursion again. This time
the idea is the following.
- multiplying 0 with a number is just 0.
- multiplying one more than n with a number is obtained by adding the number to multiplying n with the number.
Fixpoint mult (m n : nat) {struct m} : nat :=
match m with
| 0 => 0
| S m => add n (mult m n)
end.
Eval compute in (mult 2 3).
In the Coq library addition is defined using the usual infix
notation + and * with the usual rules of precedence.
From now on we shall use the library versions which are defined
exactly in the same way as we have defined add and mult
Addition and multiplication satisfy a number of important equations:
- 0 is a neutral element for addition 0 + m = m and m + 0 = m
- Addition is associative. m + (n + l) = (m + l) + n
- Addition is commutative. m + n = n + m
- 1 is a neutral element for multiplication 1 * m = m and m * 1 = m
- Multiplication is associative. m * (n * l) = (m * n) * l
- Multiplication is commutative. m * n = n * m
- 0 is a null for multiplication. m * 0 = 0 and 0 * m = 0
- Addition distributes over multiplication. m * (n + l) = m * n + m * l and (m + n) * l = m * l + n * l
- (+,0) is a commutative monoid, because 0 is neutral, + is associative and commutative.
- ( *,1) is a commutative monoid, because 1 is neutral, * is associative and commutative.
- (+,0,*,1) is a commutative semiring because (+,0) and ( *,1) are commutative monoids and 0 is a zero for multiplication and addition distributes over multiplication.
Lemma plus_O_n : forall n:nat, n = 0 + n.
This property is very easy to prove.
Can you see why?
intro n.
reflexivity.
Qed.
Lemma plus_n_O : forall n:nat, n = n + 0.
intro n.
reflexivity.
Qed.
Lemma plus_n_O : forall n:nat, n = n + 0.
intro n.
This one cannot be proven by reflexivity.
So we have to use induction.
induction n.
n = 0
This is easy.
simpl.
reflexivity.
We can simplify S n + 0 using the definition of +
simpl.
rewrite<- IHn.
reflexivity.
Qed.
Lemma plus_assoc : forall (l m n:nat),l + (m + n) = (l + m) + n.
intros l m n.
There seems to be quite a choice what to do induction over:
l,m,n but only one of them works. Why?
induction l.
simpl.
reflexivity.
simpl.
rewrite IHl.
reflexivity.
Qed.
To prove commutativity we first prove a lemma
we know already that 0 + m = m = m + 0
but what about S m + n = S (m + n) = m + S n ?
Lemma plus_n_Sm : forall n m : nat, S (m + n) = m + S n.
intros.
induction m.
simpl.
reflexivity.
simpl.
rewrite IHm.
reflexivity.
Qed.
We are now ready to prove commutativity.
Lemma plus_comm : forall n m:nat, n + m = m + n.
intros.
induction n.
simpl.
apply plus_n_O.
simpl.
rewrite IHn.
apply plus_n_Sm.
Qed.
We define the relation <= on natural numbers by saying
that m <= n holds if there is a number k such that
m = k + n.
Definition leq (m n : nat) : Prop :=
exists k : nat, n = k + m.
Notation "m <= n" := (leq m n).
We verify some basic properties of <=:
- <= is reflexive. forall n:nat, n <= n
- <= is transitive. forall l m n:nat, l <= m -> m <= n -> l <= n
- <= is antisymmetric. forall l m : nat, l <= m -> m <= l -> m = l
Lemma le_refl: forall n:nat,n <= n.
intro n.
exists 0.
reflexivity.
Qed.
Lemma le_trans : forall (l m n : nat), l <= m -> m <= n -> l <= n.
intros l m n lm mn.
destruct lm as [k klm].
destruct mn as [j jmn].
exists (j+k).
rewrite<- plus_assoc.
rewrite<- klm.
rewrite<- jmn.
reflexivity.
Qed.
We say a predicate is P : A -> Prop decidable if we can define
a boolean function decP : A -> bool which agrees with the predicate,
i.e. forall a:A, P a <-> decP a = true. This also extends to relations
in the obvious way.
We show below that equality on natural numbers is decidable. Do you know any undecidable predicates? Is equality always decidable?
We show below that equality on natural numbers is decidable. Do you know any undecidable predicates? Is equality always decidable?
First we define the decision procedure. In the case of equality this is quite obvious:
we inspect both parameters, if they start with different constructors (i.e. 0 vs S) they are certainly
not equal. If they are both 0 they are equal, and if they both start with S then we recursively
compare the arguments.
Fixpoint eqnat (m n : nat) {struct m} : bool :=
match m with
| 0 => match n with
| 0 => true
| S n' => false
end
| S m' => match n with
| 0 => false
| S n' => eqnat m' n'
end
end.
Now we show both direction seperately. The -> direction just boils down
to showing that eqnat is reflexive. Why?
Lemma eqnat_refl : forall m : nat, eqnat m m = true.
intro m.
induction m.
reflexivity.
simpl.
exact IHm.
Qed.
The other direction is more interesting and requires a double induction
over m and n.
Lemma eqnat_compl : forall m n : nat, eqnat m n = true -> m = n.
intro m.
Here it would have been a mistake to do intros m n. Why?
m = 0
induction m.
intro n.
induction n.
intro n.
induction n.
n = 0
intro h.
reflexivity.
reflexivity.
n = S n'
intro h.
simpl in h.
discriminate h.
simpl in h.
discriminate h.
m = S m'
intro n.
induction n.
induction n.
n = 0
intro h.
discriminate h.
discriminate h.
n = S n'
intro h.
assert (h' : m = n).
apply IHm.
exact h.
rewrite h'.
reflexivity.
Qed.
assert (h' : m = n).
apply IHm.
exact h.
rewrite h'.
reflexivity.
Qed.
Finally, we can prove the theorem that equality for natural numbers is decidable.
Theorem eqnat_dec : forall m n : nat, m = n <-> eqnat m n = true.
intros m n.
split.
intro h.
rewrite h.
apply eqnat_refl.
apply eqnat_compl.
Qed.
End Arith.