# Library CoinductiveExamples.STREAMS.Examples

Set Asymmetric Patterns.

Require Import Plus.
Require Import Streams.

Section Examples.
Section Map.

Variable A B : Set.
Variable f : A B.

CoFixpoint map : Stream A Stream B :=
fun s : Stream Amatch s with
| Cons a sCons (f a) (map s)
end.

End Map.

CoFixpoint zeros : Stream nat := Cons 0 zeros.

CoFixpoint alter : Stream nat := Cons 0 (Cons 1 alter).

CoFixpoint alter1 : Stream nat := Cons 0 alter2
with alter2 : Stream nat := Cons 1 alter1.

CoFixpoint from : nat Stream nat := fun n : natCons n (from (S n)).
Definition allnats : Stream nat := from 0.

Lemma all_greater_than_m__are_here :
n m : nat, Str_nth n (from m) = n + m.
simple induction n.
trivial.
intros.
rewrite plus_Snm_nSm.
unfold Str_nth in |- ×.
unfold Str_nth in H.
simpl in |- ×.
apply H.
Qed.

CoFixpoint mapS : Stream nat Stream nat :=
fun s : Stream natmatch s with
| Cons n s1Cons (S n) (mapS s1)
end.

Inductive Times (A B : Set) : Set :=
times : A B Times A B.

CoInductive St2 : Set :=
Cons2 : Times nat St2 St2.

CoFixpoint mapS2 : St2 St2 :=
fun x : St2
match x return St2 with
| Cons2 (times x1 x2) ⇒ Cons2 (times nat St2 (S x1) (mapS2 x2))
end.

Theorem zeros_unfold : zeros = Cons 0 zeros.
apply (unfold_Stream zeros).
Qed.

End Examples.

Section Stream_Equalities.

Variable A : Set.

Theorem Equiv1 :
s1 s2 : Stream A,
EqSt s1 s2 n : nat, Str_nth n s1 = Str_nth n s2.
unfold Str_nth in |- ×.
fix u 4.
intros s1 s2 H n.
case H.
intros.
case n.
assumption.
intros.
simpl in |- ×.
apply u.
assumption.
Qed.

Theorem Equiv2 :
s1 s2 : Stream A,
( n : nat, Str_nth n s1 = Str_nth n s2) EqSt s1 s2.
unfold Str_nth in |- ×.
cofix u.
intros.
apply eqst.
apply (H 0).
apply u.
intros n.
apply (H (S n)).
Qed.

Section Example.

Variable f : A A.

CoFixpoint iter : A Stream A := fun x : ACons (f x) (iter (f x)).

Lemma map_iter_eq : x : A, EqSt (iter (f x)) (map A A f (iter x)).
cofix u.
intros.
apply eqst.
trivial.
simpl in |- ×.
apply u.
Qed.

End Example.

CoInductive EqSt2 (A : Set) : Stream A Stream A Prop :=
eqst2 :
(s1 s2 : Stream A) (a : A),
EqSt2 A s1 s2 EqSt2 A (Cons a s1) (Cons a s2).

Theorem EqSt2_reflex : s : Stream A, EqSt2 A s s.
cofix u.
intros.
case s.
intros.
apply eqst2.
apply u.
Qed.

Theorem EqSt2_sym : s1 s2 : Stream A, EqSt2 A s1 s2 EqSt2 A s2 s1.
cofix u.
intros.
case H.
intros.
apply eqst2.
apply u.
assumption.
Qed.

Theorem EqSt2_trans :
s1 s2 s3 : Stream A, EqSt2 A s1 s2 EqSt2 A s2 s3 EqSt2 A s1 s3.
cofix u.
intros s1 s2 s3.
intro.
inversion_clear H.
intro.
inversion_clear H.
apply eqst2.
apply (u s0 s4 s6).
assumption.
assumption.
Qed.

Definition derived_eqst (s1 s2 : Stream A) (a : A)
(H : EqSt s1 s2) : EqSt (Cons a s1) (Cons a s2) :=
eqst (Cons a s1) (Cons a s2) (refl_equal (hd (Cons a s2))) H.

Definition derived_eqst2 (s1 s2 : Stream A) :
hd s1 = hd s2 EqSt2 A (tl s1) (tl s2) EqSt2 A s1 s2 :=
let (x, x0) as s
return (hd s = hd s2 EqSt2 A (tl s) (tl s2) EqSt2 A s s2) :=
s1 in
(let (a, s) as s
return
( (a : A) (s0 : Stream A),
hd (Cons a s0) = hd s
EqSt2 A (tl (Cons a s0)) (tl s) EqSt2 A (Cons a s0) s) := s2 in
fun (a0 : A) (s0 : Stream A) (H : hd (Cons a0 s0) = hd (Cons a s))
(H0 : EqSt2 A (tl (Cons a0 s0)) (tl (Cons a s))) ⇒
match H in (_ = a1) return (EqSt2 A (Cons a0 s0) (Cons a1 s)) with
| refl_equaleqst2 A s0 s a0 H0
end) x x0.

End Stream_Equalities.