(* iris_unstable/base_logic/mono_list.v *)
From iris.proofmode Require Import proofmode
From iris.algebra.lib Require Import mono_list
From iris.bi.lib Require Import fractional
From iris.base_logic.lib Require Export own
From iris.prelude Require Import options

Class mono_listG(A : Type) Σ :=
  MonoListG { #[local] mono_list_inG :: inG Σ (mono_listR (leibnizO A)) }.

Definition mono_listΣ(A : Type) : gFunctors :=
  #[GFunctor (mono_listR (leibnizO A))].

Global InstancesubG_mono_listΣ {A Σ} :
  subG (mono_listΣ A) Σ → (mono_listG A) Σ.
Proof. solve_inG. Qed.

Local Definitionmono_list_auth_own_def `{!mono_listG A Σ}
    (γ : gname) (q : Qp) (l : list A) : iProp Σ :=
  own γ (●ML{#q} (l : listO (leibnizO A))).

Local Definitionmono_list_auth_own_aux : seal (@mono_list_auth_own_def).
Proof. by eexists. Qed.

Definition mono_list_auth_own:= mono_list_auth_own_aux.(unseal).

Local Definitionmono_list_auth_own_unseal :
  @mono_list_auth_own = @mono_list_auth_own_def := mono_list_auth_own_aux.(seal_eq).

Global Argumentsmono_list_auth_own {A Σ _} γ q l.

Local Definitionmono_list_lb_own_def `{!mono_listG A Σ}
    (γ : gname) (l : list A) : iProp Σ :=
  own γ (◯ML (l : listO (leibnizO A))).

Local Definitionmono_list_lb_own_aux : seal (@mono_list_lb_own_def).
Proof. by eexists. Qed.

Definition mono_list_lb_own:= mono_list_lb_own_aux.(unseal).

Local Definitionmono_list_lb_own_unseal :
  @mono_list_lb_own = @mono_list_lb_own_def := mono_list_lb_own_aux.(seal_eq).

Global Argumentsmono_list_lb_own {A Σ _} γ l.

Definition mono_list_idx_own`{!mono_listG A Σ}
    (γ : gname) (i : nat) (a : A) : iProp Σ :=
  ∃ l : list A, ⌜ l !! i = Some a ⌝ ∗ mono_list_lb_own γ l.

Local Ltacunseal := rewrite
  /mono_list_idx_own ?mono_list_auth_own_unseal /mono_list_auth_own_def
  ?mono_list_lb_own_unseal /mono_list_lb_own_def.

Global Instancemono_list_auth_own_timeless γ q l : Timeless (mono_list_auth_own γ q l).
  Proof. unseal. apply _. Qed.

Global Instancemono_list_lb_own_timeless γ l : Timeless (mono_list_lb_own γ l).
  Proof. unseal. apply _. Qed.

Global Instancemono_list_lb_own_persistent γ l : Persistent (mono_list_lb_own γ l).
  Proof. unseal. apply _. Qed.

Global Instancemono_list_idx_own_timeless γ i a :
    Timeless (mono_list_idx_own γ i a) := _.

Global Instancemono_list_idx_own_persistent γ i a :
    Persistent (mono_list_idx_own γ i a) := _.

Global Instancemono_list_auth_own_fractional γ l :
    Fractional (λ q, mono_list_auth_own γ q l).
  Proof. unseal. intros p q. by rewrite -own_op -mono_list_auth_dfrac_op. Qed.

Global Instancemono_list_auth_own_as_fractional γ q l :
    AsFractional (mono_list_auth_own γ q l) (λ q, mono_list_auth_own γ q l) q.
  Proof. split; [auto|apply _]. Qed.

Lemma mono_list_auth_own_agreeγ q1 q2 l1 l2 :
    mono_list_auth_own γ q1 l1 -∗
    mono_list_auth_own γ q2 l2 -∗
    ⌜(q1 + q2 ≤ 1)%Qp ∧ l1 = l2⌝.
  Proof.
    unseal. iIntros "H1 H2".
    by iCombine "H1 H2" gives %?%mono_list_auth_dfrac_op_valid_L.
  Qed.

Lemma mono_list_auth_own_exclusiveγ l1 l2 :
    mono_list_auth_own γ 1 l1 -∗ mono_list_auth_own γ 1 l2 -∗ False.
  Proof.
    iIntros "H1 H2".
    iDestruct (mono_list_auth_own_agree with "H1 H2") as %[]; done.
  Qed.

Lemma mono_list_auth_lb_validγ q l1 l2 :
    mono_list_auth_own γ q l1 -∗
    mono_list_lb_own γ l2 -∗
    ⌜ (q ≤ 1)%Qp ∧ l2 `prefix_of` l1 ⌝.
  Proof.
    unseal. iIntros "Hauth Hlb".
    by iCombine "Hauth Hlb" gives %?%mono_list_both_dfrac_valid_L.
  Qed.

Lemma mono_list_lb_validγ l1 l2 :
    mono_list_lb_own γ l1 -∗
    mono_list_lb_own γ l2 -∗
    ⌜ l1 `prefix_of` l2 ∨ l2 `prefix_of` l1 ⌝.
  Proof.
    unseal. iIntros "H1 H2".
    by iCombine "H1 H2" gives %?%mono_list_lb_op_valid_L.
  Qed.

Lemma mono_list_idx_agreeγ i a1 a2 :
    mono_list_idx_own γ i a1 -∗ mono_list_idx_own γ i a2 -∗ ⌜ a1 = a2 ⌝.
  Proof.
    iDestruct 1 as (l1 Hl1) "H1". iDestruct 1 as (l2 Hl2) "H2".
    iDestruct (mono_list_lb_valid with "H1 H2") as %Hpre.
    iPureIntro.
    destruct Hpre as [Hpre|Hpre]; eapply prefix_lookup_Some in Hpre; eauto; congruence.
  Qed.

Lemma mono_list_auth_idx_lookupγ q l i a :
    mono_list_auth_own γ q l -∗ mono_list_idx_own γ i a -∗ ⌜ l !! i = Some a ⌝.
  Proof.
    iIntros "Hauth". iDestruct 1 as (l1 Hl1) "Hl1".
    iDestruct (mono_list_auth_lb_valid with "Hauth Hl1") as %[_ Hpre].
    iPureIntro.
    eapply prefix_lookup_Some in Hpre; eauto; congruence.
  Qed.

Lemma mono_list_lb_own_getγ q l :
    mono_list_auth_own γ q l ⊢ mono_list_lb_own γ l.
  Proof. intros. unseal. by apply own_mono, mono_list_included. Qed.

Lemma mono_list_lb_own_le{γ l} l' :
    l' `prefix_of` l →
    mono_list_lb_own γ l ⊢ mono_list_lb_own γ l'.
  Proof. unseal. intros. by apply own_mono, mono_list_lb_mono. Qed.

Lemma mono_list_idx_own_get{γ l} i a :
    l !! i = Some a →
    mono_list_lb_own γ l -∗ mono_list_idx_own γ i a.
  Proof. iIntros (Hli) "Hl". iExists l. by iFrame. Qed.

Lemma mono_list_own_allocl :
    ⊢ |==> ∃ γ, mono_list_auth_own γ 1 l ∗ mono_list_lb_own γ l.
  Proof.
    unseal. setoid_rewrite <- own_op. by apply own_alloc, mono_list_both_valid_L.
  Qed.

Lemma mono_list_auth_own_update{γ l} l' :
    l `prefix_of` l' →
    mono_list_auth_own γ 1 l ==∗ mono_list_auth_own γ 1 l' ∗ mono_list_lb_own γ l'.
  Proof.
    iIntros (?) "Hauth".
    iAssert (mono_list_auth_own γ 1 l') with "[> Hauth]" as "Hauth".
    { unseal. iApply (own_update with "Hauth"). by apply mono_list_update. }
    iModIntro. iSplit; [done|]. by iApply mono_list_lb_own_get.
  Qed.

Lemma mono_list_auth_own_update_app{γ l} l' :
    mono_list_auth_own γ 1 l ==∗
    mono_list_auth_own γ 1 (l ++ l') ∗ mono_list_lb_own γ (l ++ l').
  Proof. by apply mono_list_auth_own_update, prefix_app_r. Qed.