Streams.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Set Implicit Arguments.

Streams

CoInductive Stream (A : Type) :=
  Cons : A -> Stream A -> Stream A.

Section Streams.
  Variable A : Type.

  Notation Stream := (Stream A).


Definition hd (x:Stream) := match x with
                            | Cons a _ => a
                            end.

Definition tl (x:Stream) := match x with
                            | Cons _ s => s
                            end.


Fixpoint Str_nth_tl (n:nat) (s:Stream) : Stream :=
  match n with
  | O => s
  | S m => Str_nth_tl m (tl s)
  end.

Definition Str_nth (n:nat) (s:Stream) : A := hd (Str_nth_tl n s).


Lemma unfold_Stream :
 forall x:Stream, x = match x with
                      | Cons a s => Cons a s
                      end.A:Type
forall x : Stream,
x = match x with
    | Cons a s => Cons a s
    end
Proof.A:Type
forall x : Stream,
x = match x with
    | Cons a s => Cons a s
    end
  intro x.A:Type
x:Stream
x = match x with
    | Cons a s => Cons a s
    end
  case x.A:Type
x:Stream
forall (a : A) (s : Stream), Cons a s = Cons a s
  trivial.
Qed.

Lemma tl_nth_tl :
 forall (n:nat) (s:Stream), tl (Str_nth_tl n s) = Str_nth_tl n (tl s).A:Type
forall (n : nat) (s : Stream),
tl (Str_nth_tl n s) = Str_nth_tl n (tl s)
Proof.A:Type
forall (n : nat) (s : Stream),
tl (Str_nth_tl n s) = Str_nth_tl n (tl s)
  simple induction n; simpl; auto.
Qed.
Hint Resolve tl_nth_tl: datatypes.

Lemma Str_nth_tl_plus :
 forall (n m:nat) (s:Stream),
   Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s.A:Type
forall (n m : nat) (s : Stream),
Str_nth_tl n (Str_nth_tl m s) = Str_nth_tl (n + m) s
simple induction n; simpl; intros; auto with datatypes.A:Type
n, n0:nat
H:forall (m0 : nat) (s0 : Stream),
Str_nth_tl n0 (Str_nth_tl m0 s0) =
Str_nth_tl (n0 + m0) s0
m:nat
s:Stream
Str_nth_tl n0 (tl (Str_nth_tl m s)) =
Str_nth_tl (n0 + m) (tl s)
rewrite <- H.A:Type
n, n0:nat
H:forall (m0 : nat) (s0 : Stream),
Str_nth_tl n0 (Str_nth_tl m0 s0) =
Str_nth_tl (n0 + m0) s0
m:nat
s:Stream
Str_nth_tl n0 (tl (Str_nth_tl m s)) =
Str_nth_tl n0 (Str_nth_tl m (tl s))
rewrite tl_nth_tl; trivial with datatypes.
Qed.

Lemma Str_nth_plus :
 forall (n m:nat) (s:Stream), Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s.A:Type
forall (n m : nat) (s : Stream),
Str_nth n (Str_nth_tl m s) = Str_nth (n + m) s
intros; unfold Str_nth; rewrite Str_nth_tl_plus;
 trivial with datatypes.
Qed.

Extensional Equality between two streams

CoInductive EqSt (s1 s2: Stream) : Prop :=
    eqst :
        hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.

A coinduction principle

Ltac coinduction proof :=
  cofix proof; intros; constructor;
   [ clear proof | try (apply proof; clear proof) ].

Extensional equality is an equivalence relation

Theorem EqSt_reflex : forall s:Stream, EqSt s s.A:Type
forall s : Stream, EqSt s s
coinduction EqSt_reflex.A:Type
s:Stream
hd s = hd s
reflexivity.
Qed.

