Commit 4fc7ee79 authored by Robbert Krebbers's avatar Robbert Krebbers

Revert "Some results about `frac_auth` by Danny and Ales."

These results turned out to be neither that useful nor canonical, and can easily
be derived from local updates.

This reverts commit 465dd9f4.
parent 876771df
......@@ -105,17 +105,4 @@ Section frac_auth.
Proof.
intros. by apply auth_update, option_local_update, prod_local_update_2.
Qed.
Lemma frac_auth_update_alloc q a b c :
( n : nat, {n} a {n} (c a))
! a !{q} b ~~> ! (c a) !{q} (c b).
Proof. intros ?. by apply frac_auth_update, op_local_update. Qed.
Lemma frac_auth_dealloc q a b c `{!Cancelable c} :
! (c a) !{q} (c b) ~~> ! a !{q} b.
Proof.
apply frac_auth_update.
move=> n [x|] /= Hvalid Heq; split; eauto using cmra_validN_op_r.
eapply (cancelableN c); by rewrite ?assoc.
Qed.
End frac_auth.
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