streams.v 2.21 KB
Newer Older
1
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
2
(* This file is distributed under the terms of the BSD license. *)
3
From stdpp Require Export tactics.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5 6

CoInductive stream (A : Type) : Type := scons : A  stream A  stream A.
7
Arguments scons {_} _ _ : assert.
Robbert Krebbers's avatar
Robbert Krebbers committed
8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
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
27 28 29 30 31
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
32
CoFixpoint srepeat {A} (x : A) : stream A := x :.: srepeat x.
Robbert Krebbers's avatar
Robbert Krebbers committed
33

Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36 37 38 39 40
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.
41
Global Instance equal_equivalence : Equivalence (@{stream A}).
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
Proof.
  split.
44 45 46
  - now cofix FIX; intros [??]; constructor.
  - now cofix FIX; intros ?? [??]; constructor.
  - cofix FIX; intros ??? [??] [??]; constructor; etrans; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48 49
Qed.
Global Instance scons_proper x : Proper (() ==> ()) (scons x).
Proof. by constructor. Qed.
50
Global Instance shead_proper : Proper (() ==> (=@{A})) shead.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Proof. by intros ?? [??]. Qed.
52
Global Instance stail_proper : Proper (() ==> (@{stream A})) stail.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
Proof. by intros ?? [??]. Qed.
54
Global Instance slookup_proper : Proper ((@{stream A}) ==> (=)) (slookup i).
Robbert Krebbers's avatar
Robbert Krebbers committed
55 56
Proof. by induction i as [|i IH]; intros s1 s2 Hs; simpl; rewrite Hs. Qed.
End stream_properties.