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



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

Section Auth_nat.

  Context `{inG Σ (authR natUR)}.

  Lemma auth_nat_alloc (n : nat) :
14
     |==>  γ, own γ (nat n)  own γ (nat n).
MEVEL Glen's avatar
MEVEL Glen committed
15
  Proof.
16 17 18
    iMod (own_alloc (nat n  nat n)) as (γ) "[? ?]".
    - by apply auth_both_valid_2.
    - by auto with iFrame.
MEVEL Glen's avatar
MEVEL Glen committed
19 20 21 22 23 24 25 26 27
  Qed.

  Lemma own_auth_nat_le (γ : gname) (m n : nat) :
    own γ (nat m) -
    own γ (nat n) -
    (n  m)%nat.
  Proof.
    iIntros "H● H◯".
    by iDestruct (own_valid_2 with "H● H◯")
28
      as % [?%nat_le_sum _] % auth_both_valid.
MEVEL Glen's avatar
MEVEL Glen committed
29 30
  Qed.

31 32 33 34 35 36 37 38 39 40
  Lemma own_auth_nat_weaken (γ : gname) (n n : nat) :
    (n  n)%nat 
    own γ (nat n) -
    own γ (nat n).
  Proof.
    iIntros (I) "H".
    rewrite (_ : n = (n - n) + n)%nat ; last lia.
    iDestruct "H" as "[_$]".
  Qed.

MEVEL Glen's avatar
MEVEL Glen committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
  Lemma own_auth_nat_null (γ : gname) (m : nat) :
    own γ (nat m) -
    own γ (nat m)  own γ (nat 0).
  Proof.
    by rewrite - own_op (_ : nat m  nat 0 = nat m).
  Qed.

  Lemma auth_nat_update_incr (γ : gname) (m k : nat) :
    own γ (nat m) -
    |==> own γ (nat (m + k))  own γ (nat k).
  Proof.
    iIntros "H●". iDestruct (own_auth_nat_null with "H●") as "[H● H◯]".
    iMod (own_update_2 with "H● H◯") as "[$ $]" ; last done.
    apply auth_update, nat_local_update. lia.
  Qed.

  Lemma auth_nat_update_decr (γ : gname) (m n k : nat) :
    (k  n)%nat 
    own γ (nat m) -
    own γ (nat n) -
    |==> own γ (nat (m - k))  own γ (nat (n - k)).
  Proof.
    iIntros (I) "H● H◯".
    iDestruct (own_auth_nat_le with "H● H◯") as %J.
    iMod (own_update_2 with "H● H◯") as "[$ $]" ; last done.
    apply auth_update, nat_local_update. lia.
  Qed.

69
End Auth_nat.