Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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). Proof. 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. Proof. induction n;simpl;auto. rewrite addnS. rewrite IHn;trivial. Qed. Lemma add_comm : forall n m, add n m = add m n. Proof. induction n;simpl. intro;rewrite addn0;auto. intros;rewrite addnS. rewrite IHn;trivial. rewrite addnS. trivial. Qed. (* Q2. Now state and prove the associativity of this function. *) Lemma plus_assoc : forall n m p, add n (add m p)= add (add n m) p. Proof. induction n. simpl;auto. intros. simpl. repeat rewrite <- addnS. rewrite IHn. repeat rewrite addnS. simpl. rewrite addnS. trivial. Qed. (* 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 p, add n p = n+p. Proof. induction n; simpl; auto. intro; rewrite addnS. rewrite IHn;trivial. Qed. (* 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. Proof. induction l1;simpl;auto. case (Zeq_bool x a). intros;rewrite IHl1. simpl;auto. intros;rewrite IHl1. simpl;auto. Qed. (* Q5. State and prove a theorem that expresses that element counts are preserved by reverse. *) Require Import ArithRing. Lemma multiplicity_rev : forall x l, multiplicity x (rev l) = multiplicity x l. Proof. induction l;simpl;auto. rewrite multiplicity_app. simpl. case (Zeq_bool x a). rewrite IHl;auto with arith. ring. rewrite IHl;ring. Qed. (* --------------------------------------------*) (* 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). Proof. intros;unfold is_perm;intros. replace (l1 ++ x :: l2 ++ y :: l3) with (l1 ++ (x::nil) ++ l2 ++ (y::nil)++l3). 2:simpl;auto. replace (l1 ++ y:: l2 ++ x :: l3) with (l1 ++ (y::nil) ++ l2 ++ (x::nil)++l3). 2:simpl;auto. repeat rewrite multiplicity_app. ring. Qed. (* 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. Functional Scheme fib_ind := Induction for fib Sort Prop. Check fib_ind. Lemma fib_SSn_eq : forall p q, p = S (S q) -> fib p = fib q + fib (S q). Proof. intros p q. destruct p. intro;discriminate. simpl (fib (S p)). injection 1. destruct p. intro;discriminate. injection 1. intro;subst p;auto. auto with arith. Qed. Lemma fib_SSn_rw: forall n, fib (S (S n)) = fib n + fib (S n). Proof. intro. rewrite plus_comm; reflexivity. Qed. 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. Lemma fibt_Sn : forall n a b, fibt a b (S n) = fibt b (a+b) n. Proof. intros;simpl. auto. Qed. Definition fib' := fibt 0 1. Eval vm_compute in map fib' (seq 0 10). Require Import Bool. Eval vm_compute in map fib (seq 0 10). (* 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'_gen : forall p n, fibt (fib n) (fib (S n)) p = fib (p+n). Proof. induction p. intros;simpl. trivial. intro n;rewrite fibt_Sn. replace (fib n + fib (S n)) with (fib (S (S n))). rewrite (IHp (S n)). replace (S p + n) with (p+S n). auto. simpl;auto with arith. rewrite fib_SSn_rw. trivial. Qed.