Require Import Arith. (* We first want to prove that our definition of add satisfies commutativity. *) Fixpoint add n m := match n with 0 => m | S p => add p (S m) end. Lemma addnS : forall n m, add n (S m) = S (add n m). induction n. intros m; simpl. reflexivity. intros m; simpl. apply IHn. Qed. (* Q1. Prove the following two theorems: beware that you will probably need addnS. *) Lemma addn0 : forall n, add n 0 = n. Admitted. Lemma add_comm : forall n m, add n m = add m n. Admitted. (* Q2. Now state and prove the associativity of this function. *) Lemma add_assoc : forall n m p, add (add n m) p = add n (add m p). Admitted. (* Q3. Now state and prove a theorem that expresses that this add function returns the same result as plain addition (given by function plus) *) Lemma add_plus : forall n m, add n m = n + m. Admitted. (* Note that the theorems about commutativity and associativity could be consequences of add_plus. *) (* Prove The following induction principle *) Lemma nat_double_ind : forall (P:nat->Prop), P 0 -> P 1 -> (forall n:nat, P n -> P (S n) -> P (S (S n))) -> forall n : nat, P n. Proof. Admitted. (* usage *) Goal forall n:nat, exists q:nat, n = 2* q \/ n = S (2*q). intro n; induction n using nat_double_ind. Admitted. (* More advanced: the Fibonacci function. *) Fixpoint fib n := match n with | S p => match p with 0 => 1 | S q => fib p + fib q end | 0 => 1 end. Time Compute fib 20. (* Alternative implementation, slightly more efficient. *) Fixpoint fibt v0 v1 n := match n with 0 => v0 | S p => fibt v1 (v0 + v1) p end. Definition fib' := fibt 1 1. Time Compute fib' 20. Lemma fibtSn: forall n a b , fibt a b (S n) = fibt b (a + b) n. simpl;auto. Qed. Lemma fibSSn : forall n, fib (S (S n)) = fib (S n) + fib n. intro n;simpl;auto. Qed. Goal forall n:nat, fib n >= 1. Admitted. (* Q4. A test is not a proof. How do you prove, forall n, fib' n = fib n? You will have to use an induction. Please find a generalized statement, about fibt. What are the values given as second and third arguments to this function? how are they related to the final result? *) Lemma fib'_fib : forall n, fib' n = fib n. Admitted.