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. *)
(* Q3. Now state and prove a theorem that expresses that this add function
returns the same result as plain addition (given by function plus) *)
(* Note that the theorems about commutativity and associativity could be
consequences of add_plus. *)
(* Programs about lists. *)
Require Import List ZArith.
(* We re-use the permutation defined in course C2. *)
Fixpoint multiplicity (n:Z)(l:list Z) : nat :=
match l with
nil => 0%nat
| a::l' => if Zeq_bool n a then S (multiplicity n l') else multiplicity n l'
end.
Definition is_perm (l l':list Z) :=
forall n, multiplicity n l = multiplicity n l'.
(* Q4. Show the following theorem: *)
Lemma multiplicity_app : forall x l1 l2, multiplicity x (l1++l2) =
multiplicity x l1 + multiplicity x l2.
Admitted.
(* Q5. State and prove a theorem that expresses that element counts are
preserved by reverse. *)
Lemma multiplicity_rev : forall x l, multiplicity x (rev l) = multiplicity x l.
Admitted.
(* --------------------------------------------*)
(* The following questions are more advanced and can be kept for later. *)
(* Q6. Show the following theorem. You will probably have an occasion
to use the ring tactic *)
Lemma is_perm_transpose :
forall x y l1 l2 l3, is_perm (l1++x::l2++y::l3) (l1++y::l2++x::l3).
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 => 0
end.
Eval vm_compute in map fib (seq 0 10).
(* 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 0 1.
Eval vm_compute in map fib' (seq 0 10).
Require Import Bool.
Eval vm_compute in map fib (seq 5 15).
(* This is a test of fib and fib' *)
Eval vm_compute in
let s := seq 5 15 in
fold_right (fun (p : nat * nat) (r:bool)
=> let (x,y) := p in beq_nat x y && r)
true (combine (map fib s) (map fib' (seq 5 15))).
(* Q7. 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.