Require Import LogicalRelations.


(** * The [option_le] relator *)

Inductive option_le {A1 A2} (RA: rel A1 A2): rel (option A1) (option A2) :=
  | Some_le_def x y: RA x y -> option_le RA (Some x) (Some y)
  | None_le_def y: option_le RA None y.

Global Instance Some_le:
  Monotonic (@Some) (forallr R @ A1 A2 : rel, R ++> option_le R).
Proof.
(* Goal: @Related (forall (A : Type) (_ : A), option A) (forall (A : Type) (_ : A), option A) (@Some) (@Some) (@forall_rel Type Type (fun A1 A2 : Type => rel A1 A2) (fun A1 : Type => forall _ : A1, option A1) (fun A2 : Type => forall _ : A2, option A2) (fun (A1 A2 : Type) (R : (fun A3 A4 : Type => rel A3 A4) A1 A2) => @arrow_rel A1 A2 (option A1) (option A2) R (@option_le A1 A2 R))) *)
  exact @Some_le_def.
Qed.

Lemma None_le {A B} R y:
  RIntro True (@option_le A B R) None y.
Proof.
(* Goal: @RIntro (option A) (option B) True (@option_ge A B R) x (@None B) *)
  intros _.
(* Goal: @option_le A B R (@None A) y *)
  apply @None_le_def.
Qed.

Hint Extern 0 (RIntro _ (option_le _) None _) =>
  eapply None_le : typeclass_instances.

Global Instance option_le_subrel A B:
  Monotonic (@option_le A B) (subrel ++> subrel).
Proof.
(* Goal: @Related (forall _ : rel A B, rel (option A) (option B)) (forall _ : rel A B, rel (option A) (option B)) (@option_ge A B) (@option_ge A B) (@arrow_rel (rel A B) (rel A B) (rel (option A) (option B)) (rel (option A) (option B)) (@subrel A B) (@subrel (option A) (option B))) *)
  intros R1 R2 HR x y Hxy.
(* Goal: @option_ge B1 B2 RB (@option_map A1 B1 f x) (@option_map A2 B2 g y) *)
  destruct Hxy; constructor; eauto.
Qed.

Global Instance option_le_subrel_params:
  Params (@option_le) 3.

Global Instance option_le_rel {A B}:
  Related (@option_rel A B) (@option_le A B) (subrel ++> subrel) | 10.
Proof.
(* Goal: @Related (forall _ : rel A B, rel (option A) (option B)) (forall _ : rel A B, rel (option A) (option B)) (@option_rel A B) (@option_ge A B) (@arrow_rel (rel A B) (rel A B) (rel (option A) (option B)) (rel (option A) (option B)) (@subrel A B) (@subrel (option A) (option B))) *)
  intros R1 R2 HR _ _ []; constructor; eauto.
Qed.

Lemma option_le_refl {A} (R: relation A):
  Reflexive R -> Reflexive (option_le R).
Proof.
(* Goal: forall _ : @Transitive A R, @Transitive (option A) (@option_ge A A R) *)
  intros H.
(* Goal: @Reflexive (option A) (@option_ge A A R) *)
  intros [x|]; constructor; reflexivity.
Qed.

Hint Extern 1 (Reflexive (option_le ?R)) =>
  eapply option_le_refl : typeclass_instances.

Lemma option_le_trans {A} (R: relation A):
  Transitive R -> Transitive (option_le R).
Proof.
(* Goal: forall _ : @Transitive A R, @Transitive (option A) (@option_ge A A R) *)
  intros H.
(* Goal: @Transitive (option A) (@option_ge A A R) *)
  intros _ _ z [x y Hxy | y] Hz; inversion Hz; subst; clear Hz.
  - constructor.
(* Goal: R x y0 *)
    etransitivity; eassumption.
  - constructor.
  - constructor.
Qed.

Hint Extern 1 (Transitive (option_le ?R)) =>
  eapply option_le_trans : typeclass_instances.

Global Instance option_map_le:
  Monotonic
    (@option_map)
    (forallr RA, forallr RB, (RA ++> RB) ++> option_le RA ++> option_le RB).
