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
Joshua Yanovski
iriscoq
Commits
a48f3430
Commit
a48f3430
authored
Mar 11, 2016
by
Robbert Krebbers
Browse files
Merge branch 'master' of gitlab.mpisws.org:FP/iriscoq
parents
2386287d
7fc5808c
Changes
1
Hide whitespace changes
Inline
Sidebyside
algebra/one_shot.v
View file @
a48f3430
...
...
@@ 2,6 +2,8 @@ From iris.algebra Require Export cmra.
From
iris
.
algebra
Require
Import
upred
.
Local
Arguments
validN
_
_
_
!
_
/
.
Local
Arguments
valid
_
_
!
_
/
.
Local
Arguments
cmra_validN
_
_
!
_
/
.
Local
Arguments
cmra_valid
_
!
_
/
.
(
*
TODO
:
Really
,
we
should
have
sums
,
and
then
this
should
be
just
"excl unit + A"
.
*
)
Inductive
one_shot
{
A
:
Type
}
:=
...
...
@@ 92,3 +94,198 @@ End cofe.
Arguments
one_shotC
:
clear
implicits
.
(
*
Functor
on
COFEs
*
)
Definition
one_shot_map
{
A
B
}
(
f
:
A
→
B
)
(
x
:
one_shot
A
)
:
one_shot
B
:=
match
x
with

OneShotPending
=>
OneShotPending

Shot
a
=>
Shot
(
f
a
)

OneShotUnit
=>
OneShotUnit

OneShotBot
=>
OneShotBot
end
.
Instance:
Params
(
@
one_shot_map
)
2.
Lemma
one_shot_map_id
{
A
}
(
x
:
one_shot
A
)
:
one_shot_map
id
x
=
x
.
Proof
.
by
destruct
x
.
Qed
.
Lemma
one_shot_map_compose
{
A
B
C
}
(
f
:
A
→
B
)
(
g
:
B
→
C
)
(
x
:
one_shot
A
)
:
one_shot_map
(
g
∘
f
)
x
=
one_shot_map
g
(
one_shot_map
f
x
).
Proof
.
by
destruct
x
.
Qed
.
Lemma
one_shot_map_ext
{
A
B
:
cofeT
}
(
f
g
:
A
→
B
)
x
:
(
∀
x
,
f
x
≡
g
x
)
→
one_shot_map
f
x
≡
one_shot_map
g
x
.
Proof
.
by
destruct
x
;
constructor
.
Qed
.
Instance
one_shot_map_cmra_ne
{
A
B
:
cofeT
}
n
:
Proper
((
dist
n
==>
dist
n
)
==>
dist
n
==>
dist
n
)
(
@
one_shot_map
A
B
).
Proof
.
intros
f
f
'
Hf
;
destruct
1
;
constructor
;
by
try
apply
Hf
.
Qed
.
Definition
one_shotC_map
{
A
B
}
(
f
:
A

n
>
B
)
:
one_shotC
A

n
>
one_shotC
B
:=
CofeMor
(
one_shot_map
f
).
Instance
one_shotC_map_ne
A
B
n
:
Proper
(
dist
n
==>
dist
n
)
(
@
one_shotC_map
A
B
).
Proof
.
intros
f
f
'
Hf
[];
constructor
;
by
try
apply
Hf
.
Qed
.
Section
cmra
.
Context
{
A
:
cmraT
}
.
Implicit
Types
a
b
:
A
.
Implicit
Types
x
y
:
one_shot
A
.
(
*
CMRA
*
)
Instance
one_shot_valid
:
Valid
(
one_shot
A
)
:=
λ
x
,
match
x
with

OneShotPending
=>
True

Shot
a
=>
✓
a

OneShotUnit
=>
True

OneShotBot
=>
False
end
.
Instance
one_shot_validN
:
ValidN
(
one_shot
A
)
:=
λ
n
x
,
match
x
with

OneShotPending
=>
True

Shot
a
=>
✓
{
n
}
a

OneShotUnit
=>
True

OneShotBot
=>
False
end
.
Global
Instance
one_shot_empty
:
Empty
(
one_shot
A
)
:=
OneShotUnit
.
Instance
one_shot_core
:
Core
(
one_shot
A
)
:=
λ
x
,
match
x
with

Shot
a
=>
Shot
(
core
a
)

OneShotBot
=>
OneShotBot

_
=>
∅
end
.
Instance
one_shot_op
:
Op
(
one_shot
A
)
:=
λ
x
y
,
match
x
,
y
with

