(* iris/algebra/updates.v *)
From iris.algebra Require Export cmra
From iris.prelude Require Import options

Definition cmra_updateP{SI : sidx} {A : cmra} (x : A) (P : A → Prop) := ∀ n mz,
  ✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).

Global Instance: Params (@cmra_updateP) 1 := {}.
Infix "~~>:" := cmra_updateP (at level 70).

Definition cmra_update{SI : sidx} {A : cmra} (x y : A) := ∀ n mz,
  ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz).
Infix "~~>" := cmra_update (at level 70).

Global Instance: Params (@cmra_update) 1 := {}.

Global Instancecmra_updateP_proper :
  Proper ((≡) ==> pointwise_relation _ iff ==> iff) (@cmra_updateP SI A).
Proof.
  rewrite /pointwise_relation /cmra_updateP=> x x' Hx P P' HP;
    split=> ? n mz; setoid_subst; naive_solver.
Qed.

Global Instancecmra_update_proper :
  Proper ((≡) ==> (≡) ==> iff) (@cmra_update SI A).
Proof.
  rewrite /cmra_update=> x x' Hx y y' Hy; split=> ? n mz ?; setoid_subst; auto.
Qed.

Lemma cmra_update_updatePx y : x ~~> y ↔ x ~~>: (y =.).
Proof. split=> Hup n z ?; eauto. destruct (Hup n z) as (?&<-&?); auto. Qed.

Lemma cmra_updateP_id(P : A → Prop) x : P x → x ~~>: P.
Proof. intros ? n mz ?; eauto. Qed.

Lemma cmra_updateP_compose(P Q : A → Prop) x :
  x ~~>: P → (∀ y, P y → y ~~>: Q) → x ~~>: Q.
Proof. intros Hx Hy n mz ?. destruct (Hx n mz) as (y&?&?); naive_solver. Qed.

Lemma cmra_updateP_compose_l(Q : A → Prop) x y : x ~~> y → y ~~>: Q → x ~~>: Q.
Proof.
  rewrite cmra_update_updateP.
  intros; apply cmra_updateP_compose with (y =.); naive_solver.
Qed.

Lemma cmra_updateP_weaken(P Q : A → Prop) x :
  x ~~>: P → (∀ y, P y → Q y) → x ~~>: Q.
Proof. eauto using cmra_updateP_compose, cmra_updateP_id. Qed.

Lemma cmra_update_exclusive`{!Exclusive x} y:
  ✓ y → x ~~> y.
Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.

Global Instancecmra_update_rewrite_relation :
  RewriteRelation (@cmra_update SI A) | 170 := {}.

Global Instancecmra_update_preorder : PreOrder (@cmra_update SI A).
Proof.
  split.
  - intros x. by apply cmra_update_updateP, cmra_updateP_id.
  - intros x y z. rewrite !cmra_update_updateP.
    eauto using cmra_updateP_compose with subst.
Qed.

Global Instancecmra_update_proper_update :
  Proper (flip cmra_update ==> cmra_update ==> impl) (@cmra_update SI A).
Proof.
  intros x1 x2 Hx y1 y2 Hy ?. etrans; [apply Hx|]. by etrans; [|apply Hy].
Qed.

Global Instancecmra_update_flip_proper_update :
  Proper (cmra_update ==> flip cmra_update ==> flip impl) (@cmra_update SI A).
Proof.
  intros x1 x2 Hx y1 y2 Hy ?. etrans; [apply Hx|]. by etrans; [|apply Hy].
Qed.

Lemma cmra_updateP_op(P1 P2 Q : A → Prop) x1 x2 :
  x1 ~~>: P1 → x2 ~~>: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) →
  x1 ⋅ x2 ~~>: Q.
Proof.
  intros Hx1 Hx2 Hy n mz ?.
  destruct (Hx1 n (Some (x2 ⋅? mz))) as (y1&?&?).
  { by rewrite /= -cmra_op_opM_assoc. }
  destruct (Hx2 n (Some (y1 ⋅? mz))) as (y2&?&?).
  { by rewrite /= -cmra_op_opM_assoc (comm _ x2) cmra_op_opM_assoc. }
  exists (y1 ⋅ y2); split; last rewrite (comm _ y1) cmra_op_opM_assoc; auto.
Qed.

Lemma cmra_updateP_op'(P1 P2 : A → Prop) x1 x2 :
  x1 ~~>: P1 → x2 ~~>: P2 →
  x1 ⋅ x2 ~~>: λ y, ∃ y1 y2, y = y1 ⋅ y2 ∧ P1 y1 ∧ P2 y2.
Proof. eauto 10 using cmra_updateP_op. Qed.

Lemma cmra_update_opx1 x2 y1 y2 : x1 ~~> y1 → x2 ~~> y2 → x1 ⋅ x2 ~~> y1 ⋅ y2.
Proof.
  rewrite !cmra_update_updateP; eauto using cmra_updateP_op with congruence.
Qed.

Global Instancecmra_update_op_proper :
  Proper (cmra_update ==> cmra_update ==> cmra_update) (op (A:=A)).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_update_op. Qed.

Global Instancecmra_update_op_flip_proper :
  Proper (flip cmra_update ==> flip cmra_update ==> flip cmra_update) (op (A:=A)).
Proof. intros x1 x2 Hx y1 y2 Hy. by apply cmra_update_op. Qed.

Lemma cmra_update_op_lx y : x ⋅ y ~~> x.
Proof. intros n mz. rewrite comm cmra_op_opM_assoc. apply cmra_validN_op_r. Qed.

Lemma cmra_update_op_rx y : x ⋅ y ~~> y.
Proof. rewrite comm. apply cmra_update_op_l. Qed.

Lemma cmra_update_includedx y : x ≼ y → y ~~> x.
Proof. intros [z ->]. apply cmra_update_op_l. Qed.

Lemma cmra_update_valid0x y : (✓{0ᵢ} x → x ~~> y) → x ~~> y.
Proof.
  intros H n mz Hmz. apply H, Hmz.
  apply (cmra_validN_le n), SIdx.le_0_l.
  destruct mz.
  - eapply cmra_validN_op_l, Hmz.
  - apply Hmz.
Qed.

Lemma cmra_total_updateP`{!CmraTotal A} x (P : A → Prop) :
  x ~~>: P ↔ ∀ n z, ✓{n} (x ⋅ z) → ∃ y, P y ∧ ✓{n} (y ⋅ z).
Proof.
  split=> Hup; [intros n z; apply (Hup n (Some z))|].
  intros n [z|] ?; simpl; [by apply Hup|].
  destruct (Hup n (core x)) as (y&?&?); first by rewrite cmra_core_r.
  eauto using cmra_validN_op_l.
Qed.

Lemma cmra_total_update`{!CmraTotal A} x y :
   x ~~> y ↔ ∀ n z, ✓{n} (x ⋅ z) → ✓{n} (y ⋅ z).
Proof. rewrite cmra_update_updateP cmra_total_updateP. naive_solver. Qed.

Lemma cmra_discrete_updateP`{!CmraDiscrete A} (x : A) (P : A → Prop) :
  x ~~>: P ↔ ∀ mz, ✓ (x ⋅? mz) → ∃ y, P y ∧ ✓ (y ⋅? mz).
Proof.
  unfold cmra_updateP. setoid_rewrite <-cmra_discrete_valid_iff.
  pose 0ᵢ. naive_solver.
Qed.

Lemma cmra_discrete_update`{!CmraDiscrete A} (x y : A) :
  x ~~> y ↔ ∀ mz, ✓ (x ⋅? mz) → ✓ (y ⋅? mz).
Proof.
  unfold cmra_update. setoid_rewrite <-cmra_discrete_valid_iff.
  pose 0ᵢ. naive_solver.
Qed.

Lemma cmra_discrete_total_updateP`{!CmraDiscrete A, !CmraTotal A}
    (x : A) (P : A → Prop) :
  x ~~>: P ↔ ∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z).
Proof.
  rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff.
  pose 0ᵢ. naive_solver.
Qed.

