Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Simon Spies
Iris
Commits
cbad1f38
Commit
cbad1f38
authored
Feb 26, 2016
by
Robbert Krebbers
Browse files
Some decidable agreement CMRA properties.
parent
96e5b762
Changes
1
Show whitespace changes
Inline
Side-by-side
algebra/dec_agree.v
View file @
cbad1f38
...
...
@@ -49,10 +49,13 @@ Qed.
Canonical
Structure
dec_agreeRA
:
cmraT
:
=
discreteRA
dec_agree_ra
.
(* Some properties of this CMRA *)
Lemma
dec_agree_
idemp
(
x
:
dec_agree
A
)
:
x
⋅
x
≡
x
.
Proof
.
destruct
x
;
by
repeat
(
simplify_eq
/=
||
case_match
)
.
Qed
.
Lemma
dec_agree_
ne
a
b
:
a
≠
b
→
DecAgree
a
⋅
DecAgree
b
=
DecAgreeBot
.
Proof
.
intros
.
by
rewrite
/=
decide_False
.
Qed
.
Lemma
dec_agree_op_inv
(
x1
x2
:
dec_agree
A
)
:
✓
(
x1
⋅
x2
)
→
x1
≡
x2
.
Lemma
dec_agree_idemp
(
x
:
dec_agree
A
)
:
x
⋅
x
=
x
.
Proof
.
destruct
x
;
by
rewrite
/=
?decide_True
.
Qed
.
Lemma
dec_agree_op_inv
(
x1
x2
:
dec_agree
A
)
:
✓
(
x1
⋅
x2
)
→
x1
=
x2
.
Proof
.
destruct
x1
,
x2
;
by
repeat
(
simplify_eq
/=
||
case_match
).
Qed
.
End
dec_agree
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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