From Tealeaves Require Export
  Classes.Kleisli.Monad
  Classes.Categorical.Applicative.

(** * The [option] Monad *)

(** [option] is defined by the Coq standard library. *)
(**********************************************************************)

(** ** Functor Instance *)
(**********************************************************************)
#[export] Instance Map_option: Map option :=
  fun A B (f: A -> B) (m: option A) =>
    match m with
    | Some a => Some (f a)
    | None => None
    end.

#[export] Instance Functor_option: Functor option.
Functor option
Proof.
Functor option
  constructor.
forall A : Type, map id = id
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
  -
forall A : Type, map id = id intros.
A: Type
map id = id now ext [|].
  -
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f) intros.
A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f) now ext [|].
Qed.

(** ** Applicative Instance *)
(**********************************************************************)
#[export] Instance Pure_option: Pure option :=
  @Some.

#[export] Instance Mult_option: Mult option.
Mult option
Proof.
Mult option
  hnf.
forall A B : Type,
option A * option B -> option (A * B)
  intros A B [[a|] [b|]].
A, B: Type
a: A
b: B
option (A * B)
A, B: Type
a: A
option (A * B)
A, B: Type
b: B
option (A * B)
A, B: Type
option (A * B)
  -
A, B: Type
a: A
b: B
option (A * B) exact (Some (a, b)).
  -
A, B: Type
a: A
option (A * B) exact None.
  -
A, B: Type
b: B
option (A * B) exact None.
  -
A, B: Type
option (A * B) exact None.
Defined.

#[export] Instance Applicative_option: Applicative option.
Applicative option
Proof.
Applicative option
  constructor; try typeclasses eauto.
forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x)
forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : option A) (y : option B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y))
forall (A B C : Type) (x : option A) (y : option B)
  (z : option C),
map associator (mult (mult (x, y), z)) =
mult (x, mult (y, z))
forall (A : Type) (x : option A),
map left_unitor (mult (pure tt, x)) = x
forall (A : Type) (x : option A),
map right_unitor (mult (x, pure tt)) = x
forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b)
  -
forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x) reflexivity.
  -
forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : option A) (y : option B),
mult (map f x, map g y) =
map (map_tensor f g) (mult (x, y)) destruct x as [x|];
      destruct y as [y|];
      reflexivity.
  -
forall (A B C : Type) (x : option A) (y : option B)
  (z : option C),
map associator (mult (mult (x, y), z)) =
mult (x, mult (y, z)) destruct x as [x|];
      destruct y as [y|];
      destruct z as [z|];
      reflexivity.
  -
forall (A : Type) (x : option A),
map left_unitor (mult (pure tt, x)) = x destruct x as [x|]; reflexivity.
  -
forall (A : Type) (x : option A),
map right_unitor (mult (x, pure tt)) = x destruct x as [x|]; reflexivity.
  -
forall (A B : Type) (a : A) (b : B),
mult (pure a, pure b) = pure (a, b) reflexivity.
Qed.


(** ** Monad Instance *)
(**********************************************************************)
#[export] Instance Return_option: Return option :=
  @Some.

#[export] Instance Join_option: Monad.Join option :=
  fun A (m: option (option A)) =>
    match m with
    | Some m' => m'
    | None => None
    end.

#[export] Instance: Natural (@ret option _).
Natural (@ret option Return_option)
Proof.
Natural (@ret option Return_option)
  constructor; try typeclasses eauto.
forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f
  reflexivity.
Qed.

#[export] Instance: Natural (@Monad.join option _).
Natural (@Monad.join option Join_option)
Proof.
Natural (@Monad.join option Join_option)
  constructor; try typeclasses eauto.
forall (A B : Type) (f : A -> B),
map f ∘ Monad.join = Monad.join ∘ map f
  intros.
A, B: Type
f: A -> B
map f ∘ Monad.join = Monad.join ∘ map f now ext [[|]|].
Qed.

#[export] Instance Monad_option: Categorical.Monad.Monad option.
Categorical.Monad.Monad option
Proof.
Categorical.Monad.Monad option
  constructor; try typeclasses eauto.
forall A : Type, Monad.join ∘ ret = id
forall A : Type, Monad.join ∘ map ret = id
forall A : Type,
Monad.join ∘ Monad.join = Monad.join ∘ map Monad.join
  -
forall A : Type, Monad.join ∘ ret = id intros.
A: Type
Monad.join ∘ ret = id now ext [|].
  -
forall A : Type, Monad.join ∘ map ret = id intros.
A: Type
Monad.join ∘ map ret = id now ext [|].
  -
forall A : Type,
Monad.join ∘ Monad.join = Monad.join ∘ map Monad.join intros.
A: Type
Monad.join ∘ Monad.join = Monad.join ∘ map Monad.join now ext [|].
Qed.