(* 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 function that unfolds a stream several times. In the proofs you can use the library lemma unfold_Stream. *) 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 := ? (* Define two functions that take the even and odd elements of a stream: evens (Cons a0 (Cons a1 (Cons a2 (Cons a3 ...)))) = Cons a0 (Cons a2 ...) odds (Cons a0 (Cons a1 (Cons a2 (Cons a3 ...)))) = Cons a1 (Cons a3 ...) *) CoFixpoint evens (A:Set)(s:Stream A): Stream A := ? Definition odds (A:Set)(s:Stream A): Stream A := ? (* 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. ? Qed. Theorem evens_eq: forall (A:Set)(s1 s2:Stream A), EqSt s1 (evens (interleave s1 s2)). Proof. ? Qed. Theorem odds_eq: forall (A:Set)(s1 s2:Stream A), EqSt s2 (odds (interleave s1 s2)). Proof. ? Qed. (* PART 3 *) Require Import ZArith. Open Scope Z_scope. (* Define the multiplication of two streams of integers: smult (Cons a0 (Cons a1 ...)) (Cons b0 (Cons b1 ...)) = Cons (a0 * b0) (Cons (a1 * b1) ...) *) CoFixpoint smult (s1 s2: Stream Z): Stream Z := ? (* 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+2)) ...)) *) CoFixpoint sfact_aux (x n:Z):= ? 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 := ? (* 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. ? 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 := ? (* 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 := ? (* 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. ? Qed.