(* iris/algebra/lib/mono_list.v *)
From iris.algebra Require Export auth dfrac max_prefix_list
From iris.algebra Require Import updates local_updates proofmode_classes
From iris.prelude Require Import options

Definition mono_listR{SI : sidx} (A : ofe) : cmra := authR (max_prefix_listUR A).

Definition mono_listUR{SI : sidx} (A : ofe) : ucmra := authUR (max_prefix_listUR A).

Definition mono_list_auth{SI : sidx}
    {A : ofe} (q : dfrac) (l : list A) : mono_listR A :=
  ●{q} (to_max_prefix_list l) ⋅ ◯ (to_max_prefix_list l).

Definition mono_list_lb{SI : sidx} {A : ofe} (l : list A) : mono_listR A :=
  ◯ (to_max_prefix_list l).

Global Instance: Params (@mono_list_auth) 3 := {}.

Global Instance: Params (@mono_list_lb) 2 := {}.

Global TypeclassesOpaque mono_list_auth mono_list_lb.

Global Instancemono_list_auth_ne dq : NonExpansive (@mono_list_auth SI A dq).
  Proof. solve_proper. Qed.

Global Instancemono_list_auth_proper dq :
    Proper ((≡) ==> (≡)) (@mono_list_auth SI A dq).
  Proof. solve_proper. Qed.

Global Instancemono_list_lb_ne : NonExpansive (@mono_list_lb SI A).
  Proof. solve_proper. Qed.

Global Instancemono_list_lb_proper : Proper ((≡) ==> (≡)) (@mono_list_lb SI A).
  Proof. solve_proper. Qed.

Global Instancemono_list_lb_dist_inj n :
    Inj (dist n) (dist n) (@mono_list_lb SI A).
  Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.

Global Instancemono_list_lb_inj : Inj (≡) (≡) (@mono_list_lb SI A).
  Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.

Global Instancemono_list_lb_core_id l : CoreId (◯ML l).
  Proof. rewrite /mono_list_lb. apply _. Qed.

Global Instancemono_list_auth_core_id l : CoreId (●ML□ l).
  Proof. rewrite /mono_list_auth. apply _. Qed.

Lemma mono_list_auth_dfrac_opdq1 dq2 l :
    ●ML{dq1 ⋅ dq2} l ≡ ●ML{dq1} l ⋅ ●ML{dq2} l.
  Proof.
    rewrite /mono_list_auth auth_auth_dfrac_op.
    rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
    by rewrite -core_id_dup (comm _ (◯ _)).
  Qed.

Lemma mono_list_lb_op_ll1 l2 : l1 `prefix_of` l2 → ◯ML l1 ⋅ ◯ML l2 ≡ ◯ML l2.
  Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_l. Qed.

Lemma mono_list_lb_op_rl1 l2 : l1 `prefix_of` l2 → ◯ML l2 ⋅ ◯ML l1 ≡ ◯ML l2.
  Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_r. Qed.

Lemma mono_list_auth_lb_opdq l : ●ML{dq} l ≡ ●ML{dq} l ⋅ ◯ML l.
  Proof.
    by rewrite /mono_list_auth /mono_list_lb -!assoc -auth_frag_op -core_id_dup.
  Qed.

Global Instancemono_list_auth_dfrac_is_op dq dq1 dq2 l :
    IsOp dq dq1 dq2 → IsOp' (●ML{dq} l) (●ML{dq1} l) (●ML{dq2} l).
  Proof. rewrite /IsOp' /IsOp=> ->. rewrite mono_list_auth_dfrac_op //. Qed.

Lemma mono_list_auth_dfrac_validNn dq l : ✓{n} (●ML{dq} l) ↔ ✓ dq.
  Proof.
    rewrite /mono_list_auth auth_both_dfrac_validN.
    naive_solver apply to_max_prefix_list_validN.
  Qed.

Lemma mono_list_auth_validNn l : ✓{n} (●ML l).
  Proof. by apply mono_list_auth_dfrac_validN. Qed.

Lemma mono_list_auth_dfrac_validdq l : ✓ (●ML{dq} l) ↔ ✓ dq.
  Proof.
    rewrite /mono_list_auth auth_both_dfrac_valid.
    naive_solver apply to_max_prefix_list_valid.
  Qed.

Lemma mono_list_auth_validl : ✓ (●ML l).
  Proof. by apply mono_list_auth_dfrac_valid. Qed.