Theorem sym_EqSt : forall s1 s2:Stream, EqSt s1 s2 -> EqSt s2 s1.A:Type
forall s1 s2 : Stream, EqSt s1 s2 -> EqSt s2 s1
coinduction Eq_sym.A:Type
s1, s2:Stream
H:EqSt s1 s2
hd s2 = hd s1
A:Type
s1, s2:Stream
H:EqSt s1 s2
EqSt (tl s1) (tl s2)
+A:Type
s1, s2:Stream
H:EqSt s1 s2
hd s2 = hd s1 case H; intros; symmetry ; assumption.
+A:Type
s1, s2:Stream
H:EqSt s1 s2
EqSt (tl s1) (tl s2) case H; intros; assumption.
Qed.


Theorem trans_EqSt :
 forall s1 s2 s3:Stream, EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3.A:Type
forall s1 s2 s3 : Stream,
EqSt s1 s2 -> EqSt s2 s3 -> EqSt s1 s3
coinduction Eq_trans.A:Type
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
hd s1 = hd s3
A:Type
Eq_trans:forall s0 s4 s5 : Stream,
EqSt s0 s4 -> EqSt s4 s5 -> EqSt s0 s5
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
EqSt (tl s1) (tl s3)
-A:Type
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
hd s1 = hd s3 transitivity (hd s2).A:Type
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
hd s1 = hd s2
A:Type
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
hd s2 = hd s3
  +A:Type
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
hd s1 = hd s2 case H; intros; assumption.
  +A:Type
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
hd s2 = hd s3 case H0; intros; assumption.
-A:Type
Eq_trans:forall s0 s4 s5 : Stream,
EqSt s0 s4 -> EqSt s4 s5 -> EqSt s0 s5
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
EqSt (tl s1) (tl s3) apply (Eq_trans (tl s1) (tl s2) (tl s3)).A:Type
Eq_trans:forall s0 s4 s5 : Stream,
EqSt s0 s4 -> EqSt s4 s5 -> EqSt s0 s5
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
EqSt (tl s1) (tl s2)
A:Type
Eq_trans:forall s0 s4 s5 : Stream,
EqSt s0 s4 -> EqSt s4 s5 -> EqSt s0 s5
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
EqSt (tl s2) (tl s3)
  +A:Type
Eq_trans:forall s0 s4 s5 : Stream,
EqSt s0 s4 -> EqSt s4 s5 -> EqSt s0 s5
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
EqSt (tl s1) (tl s2) case H; trivial with datatypes.
  +A:Type
Eq_trans:forall s0 s4 s5 : Stream,
EqSt s0 s4 -> EqSt s4 s5 -> EqSt s0 s5
s1, s2, s3:Stream
H:EqSt s1 s2
H0:EqSt s2 s3
EqSt (tl s2) (tl s3) case H0; trivial with datatypes.
Qed.

The definition given is equivalent to require the elements at each position to be equal

Theorem eqst_ntheq :
 forall (n:nat) (s1 s2:Stream), EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2.A:Type
forall (n : nat) (s1 s2 : Stream),
EqSt s1 s2 -> Str_nth n s1 = Str_nth n s2
unfold Str_nth; simple induction n.A:Type
n:nat
forall s1 s2 : Stream,
EqSt s1 s2 ->
hd (Str_nth_tl 0 s1) = hd (Str_nth_tl 0 s2)
A:Type
n:nat
forall n0 : nat,
(forall s1 s2 : Stream,
 EqSt s1 s2 ->
 hd (Str_nth_tl n0 s1) = hd (Str_nth_tl n0 s2)) ->
forall s1 s2 : Stream,
EqSt s1 s2 ->
hd (Str_nth_tl (S n0) s1) = hd (Str_nth_tl (S n0) s2)
-A:Type
n:nat
forall s1 s2 : Stream,
EqSt s1 s2 ->
hd (Str_nth_tl 0 s1) = hd (Str_nth_tl 0 s2) intros s1 s2 H; case H; trivial with datatypes.
-A:Type
n:nat
forall n0 : nat,
(forall s1 s2 : Stream,
 EqSt s1 s2 ->
 hd (Str_nth_tl n0 s1) = hd (Str_nth_tl n0 s2)) ->