Lemma cmra_discrete_total_update`{!CmraDiscrete A, !CmraTotal A} (x y : A) :
  x ~~> y ↔ ∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z).
Proof.
  rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff.
  pose 0ᵢ. naive_solver.
Qed.

Notation T:= (cmra_transport H).

Lemma cmra_transport_updateP(P : A → Prop) (Q : B → Prop) x :
    x ~~>: P → (∀ y, P y → Q (T y)) → T x ~~>: Q.
  Proof. destruct H; eauto using cmra_updateP_weaken. Qed.

Lemma cmra_transport_updateP'(P : A → Prop) x :
    x ~~>: P → T x ~~>: λ y, ∃ y', y = cmra_transport H y' ∧ P y'.
  Proof. eauto using cmra_transport_updateP. Qed.

Lemma iso_cmra_updateP(P : B → Prop) (Q : A → Prop) y
      (gf : ∀ x, g (f x) ≡ x)
      (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
      (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
    y ~~>: P →
    (∀ y', P y' → Q (g y')) →
    g y ~~>: Q.
  Proof.
    intros Hup Hx n mz Hmz.
    destruct (Hup n (f <$> mz)) as (y'&HPy'&Hy'%g_validN).
    { apply g_validN. destruct mz as [z|]; simpl in *; [|done].
      by rewrite g_op gf. }
    exists (g y'); split; [by eauto|].
    destruct mz as [z|]; simpl in *; [|done].
    revert Hy'. by rewrite g_op gf.
  Qed.

Lemma iso_cmra_updateP'(P : B → Prop) y
      (gf : ∀ x, g (f x) ≡ x)
      (g_op : ∀ y1 y2, g (y1 ⋅ y2) ≡ g y1 ⋅ g y2)
      (g_validN : ∀ n y, ✓{n} (g y) ↔ ✓{n} y) :
    y ~~>: P →
    g y ~~>: λ x, ∃ y, x = g y ∧ P y.
  Proof. eauto using iso_cmra_updateP. Qed.

Lemma cmra_update_lift_updateP(f : B → A) b b' :
    (∀ P, b ~~>: P → f b ~~>: λ a', ∃ b', a' = f b' ∧ P b') →
    b ~~> b' →
    f b ~~> f b'.
  Proof.
    intros Hgen Hupd.
    eapply cmra_update_updateP, cmra_updateP_weaken.
    { eapply Hgen, cmra_update_updateP, Hupd. }
    naive_solver.
  Qed.

Lemma prod_updatePP1 P2 (Q : A * B → Prop) x :
    x.1 ~~>: P1 → x.2 ~~>: P2 → (∀ a b, P1 a → P2 b → Q (a,b)) → x ~~>: Q.
  Proof.
    intros Hx1 Hx2 HP n mz [??]; simpl in *.
    destruct (Hx1 n (fst <$> mz)) as (a&?&?); first by destruct mz.
    destruct (Hx2 n (snd <$> mz)) as (b&?&?); first by destruct mz.
    exists (a,b); repeat split; destruct mz; auto.
  Qed.

Lemma prod_updateP'P1 P2 x :
    x.1 ~~>: P1 → x.2 ~~>: P2 → x ~~>: λ y, P1 (y.1) ∧ P2 (y.2).
  Proof. eauto using prod_updateP. Qed.

Lemma prod_updatex y : x.1 ~~> y.1 → x.2 ~~> y.2 → x ~~> y.
  Proof.
    rewrite !cmra_update_updateP.
    destruct x, y; eauto using prod_updateP with subst.
  Qed.

Lemma option_updateP(P : A → Prop) (Q : option A → Prop) x :
    x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
  Proof.
    intros Hx Hy; apply cmra_total_updateP=> n [y|] ?.
    { destruct (Hx n (Some y)) as (y'&?&?); auto. exists (Some y'); auto. }
    destruct (Hx n None) as (y'&?&?); rewrite ?cmra_core_r; auto.
    by exists (Some y'); auto.
  Qed.

Lemma option_updateP'(P : A → Prop) x :
    x ~~>: P → Some x ~~>: from_option P False.
  Proof. eauto using option_updateP. Qed.

Lemma option_updatex y : x ~~> y → Some x ~~> Some y.
  Proof. rewrite !cmra_update_updateP; eauto using option_updateP with subst. Qed.