Library liblayers.logic.GlobalVars

Require Import Decision.
Require Import PseudoJoin.
Require Import OptionOrders.
Require Import ErrorMonad.

Class GlobalVarsOps (V: Type): Type :=
  {
    globalvar_eq_dec :> EqDec V
  }.


Section WITHGLOBALVARSOPS.
Context `{gvar_ops: GlobalVarsOps}.

Global Instance res_globalvar_oplus:
  Oplus (res V) :=
  {
    oplus rv1 rv2 :=
      _ <- eassert nil (rv1 = rv2);
    rv1
  }.

Lemma res_globalvar_oplus_def rv1 rv2:
  rv1 rv2 =
      _ <- eassert nil (rv1 = rv2);
    rv1.
Proof.
  reflexivity.
Qed.

Global Opaque res_globalvar_oplus.

Lemma res_globalvar_oplus_idem (rv: res V):
  rv rv = rv.
Proof.
  rewrite res_globalvar_oplus_def.
  eassert_true; auto.
Qed.

Hint Rewrite res_globalvar_oplus_idem: res_globalvar.

Lemma res_globalvar_oplus_diff (rv1 rv2: res V):
  rv1 rv2
  rv1 rv2 = Error nil.
Proof.
  intros.
  rewrite res_globalvar_oplus_def.
  eassert_false; auto.
Qed.

Lemma res_globalvar_oplus_comm (rv1 rv2: res V):
  rv1 rv2 = rv2 rv1.
Proof.
  rewrite res_globalvar_oplus_def.
  destruct (decide (rv1 = rv2));
    rewrite res_globalvar_oplus_def.
  + repeat (eassert_true; auto).
  + repeat (eassert_false; auto).
Qed.

Lemma res_globalvar_oplus_error_nil_left rv:
  rv Error nil = Error nil.
Proof.
  destruct (decide (rv = Error nil));
  subst;
  autorewrite with res_globalvar;
  auto.
  apply res_globalvar_oplus_diff; auto.
Qed.

Hint Rewrite res_globalvar_oplus_error_nil_left: res_globalvar.

Lemma res_globalvar_oplus_error_nil_right rv:
  Error nil rv = Error nil.
Proof.
  rewrite res_globalvar_oplus_comm.
  autorewrite with res_globalvar.
  reflexivity.
Qed.

Hint Rewrite res_globalvar_oplus_error_nil_right: res_globalvar.

Lemma res_globalvar_oplus_ok_error v e:
  OK v Error e = Error nil.
Proof.
  reflexivity.
Qed.

Hint Rewrite res_globalvar_oplus_ok_error: res_globalvar.

Lemma res_globalvar_oplus_error_ok e v:
  Error e OK v = Error nil.
Proof.
  reflexivity.
Qed.

Hint Rewrite res_globalvar_oplus_error_ok: res_globalvar.

Lemma res_globalvar_oplus_error_left e1 v:
  isError (Error e1 v).
Proof.
  rewrite res_globalvar_oplus_def.
  destruct (decide (Error e1 = v)).
  + eassert_true; eauto.
  + eassert_false; eauto.
Qed.

Lemma res_globalvar_oplus_error_right v e1:
  isError (v Error e1).
Proof.
  rewrite res_globalvar_oplus_comm.
  apply res_globalvar_oplus_error_left.
Qed.

Lemma res_globalvar_oplus_assoc (rv1 rv2 rv3: res V):
  (rv1 rv2) rv3 = rv1 (rv2 rv3).
Proof.
  destruct (decide (rv1 = rv2)).
  + subst. autorewrite with res_globalvar.
    destruct (decide (rv2 = rv3)).
    - subst. autorewrite with res_globalvar. reflexivity.
    - rewrite (res_globalvar_oplus_diff rv2 rv3); auto.
      autorewrite with res_globalvar.
      reflexivity.
  + rewrite (res_globalvar_oplus_diff rv1 rv2); auto.
    autorewrite with res_globalvar.
    destruct (decide (rv2 = rv3)).
    - subst. autorewrite with res_globalvar.
      symmetry. apply res_globalvar_oplus_diff. assumption.
    - rewrite (res_globalvar_oplus_diff rv2 rv3); auto.
      autorewrite with res_globalvar.
      reflexivity.
Qed.

Local Instance res_globalvar_le {gvar_ops: GlobalVarsOps V}:
  Le (res V) :=
  {
    le := res_le eq
  }.

Local Instance res_globalvar_oplus_left_upper_bound:
  LeftUpperBound (A := res V) (≤) (⊕).
Proof.
  repeat red.
  intros x y.
  destruct (decide (x = y)); subst; autorewrite with res_globalvar.
  + subst. reflexivity.
  + rewrite res_globalvar_oplus_diff; auto. constructor.
Qed.

Local Instance res_globalvar_oplus_mono:
  @Proper (res V res V res V) ((≤) ++> (≤) ++> (≤)) (⊕).
Proof.
  repeat red.
  intros x y H x0 y0 H0.
  rewrite (res_globalvar_oplus_def y y0).
  destruct (decide (y = y0)); [ eassert_true | eassert_false ]; auto;
  try constructor.
  subst.
  inversion H0; subst; inversion H; subst; try constructor.
  rewrite res_globalvar_oplus_def.
  eassert_true; auto.
Qed.

Ltac res_globalvar_red :=
  autorewrite with res_globalvar;
  repeat (
      match goal with
          [ |- context [ Error ?v1 ?v2 ] ] ⇒
          let e := fresh "e" in
          let He := fresh "H" e in
          destruct (res_globalvar_oplus_error_left v1 v2) as [e He];
          rewrite He;
          autorewrite with res_globalvar
      end
    ).

Lemma res_globalvar_lub (v1 v2 v: res V):
  v1 v
  v2 v
  v1 v2 v.
Proof.
  inversion 1; subst; inversion 1; subst;
  res_globalvar_red;
  auto;
  constructor.
Qed.

Global Instance option_res_globalvar_oplus:
  Oplus (option (res V)) :=
  {
    oplus orv1 orv2 :=
      match orv1, orv2 with
        | None, _orv2
        | _, Noneorv1
        | Some rv1, Some rv2Some (rv1 rv2)
      end
  }.

Lemma option_res_globalvar_oplus_def orv1 orv2:
  orv1 orv2 =
  match orv1, orv2 with
    | None, _orv2
    | _, Noneorv1
    | Some rv1, Some rv2Some (rv1 rv2)
  end.
Proof.
  reflexivity.
Qed.

Global Opaque option_res_globalvar_oplus.

Lemma option_res_globalvar_oplus_none_left rv:
  None rv = rv.
Proof.
  destruct rv; auto.
Qed.

Hint Rewrite option_res_globalvar_oplus_none_left: option_res_globalvar.

Lemma option_res_globalvar_oplus_none_right rv:
  rv None = rv.
Proof.
  destruct rv; auto.
Qed.

Hint Rewrite option_res_globalvar_oplus_none_right: option_res_globalvar.

Lemma option_res_globalvar_oplus_some rv1 rv2:
  Some rv1 Some rv2 = Some (rv1 rv2).
Proof.
  reflexivity.
Qed.

Hint Rewrite option_res_globalvar_oplus_some: option_res_globalvar.

Lemma option_res_globalvar_oplus_idem rv:
  rv rv = rv.
Proof.
  destruct rv; auto.
  rewrite option_res_globalvar_oplus_def.
  autorewrite with res_globalvar.
  reflexivity.
Qed.

Hint Rewrite option_res_globalvar_oplus_idem: option_res_globalvar.

Lemma option_res_globalvar_oplus_comm (rv1 rv2: option (res V)):
  rv1 rv2 = rv2 rv1.
Proof.
  destruct rv1; destruct rv2; autorewrite with option_res_globalvar; auto.
  rewrite res_globalvar_oplus_comm.
  reflexivity.
Qed.

Lemma option_res_globalvar_oplus_assoc (rv1 rv2 rv3: option (res V)):
  (rv1 rv2) rv3 = rv1 (rv2 rv3).
Proof.
  destruct rv1; destruct rv2; destruct rv3;
  autorewrite with option_res_globalvar;
  auto.
  rewrite res_globalvar_oplus_assoc.
  reflexivity.
Qed.

Lemma option_res_globalvar_oplus_error_nil_left rv:
  Some (Error nil) rv = Some (Error nil).
Proof.
  destruct rv; autorewrite with option_res_globalvar; auto.
  autorewrite with res_globalvar; auto.
Qed.

Hint Rewrite option_res_globalvar_oplus_error_nil_left: option_res_globalvar.

Lemma option_res_globalvar_oplus_error_nil_right rv:
  rv Some (Error nil) = Some (Error nil).
Proof.
  rewrite option_res_globalvar_oplus_comm.
  autorewrite with option_res_globalvar.
  reflexivity.
Qed.

Hint Rewrite option_res_globalvar_oplus_error_nil_right: option_res_globalvar.

Global Instance option_res_globalvar_le {gvar_ops: GlobalVarsOps V}:
  Le (option (res V)) :=
  {
    le := option_le (≤)
  }.

Local Instance option_res_globalvar_oplus_mono:
  @Proper (option (res V) _ _) ((≤) ++> (≤) ++> (≤)) (⊕).
Proof.
  repeat red.
  intros x y H x0 y0 H0.
  inversion H; clear H; subst; inversion H0; clear H0; subst;
  autorewrite with option_res_globalvar.
  + constructor.
  + destruct y; autorewrite with option_res_globalvar; constructor; auto.
    rewrite res_globalvar_oplus_comm.
    simpl (≤).
    etransitivity; eauto.
    apply res_globalvar_oplus_left_upper_bound.
  + destruct y0; autorewrite with option_res_globalvar; constructor; auto.
    simpl (≤).
    etransitivity; eauto.
    apply res_globalvar_oplus_left_upper_bound.
  + constructor.
    solve_monotonic.
Qed.

Global Instance option_res_globalvar_pseudojoin:
  PseudoJoin (option (res V)) None.
Proof.
  constructor; simpl (≤); try typeclasses eauto.
  + split; typeclasses eauto.
  + repeat red. intros; autorewrite with option_res_globalvar; reflexivity.
  + repeat red. intros. rewrite option_res_globalvar_oplus_assoc. reflexivity.
  + repeat red. intros. rewrite option_res_globalvar_oplus_comm. reflexivity.
  + repeat red. intros x y.
    destruct x; try constructor.
    destruct y; autorewrite with option_res_globalvar; repeat constructor.
    - apply res_globalvar_oplus_left_upper_bound.
    - reflexivity.
Qed.

Lemma option_res_globalvar_lub (v1 v2 v: option (res V)):
  v1 v
  v2 v
  v1 v2 v.
Proof.
  inversion 1; subst; inversion 1; subst;
  autorewrite with option_res_globalvar;
  constructor; auto using res_globalvar_lub.
Qed.

Global Instance res_option_globalvar_oplus:
  Oplus (res (option V)) :=
  {
    oplus rov1 rov2 :=
      option_res_flip (res_option_flip rov1 res_option_flip rov2)
  }.

Lemma res_option_globalvar_oplus_def rov1 rov2:
  rov1 rov2 =
  option_res_flip (res_option_flip rov1 res_option_flip rov2).
Proof.
  reflexivity.
Qed.

Global Opaque res_option_globalvar_oplus.

Lemma res_option_globalvar_oplus_none_left (rv: res (option V)):
  OK None rv = rv.
Proof.
  rewrite res_option_globalvar_oplus_def.
  simpl.
  autorewrite with option_res_globalvar.
  apply res_option_flip_inv.
Qed.

Hint Rewrite res_option_globalvar_oplus_none_left: res_option_globalvar.

Lemma res_option_globalvar_oplus_comm (rv1 rv2: res (option V)):
  rv1 rv2 = rv2 rv1.
Proof.
  repeat rewrite res_option_globalvar_oplus_def.
  rewrite option_res_globalvar_oplus_comm.
  reflexivity.
Qed.

Lemma res_option_globalvar_oplus_none_right (rv: res (option V)):
  rv OK None = rv.
Proof.
  rewrite res_option_globalvar_oplus_comm.
  autorewrite with res_option_globalvar.
  reflexivity.
Qed.

Hint Rewrite res_option_globalvar_oplus_none_right: res_option_globalvar.

Lemma res_option_globalvar_oplus_idem (rv: res (option V)):
  rv rv = rv.
Proof.
  rewrite res_option_globalvar_oplus_def.
  autorewrite with option_res_globalvar.
  apply res_option_flip_inv.
Qed.

Hint Rewrite res_option_globalvar_oplus_idem: res_option_globalvar.

Lemma res_option_globalvar_oplus_error_nil_left (rv: res (option V)):
  Error nil rv = Error nil.
Proof.
  rewrite res_option_globalvar_oplus_def.
  autorewrite with option_res_globalvar.
  reflexivity.
Qed.

Hint Rewrite res_option_globalvar_oplus_error_nil_left: res_option_globalvar.

Lemma res_option_globalvar_oplus_error_nil_right (rv: res (option V)):
  rv Error nil = Error nil.
Proof.
  rewrite res_option_globalvar_oplus_comm.
  autorewrite with res_option_globalvar.
  reflexivity.
Qed.

Hint Rewrite res_option_globalvar_oplus_error_nil_right: res_option_globalvar.

Lemma res_option_globalvar_oplus_diff (v1 v2: V):
  v1 v2
  OK (Some v1) OK (Some v2) = Error nil.
Proof.
  intros H.
  rewrite res_option_globalvar_oplus_def.
  simpl.
  rewrite option_res_globalvar_oplus_def.
  rewrite res_globalvar_oplus_diff by congruence.
  reflexivity.
Qed.

Lemma res_option_globalvar_oplus_ok_error v e:
  OK (Some v) Error e = Error nil.
Proof.
  reflexivity.
Qed.

Hint Rewrite res_option_globalvar_oplus_ok_error: res_option_globalvar.

Lemma res_option_globalvar_oplus_error_ok v e:
  Error e OK (Some v) = Error nil.
Proof.
  reflexivity.
Qed.

Hint Rewrite res_option_globalvar_oplus_error_ok: res_option_globalvar.

Lemma res_option_globalvar_oplus_error_left e (rv: res (option V)):
  isError (Error e rv).
Proof.
  rewrite res_option_globalvar_oplus_def.
  simpl.
  destruct rv as [ [ | ] | e' ]; simpl;
  autorewrite with option_res_globalvar;
  simpl; eauto;
  res_globalvar_red;
  eauto.
Qed.

Lemma res_option_globalvar_oplus_error_right (rv: res (option V)) e:
  isError (rv Error e).
Proof.
  rewrite res_option_globalvar_oplus_comm.
  apply res_option_globalvar_oplus_error_left.
Qed.

Lemma res_option_globalvar_oplus_assoc (rv1 rv2 rv3: res (option V)):
  (rv1 rv2) rv3 = rv1 (rv2 rv3).
Proof.
  repeat rewrite res_option_globalvar_oplus_def.
  repeat rewrite option_res_flip_inv.
  rewrite option_res_globalvar_oplus_assoc.
  reflexivity.
Qed.

Global Instance res_option_globalvar_le {gvar_ops: GlobalVarsOps V}:
  Le (res (option V)) :=
  {
    le := res_le (option_le eq)
  }.

Global Instance res_option_globalvar_pseudojoin:
  PseudoJoin (res (option V)) (OK None).
Proof.
  constructor; simpl (≤); try typeclasses eauto.
  + split; typeclasses eauto.
  + repeat red.
    intros.
    repeat rewrite res_option_globalvar_oplus_def.
    apply option_res_le_flip.
    solve_monotonic.
  + repeat red.
    intros.
    autorewrite with res_option_globalvar.
    reflexivity.
  + repeat red.
    intros.
    rewrite res_option_globalvar_oplus_assoc.
    reflexivity.
  + repeat red.
    intros.
    rewrite res_option_globalvar_oplus_comm.
    reflexivity.
  + repeat red.
    intros.
    rewrite res_option_globalvar_oplus_def.
    etransitivity;
      [ |
        eapply option_res_le_flip;
          exact (oplus_le_left (res_option_flip x) (res_option_flip y)) ].
    rewrite res_option_flip_inv.
    reflexivity.
Qed.

Lemma res_option_globalvar_lub (v1 v2 v: res (option V)):
  v1 v
  v2 v
  v1 v2 v.
Proof.
  simpl.
  intros H H0.
  rewrite <- res_option_le_flip in H.
  rewrite <- res_option_le_flip in H0.
  rewrite <- res_option_le_flip.
  rewrite res_option_globalvar_oplus_def.
  rewrite option_res_flip_inv.
  apply option_res_globalvar_lub; auto.
Qed.

End WITHGLOBALVARSOPS.

Hint Rewrite @res_globalvar_oplus_idem: res_globalvar.
Hint Rewrite @res_globalvar_oplus_error_nil_left: res_globalvar.
Hint Rewrite @res_globalvar_oplus_error_nil_right: res_globalvar.
Hint Rewrite @res_globalvar_oplus_ok_error: res_globalvar.
Hint Rewrite @res_globalvar_oplus_error_ok: res_globalvar.
Hint Rewrite @option_res_globalvar_oplus_none_left: option_res_globalvar.
Hint Rewrite @option_res_globalvar_oplus_none_right: option_res_globalvar.
Hint Rewrite @option_res_globalvar_oplus_some: option_res_globalvar.
Hint Rewrite @option_res_globalvar_oplus_idem: option_res_globalvar.
Hint Rewrite @option_res_globalvar_oplus_error_nil_left: option_res_globalvar.
Hint Rewrite @option_res_globalvar_oplus_error_nil_right: option_res_globalvar.
Hint Rewrite @res_option_globalvar_oplus_none_left: res_option_globalvar.
Hint Rewrite @res_option_globalvar_oplus_none_right: res_option_globalvar.
Hint Rewrite @res_option_globalvar_oplus_idem: res_option_globalvar.
Hint Rewrite @res_option_globalvar_oplus_error_nil_left: res_option_globalvar.
Hint Rewrite @res_option_globalvar_oplus_error_nil_right: res_option_globalvar.
Hint Rewrite @res_option_globalvar_oplus_ok_error: res_option_globalvar.
Hint Rewrite @res_option_globalvar_oplus_error_ok: res_option_globalvar.

Ltac res_globalvar_red :=
  autorewrite with res_globalvar;
  repeat (
      match goal with
          [ |- context [ Error ?v1 ?v2 ] ] ⇒
          let e := fresh "e" in
          let He := fresh "H" e in
          destruct (res_globalvar_oplus_error_left v1 v2) as [e He];
          rewrite He;
          autorewrite with res_globalvar
          | [ |- context [ ?v2 Error ?v1 ] ] ⇒
          let e := fresh "e" in
          let He := fresh "H" e in
          destruct (res_globalvar_oplus_error_right v2 v1) as [e He];
          rewrite He;
          autorewrite with res_globalvar
      end
    ).

Ltac res_option_globalvar_red :=
  autorewrite with res_option_globalvar;
  repeat (
      match goal with
          [ |- context [ Error ?v1 ?v2 ] ] ⇒
          let e := fresh "e" in
          let He := fresh "H" e in
          destruct (res_option_globalvar_oplus_error_left v1 v2) as [e He];
          rewrite He;
          autorewrite with res_option_globalvar
          | [ |- context [ ?v2 Error ?v1 ] ] ⇒
          let e := fresh "e" in
          let He := fresh "H" e in
          destruct (res_option_globalvar_oplus_error_right v2 v1) as [e He];
          rewrite He;
          autorewrite with res_option_globalvar
      end
    ).