Library Prelude.Control.Option

From Prelude Require Import Init Control Equality.

#[local]
Open Scope prelude_scope.

Bind Scope monad_scope with option.

Inductive is_some {a}: option a -> Prop :=
| is_some_rule (x: a): is_some (Some x).

#[program]
Definition is_some_dec {a} (x : option a) : { is_some x } + { ~ is_some x } :=
  match x with
  | Some x => left (is_some_rule x)
  | None => right _
  end.

Next Obligation.
  now intro H.
Defined.

Definition maybe {a b} (f : a -> b) (x : b) (o : option a) : b :=
  match o with
  | Some o => f o
  | None => x
  end.

Definition fromMaybe {a} (x : a) (o : option a) : a :=
  maybe id x o.

#[program]
Instance option_Functor : Functor option :=
  { map := option_map
  }.

Next Obligation.
  destruct x.
  + now constructor.
  + constructor.
Defined.

Next Obligation.
  destruct x.
  + now constructor.
  + constructor.
Defined.

Definition option_app {a b} (f : option (a -> b)) (x : option a) : option b :=
  match f with
  | Some f => f <$> x
  | None => None
  end.

#[program]
Instance option_Applicative : Applicative option :=
  { apply := @option_app
  ; pure := @Some
  }.

Next Obligation.
  destruct v; now constructor.
Defined.

Next Obligation.
  destruct w; destruct v; destruct u; now constructor.
Defined.

Next Obligation.
  now constructor.
Defined.

Next Obligation.
  destruct u; now constructor.
Defined.

Next Obligation.
  destruct x; now constructor.
Defined.

Definition option_bind {a b} (x : option a) (f : a -> option b) : option b :=
  match x with
  | Some x => f x
  | None => None
  end.

#[program]
Instance option_Monad
  : Monad option :=
  { bind := @option_bind
  }.

Next Obligation.
  destruct (f x); now constructor.
Defined.

Next Obligation.
  destruct x; now constructor.
Defined.

Next Obligation.
  destruct f; cbn; [| constructor ].
  destruct (g a0); cbn; [| constructor ].
  destruct (h b0); now constructor.
Defined.

Next Obligation.
  destruct x; [| constructor].
  apply H0.
Defined.

Next Obligation.
  destruct x; now constructor.
Defined.