Proof.
(* Goal: @Related (forall (A B : Type) (_ : forall _ : A, B) (_ : option A), option B) (forall (A B : Type) (_ : forall _ : A, B) (_ : option A), option B) option_map option_map (@forall_rel Type Type (fun H H0 : Type => rel H H0) (fun H : Type => forall v1 : Type, (fun H0 : Type => forall (_ : forall _ : H, H0) (_ : option H), option H0) v1) (fun H : Type => forall v2 : Type, (fun H0 : Type => forall (_ : forall _ : H, H0) (_ : option H), option H0) v2) (fun (v1 v2 : Type) (RA : (fun H H0 : Type => rel H H0) v1 v2) => @forall_rel Type Type (fun H H0 : Type => rel H H0) (fun H : Type => forall (_ : forall _ : v1, H) (_ : option v1), option H) (fun H : Type => forall (_ : forall _ : v2, H) (_ : option v2), option H) (fun (v3 v4 : Type) (RB : (fun H H0 : Type => rel H H0) v3 v4) => @arrow_rel (forall _ : v1, v3) (forall _ : v2, v4) (forall _ : option v1, option v3) (forall _ : option v2, option v4) (@arrow_rel v1 v2 v3 v4 RA RB) (@arrow_rel (option v1) (option v2) (option v3) (option v4) (@option_ge v1 v2 RA) (@option_ge v3 v4 RB))))) *)
  intros A1 A2 RA B1 B2 RB f g Hfg x y Hxy.
(* Goal: @option_ge B1 B2 RB (@option_map A1 B1 f x) (@option_map A2 B2 g y) *)
  destruct Hxy; constructor; eauto.
Qed.


(** * The [option_ge] relator *)

Inductive option_ge {A1 A2} (RA: rel A1 A2): rel (option A1) (option A2) :=
  | Some_ge_def x y: RA x y -> option_ge RA (Some x) (Some y)
  | None_ge_def x: option_ge RA x None.

Global Instance Some_ge:
  Monotonic (@Some) (forallr R @ A1 A2 : rel, R ++> option_ge R).
Proof.
(* Goal: @Related (forall (A : Type) (_ : A), option A) (forall (A : Type) (_ : A), option A) (@Some) (@Some) (@forall_rel Type Type (fun A1 A2 : Type => rel A1 A2) (fun A1 : Type => forall _ : A1, option A1) (fun A2 : Type => forall _ : A2, option A2) (fun (A1 A2 : Type) (R : (fun A3 A4 : Type => rel A3 A4) A1 A2) => @arrow_rel A1 A2 (option A1) (option A2) R (@option_ge A1 A2 R))) *)
  exact @Some_ge_def.
Qed.

Lemma None_ge {A B} R x:
  RIntro True (@option_ge A B R) x None.
Proof.
(* Goal: @RIntro (option A) (option B) True (@option_ge A B R) x (@None B) *)
  intros _.
(* Goal: @option_ge A B R x (@None B) *)
  apply @None_ge_def.
Qed.

Hint Extern 0 (RIntro _ (option_ge _) _ None) =>
  eapply None_ge : typeclass_instances.

Global Instance option_ge_subrel A B:
  Monotonic (@option_ge A B) (subrel ++> subrel).
Proof.
(* Goal: @Related (forall _ : rel A B, rel (option A) (option B)) (forall _ : rel A B, rel (option A) (option B)) (@option_ge A B) (@option_ge A B) (@arrow_rel (rel A B) (rel A B) (rel (option A) (option B)) (rel (option A) (option B)) (@subrel A B) (@subrel (option A) (option B))) *)
  intros R1 R2 HR x y Hxy.
(* Goal: @option_ge B1 B2 RB (@option_map A1 B1 f x) (@option_map A2 B2 g y) *)
  destruct Hxy; constructor; eauto.
Qed.

Global Instance option_ge_subrel_params:
  Params (@option_ge) 3.

Global Instance option_ge_rel {A B}:
  Related (@option_rel A B) (@option_ge A B) (subrel ++> subrel) | 10.
Proof.
(* Goal: @Related (forall _ : rel A B, rel (option A) (option B)) (forall _ : rel A B, rel (option A) (option B)) (@option_rel A B) (@option_ge A B) (@arrow_rel (rel A B) (rel A B) (rel (option A) (option B)) (rel (option A) (option B)) (@subrel A B) (@subrel (option A) (option B))) *)
  intros R1 R2 HR _ _ []; constructor; eauto.
