From iris.algebra Require Export cmra.

Record local_update {A : cmraT} (mz : option A) (x y : A) := {
  local_update_valid n : ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz);
  local_update_go n mz' :
    ✓{n} (x ⋅? mz) → x ⋅? mz ≡{n}≡ x ⋅? mz' → y ⋅? mz ≡{n}≡ y ⋅? mz'
}.
Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
Instance: Params (@local_update) 1.

Section updates.
Context {A : cmraT}.
Implicit Types x y : A.

Global Instance local_update_proper :
  Proper ((≡) ==> (≡) ==> (≡) ==> iff) (@local_update A).
Proof.
  cut (Proper ((≡) ==> (≡) ==> (≡) ==> impl) (@local_update A)).
  { intros Hproper; split; by apply Hproper. }
  intros mz mz' Hmz x x' Hx y y' Hy [Hv Hup]; constructor; setoid_subst; auto.
Qed.

Global Instance local_update_preorder mz : PreOrder (@local_update A mz).
Proof.
  split.
  - intros x; by split.
  - intros x1 x2 x3 [??] [??]; split; eauto.
Qed.

Lemma exclusive_local_update `{!Exclusive x} y mz : ✓ y → x ¬l~> y @ mz.
Proof.
  split; intros n.
  - move⇒ /exclusiveN_opM →. by apply cmra_valid_validN.
  - intros mz' ? Hmz.
    by rewrite (exclusiveN_opM n x mz) // (exclusiveN_opM n x mz') -?Hmz.
Qed.

Lemma op_local_update x1 x2 y mz :
  x1 ¬l~> x2 @ Some (y ⋅? mz) → x1 ⋅ y ¬l~> x2 ⋅ y @ mz.
Proof.
  intros [Hv1 H1]; split.
  - intros n. rewrite !cmra_opM_assoc. move⇒ /Hv1 /=; auto.
  - intros n mz'. rewrite !cmra_opM_assoc. move⇒ Hv /(H1 _ (Some _) Hv) /=; auto.
Qed.

Lemma alloc_local_update x y mz :
  (∀ n, ✓{n} (x ⋅? mz) → ✓{n} (x ⋅ y ⋅? mz)) → x ¬l~> x ⋅ y @ mz.
Proof.
  split; first done.
  intros n mz' _. by rewrite !(comm _ x) !cmra_opM_assoc⇒ →.
Qed.

Lemma local_update_total `{CMRADiscrete A} x y mz :
  x ¬l~> y @ mz ↔
    (✓ (x ⋅? mz) → ✓ (y ⋅? mz)) ∧
    (∀ mz', ✓ (x ⋅? mz) → x ⋅? mz ≡ x ⋅? mz' → y ⋅? mz ≡ y ⋅? mz').
Proof.
  split.
  - destruct 1. split; intros until 0;
      rewrite !(cmra_discrete_valid_iff 0) ?(timeless_iff 0); auto.
  - intros [??]; split; intros until 0;
      rewrite -!cmra_discrete_valid_iff -?timeless_iff; auto.
Qed.
End updates.

Lemma prod_local_update {A B : cmraT} (x y : A × B) mz :
  x.1 ¬l~> y.1 @ fst <$> mz → x.2 ¬l~> y.2 @ snd <$> mz →
  x ¬l~> y @ mz.
Proof.
  intros [Hv1 H1] [Hv2 H2]; split.
  - intros n [??]; destruct mz; split; auto.
  - intros n mz' [??] [??].
    specialize (H1 n (fst <$> mz')); specialize (H2 n (snd <$> mz')).
    destruct mz, mz'; split; naive_solver.
Qed.

Lemma option_local_update {A : cmraT} (x y : A) mmz :
  x ¬l~> y @ mjoin mmz →
  Some x ¬l~> Some y @ mmz.
Proof.
  intros [Hv H]; split; first destruct mmz as [[?|]|]; auto.
  intros n mmz'. specialize (H n (mjoin mmz')).
  destruct mmz as [[]|], mmz' as [[]|]; inversion_clear 2; constructor; auto.
Qed.

Lemma nat_local_update (x y : nat) mz : x ¬l~> y @ mz.
Proof.
  split; first done.
  compute -[plus]; destruct mz as [z|]; intros n [z'|]; lia.
Qed.

Lemma mnat_local_update (x y : mnat) mz : x ≤ y → x ¬l~> y @ mz.
Proof.
  split; first done.
  compute -[max]; destruct mz as [z|]; intros n [z'|]; lia.
Qed.