forall s1 s2 : Stream,
EqSt s1 s2 ->
hd (Str_nth_tl (S n0) s1) = hd (Str_nth_tl (S n0) s2) intros m hypind.A:Type
n, m:nat
hypind:forall s1 s2 : Stream,
EqSt s1 s2 ->
hd (Str_nth_tl m s1) = hd (Str_nth_tl m s2)
forall s1 s2 : Stream,
EqSt s1 s2 ->
hd (Str_nth_tl (S m) s1) = hd (Str_nth_tl (S m) s2)
  simpl.A:Type
n, m:nat
hypind:forall s1 s2 : Stream,
EqSt s1 s2 ->
hd (Str_nth_tl m s1) = hd (Str_nth_tl m s2)
forall s1 s2 : Stream,
EqSt s1 s2 ->
hd (Str_nth_tl m (tl s1)) = hd (Str_nth_tl m (tl s2))
  intros s1 s2 H.A:Type
n, m:nat
hypind:forall s0 s3 : Stream,
EqSt s0 s3 ->
hd (Str_nth_tl m s0) = hd (Str_nth_tl m s3)
s1, s2:Stream
H:EqSt s1 s2
hd (Str_nth_tl m (tl s1)) = hd (Str_nth_tl m (tl s2))
  apply hypind.A:Type
n, m:nat
hypind:forall s0 s3 : Stream,
EqSt s0 s3 ->
hd (Str_nth_tl m s0) = hd (Str_nth_tl m s3)
s1, s2:Stream
H:EqSt s1 s2
EqSt (tl s1) (tl s2)
  case H; trivial with datatypes.
Qed.

Theorem ntheq_eqst :
 forall s1 s2:Stream,
   (forall n:nat, Str_nth n s1 = Str_nth n s2) -> EqSt s1 s2.A:Type
forall s1 s2 : Stream,
(forall n : nat, Str_nth n s1 = Str_nth n s2) ->
EqSt s1 s2
coinduction Equiv2.A:Type
s1, s2:Stream
H:forall n : nat, Str_nth n s1 = Str_nth n s2
hd s1 = hd s2
A:Type
s1, s2:Stream
H:forall n : nat, Str_nth n s1 = Str_nth n s2
forall n : nat, Str_nth n (tl s1) = Str_nth n (tl s2)
-A:Type
s1, s2:Stream
H:forall n : nat, Str_nth n s1 = Str_nth n s2
hd s1 = hd s2 apply (H 0).
-A:Type
s1, s2:Stream
H:forall n : nat, Str_nth n s1 = Str_nth n s2
forall n : nat, Str_nth n (tl s1) = Str_nth n (tl s2) intros n; apply (H (S n)).
Qed.

Section Stream_Properties.

Variable P : Stream -> Prop.

(*i
Inductive Exists : Stream -> Prop :=
  | Here    : forall x:Stream, P x -> Exists x
  | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
i*)

Inductive Exists ( x: Stream ) : Prop :=
  | Here : P x -> Exists x
  | Further : Exists (tl x) -> Exists x.

CoInductive ForAll (x: Stream) : Prop :=
    HereAndFurther : P x -> ForAll (tl x) -> ForAll x.

Lemma ForAll_Str_nth_tl : forall m x, ForAll x -> ForAll (Str_nth_tl m x).A:Type
P:Stream -> Prop
forall (m : nat) (x : Stream),
ForAll x -> ForAll (Str_nth_tl m x)
Proof.A:Type
P:Stream -> Prop
forall (m : nat) (x : Stream),
ForAll x -> ForAll (Str_nth_tl m x)
induction m.A:Type
P:Stream -> Prop
forall x : Stream, ForAll x -> ForAll (Str_nth_tl 0 x)
A:Type
P:Stream -> Prop
m:nat
IHm:forall x : Stream, ForAll x -> ForAll (Str_nth_tl m x)
forall x : Stream,
ForAll x -> ForAll (Str_nth_tl (S m) x)
-A:Type
P:Stream -> Prop
forall x : Stream, ForAll x -> ForAll (Str_nth_tl 0 x) tauto.
-A:Type
P:Stream -> Prop
m:nat
IHm:forall x : Stream, ForAll x -> ForAll (Str_nth_tl m x)
forall x : Stream,
ForAll x -> ForAll (Str_nth_tl (S m) x) intros x [_ H].A:Type
P:Stream -> Prop
m:nat
IHm:forall x0 : Stream, ForAll x0 -> ForAll (Str_nth_tl m x0)
x:Stream
H:ForAll (tl x)
ForAll (Str_nth_tl (S m) x)
  simpl.A:Type
