streams.v 2.14 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
(* Copyright (c) 2012-2015, Robbert Krebbers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
(* This file is distributed under the terms of the BSD license. *)
Require Export tactics.

CoInductive stream (A : Type) : Type := scons : A  stream A  stream A.
Arguments scons {_} _ _.
Delimit Scope stream_scope with stream.
Bind Scope stream_scope with stream.
Open Scope stream_scope.
Infix ":.:" := scons (at level 60, right associativity) : stream_scope.

Definition shead {A} (s : stream A) : A := match s with x :.: _ => x end.
Definition stail {A} (s : stream A) : stream A := match s with _ :.: s => s end.

CoInductive stream_equiv' {A} (s1 s2 : stream A) : Prop :=
  scons_equiv' :
    shead s1 = shead s2  stream_equiv' (stail s1) (stail s2) 
    stream_equiv' s1 s2.
Instance stream_equiv {A} : Equiv (stream A) := stream_equiv'.

Reserved Infix "!.!" (at level 20).
Fixpoint slookup {A} (i : nat) (s : stream A) : A :=
  match i with O => shead s | S i => stail s !.! i end
where "s !.! i" := (slookup i s).

Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28 29 30
Global Instance stream_fmap : FMap stream := λ A B f,
  cofix go s := f (shead s) :.: go (stail s).

Fixpoint stake {A} (n : nat) (s : stream A) :=
  match n with 0 => [] | S n => shead s :: stake n (stail s) end.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
CoFixpoint srepeat {A} (x : A) : stream A := x :.: srepeat x.
Robbert Krebbers's avatar
Robbert Krebbers committed
32

Robbert Krebbers's avatar
Robbert Krebbers committed
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
Section stream_properties.
Context {A : Type}.
Implicit Types x y : A.
Implicit Types s t : stream A.

Lemma scons_equiv s1 s2 : shead s1 = shead s2  stail s1  stail s2  s1  s2.
Proof. by constructor. Qed.
Global Instance equal_equivalence : Equivalence (@equiv (stream A) _).
Proof.
  split.
  * now cofix; intros [??]; constructor.
  * now cofix; intros ?? [??]; constructor.
  * cofix; intros ??? [??] [??]; constructor; etransitivity; eauto.
Qed.
Global Instance scons_proper x : Proper (() ==> ()) (scons x).
Proof. by constructor. Qed.
Global Instance shead_proper : Proper (() ==> (=)) (@shead A).
Proof. by intros ?? [??]. Qed.
Global Instance stail_proper : Proper (() ==> ()) (@stail A).
Proof. by intros ?? [??]. Qed.
Global Instance slookup_proper : Proper (() ==> eq) (@slookup A i).
Proof. by induction i as [|i IH]; intros s1 s2 Hs; simpl; rewrite Hs. Qed.
End stream_properties.