Module FormalML.utils.StreamAdd

Require Import Utils.

Require Import List.
Require Import Streams.
Require Import Equivalence.
Require Import Morphisms.

Local Open Scope equiv_scope.

Global Instance EqSt_equiv {A} : Equivalence (@EqSt A).

Fixpoint ConsList {A:Type} (l:list A) (s:Stream A) : Stream A
  := match l with
     | nil => s
     | cons x xs => Cons x (ConsList xs s)
     end.

Global Instance ConsList_proper {A} : Proper (eq ==> @EqSt A ==> @EqSt A) (@ConsList A).

Lemma ConsList_app {A:Type} (l1 l2:list A) (s:Stream A) :
  ConsList (l1++l2) s = ConsList l1 (ConsList l2 s).

Section Cutting.

  Context {A:Type}.

  Fixpoint firstn (n:nat) (l:Stream A) : list A :=
    match n with
      | 0 => nil
      | S n => match l with
                 | Cons a l => a::(firstn n l)
               end
    end.

  Global Instance firstn_proper : Proper (eq ==> @EqSt A ==> eq) firstn.

    Fixpoint skipn (n:nat)(s:Stream A) : Stream A :=
    match n with
      | 0 => s
      | S n => match s with
                 | Cons a s' => skipn n s'
               end
    end.

  Global Instance skipn_proper : Proper (eq ==> @EqSt A ==> @EqSt A) skipn.

  Lemma firstn_length n l : length (firstn n l) = n.
  
  Lemma firstn_cons n a l: firstn (S n) (Streams.Cons a l) = cons a (firstn n l).
    
  Lemma firstn_O l: firstn 0 l = nil.

  Lemma firstn_ConsList n (l:list A) (s:Stream A) :
    n < length l ->
    firstn n (ConsList l s) = List.firstn n l.
  
  Lemma firstn_skipn n s : ConsList (firstn n s) (skipn n s) = s.

  Lemma firstn_skipn_swap n1 n2 s : firstn n1 (skipn n2 s) = List.skipn n2 (firstn (n2+n1) s).
    
  Lemma firstn_firstn (s:Stream A) (i j : nat) :
    List.firstn i (firstn j s) = firstn (min i j) s.
  
  Lemma firstn_firstn_swap (s:Stream A) (i j : nat) :
    List.firstn i (firstn j s) = List.firstn j (firstn i s).
  
End Cutting.