P:Stream -> Prop
m:nat
IHm:forall x0 : Stream, ForAll x0 -> ForAll (Str_nth_tl m x0)
x:Stream
H:ForAll (tl x)
ForAll (Str_nth_tl m (tl x))
  apply IHm.A:Type
P:Stream -> Prop
m:nat
IHm:forall x0 : Stream, ForAll x0 -> ForAll (Str_nth_tl m x0)
x:Stream
H:ForAll (tl x)
ForAll (tl x)
  assumption.
Qed.

Section Co_Induction_ForAll.
Variable Inv : Stream -> Prop.
Hypothesis InvThenP : forall x:Stream, Inv x -> P x.
Hypothesis InvIsStable : forall x:Stream, Inv x -> Inv (tl x).

Theorem ForAll_coind : forall x:Stream, Inv x -> ForAll x.A:Type
P, Inv:Stream -> Prop
InvThenP:forall x : Stream, Inv x -> P x
InvIsStable:forall x : Stream, Inv x -> Inv (tl x)
forall x : Stream, Inv x -> ForAll x
coinduction ForAll_coind; auto.
Qed.
End Co_Induction_ForAll.

End Stream_Properties.

End Streams.

Section Map.
Variables A B : Type.
Variable f : A -> B.
CoFixpoint map (s:Stream A) : Stream B := Cons (f (hd s)) (map (tl s)).

Lemma Str_nth_tl_map : forall n s, Str_nth_tl n (map s)= map (Str_nth_tl n s).A, B:Type
f:A -> B
forall (n : nat) (s : Stream A),
Str_nth_tl n (map s) = map (Str_nth_tl n s)
Proof.A, B:Type
f:A -> B
forall (n : nat) (s : Stream A),
Str_nth_tl n (map s) = map (Str_nth_tl n s)
induction n.A, B:Type
f:A -> B
forall s : Stream A,
Str_nth_tl 0 (map s) = map (Str_nth_tl 0 s)
A, B:Type
f:A -> B
n:nat
IHn:forall s : Stream A, Str_nth_tl n (map s) = map (Str_nth_tl n s)
forall s : Stream A,
Str_nth_tl (S n) (map s) = map (Str_nth_tl (S n) s)
-A, B:Type
f:A -> B
forall s : Stream A,
Str_nth_tl 0 (map s) = map (Str_nth_tl 0 s) reflexivity.
-A, B:Type
f:A -> B
n:nat
IHn:forall s : Stream A, Str_nth_tl n (map s) = map (Str_nth_tl n s)
forall s : Stream A,
Str_nth_tl (S n) (map s) = map (Str_nth_tl (S n) s) simpl.A, B:Type
f:A -> B
n:nat
IHn:forall s : Stream A, Str_nth_tl n (map s) = map (Str_nth_tl n s)
forall s : Stream A,
Str_nth_tl n (map (tl s)) = map (Str_nth_tl n (tl s))
  intros s.A, B:Type
f:A -> B
n:nat
IHn:forall s0 : Stream A, Str_nth_tl n (map s0) = map (Str_nth_tl n s0)
s:Stream A
Str_nth_tl n (map (tl s)) = map (Str_nth_tl n (tl s))
  apply IHn.
Qed.

