(************************************************************************)
(*  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 lists: F A = mu X. 1 + A x X.
 * This modules defines a coinductive equality predicate on [ilist] 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].
 * Only one class instance is defined: [Functor]. An [Alternative] instance could also be defined if 
 * the coinductives were less limited...
 *
 *)

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

Require Import Coq.Program.Program.
Require Import Coq.Program.Basics.

Set Implicit Arguments.
Unset Strict Implicit.

Require Import Coq.Classes.SetoidTactics.

(** A coinduction principle *)

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

CoInductive ilist (A : Type) : Type :=
| inil : ilist A
| icons : A -> forall (l : ilist A), ilist A.

Implicit Arguments inil [[A]].
Implicit Arguments icons [[A]].

Lemma unfold_ilist : forall A (x : ilist A), x = match x with inil => inil | icons a x => icons a x end.
Proof.
  intros. case x ; reflexivity.
Qed.

(** Extensional Equality between two lazy lists  *)

CoInductive eq_ilist (A : Type) : ilist A -> ilist A -> Prop :=
| eq_inil : eq_ilist inil inil
| eq_icons : forall x y, x = y -> forall tl tl', eq_ilist tl tl' -> eq_ilist (icons x tl) (icons y tl').

Implicit Arguments eq_ilist [A].

Program Instance ilist_setoid : Setoid (ilist A) (eq_ilist (A:=A)) :=
  equiv_prf := Build_equivalence _ _ _ _ _.

Next Obligation. (* refl *)
Proof.
  red ; cofix IH ; intros.

  rewrite unfold_ilist.
  case x ; constructor ; auto.
Qed.

Next Obligation. (* trans *)
Proof.
  red ; cofix IH ; intros.

  inversion H ; subst ; auto.
  inversion H0 ; subst.
  constructor ; auto.
  apply (IH tl tl' tl'0) ; auto.
Qed.

Next Obligation. (* sym *)
Proof.    
  red ; cofix IH ; intros.

  inversion H ; subst ; constructor ; auto.
Qed.

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

Tactic Notation "simpl_ilist" constr(x) :=
  rewrite (unfold_ilist x) ; simpl.

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

Program Instance ? Morphism ilist_setoid ilist_setoid (@icons A x).

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

CoFixpoint map `a b` (f : a -> b) (l : ilist a) : ilist b :=
  match l with
    | inil => inil
    | icons hd tl => icons (f hd) (map f tl)
  end.

Program Instance ? Morphism ilist_setoid ilist_setoid (@map A B f).

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

  rewrite (unfold_ilist (map f (icons a0 x))).
  rewrite (unfold_ilist (map f (icons a0 y))).
  simpl ; constructor ; auto.
Qed.

Require Import Prelude.Functor.

Program Instance ilist_functor : Functor ilist :=
  fmap a b f x := map f x.

Next Obligation.
Proof.
  extensionality x.
  setoideq_ext ; revert x.
  cofix IH ; intros.
  rewrite (unfold_ilist (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 ; setoideq_ext ; revert x ; simpl @equiv.
  unfold compose.
  cofix IH. intros x.

  rewrite (unfold_ilist (map f (map g x))).
  rewrite (unfold_ilist (map (fun x => f (g x)) x)).

  case x ; simpl ; try constructor ; auto.
Qed.

CoFixpoint ilist_cobind `a b` (f : ilist a -> b) (x : ilist a) : ilist b :=
  match x with
    | inil => inil
    | icons hd tl => 
      icons (f x) (ilist_cobind f tl)
  end.

CoFixpoint iapp `A` (l l' : ilist A) : ilist A :=
  match l with
    | inil => l'
    | icons x l => icons x (iapp l l')
  end.

Infix "ooo" := iapp (right associativity, at level 60) : ilist_scope.

Open Scope ilist_scope.


Lemma iapp_inil_left : forall a (l : ilist a), iapp inil l == l.
Proof.
  simpl ; intros.
  simpl_ilist (inil ooo l).
  destruct l ; refl.
Qed.

Lemma iapp_inil_right : forall a (l : ilist a), iapp l inil == l.
Proof.
  simpl ; intros a ; cofix IH.

  intros l ; rewrite_neeq. 
  case l ; simpl.
  
  refl.

  intros.
  constructor ; auto.
  apply IH.
Qed.

Program Instance iapp_morphism : ? BinaryMorphism (@iapp A).

Next Obligation.
Proof.
  red. 
  cofix IH ; intros.

  destruct x ; destruct y ; inversion H ; subst.

  clrewrite (iapp_inil_left z).
  clrewrite (iapp_inil_left w).
  apply H0.

  rewrite_neeq.
  simpl.
  constructor ; auto.
Qed.

Lemma iapp_assoc : forall a (l l' l'' : ilist a), l ooo l' ooo l'' == (l ooo l') ooo l''.
Proof with auto.
  intros a.
  cofix IH ; intros.

  rewrite_neeq.
  destruct l ; simpl.
  refl.

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

  case l ; simpl ; intros.
  refl.

  (* interesting guardness condition bug :) *)
  (*   clrewrite (IH l0 l' f). *)
  (*   refl. *)
  constructor...
  apply IH.
Qed.
  
CoFixpoint repeat `A` (a : A) := icons a (repeat a).

Require Import Prelude.Alternative.

(** Have to rebind... again, pure bug *)
Infix "<*>" := ap (at level 60).

Section Alternative.
  Context [ Alternative f ].

  (** Just can't define it this way, as [f] is not necessarily coinductive and this breaks 
     * the guardness criterion...
     *)
(*   Definition some `a` (v : f a) : f (ilist a) := *)
(*     cofix some_v : f (ilist a) := icons <$> v <*> (some_v <|> pure inil). *)

End Alternative.