(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Certified Haskell Prelude.
 * Author: Matthieu Sozeau
 * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
 *              91405 Orsay, France
 * 
 * Infinite streams: F A = mu X. A x X.
 * This modules defines a coinductive equality predicate on [Stream] and
 * defines the corresponding parameterized [Setoid] instance. 
 * It also implements the usual combinators on lists (app, map), and proves various lemmas about them.
 * Each of them gives rise to a [Morphism] instance that can be used by [clrewrite].
 * Streams form a [Functor] and a [Comonad]. 
 *)

(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)

Require Import Coq.Program.Program.
Require Import Coq.Program.Basics.
Require Import Coq.Classes.SetoidTactics.
Require Import Coq.Classes.SetoidClass.

Require Import Coq.Lists.Streams.

Set Implicit Arguments.
Unset Strict Implicit.

Implicit Arguments Cons [[A]].

(** A coinduction principle *)

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

(** Extensional equality between two streams  *)

Program Instance stream_setoid : Setoid (@EqSt A) :=
  { equiv_prf := Build_equivalence _ _ _ _ _ }.

Next Obligation. (* refl *)
Proof.
  red ; intros ; apply EqSt_reflex.
Qed.

Next Obligation. (* trans *)
Proof.    
  red ; intros. 
  apply trans_EqSt with y ; auto.
Qed.

Next Obligation. (* sym *)
Proof. 
  red ; intros.
  apply sym_EqSt ; auto.
Qed.

Program Instance tl_morphism : ? Morphism stream_setoid stream_setoid (@tl A).

Next Obligation.
Proof.
  red ; intros.
  destruct x ; destruct y ; inversion H ; subst ; try discriminate.
  apply H1.
Qed.

Require Import Prelude.Functor.

Program Instance stream_functor : Functor Stream :=
  fmap a b f x := map f x.

(** Why have to rebind it ? *)
Ltac setoideq :=
  match goal with
    [ |- ?X = ?Y ] => apply (setoideq_eq X Y)
  end.

Ltac simpl_Stream t := rewrite (unfold_Stream t).

Next Obligation.
Proof.
  extensionality x ; setoideq ; revert x.
  cofix mapx ; intros.
  case x ; simpl ; intros.

  unfold id at 2.
  rewrite (unfold_Stream (map id (Cons a s))).
  simpl.
  constructor ; auto.
  apply (mapx s).
Qed.

Next Obligation.
Proof.
  extensionality x ; setoideq ; revert x ; simpl @equiv.
  unfold compose.
  cofix mapH ; intros.

  pattern x at 2.
  rewrite (unfold_Stream x).
  case x ; simpl ; constructor ; auto.

  apply (mapH s).
Qed.

Require Import Prelude.CoMonad.

CoFixpoint stream_cobind `a b` (f : Stream a -> b) (x : Stream a) : Stream b :=
  Cons (f x) (stream_cobind f (tl x)).

Program Instance stream_comonad : Comonad Stream :=
  counit a x := hd x ;
  cobind a b := stream_cobind.

Next Obligation.
Proof.
  setoideq. 
  
  revert x ; cofix IH.
  intros x.
  rewrite (unfold_Stream x).
  case x ; simpl ; intros.
  constructor ; simpl ; auto.
Qed.

Next Obligation.
Proof.
  extensionality m.
  setoideq. revert m ; cofix IH.
  intros.
  rewrite (unfold_Stream m).
  case m ; simpl ; intros.
  constructor ; simpl ; auto.

  unfold compose in IH.
  apply (IH s). 
Qed.

CoFixpoint repeat `A` (a : A) := Cons a (repeat a).

Definition next `A` : Stream A -> Stream A := tl (A:=A).

(** The isomorphism with functions from naturals to streams. *)

Fixpoint fun_of_stream `A` (s : Stream A) (n : nat) : A :=
  match n with
    | 0 => hd s
    | S n' => fun_of_stream (tl s) n'
  end.

Definition stream_of_fun_aux `A` (f : nat -> A) : nat -> Stream A :=
  cofix sof (i : nat) : Stream A := Cons (f i) (sof (S i)).

Definition stream_of_fun `A` (f : nat -> A) : Stream A := stream_of_fun_aux f 0.

Fixpoint skip `A` (s : Stream A) n := 
  match n with
    | 0 => s
    | S n' => skip (tl s) n'
  end.

Ltac rewrite_neeq :=
  match goal with
    | [ |- ?X == ?Y ] => rewrite (unfold_Stream X) ; rewrite (unfold_Stream Y)
    | [ |- EqSt ?X ?Y ] => rewrite (unfold_Stream X) ; rewrite (unfold_Stream Y)
  end.

Lemma fun_of_stream_skip : forall A (n : nat) (s : Stream A) ,
  fun_of_stream s n = hd (skip s n).
Proof.
  intros A.
  induction n ; simpl ; auto.
Qed.

Lemma stream_fun_isomorphism : forall A (s : Stream A) (n : nat), 
  stream_of_fun_aux (fun_of_stream s) n == skip s n.
Proof.
  intros A.
  cofix IH ; intros.
  induction n ; simpl ; intros.

  destruct s.
  constructor ; simpl ; auto.
  apply (IH (Cons a s) 1).

  destruct s.
  constructor ; auto.
  simpl ; auto.
  apply fun_of_stream_skip.

  pose (IH (Cons a s) (S n)).
  simpl in e.
  clrewrite e.
  simpl.
  refl.
Admitted. (* guard... *)

Definition FunArg s a : Type := ((s -> a) * s)%type.

Program Instance funarg_comonad : Comonad (FunArg s) :=
  counit A a := let (f, s) := a in f s ;
  cobind a b k x := let (f, s) := x in (fun s' => k (f, s'), s).

Next Obligation.
Proof.
  destruct x ; simpl.
  rewrite <- (eta_expansion a).
  reflexivity.
Qed.

Next Obligation.
Proof.
  destruct x ; simpl.
  reflexivity.
Qed.

Next Obligation.
Proof.
  unfold compose.
  extensionality x.
  destruct x ; simpl.
  reflexivity.
Qed.

(* Definition runFA `a b` (f : FunArg nat a -> b) (s : Stream a) : Stream b := *)