(************************************************************************)
(*  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 Implicit Arguments.
Unset Strict Implicit.

Require Import Prelude.Functor.

Program Instance option_functor : Functor (fun A => option_setoid A) :=
  { fmap A B := mkMap2 (fun f x =>
    match x return _ with
      | Some x' => Some (f x') 
      | None => None
    end) }.

  Next Obligation.
  Proof. simpl_morph. destruct x0 ; destruct y0 ; intros ; pauto. rewrite Hxy0. apply Hxy. Qed.

  Next Obligation.
  Proof. intro b. simpl. destruct b. now simpl. now simpl. Qed.


  Next Obligation.
  Proof. intro b. simpl. destruct b. now simpl. now simpl. Qed.

Require Import Prelude.Monad.

Definition option_join {A} (x : option (option A)) :=
  match x return _ with Some a => a | None => None end.

Definition option_bind {A B} (x : option A) (f : A -> option B) := 
  match x return _ with Some a => f a | None => None end.
About Monad.

Program Instance option_pointed : ! Pointed option_setoid := {
  point A := SomeS }.

  Next Obligation. intro a. simpl. reflexivity. Qed.

Program Instance option_monad : ! Monad option_setoid := {
  join A := mkMap option_join }.


  Next Obligation. intros x y Hxy. unfold option_join. destruct x ; destruct y ; now simpl. Qed.

  Next Obligation. intros [[a|]|] ; now simpl. Qed.

  Solve Obligations using program_simpl ; intros [a|] ; try now simpl. 

  Next Obligation. intros [[[a|]|]|]; now simpl. Qed.

Require Import Prelude.MonadPlus.


About option_setoid_obligation_1.

Existing Instance option_setoid_obligation_1.

Program Instance option_mzero : ! MonadZero option_setoid := {
  mzero A := NoneS }.

  Next Obligation.
  Proof. intro. reflexivity. Qed.

  Next Obligation.
  Proof. intro. unfold flip, const. unfold bind. simpl. destruct x; simpl ; try reflexivity. Qed.
  
Program Instance option_mplus : ! MonadPlus option_setoid := {
  mplus A := mkMap2 (fun x y =>
    match x return _ with
      | None => y
      | x => x
    end) }.

  Next Obligation.
  Proof. simpl_morph. destruct x ; destruct y. simpl in * ; pauto. inversion Hxy. 
    inversion Hxy. assumption.
  Qed.

  Next Obligation.
  Proof. constructor. now simpl. 
    intro. unfold flip. now destruct x.
  Qed.

Require Import Prelude.Alternative.

Program Instance option_alternative : ! Alternative option_setoid := {
  empty a := NoneS ;
  alternative a := mkMap2 (fun x y => match x return _ with None => y | _ => x end) }.

  Solve Obligations using intros ; destruct x ; auto.