Auth_mnat.v 2.79 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
From iris Require Export  algebra.auth  base_logic.lib.own  proofmode.tactics.



Notation "'●mnat' n" := (Auth (A:=mnat) (Excl' n%nat) ε) (at level 20).
Notation "'◯mnat' n" := (Auth (A:=mnat) None n%nat) (at level 20).

Section Auth_mnat.

  Context `{inG Σ (authR mnatUR)}.

12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
  Lemma auth_mnat_alloc (n : mnat) :
    (|==>  γ, own γ (mnat n)  own γ (mnat n))%I.
  Proof.
    by iMod (own_alloc (mnat n  mnat n)) as (γ) "[? ?]" ; auto with iFrame.
  Qed.
  Global Arguments auth_mnat_alloc _%nat.

  Lemma own_auth_mnat_le (γ : gname) (m n : mnat) :
    own γ (mnat m) -
    own γ (mnat n) -
    (n  m)%nat.
  Proof.
    iIntros "H● H◯".
    iDestruct (own_valid_2 with "H● H◯") as % [[k ->] _] % auth_valid_discrete_2.
    iPureIntro. apply Max.le_max_l.
  Qed.

  Lemma own_auth_mnat_weaken (γ : gname) (n n : mnat) :
    (n  n)%nat 
    own γ (mnat n) -
    own γ (mnat n).
  Proof.
    iIntros (I) "H".
    rewrite (_ : n = n `max` n)%nat ; last (by rewrite max_l).
    iDestruct "H" as "[_$]".
  Qed.
  Global Arguments own_auth_mnat_weaken _ (_ _ _)%nat_scope.

40 41 42 43
  Lemma own_auth_mnat_null (γ : gname) (m : mnat) :
    own γ (mnat m) -
    own γ (mnat m)  own γ (mnat 0).
  Proof.
44
    by rewrite - own_op.
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
  Qed.
  Global Arguments own_auth_mnat_null _ _%nat_scope.

  Lemma auth_mnat_update_read_auth (γ : gname) (m : mnat) :
    own γ (mnat m) -
    |==> own γ (mnat m)  own γ (mnat m).
  Proof.
    iIntros "H●".
    iDestruct (own_auth_mnat_null with "H●") as "[H● H◯]".
    (iMod (own_update_2 with "H● H◯") as "[$ $]" ; last done).
    apply auth_update, mnat_local_update. lia.
  Qed.
  Global Arguments auth_mnat_update_read_auth _ _%nat_scope.

  Lemma auth_mnat_update_incr (γ : gname) (m k : mnat) :
    own γ (mnat m) -
    |==> own γ (mnat (m + k : mnat)).
  Proof.
    iIntros "H●". iDestruct (own_auth_mnat_null with "H●") as "[H● H◯]".
    iMod (own_update_2 with "H● H◯") as "[$ _]" ; last done.
    apply auth_update, mnat_local_update. lia.
  Qed.
  Global Arguments auth_mnat_update_incr _ (_ _)%nat_scope.

69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
  Lemma auth_mnat_update_incr' (γ : gname) (m n k : mnat) :
    own γ (mnat m) -
    own γ (mnat n) -
    |==> own γ (mnat (m + k : mnat))  own γ (mnat (n + k : mnat)).
  Proof.
    iIntros "H● H◯".
    iDestruct (own_auth_mnat_le with "H● H◯") as %I. iClear "H◯".
    iDestruct (auth_mnat_update_incr _ _ k with "H●") as ">H●".
    iDestruct (auth_mnat_update_read_auth with "H●") as ">[$ H◯]".
    iModIntro.
    rewrite (_ : m + k = (n + k) `max` (m + k))%nat ; last lia.
    iDestruct "H◯" as "[$ _]".
  Qed.
  Global Arguments auth_mnat_update_incr' _ (_ _ _)%nat_scope.

84
End Auth_mnat.