(************************************************************************)
(*  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 *)

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

Set Manual Implicit Arguments.

Require Import Prelude.Basics.
Require Import Prelude.Functor.
Require Import Prelude.Monad.
Require Export Prelude.List.

Open Local Scope list_scope.

Hint Unfold const constS Basics.id : core.

Notation " { x , p } " := (exist _ x p) (at level 0).

Lemma gen α [ Equivalence β eqβ ] (f g : α -> β) : f =∙= g -> Π l, eqβ (f l) (g l).
Proof. intros. apply H0. Qed.

Program Instance list_monad : ! Monad list_setoid :=
  join α := concat.

  Next Obligation.
  Proof. 
    unfold concat_map, composeS. simpl.
    clear_subset_proofs. intro l. simpl. 
    induction l ; auto; simpl. 
    constructor.
    unfold compose in *. simpl.
    rewrite <- IHl.
    rewrite (map_app f). reflexivity.
  Qed.

  Next Obligation.
  Proof. intro x ; simpl.
    unfold compose.
    induction x ; simpl ; trivial. reflexivity.
    simpl.
    rewrite IHx.
    reflexivity.
  Qed.

  Next Obligation.
  Proof. intro x ; simpl.
    unfold compose ; induction x ; auto.
    reflexivity.
    simpl in *.
    rewrite IHx. reflexivity.
  Qed.

  Next Obligation.
  Proof. intro x ; simpl.
    unfold compose.
    induction x ; subst ; auto.
    reflexivity.
    simpl ; rewrite <- IHx.
    typeclass_app concat_app. 
  Qed.

Require Import Prelude.MonadPlus.

Program Instance list_monad_zero : ! MonadZero list_setoid :=
  mzero A := nil.

  Next Obligation.
  Proof. reduce. unfold const. reflexivity. Qed.

  Next Obligation.
  Proof. reduce. unfold constS, const, flip. 
    induction x ; compute ; auto.
  Qed.

Program Instance list_monad_plus : ! MonadPlus list_setoid :=
  mplus A x y := x ++ y.

  Next Obligation.
  Proof.
    constructor ; reduce ; autosimpl.
    reflexivity.

    unfold flip.
    typeclass_app right_neutral.
  Qed.