Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rice Wine
Iris
Commits
465dd9f4
Commit
465dd9f4
authored
May 09, 2018
by
Robbert Krebbers
Browse files
Some results about `frac_auth` by Danny and Ales.
parent
d44bf0ee
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/algebra/frac_auth.v
View file @
465dd9f4
...
...
@@ -105,4 +105,17 @@ 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
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment