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