Qed.

Lemma option_ge_refl {A} (R: relation A):
  Reflexive R -> Reflexive (option_ge R).
Proof.
(* Goal: forall _ : @Transitive A R, @Transitive (option A) (@option_ge A A R) *)
  intros H.
(* Goal: @Reflexive (option A) (@option_ge A A R) *)
  intros [x|]; constructor; reflexivity.
Qed.

Hint Extern 1 (Reflexive (option_ge ?R)) =>
  eapply option_ge_refl : typeclass_instances.

Lemma option_ge_trans {A} (R: relation A):
  Transitive R -> Transitive (option_ge R).
Proof.
(* Goal: forall _ : @Transitive A R, @Transitive (option A) (@option_ge A A R) *)
  intros H.
(* Goal: @Transitive (option A) (@option_ge A A R) *)
  intros _ _ z [x y Hxy | y] Hz; inversion Hz; subst; clear Hz.
  - constructor.
(* Goal: R x y0 *)
    etransitivity; eassumption.
  - constructor.
  - constructor.
Qed.

Hint Extern 1 (Transitive (option_ge ?R)) =>
  eapply option_ge_trans : typeclass_instances.

Global Instance option_map_ge:
  Monotonic
    (@option_map)
    (forallr RA, forallr RB, (RA ++> RB) ++> option_ge RA ++> option_ge RB).
Proof.
(* Goal: @Related (forall (A B : Type) (_ : forall _ : A, B) (_ : option A), option B) (forall (A B : Type) (_ : forall _ : A, B) (_ : option A), option B) option_map option_map (@forall_rel Type Type (fun H H0 : Type => rel H H0) (fun H : Type => forall v1 : Type, (fun H0 : Type => forall (_ : forall _ : H, H0) (_ : option H), option H0) v1) (fun H : Type => forall v2 : Type, (fun H0 : Type => forall (_ : forall _ : H, H0) (_ : option H), option H0) v2) (fun (v1 v2 : Type) (RA : (fun H H0 : Type => rel H H0) v1 v2) => @forall_rel Type Type (fun H H0 : Type => rel H H0) (fun H : Type => forall (_ : forall _ : v1, H) (_ : option v1), option H) (fun H : Type => forall (_ : forall _ : v2, H) (_ : option v2), option H) (fun (v3 v4 : Type) (RB : (fun H H0 : Type => rel H H0) v3 v4) => @arrow_rel (forall _ : v1, v3) (forall _ : v2, v4) (forall _ : option v1, option v3) (forall _ : option v2, option v4) (@arrow_rel v1 v2 v3 v4 RA RB) (@arrow_rel (option v1) (option v2) (option v3) (option v4) (@option_ge v1 v2 RA) (@option_ge v3 v4 RB))))) *)
  intros A1 A2 RA B1 B2 RB f g Hfg x y Hxy.
(* Goal: @option_ge B1 B2 RB (@option_map A1 B1 f x) (@option_map A2 B2 g y) *)
  destruct Hxy; constructor; eauto.
Qed.


(** * [Transport] instances for [option] relations *)

Global Instance option_le_transport_eq_some {A B} (R: rel A B) x y a:
  Transport (option_le R) x y (x = Some a) (exists b, y = Some b /\ R a b).
Proof.
(* Goal: @Transport (option A) (option B) (@option_ge A B R) x y (@eq (option A) x (@None A)) (@eq (option B) y (@None B)) *)
  intros Hxy Hx.
(* Goal: @eq (option B) y (@None B) *)
  subst; inversion Hxy; eauto.
Qed.

Global Instance option_ge_transport_eq_none {A B} (R: rel A B) x y:
  Transport (option_ge R) x y (x = None) (y = None).
Proof.
(* Goal: @Transport (option A) (option B) (@option_ge A B R) x y (@eq (option A) x (@None A)) (@eq (option B) y (@None B)) *)
  intros Hxy Hx.
(* Goal: @eq (option B) y (@None B) *)
  subst; inversion Hxy; eauto.
Qed.