Shot
a
,
Shot
b
=>
Shot
(
a
⋅
b
)

Shot
a
,
OneShotUnit

OneShotUnit
,
Shot
a
=>
Shot
a

OneShotUnit
,
OneShotPending

OneShotPending
,
OneShotUnit
=>
OneShotPending

OneShotUnit
,
OneShotUnit
=>
OneShotUnit

_
,
_
=>
OneShotBot
end
.
Lemma
Shot_op
a
b
:
Shot
a
⋅
Shot
b
=
Shot
(
a
⋅
b
).
Proof
.
done
.
Qed
.
Lemma
Shot_incl
a
b
:
Shot
a
≼
Shot
b
↔
a
≼
b
.
Proof
.
split
;
intros
[
c
H
].

destruct
c
;
inversion_clear
H
;
first
by
eexists
.
by
rewrite
(
_
:
b
≡
a
).

exists
(
Shot
c
).
constructor
.
done
.
Qed
.
Definition
one_shot_cmra_mixin
:
CMRAMixin
(
one_shot
A
).
Proof
.
split
.

intros
n
[];
destruct
1
;
constructor
;
by
cofe_subst
.

intros
?
[

a


]
[

b


]
H
;
inversion_clear
H
;
constructor
;
by
f_equiv
.

intros
?
[

a


]
[

b


]
H
;
inversion_clear
H
;
cofe_subst
;
done
.

intros
[

a


];
rewrite
/=
?
cmra_valid_validN
;
naive_solver
eauto
using
O
.

intros
n
[

a


];
simpl
;
auto
using
cmra_validN_S
.

intros
[

a1


]
[

a2


]
[

a3


];
constructor
;
by
rewrite
?
assoc
.

intros
[

a1


]
[

a2


];
constructor
;
by
rewrite
1
?
comm
.

intros
[

a


];
constructor
;
[].
exact
:
cmra_core_l
.

intros
[

a


];
constructor
;
[].
exact
:
cmra_core_idemp
.

intros
[

a1


]
[

a2


];
simpl
;
try
solve
[
by
exists
OneShotUnit
;
constructor

by
exists
OneShotBot
;
constructor

by
intros
[[

a3


]
H
];
inversion_clear
H
].
+
intros
H
%
Shot_incl
.
apply
Shot_incl
,
cmra_core_preserving
.
done
.
+
intros
_.
exists
(
Shot
(
core
a2
)).
by
constructor
.

intros
n
[

a1


]
[

a2


];
simpl
;
eauto
using
cmra_validN_op_l
;
done
.

