Library nat_ex_answers

Natural Numbers in the Standard Library

In the file nat_base.v we defined a type of natural numbers and a plus operation on it. As a matter of fact those definitions (and many more) are part of the standard library of Rocq, see: http://coq.inria.fr/library-eng.html They are part of the core library which is loaded automatically when Rocq is started.
Print nat.
Print plus.

Moreover Rocq 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_n_Sm.

Prove the following Lemma possibly using plus_n_O, plus_O_n and plus_n_Sm
Lemma plus_comm : forall m n, m + n = n + m.
Proof.
intros.
induction m.
- simpl.
  rewrite <- plus_n_O.
  reflexivity.
- simpl.
  rewrite -> IHm.
  rewrite plus_n_Sm.
  reflexivity.
General pattern that often works:
= simpl (to do some computation steps with the defined functions)
= find a way to rewrite with the IH
= use auxiliary lemmas
Qed.

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.
intros.
As plus is defined by recursion over the first argument, induction m is the obvious thing to try first
induction m.
- simpl.
  reflexivity.
- simpl.
  rewrite IHm.
  reflexivity.
Qed.

Trying induction n in teh previous exercise gets very complicated
Lemma plus_assoc' : forall m n p, m + (n + p) = (m + n) + p.
Proof.
intros.
Trying induction n
induction n.
- simpl.
  rewrite <- plus_n_O.
  reflexivity.
- simpl.
And now we are pretty stuck...
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 Rocq, 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 Rocq 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.
intros.
Rule of thumb: Do induction over the argument that the function does recursion over. For plus and mult, that is the first argument
induction n.
- simpl.
 reflexivity.
General pattern that often works:
= simpl (to do some computation steps with the defined functions)
= find a way to rewrite with the IH
= use auxiliary lemmas
- simpl.
  rewrite <- IHn.
  rewrite plus_assoc.
  rewrite (plus_comm n m).
Note the explicit argument I give to plus_comm to rewrite the specific subterm
  rewrite <- plus_assoc.
  reflexivity.
Qed.

Lemma mult_comm : forall m n, m * n = n * m.
Proof.
intros.
induction n.
- simpl.
  rewrite mult_0_r.
  reflexivity.
- simpl.
  rewrite <- IHn.
  rewrite mult_succ.
  reflexivity.
Qed.

As commutativity is very much a symmetric property in the two arguments, you can also do induction m and the proof is basically the same
Lemma mult_comm' : forall m n, m * n = n * m.
Proof.
intros.
induction m.
- simpl.
  rewrite mult_0_r.
  reflexivity.
- simpl.
  rewrite IHm.
  rewrite mult_succ.
  reflexivity.
Qed.

Multiplication distributes over addition

Lemma mult_plus_distr : forall m n p, m * (n + p) = m * n + m * p.
Proof.
intros.
induction m.
- auto.
- simpl.
  rewrite IHm.
  rewrite plus_assoc.
  rewrite plus_assoc.
The goal now is, with all brackets put in: (((n + p) + m * n) + m * p) = (((n + m * n) + p) + m * p)
  rewrite <- (plus_assoc n p (m*n)).
  rewrite <- (plus_assoc n (m*n) p).
  rewrite (plus_comm (m * n) p).
  reflexivity.
Qed.

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 Rocq 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 Rocq 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.

Note that lia solves many of the problems above quite easily

Lemma mult_plus_distr' : forall m n p, m * (n + p) = m * n + m * p.
Proof.
intros.
lia.
Qed.

Lemma stamps : forall i, exists v3, exists v5, i + 8 = 3*v3 + 5*v5.
Proof.
induction i.
- exists 1.
  exists 1.
  auto.
- destruct IHi.
  destruct H.
  destruct x0.
distinguishing cases x0 = 0 or x0 = S x1
   * destruct x.
distinguishing cases x = 0 or x = S x2
     + simpl in H.
it can be shown that the context is inconsistent using some simple arithmetic, and the tactic lia can prove that
lia can solve simple arithmetic goals that have no quantifiers so we proceed with just lia. To better understand what is happening, try
assert (~(i+8 = 0)).
lia.
contradiction.
       lia.
     + destruct x.
distinguishing cases x = 0 or x = S x2
       -- simpl in H.
we are in a similar situation as before, the context is inconsistent using some simple arithmetic
          lia.
       -- destruct x.
          ** simpl in H.
             lia.
Now the real choices have to be made!
          ** exists x.
             exists 2.
             lia.
   * exists (x+2).
     exists x0.
     lia.
Qed.