(* 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.