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

Class mono_natGΣ :=
  MonoNatG { #[local] mono_natG_inG :: inG Σ mono_natR; }.

Definition mono_natΣ: gFunctors := #[ GFunctor mono_natR ].

Global InstancesubG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
Proof. solve_inG. Qed.

Local Definitionmono_nat_auth_own_def `{!mono_natG Σ}
    (γ : gname) (q : Qp) (n : nat) : iProp Σ :=
  own γ (●MN{#q} n).

Local Definitionmono_nat_auth_own_aux : seal (@mono_nat_auth_own_def).
Proof. by eexists. Qed.

Definition mono_nat_auth_own:= mono_nat_auth_own_aux.(unseal).

Local Definitionmono_nat_auth_own_unseal :
  @mono_nat_auth_own = @mono_nat_auth_own_def := mono_nat_auth_own_aux.(seal_eq).

Global Argumentsmono_nat_auth_own {Σ _} γ q n.

Local Definitionmono_nat_lb_own_def `{!mono_natG Σ} (γ : gname) (n : nat): iProp Σ :=
  own γ (◯MN n).

Local Definitionmono_nat_lb_own_aux : seal (@mono_nat_lb_own_def). Proof. by eexists. Qed.

Definition mono_nat_lb_own:= mono_nat_lb_own_aux.(unseal).

Local Definitionmono_nat_lb_own_unseal :
  @mono_nat_lb_own = @mono_nat_lb_own_def := mono_nat_lb_own_aux.(seal_eq).

Global Argumentsmono_nat_lb_own {Σ _} γ n.

Local Ltacunseal := rewrite
  ?mono_nat_auth_own_unseal /mono_nat_auth_own_def
  ?mono_nat_lb_own_unseal /mono_nat_lb_own_def.

Global Instancemono_nat_auth_own_timeless γ q n : Timeless (mono_nat_auth_own γ q n).
  Proof. unseal. apply _. Qed.

Global Instancemono_nat_lb_own_timeless γ n : Timeless (mono_nat_lb_own γ n).
  Proof. unseal. apply _. Qed.

Global Instancemono_nat_lb_own_persistent γ n : Persistent (mono_nat_lb_own γ n).
  Proof. unseal. apply _. Qed.

Global Instancemono_nat_auth_own_fractional γ n :
    Fractional (λ q, mono_nat_auth_own γ q n).
  Proof. unseal. intros p q. rewrite -own_op -mono_nat_auth_dfrac_op //. Qed.

Global Instancemono_nat_auth_own_as_fractional γ q n :
    AsFractional (mono_nat_auth_own γ q n) (λ q, mono_nat_auth_own γ q n) q.
  Proof. split; [auto|apply _]. Qed.

Lemma mono_nat_auth_own_agreeγ q1 q2 n1 n2 :
    mono_nat_auth_own γ q1 n1 -∗
    mono_nat_auth_own γ q2 n2 -∗
    ⌜(q1 + q2 ≤ 1)%Qp ∧ n1 = n2⌝.
  Proof.
    unseal. iIntros "H1 H2".
    iCombine "H1 H2" gives %?%mono_nat_auth_dfrac_op_valid; done.
  Qed.

Lemma mono_nat_auth_own_exclusiveγ n1 n2 :
    mono_nat_auth_own γ 1 n1 -∗ mono_nat_auth_own γ 1 n2 -∗ False.
  Proof.
    iIntros "H1 H2".
    by iDestruct (mono_nat_auth_own_agree with "H1 H2") as %[[] _].
  Qed.

Lemma mono_nat_lb_own_validγ q n m :
    mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ m -∗ ⌜(q ≤ 1)%Qp ∧ m ≤ n⌝.
  Proof.
    unseal. iIntros "Hauth Hlb".
    iCombine "Hauth Hlb" gives %Hvalid%mono_nat_both_dfrac_valid.
    auto.
  Qed.

Lemma mono_nat_lb_own_getγ q n :
    mono_nat_auth_own γ q n -∗ mono_nat_lb_own γ n.
  Proof. unseal. iApply own_mono. apply mono_nat_included. Qed.

Lemma mono_nat_lb_own_le{γ n} n' :
    n' ≤ n →
    mono_nat_lb_own γ n -∗ mono_nat_lb_own γ n'.
  Proof. unseal. intros. iApply own_mono. by apply mono_nat_lb_mono. Qed.

Lemma mono_nat_lb_own_0γ :
    ⊢ |==> mono_nat_lb_own γ 0.
  Proof. unseal. iApply own_unit. Qed.

Lemma mono_nat_own_alloc_strongP n :
    pred_infinite P →
    ⊢ |==> ∃ γ, ⌜P γ⌝ ∗ mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
  Proof.
    unseal. intros.
    iMod (own_alloc_strong (●MN n ⋅ ◯MN n) P) as (γ) "[% [??]]"; first done.
    { apply mono_nat_both_valid; auto. }
    auto with iFrame.
  Qed.

Lemma mono_nat_own_allocn :
    ⊢ |==> ∃ γ, mono_nat_auth_own γ 1 n ∗ mono_nat_lb_own γ n.
  Proof.
    iMod (mono_nat_own_alloc_strong (λ _, True) n) as (γ) "[_ ?]".
    - by apply pred_infinite_True.
    - eauto.
  Qed.

Lemma mono_nat_own_update{γ n} n' :
    n ≤ n' →
    mono_nat_auth_own γ 1 n ==∗ mono_nat_auth_own γ 1 n' ∗ mono_nat_lb_own γ n'.
  Proof.
    iIntros (?) "Hauth".
    iAssert (mono_nat_auth_own γ 1 n') with "[> Hauth]" as "Hauth".
    { unseal. iApply (own_update with "Hauth"). by apply mono_nat_update. }
    iModIntro. iSplit; [done|]. by iApply mono_nat_lb_own_get.
  Qed.