(* Fourth assignment for the course G54DTP. *) (* Venanzio Capretta, March 2011. *) Require Import Streams. Set Implicit Arguments. (* To check whether your definitions are correct you can use the unfold function. *) Fixpoint sunf (A:Set)(s:Stream A)(n:nat): Stream A := match n with O => s | S n' => match s with Cons a s' => Cons a (sunf s' n') end end. (* PART 1 *) (* Define a function that interleaves the elements of two streams: interleave (Cons a0 (Cons a1 ...)) (Cons b0 (Cons b1 ...)) = Cons a0 (Cons b0 (Cons a1 (Cons b1 ...))) *) CoFixpoint interleave (A:Set)(s1 s2:Stream A): Stream A := match s1 with (Cons a1 s1') => Cons a1 (interleave s2 s1') end. (* Define two functions that take the even and odd elements of a stream: even (Cons a0 (Cons a1 (Cons a2 (Cons a3 ...)))) = Cons a0 (Cons a2 ...) odd (Cons a0 (Cons a1 (Cons a2 (Cons a3 ...)))) = Cons a1 (Cons a3 ...) *) CoFixpoint evens (A:Set)(s:Stream A): Stream A := match s with (Cons a s') => Cons a (evens (tl s')) end. Definition odds (A:Set)(s:Stream A): Stream A := evens (tl s). (* PART 2 *) (* Prove that interleave and evens/odds are inverses. *) Theorem interleave_eq: forall (A:Set)(s:Stream A), EqSt s (interleave (evens s) (odds s)). Proof. intro A; cofix. intro s; constructor. case s; trivial. case s; simpl. intros a s'; constructor. case s'; trivial. case s'; intros a' s''; simpl. apply interleave_eq. Qed. Theorem evens_eq: forall (A:Set)(s1 s2:Stream A), EqSt s1 (evens (interleave s1 s2)). Proof. intro A; cofix. intros s1 s2; constructor. case s1; trivial. case s1; intros a1 s1'; case s2; intros a2 s2'; simpl. apply evens_eq. Qed. Theorem odds_eq: forall (A:Set)(s1 s2:Stream A), EqSt s2 (odds (interleave s1 s2)). Proof. intros A s1 s2; case s1; intros a1 s1'; case s2; intros a2 s2'. constructor; simpl. trivial. case s1'; intros a1' s1''; simpl. apply evens_eq. Qed. (* PART 3 *) Require Import ZArith. Open Scope Z_scope. (* Define the multiplication of two streams of natural numbers: smult (Cons a0 (Cons a1 ...)) (Cons b0 (Cons b1 ...)) = Cons (a0 * b0) (Cons (a1 * b1) ...) *) CoFixpoint smult (s1 s2: Stream Z): Stream Z := match s1, s2 with (Cons a1 s1'), (Cons a2 s2') => Cons (a1*a2) (smult s1' s2') end. (* Define the streams of factorials: sfact = Cons 1 (Cons 1 (Cons 2 (Cons 6 (Cons 24 (Cons 120 ...))))) the nth element of the stream is n! I suggest you first define an auxilliary function sfact_aux: sfact x n = Cons x (Cons (x*(n+1)) (Cons (x*(n+1)*(n+2)) ...)) *) CoFixpoint sfact_aux (x n:Z):= Cons x (sfact_aux (x*(n+1)) (n+1)). Definition sfact: Stream Z := sfact_aux 1 0. Eval simpl in (sunf sfact 10). (* PART 4 *) Require Import Even. (* Remember the definition of sfrom. *) CoFixpoint sfrom (n:nat): Stream nat := Cons n (sfrom (S n)). (* Given two predicates on the set A, P and Q; define a predicate (Alternate P Q) on streams satisfied when the elements of the stream satisfy P and Q alternately: Alternate P Q (Cons a0 (Cons a1 (Cons a2 (Cons a3 ...)))) is true if (P a0) is true, (Q a1) is true, (P a2) is true, (Q a3) is true, etcetera. *) CoInductive Alternate (A:Set)(P Q:A->Prop): Stream A -> Prop := alternate: forall (a:A)(s:Stream A), P a -> Alternate Q P s -> Alternate P Q (Cons a s). (* If you defined it correctly, you should be able to prove the following. *) Theorem alt_from: forall n, even n -> Alternate even odd (sfrom n). Proof. cofix. intros n hn. rewrite unfold_Stream; simpl. apply alternate. exact hn. rewrite unfold_Stream; simpl. apply alternate. apply odd_S; exact hn. apply alt_from. apply even_S; apply odd_S; exact hn. Qed. (* PART 5 *) (* Define a predicate characterizing constant streams. It is satisfied if all elements of the stream are the same. *) CoInductive Const_Stream (A:Set): Stream A -> Prop := const_Cons: forall (a:A)(s:Stream A), Const_Stream (Cons a s) -> Const_Stream (Cons a (Cons a s)). (* Define a predicate that is true if a stream is "eventually constant", so all the elements are the same from a certain point. *) Inductive EvConst (A:Set): Stream A -> Prop := ev_const: forall s, Const_Stream s -> EvConst s | ev_diff: forall (a:A)(s:Stream A), EvConst s -> EvConst (Cons a s). (* If you defined it correctly, you should be able to prove the following. *) CoFixpoint sdec (n:nat): Stream nat := Cons n (sdec (n-1)). Theorem sdec_EvConst: forall n, EvConst (sdec n). Proof. intro n; elim n. rewrite unfold_Stream; simpl. apply ev_const. cofix. rewrite (unfold_Stream (sdec 0)); simpl. apply const_Cons. apply sdec_EvConst. intros n' Hn'; rewrite unfold_Stream; simpl. apply ev_diff. rewrite <- minus_n_O. exact Hn'. Qed.