Library Padec.Tools.OptionUtil

Require Import Relations.
Require Import SetoidClass.

Require Import SetoidUtil.

Open Scope signature_scope.
Set Implicit Arguments.

Definition eqoptionA {A: Type} (eqA: relation A): relation (option A) :=
  fun oa1 oa2 => match oa1,oa2 with
                 | None, None => True
                 | Some a1, Some a2 => eqA a1 a2
                 | _, _ => False
                 end.

Definition leoptionA {A: Type} (eqA: relation A): relation (option A) :=
  fun oa1 oa2 => match oa1, oa2 with
                 | None, _ => True
                 | Some a1, Some a2 => eqA a1 a2
                 | _, _ => False
                 end.

Global Instance leoptionA_compat {A: Type} (eqA: relation A) `{P: PER _ eqA}:
  Proper (eqoptionA eqA ==> eqoptionA eqA ==> iff) (leoptionA eqA).

Global Instance leoptionA_transitive {A: Type} (eqA: relation A):
  Transitive eqA -> Transitive (leoptionA eqA).

Global Instance eqoptionA_per {A: Type} (eqA: relation A) `{P: PER _ eqA}:
  PER (eqoptionA eqA).

Global Instance eqoptionA_equiv {A: Type} (eqA: relation A)
         `{P: Equivalence _ eqA}: Equivalence (eqoptionA eqA).

Global Instance option_PartialSetoid {A} `{SA: PartialSetoid A}:
  PartialSetoid (option A) := {| pequiv := eqoptionA pequiv |}.

Global Instance option_Setoid {A} `{SA: Setoid A}:
  Setoid (option A) := {| equiv := eqoptionA equiv |}.

Lemma eqoptionA_dec {A:Type} (eqA: relation A):
  Decider eqA -> Decider (eqoptionA eqA).

Lemma leoptionA_dec {A:Type} (eqA: relation A):
  Decider eqA -> Decider (leoptionA eqA).

Section with_Setoid.

  Context {A} `{A_Setoid: Setoid A}.

  Instance leoptionA_preorder: PreOrder (leoptionA equiv).

  Instance leoptionA_partialorder: PartialOrder equiv (leoptionA equiv).

  Global Instance Some_compat : Proper (equiv ==> equiv) (@Some A).

  Global Instance None_compat : Proper equiv (@None A) := I.

  Context {B: Type} `{B_Setoid: Setoid B}.

  Global Instance option_rect_compat:
    Proper ((equiv (A := A) ==> equiv (A := B))
              ==> equiv ==> equiv ==> equiv) (option_rect (fun _=>B)).

  Global Instance option_map_compat:
    Proper ((equiv (A := A) ==> equiv (A := B))
              ==> equiv ==> equiv) (option_map (B := B)).

End with_Setoid.

Section with_PartialSetoid.

  Context {A:Type} `{A_PartialSetoid: PartialSetoid A}.

  Global Instance Some_compat': Proper (pequiv ==> pequiv) (@Some A).

  Global Instance None_compat': Proper pequiv (@None A) := I.

  Context {B:Type} `{B_Psetoid: PartialSetoid B}.

  Global Instance option_rect_compat':
    Proper ((pequiv (A := A) ==> pequiv (A := B))
              ==> pequiv ==> pequiv ==> pequiv) (option_rect (fun _=>B)).

  Global Instance option_map_compat' eqA eqB:
    Proper ((eqA ==> eqB) ==> (eqoptionA eqA)
                          ==> (eqoptionA eqB)) (@option_map A B).

End with_PartialSetoid.

Unset Implicit Arguments.
Close Scope signature_scope.