Library coq_nat

Natural Numbers in the Coq Standard Library

In the previous exercise we defined natural numbers and a plus operation on them. As a matter of fact those definitions (and many more) are part of the standard library of Coq, see: http://coq.inria.fr/library-eng.html They are part of the core library which is loaded automatically when Coq is started.

Print nat.
Print plus.

Moreover Coq introduces notations for natural numbers allowing to write 0 for zero (instead of the letter O), + for plus, with the infix notation, and to use decimal numbers instead of the unary notation with S.

Check (2 + 2).

In the previous exercise we proved that 0 + n = n and a very simple proof it was. Now let us try to prove n + 0 = n. This is slightly more difficult. Can you see why? How would you prove that?

Lemma plus_zero_r : forall n, n + 0 = n.

Proof.
intros.
induction n.

You can also do
elim n
which is is the primitive tactic, but then you have to do additional intros. You can also do
destruct n
but that doesn't give you an induction hypothesis, only case distinction

- simpl.
  reflexivity.
- simpl.
  rewrite -> IHn.
  reflexivity.
Qed.

Let us prove a simple property concerning addition and successor

Lemma plus_succ : forall m n, S (m + n) = m + S n.

Proof.
intros.
induction m.
- simpl.
  reflexivity.
- simpl.
  rewrite IHm.
  reflexivity.
Qed.

Let us prove that addition is commutative.

For this we may need the facts that 0 is a neutral element for addition and that S (n + m) = n + S m - the facts that we proved before. However, those results are also available in the standard library. First we need to make them available with the Require Import command.

Require Import Arith.
Check plus_n_O.
Check plus_O_n.
Check plus_n_Sm.

Prove the following Lemma using plus_n_O, plus_O_n and plus_n_Sm

Lemma plus_comm : forall m n, m + n = n + m.
Proof.
Admitted.

Let us prove that addition is associative
Which argument should we do induction over?

Lemma plus_assoc : forall m n p, m + (n + p ) = (m + n ) + p.
Proof.
Admitted.

So far we have been dealing with addition on natural numbers. How about multiplication? Not surprisingly it is defined in the standard library of Coq, but before seeing the definition try to think of how would you define that (using addition).

Print mult.

Here is this definition for reference (and in the way you would type it in, which slightly differs from the way Coq presents it)

Fixpoint mult (n m:nat) {struct n} : nat := match n with | O => 0 | S p => m + mult p m end

Let us prove the 0 properties of multiplication

Lemma mult_0_l : forall n, 0 * n = 0.
Proof.
Admitted.

Lemma mult_0_r : forall n, n * 0 = 0.
Proof.
Admitted.

Now, let us prove that '1' is neutral for multiplication

Remember the properties of addition we were using. They may come in handy in this exercise. To get access to many results concerning arithmetic of natural number (including properties of addition and multiplication) we have already loaded the library Arith

Lemma mult_1_l : forall n, 1 * n = n.
Proof.
Admitted.

Lemma mult_1_r : forall n, n * 1 = n.
Proof.
Admitted.

Now, let us prove that multiplication is commutative

For this we may need to use some properties of addition and multiplication that we proved before.

Check mult_0_r.
Check plus_comm.
Check plus_assoc.

... and a following auxiliary lemma

Lemma mult_succ : forall m n, n + n * m = n * S m.
Proof.
Admitted.

Lemma mult_comm : forall m n, m * n = n * m.
Proof.
Admitted.

Multiplication distributes over addition

Lemma mult_plus_distr : forall m n p, m * (n + p ) = m * n + m * p.
Proof.
Admitted.

A more challenging problem

Do you know that with stamps of value 3 and 5 you can pay any value greater or equal than 8? Below is a Coq specification of this statemant - can you prove it?

Hint: for arithmetical reasoning you may try to use the lia tactic. This is a tactic that solves various arithmetic goals fully automatically -- but not all! You may use it later in the Coq assignment

Remark: if afterwards you decide to try to prove it without the use of lia, it should give you a good idea of how helpful such automated tactics can be

Require Import Lia.

Lemma stamps : forall i, exists v3 , exists v5 , i + 8 = 3*v3 + 5*v5.
Proof.
Admitted.