(** * 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 #<br>#
     [elim n] #<br>#
   which is is the primitive tactic, but then you have to do additional
   [intros]. You can also do #<br>#
     [destruct n] #<br>#
  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 #<br>#
    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.