intros
n
[

a


]
y1
y2
Hx
Hx
'
;
last
2
first
.
+
by
exists
(
∅
,
∅
);
destruct
y1
,
y2
;
inversion_clear
Hx
'
.
+
by
exists
(
OneShotBot
,
OneShotBot
);
destruct
y1
,
y2
;
inversion_clear
Hx
'
.
+
destruct
y1
,
y2
;
try
(
exfalso
;
by
inversion_clear
Hx
'
).
*
by
exists
(
OneShotPending
,
OneShotUnit
).
*
by
exists
(
OneShotUnit
,
OneShotPending
).
+
destruct
y1
as
[

b1


],
y2
as
[

b2


];
try
(
exfalso
;
by
inversion_clear
Hx
'
).
*
apply
(
inj
Shot
)
in
Hx
'
.
destruct
(
cmra_extend
n
a
b1
b2
)
as
([
z1
z2
]
&?&?&?
);
auto
.
exists
(
Shot
z1
,
Shot
z2
).
by
repeat
constructor
.
*
exists
(
Shot
a
,
∅
).
inversion_clear
Hx
'
.
by
repeat
constructor
.
*
exists
(
∅
,
Shot
a
).
inversion_clear
Hx
'
.
by
repeat
constructor
.
Qed
.
Canonical
Structure
one_shotR
:
cmraT
:=
CMRAT
one_shot_cofe_mixin
one_shot_cmra_mixin
.
Global
Instance
one_shot_cmra_unit
:
CMRAUnit
one_shotR
.
Proof
.
split
.
done
.
by
intros
[].
apply
_.
Qed
.
Global
Instance
one_shot_cmra_discrete
:
CMRADiscrete
A
→
CMRADiscrete
one_shotR
.
Proof
.
split
;
first
apply
_.
intros
[

a


];
simpl
;
auto
using
cmra_discrete_valid
.
Qed
.
Lemma
one_shot_validN_inv_l
n
y
:
✓
{
n
}
(
OneShotPending
⋅
y
)
→
y
=
∅
.
Proof
.
destruct
y
as
[

b


];
[
done


done

done
].
destruct
1.
Qed
.
Lemma
one_shot_valid_inv_l
y
:
✓
(
OneShotPending
⋅
y
)
→
y
=
∅
.
Proof
.
intros
.
by
apply
one_shot_validN_inv_l
with
0
,
cmra_valid_validN
.
Qed
.
Lemma
one_shot_bot_largest
y
:
y
≼
OneShotBot
.
Proof
.
destruct
y
;
exists
OneShotBot
;
constructor
.
Qed
.
(
**
Internalized
properties
*
)
Lemma
one_shot_equivI
{
M
}
(
x
y
:
one_shot
A
)
:
(
x
≡
y
)
⊣⊢
(
match
x
,
y
with

OneShotPending
,
OneShotPending
=>
True

Shot
a
,
Shot
b
=>
a
≡
b

OneShotUnit
,
OneShotUnit
=>
True

OneShotBot
,
OneShotBot
=>
True

_
,
_
=>
False
end
:
uPred
M
).
Proof
.
uPred
.
unseal
;
do
2
split
;
first
by
destruct
1.
by
destruct
x
,
y
;
try
destruct
1
;
try
constructor
.
Qed
.
Lemma
one_shot_validI
{
M
}
(
x
:
one_shot
A
)
:
(
✓
x
)
⊣⊢
(
match
x
with

Shot
a
=>
✓
a

OneShotBot
=>
False

_
=>
True
end
:
uPred
M
).
Proof
.
uPred
.
unseal
.
by
destruct
x
.
Qed
.
(
**
Updates
*
)
Lemma
one_shot_update_shoot
(
a
:
A
)
:
✓
a
→
OneShotPending
~~>
Shot
a
.
Proof
.
move
=>
?
n
y
/
one_shot_validN_inv_l
>
.
by
apply
cmra_valid_validN
.
Qed
.
Lemma
one_shot_update
(
a1
a2
:
A
)
:
a1
~~>
a2
→
Shot
a1
~~>
Shot
a2
.
Proof
.
intros
Ha
n
[

b


]
?
;
simpl
;
auto
.
apply
cmra_validN_op_l
with
(
core
a1
),
Ha
.
by
rewrite
cmra_core_r
.
Qed
.
End
cmra
.
Arguments
one_shotR
:
clear
implicits
.
(
*
Functor
*
)
Instance
one_shot_map_cmra_monotone
{
A
B
:
cmraT
}
(
f
:
A
→
B
)
:
CMRAMonotone
f
→
CMRAMonotone
(
one_shot_map
f
).
Proof
.
split
;
try
apply
_.

intros
n
[

a


];
simpl
;
auto
using
validN_preserving
.

intros
[

a1


]
[

a2


]
[[

a3


]
Hx
];
inversion
Hx
;
setoid_subst
;
try
apply
cmra_unit_least
;
try
apply
one_shot_bot_largest
;
auto
;
[].
destruct
(
included_preserving
f
a1
(
a1
⋅
a3
))
as
[
b
?
].
{
by
apply
cmra_included_l
.
}
by
exists
(
Shot
b
);
constructor
.
Qed
.
Program
Definition
one_shotRF
(
F
:
rFunctor
)
:
rFunctor
:=
{
rFunctor_car
A
B
:=
one_shotR
(
rFunctor_car
F
A
B
);
rFunctor_map
A1
A2
B1
B2
fg
:=
one_shotC_map
(
rFunctor_map
F
fg
)
}
.
Next
Obligation
.
by
intros
F
A1
A2
B1
B2
n
f
g
Hfg
;
apply
one_shotC_map_ne
,
rFunctor_ne
.
Qed
.
Next
Obligation
.
intros
F
A
B
x
.
rewrite
/=
{
2
}
(
one_shot_map_id
x
).
apply
one_shot_map_ext
=>
y
;
apply
rFunctor_id
.
Qed
.
Next
Obligation
.
intros
F
A1
A2
A3
B1
B2
B3
f
g
f
'
g
'
x
.
rewrite
/=

one_shot_map_compose
.
apply
one_shot_map_ext
=>
y
;
apply
rFunctor_compose
.
Qed
.
Instance
one_shotRF_contractive
F
:
rFunctorContractive
F
→
rFunctorContractive
(
one_shotRF
F
).
Proof
.
by
intros
?
A1
A2
B1
B2
n
f
g
Hfg
;
apply
one_shotC_map_ne
,
rFunctor_contractive
.
Qed
.
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