(************************************************************************)
(*  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 
 * 
 * Non-empty infinite lists: F A = mu X. X + A x X.
 * This modules defines a coinductive equality predicate on [neilist] and
 * defines the corresponding parameterized [Setoid] instance. 
 * It also implements the usual combinators on lists (app, concat, map), and proves various lemmas about them.
 * Each of them gives rise to a [Morphism] instance that can be used by [clrewrite].
 * Three class instances are defined: [Functor], [Monad] and [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.Lists.Streams.

Set Implicit Arguments.
Unset Strict Implicit.

(* Require Import Coq.Classes.Equivalence. *)
Require Import Coq.Classes.SetoidTactics.
Require Import Coq.Classes.SetoidClass.

CoInductive neilist {A : Type} : Type :=
| nei_nil : A -> neilist
| nei_cons : A -> forall (l : neilist), neilist.

Lemma unfold_neilist : forall A (x : neilist A), x = match x with nei_nil x => nei_nil x | nei_cons a x => nei_cons a x end.
Proof.
  intros. case x ; reflexivity.
Qed.

(** Extensional Equality between two lazy lists  *)

CoInductive eq_neilist {A : Type} : neilist A -> neilist A -> Prop :=
| eq_nei_nil : forall x y, x = y -> eq_neilist (nei_nil x) (nei_nil y)
| eq_nei_cons : forall x y, x = y -> forall tl tl', eq_neilist tl tl' -> eq_neilist (nei_cons x tl) (nei_cons y tl').

(* Infix "==" := eq_neilist (at level 70). *)

Program Instance neilist_refl : Reflexive (@eq_neilist A).

  Next Obligation.
  Proof.
    revert x.
    cofix IH ; intros.
    rewrite unfold_neilist.
    case x ; constructor ; auto.
  Qed.

Program Instance neilist_sym : Symmetric (@eq_neilist A).

  Next Obligation.
  Proof.
    revert x y H.
    cofix IH ; intros.
    inversion H ; subst ; constructor ; auto.
  Qed.

Program Instance neilist_trans : Transitive (@eq_neilist A).

  Next Obligation.
  Proof.
    revert x y z H H0.
    cofix IH ; intros.

    inversion H ; subst ; auto.
    inversion H0 ; subst.
    constructor ; auto.
    apply (IH tl tl' tl'0) ; auto.
  Qed.
    
Program Instance neilist_equiv : Equivalence (neilist A) (@eq_neilist A).

Program Instance neilist_setoid : Setoid (neilist A) :=
  equiv := (@eq_neilist A) ; setoid_equiv := neilist_equiv.
 
Ltac rewrite_neeq :=
  match goal with
    | [ |- equiv ?X ?Y ] => rewrite (unfold_neilist X) ; rewrite (unfold_neilist Y)
    | [ |- eq_neilist ?X ?Y ] => rewrite (unfold_neilist X) ; rewrite (unfold_neilist Y)
  end.

Tactic Notation "simpl_neilist" constr(x) :=
  rewrite (unfold_neilist x) ; simpl.

(** First of, constructors are morphisms... *)

Program Instance nei_cons_morphism : Morphism (equiv ++> equiv) (@nei_cons A x).

  Next Obligation.
  Proof.
    red ; cofix IH ; intros.
    constructor ; auto.
  Qed.

CoFixpoint map {a b} (f : a -> b) (l : neilist a) : neilist b :=
  match l with
    | nei_nil x => nei_nil (f x)
    | nei_cons hd tl => nei_cons (f hd) (map f tl)
  end.

(* Typeclasses unfold @equiv.  *)
(* Typeclasses unfold @neilist_equiv. *)
(* Hint Unfold neilist_equiv. *)
(* Hint Unfold equiv. *)
(* Typeclasses unfold @Equivalence.equiv. *)
(* Typeclasses unfold @neilist_setoid. *)


Obligations Tactic := idtac.

Program Instance map_neilist_morphism : Morphism (equiv ++> equiv) (@map A B f).

  Next Obligation.
  Proof.
    red. cofix IH ; intros.
    
    destruct x ; destruct y ; inversion H ; subst ; try discriminate ; intros.
    reflexivity.

    rewrite_neeq.
    Set Printing All.
    simpl ; constructor ; auto.
  Qed.x

Require Import Prelude.Functor.

Require Import SetoidAxioms.

Program Instance neilist_functor : Functor neilist :=
  fmap a b f x := map f x.

  Next Obligation.
  Proof.
    extensionality x.
    setoid_extensionality ; revert x.
    cofix IH ; intros.
    rewrite (unfold_neilist (map id x)).
    case x ; simpl. 
    
    unfold id.
    constructor ; auto.
    
    intros a l.
    unfold id at 1 3.
    constructor ; auto.
    apply (IH l).
  Qed.

  Next Obligation.
  Proof.
    extensionality x ; setoid_extensionality ; revert x ; simpl @equiv.
    unfold compose.
    cofix IH. intros x.

    rewrite_neeq.
    case x ; simpl ; try constructor ; auto.
    apply IH.
  Qed.

Require Import Prelude.CoMonad.

CoFixpoint neilist_cobind {a b} (f : neilist a -> b) (x : neilist a) : neilist b :=
  match x with
    | nei_nil _ => nei_nil (f x)
    | nei_cons hd tl => 
      nei_cons (f x) (neilist_cobind f tl)
  end.

Definition hd {a} (x : neilist a) : a := 
  match x with nei_nil x => x | nei_cons hd tl => hd end.

Program Instance neilist_comonad : Comonad neilist :=
  counit a := hd ;
  cobind a b := neilist_cobind.

  Next Obligation.
  Proof.
    setoid_extensionality ; simpl @equiv.
    
    revert x ; cofix IH.
    intros x.
    simpl_neilist (neilist_cobind hd x).
    case x ; simpl ; intros ;
      constructor ; simpl ; auto.
    apply IH.
  Qed.

  Next Obligation.
  Proof.
    intros.
    case x ; simpl ; reflexivity.
  Qed.
  
  Next Obligation.
  Proof.
    extensionality x ; setoid_extensionality ; revert x ; simpl @equiv.
    
    unfold compose.
    cofix IH ; intros.
    
    rewrite_neeq.
    
    case x ; simpl ; intros ;
      constructor ; auto.
    apply IH.
  Qed.

CoFixpoint lapp {A} (l l' : neilist A) : neilist A :=
  match l with
    | nei_nil a => nei_cons a l'
    | nei_cons x l => nei_cons x (lapp l l')
  end.

Infix "oo" := lapp (right associativity, at level 60) : llist_scope.

Open Scope llist_scope.

Program Instance lapp_morphism : Morphism (SetoidClass.equiv ++> SetoidClass.equiv ++> equiv) (@lapp A).

  Next Obligation.
  Proof.
    do 3 red. 
    cofix IH ; intros.
    
    destruct x ; destruct y ; inversion H ; subst.

    rewrite_neeq.
    simpl.
    constructor ; auto.
    
    rewrite_neeq.
    simpl.
    constructor ; auto.
  Qed.

Lemma lapp_assoc : forall a (l l' l'' : neilist a), l oo l' oo l'' == (l oo l') oo l''.
Proof with auto.
  intros a.
  cofix IH ; intros.

  rewrite_neeq.
  destruct l ; simpl.
  reflexivity.

  constructor...
  apply IH.
Qed.
  
Lemma map_lapp : forall a b (l l' : neilist a) (f : a -> b), map f (l oo l') == map f l oo map f l'.
Proof with auto.
  intros a b.
  cofix IH ; intros.
  rewrite_neeq.

  case l ; simpl ; intros.
  reflexivity.

  (* interesting guardness condition bug :) *)
  (*   clrewrite (IH l0 l' f). *)
  (*   refl. *)
  constructor...
  apply IH.
Qed.
  
CoFixpoint concat {A} (l : neilist (neilist A)) : neilist A :=
  match l with
    | nei_cons hd tl => 
      match hd with
        | nei_nil hd => nei_cons hd (concat tl)
        | nei_cons hd tl' => nei_cons hd (concat (nei_cons tl' tl))
      end
    | nei_nil a => a
  end.

Program Instance concat_morphism : Morphism (equiv ++> equiv) (@concat A).

  Next Obligation.
  Proof.
    do 2 red. 
    cofix IH ; intros.
    
    destruct x ; destruct y ; inversion H ; subst.
    
    reflexivity.

    rewrite_neeq.
    simpl.
    destruct n0 ; simpl ; constructor ; auto.
    apply IH.
    constructor ; auto.
  Qed.

Lemma concat_nei_cons : forall A (x : neilist A) (l : neilist (neilist A)), 
  concat (nei_cons x l) == x oo concat l.
Proof.
  intros A ; cofix IH ; intros.

  rewrite_neeq.
  case x ; simpl ; intros.

  constructor ; reflexivity.

  constructor ; auto.
  apply IH.
Qed.

Require Import Coq.Classes.Init.

(* Ltac typeclass_instantiation ::= unfold equiv, equivalence_setoid ; dfs eauto 10 with typeclass_instances. *)

Lemma lapp_compat : forall a (x : neilist a) l l', l == l' -> x oo l == x oo l'.
Proof.
  intros.
  Set Printing All.
    intros.
  Print lapp_morphism.
  setoid_rewrite H.
  refl.
Qed.

Lemma concat_lapp : forall a (l l' : neilist (neilist a)), 
  concat (l oo l') == concat l oo concat l'.
Proof with auto.
  intros a.
  cofix IH ; intros.

  rewrite_neeq.

  case l ; simpl ; intros.
  destruct n ; simpl.
  refl.

  constructor...
  clrewrite (concat_nei_cons n l').
  refl.

  destruct n.
  constructor... apply IH.

  constructor...

  clrewrite (concat_nei_cons n (l0 oo l')).
  pose (concat_nei_cons n l0).
  clrewrite e.
  clrewrite <- (lapp_assoc n (concat l0) (concat l')).
  apply lapp_compat.
  apply IH.
Admitted. (* guard bug again!!! *)

Definition concat_map `A B` (f : A -> neilist B) : neilist A -> neilist B := 
  concat ∘ map f.

Require Import Prelude.Monad.

Program Instance neilist_monad : Monad neilist :=
  unit a := nei_nil ;
  bind a b := flip concat_map.

Next Obligation.
Proof.
  unfold flip. 
  unfold concat_map, compose.
  rewrite (unfold_neilist (map f (nei_nil x))).
  simpl.
  rewrite (unfold_neilist (concat (nei_nil (f x)))).
  simpl.
  case (f x) ; auto.
Qed.

Next Obligation.
Proof.
  unfold flip, concat_map, compose.
  setoideq_ext.
  revert x ; cofix IH ; intros.
  simpl_neilist (concat (map nei_nil x)).
  destruct x ; simpl.
  refl.

  constructor ; eauto.
  apply IH.
Qed.

Hint Unfold equiv.
Hint Unfold neilist_equiv.

(* Ltac setoidify ::=  *)
(*   on_call @eq_neilist ltac:(fun c => change c with equiv). *)
Ltac setoidify ::= 
  on_call eq_neilist
  ltac:(fun c => match c with
                   @eq_neilist ?A ?x ?y => change c with (equiv x y)
                 end).

Next Obligation.
Proof with auto.
  unfold flip, concat_map, compose.
  setoideq_ext.
  revert x ; cofix IH ; intros.
  rewrite_neeq.
  destruct x ; simpl.
  
  refl.

  destruct (f a0).
  destruct (g b0).
  constructor. auto. apply IH.

  constructor ; auto.
  rewrite_neeq.
  destruct n ; simpl.
  
  constructor ; auto.
  apply IH.

  constructor ; auto.
  clrewrite (concat_nei_cons n (map g (concat (map f x)))).
  clrewrite <- (IH x).
  clrewrite <- (concat_nei_cons n (map (fun a => concat (map g (f a))) x)).
  refl.

  destruct (g b0) ; setoidify.
  constructor...

  setoidify.
  (** eauto universe bug if morphism instances are in eq_neilist instead of equiv.
     It tries to apply reflexive_partial_app_morphism and fails.
     *)
  clrewrite (concat_nei_cons n (map f x)).
  clrewrite (map_lapp n (concat (map f x)) g).
  clrewrite (concat_lapp (map g n) (map g (concat (map f x)))).
  clrewrite <- (IH x).
  clrewrite (concat_nei_cons (concat (map g n)) (map (fun a => concat (map g (f a))) x)).
  refl.

  constructor...
  clrewrite (concat_nei_cons n (map f x)).
  clrewrite (concat_nei_cons n0 (map g (n oo concat (map f x)))).
  clrewrite (map_lapp n (concat (map f x)) g).
  clrewrite (concat_lapp (map g n) (map g (concat (map f x)))).
  clrewrite <- (IH x).
  
  clrewrite (concat_nei_cons (concat (nei_cons n0 (map g n))) (map (fun a1 : a => concat (map g (f a1))) x)).
  clrewrite (concat_nei_cons n0 (map g n)).
  clrewrite (lapp_assoc n0 (concat (map g n)) (concat (map (fun a1 : a => concat (map g (f a1))) x))).
  refl.
Admitted.

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