Lemma Str_nth_map : forall n s, Str_nth n (map s)= f (Str_nth n s).A, B:Type
f:A -> B
forall (n : nat) (s : Stream A),
Str_nth n (map s) = f (Str_nth n s)
Proof.A, B:Type
f:A -> B
forall (n : nat) (s : Stream A),
Str_nth n (map s) = f (Str_nth n s)
intros n s.A, B:Type
f:A -> B
n:nat
s:Stream A
Str_nth n (map s) = f (Str_nth n s)
unfold Str_nth.A, B:Type
f:A -> B
n:nat
s:Stream A
hd (Str_nth_tl n (map s)) = f (hd (Str_nth_tl n s))
rewrite Str_nth_tl_map.A, B:Type
f:A -> B
n:nat
s:Stream A
hd (map (Str_nth_tl n s)) = f (hd (Str_nth_tl n s))
reflexivity.
Qed.

Lemma ForAll_map : forall (P:Stream B -> Prop) (S:Stream A), ForAll (fun s => P
(map s)) S <-> ForAll P (map S).A, B:Type
f:A -> B
forall (P : Stream B -> Prop) (S : Stream A),
ForAll (fun s : Stream A => P (map s)) S <->
ForAll P (map S)
Proof.A, B:Type
f:A -> B
forall (P : Stream B -> Prop) (S : Stream A),
ForAll (fun s : Stream A => P (map s)) S <->
ForAll P (map S)
intros P S.A, B:Type
f:A -> B
P:Stream B -> Prop
S:Stream A
ForAll (fun s : Stream A => P (map s)) S <->
ForAll P (map S)
split; generalize S; clear S; cofix ForAll_map; intros S; constructor;
destruct H as [H0 H]; firstorder.
Qed.

Lemma Exists_map : forall (P:Stream B -> Prop) (S:Stream A), Exists (fun s => P
(map s)) S -> Exists P (map S).A, B:Type
f:A -> B
forall (P : Stream B -> Prop) (S : Stream A),
Exists (fun s : Stream A => P (map s)) S ->
Exists P (map S)
Proof.A, B:Type
f:A -> B
forall (P : Stream B -> Prop) (S : Stream A),
Exists (fun s : Stream A => P (map s)) S ->
Exists P (map S)
intros P S H.A, B:Type
f:A -> B
P:Stream B -> Prop
S:Stream A
H:Exists (fun s : Stream A => P (map s)) S
Exists P (map S)
(induction H;[left|right]); firstorder.
Defined.

End Map.

Section Constant_Stream.
Variable A : Type.
Variable a : A.
CoFixpoint const  : Stream A := Cons a const.
End Constant_Stream.

Section Zip.

Variable A B C : Type.
Variable f: A -> B -> C.

CoFixpoint zipWith (a:Stream A) (b:Stream B) : Stream C :=
Cons (f (hd a) (hd b)) (zipWith (tl a) (tl b)).

Lemma Str_nth_tl_zipWith : forall n (a:Stream A) (b:Stream B),
 Str_nth_tl n (zipWith a b)= zipWith (Str_nth_tl n a) (Str_nth_tl n b).A, B, C:Type
