(* Exercise coq_nat_01 *) (* Let us give a definition of natural numbers. '0' is a natural number and if 'n' is a natural number, then the successor of 'n' is also a natural numbers. This is expressed in Coq by the following inductive definition: (note that we use the letter 'O' for zero) *) Inductive nat : Set := | O : nat | S : nat -> nat. (* This definition introduces a new type 'nat': *) Check nat. (* It also introduces two constructors for this type. 'O' that is just a natural number *) Check O. (* and 'S' that is a function that given natural number returns another natural number - the successor *) Check S. (* Now to do something interesting we need some operations on nat. Let us start with addition. To define 'm + n' we proceed by doing case analysis on 'm'. We have two cases corresponding to the two constructors of type 'nat'. If 'm' is '0' then the result is simply 'n'. Otherwise 'm' is a successor of some number 'p' and 'S p + n' equals 'S (p + n)'. This is expressed in Coq with the following recursive definition: *) Fixpoint plus (m n : nat) {struct m} : nat := match m with | O => n | S p => S (plus p n) end. (* For such recursive definition to be accepted by Coq it must be terminating, ie. it is not allowed that the sequence of recursive calls can go on forever. To ensure this Coq uses a very simple criterion - one of the arguments must be structuraly decreasing along the recursive call. The annotation '{struct m}' in the above definition is used to indicated that 'm' is the decreasing argument. Indeed in the second case the first argument to 'plus' equals 'S p' and is replaced by 'p' in the recursive call *) (* Let us check the type of 'plus' *) Check plus. (* We can also see its full definition *) Print plus. (* Now let us prove a simple lemma stating that 'O' is a neutral element for addition. *) Lemma plus_zero_l : forall n, plus O n = n. Proof. intros. unfold plus. reflexivity. Qed.