Auth_mnat.v 2.86 KB
Newer Older
MEVEL Glen's avatar
MEVEL Glen committed
1 2
From iris Require Export  algebra.auth.
From iris Require Import  algebra.excl  base_logic.lib.own  proofmode.tactics.
MEVEL Glen's avatar
MEVEL Glen committed
3 4 5



6 7
Notation "'●mnat' n" := (auth_auth (A:=mnatUR) 1%Qp n%nat) (at level 20).
Notation "'◯mnat' n" := (auth_frag (A:=mnatUR) n%nat) (at level 20).
MEVEL Glen's avatar
MEVEL Glen committed
8 9 10 11 12

Section Auth_mnat.

  Context `{inG Σ (authR mnatUR)}.

13
  Lemma auth_mnat_alloc (n : mnat) :
14
     |==>  γ, own γ (mnat n)  own γ (mnat n).
15
  Proof.
16 17 18
    iMod (own_alloc (mnat n  mnat n)) as (γ) "[? ?]".
    - by apply auth_both_valid_2.
    - by auto with iFrame.
19 20 21 22 23 24 25 26 27
  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◯".
28
    iDestruct (own_valid_2 with "H● H◯") as % [[k ->] _] % auth_both_valid.
29 30 31 32 33 34 35 36 37 38 39 40 41 42
    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.

MEVEL Glen's avatar
MEVEL Glen committed
43 44 45 46
  Lemma own_auth_mnat_null (γ : gname) (m : mnat) :
    own γ (mnat m) -
    own γ (mnat m)  own γ (mnat 0).
  Proof.
47
    by rewrite - own_op.
MEVEL Glen's avatar
MEVEL Glen committed
48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
  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.

72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
  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.

87
End Auth_mnat.