Commit d93eb054 authored by Glen Mével's avatar Glen Mével
Browse files

update lemmas about auth_min_nat do not need ◯

parent 4e8716d8
......@@ -43,23 +43,33 @@ Section Auth_min_nat.
by apply own_unit.
Qed.
Lemma auth_min_nat_update_read_auth (γ : gname) (m n : nat) :
Lemma auth_min_nat_update_read_auth (γ : gname) (m : nat) :
own γ ( MinNat' m) -
own γ ( MinNat' n) -
|==> own γ ( MinNat' m) own γ ( MinNat' m).
Proof.
iIntros "H● H◯". iCombine "H● H◯" as "H●".
rewrite -own_op. iApply (own_update with "H●◯").
by apply auth_update, option_local_update, min_nat_local_update.
iIntros "H●". rewrite -own_op. iApply (own_update with "H●").
apply auth_update_alloc. rewrite -[x in _ ~l~> (_, x)] left_id.
apply core_id_local_update; last done. by apply _.
Qed.
Lemma auth_min_nat_update_decr (γ : gname) (m n k : nat) :
Lemma auth_min_nat_update_decr (γ : gname) (m k : nat) :
own γ ( MinNat' m) -
|==> own γ ( MinNat' (m - k)).
Proof.
iIntros "H●".
iMod (auth_min_nat_update_read_auth with "H●") as "H●◯".
iAssert (|==> own γ ( MinNat' (m - k)) own γ ( MinNat' (m - k)))%I
with "[-]" as ">[$ _]"; last done.
rewrite - 2!own_op. iApply (own_update with "H●◯").
apply auth_update, option_local_update, min_nat_local_update. cbn. lia.
Qed.
Lemma auth_min_nat_update_decr' (γ : gname) (m n k : nat) :
own γ ( MinNat' m) -
own γ ( MinNat' n) -
|==> own γ ( MinNat' (m - k)) own γ ( MinNat' (n - k)).
Proof.
iIntros "H● H◯".
iDestruct (own_auth_min_nat_le with "H● H◯") as %I.
iIntros "H● H◯". iDestruct (own_auth_min_nat_le with "H● H◯") as %I.
rewrite -[in own _ ( MinNat' (_-_))] (own_auth_min_nat_weaken _ (m-k) (n-k)); last lia.
iCombine "H● H◯" as "H●◯". rewrite -own_op. iApply (own_update with "H●◯").
apply auth_update, option_local_update, min_nat_local_update. cbn. lia.
......
......@@ -47,7 +47,7 @@ Section Debits.
iIntros (?) "H Htc". iDestruct "H" as (γ) "[#Hinv H◯]".
iMod (inv_acc with "Hinv") as "[Hinner Hclose]"; first done.
iDestruct "Hinner" as (m) "[>H● HQ]".
iDestruct (auth_min_nat_update_decr with "H● H◯") as ">[H● H◯]".
iDestruct (auth_min_nat_update_decr' with "H● H◯") as ">[H● H◯]".
iMod ("Hclose" with "[H● Htc HQ]") as "_".
{ iNext. iExists (m-k). iFrame "H●". iIntros "Htc'". iApply "HQ".
iCombine "Htc Htc'" as "Htc". iApply (TC_weaken with "Htc"). lia. }
......
......@@ -495,7 +495,7 @@ Section ThunkProofs.
ThunkVal γ v -
na_own p F -
|={}=>
φ v na_own p (N).
φ v na_own p F.
Abort.
(* Example: forwarding of debt for a thunk that creates a thunk: *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment