Require Import List.

Definition option_bind {A B: Type} (f : A -> option B) (x : option A) :=
  match x with | None => None | Some y => f y end.

Fixpoint option_list_map {A : Type} (l : list (option A)) : option (list A) :=
match l with 
| nil => Some nil
| Some h :: t => option_map (cons h) (option_list_map t)
| _ => None
end.

Lemma option_list_map_Some {A : Type} (l : list (option A)) v:
 option_list_map l = Some v ->
 forall x, In x l -> exists vx, x = Some vx.
Proof.
revert v;
induction l; intros v H x Hin;
simpl option_list_map in H.
- inversion Hin.
- destruct Hin as [Ha | Hl].
  + subst.
(* Goal: @ex A (fun vx : A => @eq (option A) x (@Some A vx)) *)
    destruct x.
    * eauto.
    * inversion H.
  + destruct a as [ a |]; [| inversion H].
(* Goal: @ex A (fun vx : A => @eq (option A) x (@Some A vx)) *)
    destruct (option_list_map l) as [ ll |].
    * eauto.
    * inversion H.
Qed.

Lemma option_list_map_map {A : Type} (l : list (option A)) f :
  (forall x, In x l -> x = Some (f x)) ->
    option_list_map l = Some (map f l).
Proof.
(* Goal: forall _ : forall (x : option A) (_ : @In (option A) x l), @eq (option A) x (@Some A (f x)), @eq (option (list A)) (@option_list_map A l) (@Some (list A) (@map (option A) A f l)) *)
induction l; intros H.
- unfold option_list_map; trivial.
- assert (Ha : a = Some (f a)) by auto with *.
(* Goal: @eq (option (list A)) (@option_list_map A (@cons (option A) a l)) (@Some (list A) (@map (option A) A f (@cons (option A) a l))) *)
  rewrite Ha.
  assert (Hl : option_list_map l = Some (map f l)) by auto with *.
  unfold option_list_map, option_map in *.
  now rewrite Hl, <- Ha.
Qed.

Definition complete_option {A : Type} x0 (x : option A) : A :=
match x with
| None => x0
| Some x => x
end.

Definition option_le x y : Prop := 
 exists vx vy, x = Some vx /\ y = Some vy /\ le vx vy.

Notation "x ≤p y" := (option_le x y) (at level 60).

Definition option_choice {A B: Type} (f g: A -> option B) x :=
match f x with 
| Some v => Some v
| None => g x
end.

Notation " f ;; g " := (option_choice f g) (at level 60).

Lemma option_choice_assoc {A B: Type} (f g h : A -> option B) x:
 (f;;(g;;h)) x = (f;;g;;h) x.
Proof.
(* Goal: @eq (option B) (@option_choice A B f (@option_choice A B g h) x) (@option_choice A B (@option_choice A B f g) h x) *)
unfold option_choice.
(* Goal: @eq (option B) match f x with | Some v => @Some B v | None => match g x with | Some v => @Some B v | None => h x end end match match f x with | Some v => @Some B v | None => g x end with | Some v => @Some B v | None => h x end *)
case (f x); trivial.
Qed.

Lemma option_choice_none_right {A B: Type} (f : A -> option B) x:
 (f;;fun _ => None) x = f x.
Proof.
(* Goal: @eq (option B) match f x with | Some v => @Some B v | None => match g x with | Some v => @Some B v | None => h x end end match match f x with | Some v => @Some B v | None => g x end with | Some v => @Some B v | None => h x end *)
unfold option_choice; case (f x); trivial.
Qed.

Lemma option_choice_none_left {A B: Type} (f : A -> option B) x :
 ((fun _ => None) ;; f) x = f x.
Proof.
(* Goal: @eq (option B) match f x with | Some v => @Some B v | None => match g x with | Some v => @Some B v | None => h x end end match match f x with | Some v => @Some B v | None => g x end with | Some v => @Some B v | None => h x end *)
unfold option_choice; case (f x); trivial.
Qed.

Lemma option_choice_ext_left {A B: Type} (f f' g: A -> option B) x:
  (forall x, f x = f' x) ->
  (f;;g) x = (f';; g) x.
Proof.
(* Goal: @eq (option B) (@option_choice A B f (@option_choice A B g h) x) (@option_choice A B (@option_choice A B f g) h x) *)
intro H; unfold option_choice.
(* Goal: @eq (option B) match f x with | Some v => @Some B v | None => g x end match f' x with | Some v => @Some B v | None => g x end *)
case_eq (f x); simpl.
- intros v Hv; now rewrite <- H, Hv.
- intros Hnone; now rewrite <- H, Hnone.
Qed.

Lemma option_choice_ext_right {A B: Type} (f f' g: A -> option B) x:
  (forall x, f x = f' x) ->
  (g;;f) x = (g;;f') x.
Proof.
(* Goal: forall _ : forall x : A, @eq (option B) (f x) (f' x), @eq (option B) (@option_choice A B g f x) (@option_choice A B g f' x) *)
intro H; unfold option_choice; case_eq (g x); simpl; trivial.
Qed.

Lemma option_map_Some {A B : Type} (f : A -> B) x v:
  option_map f x = Some v -> exists v', x = Some v'.
Proof.
(* Goal: forall _ : @eq (option B) (@option_bind A B f x) (@Some B v), @ex A (fun v' : A => and (@eq (option A) x (@Some A v')) (@eq (option B) (f v') (@Some B v))) *)
intro H.
(* Goal: @ex A (fun v' : A => and (@eq (option A) x (@Some A v')) (@eq (option B) (f v') (@Some B v))) *)
destruct x as [v' |].
- eauto.
- inversion H.
Qed.

Lemma option_bind_Some {A B : Type} (f : A -> option B) x v:
 option_bind f x = Some v -> exists v', x = Some v' /\ f v' = Some v.
Proof.
(* Goal: forall _ : @eq (option B) (@option_bind A B f x) (@Some B v), @ex A (fun v' : A => and (@eq (option A) x (@Some A v')) (@eq (option B) (f v') (@Some B v))) *)
intro H.
(* Goal: @ex A (fun v' : A => and (@eq (option A) x (@Some A v')) (@eq (option B) (f v') (@Some B v))) *)
destruct x as [v' |].
- eauto.
- inversion H.
Qed.