(* Exercise coq_nat_02 *) (* 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.