Lemma mono_list_auth_dfrac_op_validNn dq1 dq2 l1 l2 :
    ✓{n} (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 ≡{n}≡ l2.
  Proof.
    rewrite /mono_list_auth (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
    rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
    - move=> /cmra_validN_op_l /auth_auth_dfrac_op_validN.
      rewrite (inj_iff to_max_prefix_list). naive_solver.
    - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op auth_both_dfrac_validN.
      naive_solver apply to_max_prefix_list_validN.
  Qed.

Lemma mono_list_auth_op_validNn l1 l2 : ✓{n} (●ML l1 ⋅ ●ML l2) ↔ False.
  Proof. rewrite mono_list_auth_dfrac_op_validN. naive_solver. Qed.

Lemma mono_list_auth_dfrac_op_validdq1 dq2 l1 l2 :
    ✓ (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 ≡ l2.
  Proof.
    rewrite cmra_valid_validN equiv_dist.
    setoid_rewrite mono_list_auth_dfrac_op_validN. pose 0ᵢ. naive_solver.
  Qed.

Lemma mono_list_auth_op_validl1 l2 : ✓ (●ML l1 ⋅ ●ML l2) ↔ False.
  Proof. rewrite mono_list_auth_dfrac_op_valid. naive_solver. Qed.

Lemma mono_list_auth_dfrac_op_valid_L`{!LeibnizEquiv A} dq1 dq2 l1 l2 :
    ✓ (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 = l2.
  Proof. unfold_leibniz. apply mono_list_auth_dfrac_op_valid. Qed.

Lemma mono_list_both_dfrac_validNn dq l1 l2 :
    ✓{n} (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ ∃ l, l1 ≡{n}≡ l2 ++ l.
  Proof.
    rewrite /mono_list_auth /mono_list_lb -assoc
      -auth_frag_op auth_both_dfrac_validN -to_max_prefix_list_includedN.
    f_equiv; split.
    - intros [Hincl _]. etrans; [apply: cmra_includedN_r|done].
    - intros. split; [|by apply to_max_prefix_list_validN].
      rewrite {2}(core_id_dup (to_max_prefix_list l1)). by f_equiv.
  Qed.

Lemma mono_list_both_validNn l1 l2 :
    ✓{n} (●ML l1 ⋅ ◯ML l2) ↔ ∃ l, l1 ≡{n}≡ l2 ++ l.
  Proof. rewrite mono_list_both_dfrac_validN. split; [naive_solver|done]. Qed.

Lemma mono_list_both_dfrac_validdq l1 l2 :
    ✓ (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ ∃ l, l1 ≡ l2 ++ l.
  Proof.
    rewrite /mono_list_auth /mono_list_lb -assoc -auth_frag_op
      auth_both_dfrac_valid -max_prefix_list_included_includedN
      -to_max_prefix_list_included.
    f_equiv; split.
    - intros [Hincl _]. etrans; [apply: cmra_included_r|done].
    - intros. split; [|by apply to_max_prefix_list_valid].
      rewrite {2}(core_id_dup (to_max_prefix_list l1)). by f_equiv.
  Qed.

Lemma mono_list_both_validl1 l2 :
    ✓ (●ML l1 ⋅ ◯ML l2) ↔ ∃ l, l1 ≡ l2 ++ l.
  Proof. rewrite mono_list_both_dfrac_valid. split; [naive_solver|done]. Qed.

Lemma mono_list_both_dfrac_valid_L`{!LeibnizEquiv A} dq l1 l2 :
    ✓ (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ l2 `prefix_of` l1.
  Proof. rewrite /prefix. rewrite mono_list_both_dfrac_valid. naive_solver. Qed.

Lemma mono_list_both_valid_L`{!LeibnizEquiv A} l1 l2 :
    ✓ (●ML l1 ⋅ ◯ML l2) ↔ l2 `prefix_of` l1.
  Proof. rewrite /prefix. rewrite mono_list_both_valid. naive_solver. Qed.

Lemma mono_list_lb_op_validNn l1 l2 :
    ✓{n} (◯ML l1 ⋅ ◯ML l2) ↔ (∃ l, l2 ≡{n}≡ l1 ++ l) ∨ (∃ l, l1 ≡{n}≡ l2 ++ l).
  Proof. by rewrite auth_frag_op_validN to_max_prefix_list_op_validN. Qed.

Lemma mono_list_lb_op_validl1 l2 :
    ✓ (◯ML l1 ⋅ ◯ML l2) ↔ (∃ l, l2 ≡ l1 ++ l) ∨ (∃ l, l1 ≡ l2 ++ l).
  Proof. by rewrite auth_frag_op_valid to_max_prefix_list_op_valid. Qed.

Lemma mono_list_lb_op_valid_L`{!LeibnizEquiv A} l1 l2 :
    ✓ (◯ML l1 ⋅ ◯ML l2) ↔ l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
  Proof. rewrite mono_list_lb_op_valid / prefix. naive_solver. Qed.

Lemma mono_list_lb_op_valid_1_L`{!LeibnizEquiv A} l1 l2 :
    ✓ (◯ML l1 ⋅ ◯ML l2) → l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
  Proof. by apply mono_list_lb_op_valid_L. Qed.

Lemma mono_list_lb_op_valid_2_L`{!LeibnizEquiv A} l1 l2 :
    l1 `prefix_of` l2 ∨ l2 `prefix_of` l1 → ✓ (◯ML l1 ⋅ ◯ML l2).
  Proof. by apply mono_list_lb_op_valid_L. Qed.

Lemma mono_list_lb_monol1 l2 : l1 `prefix_of` l2 → ◯ML l1 ≼ ◯ML l2.
  Proof. intros. exists (◯ML l2). by rewrite mono_list_lb_op_l. Qed.

Lemma mono_list_includeddq l : ◯ML l ≼ ●ML{dq} l.
  Proof. apply cmra_included_r. Qed.

Lemma mono_list_update{l1} l2 : l1 `prefix_of` l2 → ●ML l1 ~~> ●ML l2.
  Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed.

Lemma mono_list_auth_persistdq l : ●ML{dq} l ~~> ●ML□ l.
  Proof.
    rewrite /mono_list_auth. apply cmra_update_op; [|done].
    by apply auth_update_auth_persist.
  Qed.

Lemma mono_list_auth_unpersistl :
    ●ML□ l ~~>: λ k, ∃ q, k = ●ML{#q} l.
  Proof. eapply auth_updateP_both_unpersist. Qed.

Definition mono_listURF{SI : sidx} (F : oFunctor) : urFunctor :=
  authURF (max_prefix_listURF F).

Global Instancemono_listURF_contractive {SI : sidx} F :
  oFunctorContractive F → urFunctorContractive (mono_listURF F).
Proof. apply _. Qed.

Definition mono_listRF{SI : sidx} (F : oFunctor) : rFunctor :=
  authRF (max_prefix_listURF F).

Global Instancemono_listRF_contractive {SI : sidx} F :
  oFunctorContractive F → rFunctorContractive (mono_listRF F).
Proof. apply _. Qed.