f:A -> B -> C
forall (n : nat) (a : Stream A) (b : Stream B),
Str_nth_tl n (zipWith a b) =
zipWith (Str_nth_tl n a) (Str_nth_tl n b)
Proof.A, B, C:Type
f:A -> B -> C
forall (n : nat) (a : Stream A) (b : Stream B),
Str_nth_tl n (zipWith a b) =
zipWith (Str_nth_tl n a) (Str_nth_tl n b)
induction n.A, B, C:Type
f:A -> B -> C
forall (a : Stream A) (b : Stream B),
Str_nth_tl 0 (zipWith a b) =
zipWith (Str_nth_tl 0 a) (Str_nth_tl 0 b)
A, B, C:Type
f:A -> B -> C
n:nat
IHn:forall (a : Stream A) (b : Stream B),
Str_nth_tl n (zipWith a b) = zipWith (Str_nth_tl n a) (Str_nth_tl n b)
forall (a : Stream A) (b : Stream B),
Str_nth_tl (S n) (zipWith a b) =
zipWith (Str_nth_tl (S n) a) (Str_nth_tl (S n) b)
-A, B, C:Type
f:A -> B -> C
forall (a : Stream A) (b : Stream B),
Str_nth_tl 0 (zipWith a b) =
zipWith (Str_nth_tl 0 a) (Str_nth_tl 0 b) reflexivity.
-A, B, C:Type
f:A -> B -> C
n:nat
IHn:forall (a : Stream A) (b : Stream B),
Str_nth_tl n (zipWith a b) = zipWith (Str_nth_tl n a) (Str_nth_tl n b)
forall (a : Stream A) (b : Stream B),
Str_nth_tl (S n) (zipWith a b) =
zipWith (Str_nth_tl (S n) a) (Str_nth_tl (S n) b) intros [x xs] [y ys].A, B, C:Type
f:A -> B -> C
n:nat
IHn:forall (a : Stream A) (b : Stream B),
Str_nth_tl n (zipWith a b) = zipWith (Str_nth_tl n a) (Str_nth_tl n b)
x:A
xs:Stream A
y:B
ys:Stream B
Str_nth_tl (S n) (zipWith (Cons x xs) (Cons y ys)) =
zipWith (Str_nth_tl (S n) (Cons x xs))
  (Str_nth_tl (S n) (Cons y ys))
  unfold Str_nth in *.A, B, C:Type
f:A -> B -> C
n:nat
IHn:forall (a : Stream A) (b : Stream B),
Str_nth_tl n (zipWith a b) = zipWith (Str_nth_tl n a) (Str_nth_tl n b)
x:A
xs:Stream A
y:B
ys:Stream B
Str_nth_tl (S n) (zipWith (Cons x xs) (Cons y ys)) =
zipWith (Str_nth_tl (S n) (Cons x xs))
  (Str_nth_tl (S n) (Cons y ys))
  simpl in *.A, B, C:Type
f:A -> B -> C
n:nat
IHn:forall (a : Stream A) (b : Stream B),
Str_nth_tl n (zipWith a b) = zipWith (Str_nth_tl n a) (Str_nth_tl n b)
x:A
xs:Stream A
y:B
ys:Stream B
Str_nth_tl n (zipWith xs ys) =
zipWith (Str_nth_tl n xs) (Str_nth_tl n ys)
  apply IHn.
Qed.

Lemma Str_nth_zipWith : forall n (a:Stream A) (b:Stream B), Str_nth n (zipWith a
 b)= f (Str_nth n a) (Str_nth n b).A, B, C:Type
f:A -> B -> C
forall (n : nat) (a : Stream A) (b : Stream B),
Str_nth n (zipWith a b) =
f (Str_nth n a) (Str_nth n b)
Proof.A, B, C:Type
f:A -> B -> C
forall (n : nat) (a : Stream A) (b : Stream B),
Str_nth n (zipWith a b) =
f (Str_nth n a) (Str_nth n b)
intros.A, B, C:Type
f:A -> B -> C
n:nat
a:Stream A
b:Stream B
Str_nth n (zipWith a b) =
f (Str_nth n a) (Str_nth n b)
unfold Str_nth.A, B, C:Type
f:A -> B -> C
n:nat
a:Stream A
b:Stream B
hd (Str_nth_tl n (zipWith a b)) =
f (hd (Str_nth_tl n a)) (hd (Str_nth_tl n b))
rewrite Str_nth_tl_zipWith.A, B, C:Type
f:A -> B -> C
n:nat
a:Stream A
b:Stream B
hd (zipWith (Str_nth_tl n a) (Str_nth_tl n b)) =
f (hd (Str_nth_tl n a)) (hd (Str_nth_tl n b))
reflexivity.
Qed.

End Zip.

Unset Implicit Arguments.