Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Hugo Herbelin
iris-coq
Commits
7b0f3340
Commit
7b0f3340
authored
Dec 10, 2018
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Get rid of some `uPred M` coercions.
parent
261714ad
Changes
6
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
33 additions
and
33 deletions
+33
-33
theories/algebra/agree.v
theories/algebra/agree.v
+2
-2
theories/algebra/auth.v
theories/algebra/auth.v
+8
-8
theories/algebra/csum.v
theories/algebra/csum.v
+11
-11
theories/algebra/excl.v
theories/algebra/excl.v
+8
-8
theories/algebra/gmap.v
theories/algebra/gmap.v
+2
-2
theories/algebra/list.v
theories/algebra/list.v
+2
-2
No files found.
theories/algebra/agree.v
View file @
7b0f3340
...
...
@@ -233,13 +233,13 @@ Lemma agree_op_invL' `{!LeibnizEquiv A} a b : ✓ (to_agree a ⋅ to_agree b)
Proof
.
by
intros
?%
agree_op_inv'
%
leibniz_equiv
.
Qed
.
(** Internalized properties *)
Lemma
agree_equivI
{
M
}
a
b
:
to_agree
a
≡
to_agree
b
⊣
⊢
(
a
≡
b
:
uPred
M
).
Lemma
agree_equivI
{
M
}
a
b
:
to_agree
a
≡
to_agree
b
⊣
⊢
@{
uPredI
M
}
(
a
≡
b
).
Proof
.
uPred
.
unseal
.
do
2
split
.
-
intros
Hx
.
exact
:
to_agree_injN
.
-
intros
Hx
.
exact
:
to_agree_ne
.
Qed
.
Lemma
agree_validI
{
M
}
x
y
:
✓
(
x
⋅
y
)
⊢
(
x
≡
y
:
uPred
M
)
.
Lemma
agree_validI
{
M
}
x
y
:
✓
(
x
⋅
y
)
⊢
@{
uPred
I
M
}
x
≡
y
.
Proof
.
uPred
.
unseal
;
split
=>
r
n
_
?
;
by
apply
:
agree_op_invN
.
Qed
.
End
agree
.
...
...
theories/algebra/auth.v
View file @
7b0f3340
...
...
@@ -191,15 +191,15 @@ Global Instance auth_frag_core_id a : CoreId a → CoreId (◯ a).
Proof
.
do
2
constructor
;
simpl
;
auto
.
by
apply
core_id_core
.
Qed
.
(** Internalized properties *)
Lemma
auth_equivI
{
M
}
(
x
y
:
auth
A
)
:
x
≡
y
⊣
⊢
(
authoritative
x
≡
authoritative
y
∧
auth_own
x
≡
auth_own
y
:
uPred
M
)
.
Lemma
auth_equivI
{
M
}
x
y
:
x
≡
y
⊣
⊢
@{
uPredI
M
}
authoritative
x
≡
authoritative
y
∧
auth_own
x
≡
auth_own
y
.
Proof
.
by
uPred
.
unseal
.
Qed
.
Lemma
auth_validI
{
M
}
(
x
:
auth
A
)
:
✓
x
⊣
⊢
(
match
authoritative
x
with
|
Excl'
a
=>
(
∃
b
,
a
≡
auth_own
x
⋅
b
)
∧
✓
a
|
None
=>
✓
auth_own
x
|
ExclBot'
=>
False
end
:
uPred
M
)
.
Lemma
auth_validI
{
M
}
x
:
✓
x
⊣
⊢
@{
uPredI
M
}
match
authoritative
x
with
|
Excl'
a
=>
(
∃
b
,
a
≡
auth_own
x
⋅
b
)
∧
✓
a
|
None
=>
✓
auth_own
x
|
ExclBot'
=>
False
end
.
Proof
.
uPred
.
unseal
.
by
destruct
x
as
[[[]|]].
Qed
.
Lemma
auth_frag_op
a
b
:
◯
(
a
⋅
b
)
=
◯
a
⋅
◯
b
.
...
...
theories/algebra/csum.v
View file @
7b0f3340
...
...
@@ -284,22 +284,22 @@ Proof. intros ? [] ? EQ; inversion_clear EQ. by eapply id_free0_r. Qed.
(** Internalized properties *)
Lemma
csum_equivI
{
M
}
(
x
y
:
csum
A
B
)
:
x
≡
y
⊣
⊢
(
match
x
,
y
with
|
Cinl
a
,
Cinl
a'
=>
a
≡
a'
|
Cinr
b
,
Cinr
b'
=>
b
≡
b'
|
CsumBot
,
CsumBot
=>
True
|
_
,
_
=>
False
end
:
uPred
M
)
.
x
≡
y
⊣
⊢
@{
uPredI
M
}
match
x
,
y
with
|
Cinl
a
,
Cinl
a'
=>
a
≡
a'
|
Cinr
b
,
Cinr
b'
=>
b
≡
b'
|
CsumBot
,
CsumBot
=>
True
|
_
,
_
=>
False
end
.
Proof
.
uPred
.
unseal
;
do
2
split
;
first
by
destruct
1
.
by
destruct
x
,
y
;
try
destruct
1
;
try
constructor
.
Qed
.
Lemma
csum_validI
{
M
}
(
x
:
csum
A
B
)
:
✓
x
⊣
⊢
(
match
x
with
|
Cinl
a
=>
✓
a
|
Cinr
b
=>
✓
b
|
CsumBot
=>
False
end
:
uPred
M
)
.
✓
x
⊣
⊢
@{
uPredI
M
}
match
x
with
|
Cinl
a
=>
✓
a
|
Cinr
b
=>
✓
b
|
CsumBot
=>
False
end
.
Proof
.
uPred
.
unseal
.
by
destruct
x
.
Qed
.
(** Updates *)
...
...
theories/algebra/excl.v
View file @
7b0f3340
...
...
@@ -95,17 +95,17 @@ Global Instance excl_cmra_discrete : OfeDiscrete A → CmraDiscrete exclR.
Proof
.
split
.
apply
_
.
by
intros
[].
Qed
.
(** Internalized properties *)
Lemma
excl_equivI
{
M
}
(
x
y
:
excl
A
)
:
x
≡
y
⊣
⊢
(
match
x
,
y
with
|
Excl
a
,
Excl
b
=>
a
≡
b
|
ExclBot
,
ExclBot
=>
True
|
_
,
_
=>
False
end
:
uPred
M
)
.
Lemma
excl_equivI
{
M
}
x
y
:
x
≡
y
⊣
⊢
@{
uPredI
M
}
match
x
,
y
with
|
Excl
a
,
Excl
b
=>
a
≡
b
|
ExclBot
,
ExclBot
=>
True
|
_
,
_
=>
False
end
.
Proof
.
uPred
.
unseal
.
do
2
split
.
by
destruct
1
.
by
destruct
x
,
y
;
try
constructor
.
Qed
.
Lemma
excl_validI
{
M
}
(
x
:
excl
A
)
:
✓
x
⊣
⊢
(
if
x
is
ExclBot
then
False
else
True
:
uPred
M
)
.
Lemma
excl_validI
{
M
}
x
:
✓
x
⊣
⊢
@{
uPredI
M
}
if
x
is
ExclBot
then
False
else
True
.
Proof
.
uPred
.
unseal
.
by
destruct
x
.
Qed
.
(** Exclusive *)
...
...
theories/algebra/gmap.v
View file @
7b0f3340
...
...
@@ -177,9 +177,9 @@ Qed.
Canonical
Structure
gmapUR
:
=
UcmraT
(
gmap
K
A
)
gmap_ucmra_mixin
.
(** Internalized properties *)
Lemma
gmap_equivI
{
M
}
m1
m2
:
m1
≡
m2
⊣
⊢
(
∀
i
,
m1
!!
i
≡
m2
!!
i
:
uPred
M
)
.
Lemma
gmap_equivI
{
M
}
m1
m2
:
m1
≡
m2
⊣
⊢
@{
uPredI
M
}
∀
i
,
m1
!!
i
≡
m2
!!
i
.
Proof
.
by
uPred
.
unseal
.
Qed
.
Lemma
gmap_validI
{
M
}
m
:
✓
m
⊣
⊢
(
∀
i
,
✓
(
m
!!
i
)
:
uPred
M
)
.
Lemma
gmap_validI
{
M
}
m
:
✓
m
⊣
⊢
@{
uPredI
M
}
∀
i
,
✓
(
m
!!
i
).
Proof
.
by
uPred
.
unseal
.
Qed
.
End
cmra
.
...
...
theories/algebra/list.v
View file @
7b0f3340
...
...
@@ -247,9 +247,9 @@ Section cmra.
Qed
.
(** Internalized properties *)
Lemma
list_equivI
{
M
}
l1
l2
:
l1
≡
l2
⊣
⊢
(
∀
i
,
l1
!!
i
≡
l2
!!
i
:
uPred
M
)
.
Lemma
list_equivI
{
M
}
l1
l2
:
l1
≡
l2
⊣
⊢
@{
uPredI
M
}
∀
i
,
l1
!!
i
≡
l2
!!
i
.
Proof
.
uPred
.
unseal
;
constructor
=>
n
x
?.
apply
list_dist_lookup
.
Qed
.
Lemma
list_validI
{
M
}
l
:
✓
l
⊣
⊢
(
∀
i
,
✓
(
l
!!
i
)
:
uPred
M
)
.
Lemma
list_validI
{
M
}
l
:
✓
l
⊣
⊢
@{
uPredI
M
}
∀
i
,
✓
(
l
!!
i
).
Proof
.
uPred
.
unseal
;
constructor
=>
n
x
?.
apply
list_lookup_validN
.
Qed
.
End
cmra
.
...
...
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