Set Implicit Arguments.
(** Infinite streams *)

CoInductive Str (A:Set) : Set := cons : A -> Str A -> Str A.

(** Define the projection functions *)
Definition hd A (s:Str A) : A := .

Definition tl A (s:Str A) : Str A := .

(** Prove the following equality by case analysis on s *)
Lemma Str_decomp : forall A (s : Str A), s = cons (hd s) (tl s).
Proof.

Save.

CoFixpoint alt1 : Str bool := cons true (cons false alt1).

Lemma alt1_eq : alt1 = cons true (cons false alt1).
apply trans_eq with (1:=Str_decomp alt1); trivial.
Save.

(** Following the same scheme, write a function alt2 of type 
      bool -> Str bool such that 
      hd (alt2 b) = b      tl (alt2 b) = alt2 (negb b) *)

Require Export Bool.

CoFixpoint alt2 (b: bool) : Str bool := cons b (alt2 (negb b)).

(** Prove the following lemma *)
Lemma alt2_eq : forall b, alt2 b = cons b (alt2 (negb b)).
Proof.

Save.

(** CoInductive Equality of streams *)
CoInductive eqStr (A:Set) (s t : Str A) : Prop := 
     eqStri : hd s = hd t -> eqStr (tl s) (tl t) -> eqStr s t.

(** Prove the reflexivity of this relation *)
Lemma eqStr_refl : forall (A:Set) (s : Str A), eqStr s s.
Proof.
intro A; cofix.
constructor.

Save.

(** Prove alt1 = alt2 true using eqStr *)
Lemma alt12 : eqStr alt1 (alt2 true).
Proof.
cofix.

Save.

(** Write a map function of type 
      forall (A B : Set), (A -> B) -> Str A -> Str B *)
CoFixpoint map (A B : Set) (f : A -> B) : Str A -> Str B := .

(** Write a function [nth] which access the nth elt of a stream
      with nth s 0 = hd s *)

(** Given a predicate P on A, define (inductively or coinductively)
     the  following properties for streams:
       - P holds for at least one element of s 
       - P holds for all elements of s [Strall]
       - P holds for infinitely many elements of s
       - P until Q : is P is true, it will remain true until Q is satisfied
  *)

Section Predicate.

Variable A:Set.
Variable P Q: A -> Prop.

(** - Prove that [Strall s] is equivalent to forall n, P (nth s n) *)