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
Iris
Fairis
Commits
2b850ccc
Commit
2b850ccc
authored
Jun 01, 2018
by
Ralf Jung
Browse files
hopefully these are the last warnings
parent
a1e38f07
Pipeline
#9395
failed with stage
in 4 minutes and 59 seconds
Changes
2
Pipelines
6
Hide whitespace changes
Inline
Side-by-side
theories/chan_lang/protocol.v
View file @
2b850ccc
...
...
@@ -72,9 +72,9 @@ Instance prot_equiv {A} : Equiv (protocol A) := @prot_eq A.
Global
Instance
prot_equivalence
A
:
Equivalence
(
@
equiv
(
protocol
A
)
_
).
Proof
.
split
.
-
now
cofix
;
intros
[
|
|
|
|
];
constructor
.
-
now
cofix
;
intros
??
[
|
|
|
|
];
constructor
.
-
cofix
;
intros
???
.
inversion
1
;
inversion
1
;
econstructor
;
etrans
;
eauto
.
-
now
cofix
COFIX
;
intros
[
|
|
|
|
];
constructor
.
-
now
cofix
COFIX
;
intros
??
[
|
|
|
|
];
constructor
.
-
cofix
COFIX
;
intros
???
.
inversion
1
;
inversion
1
;
econstructor
;
etrans
;
eauto
.
Qed
.
Inductive
prot_modc
{
T
:
Type
}
:
protocol
T
→
list
choice
→
protocol
T
→
Prop
:=
...
...
theories/program_logic/refine_raw_adequacy.v
View file @
2b850ccc
...
...
@@ -7,6 +7,9 @@ From fri.algebra Require Export irelations.
From
fri
.
algebra
Require
Import
dra
cmra_tactics
base_logic
.
From
fri
.
prelude
Require
Import
set_finite_setoid
list
.
From
fri
.
program_logic
Require
Import
language
wsat
adequacy_inf
.
From
fri
.
algebra
Require
upred
.
Require
ClassicalEpsilon
.
(
*
TODO
:
probably
should
NOT
be
using
refine_ucmra
directly
the
way
I
am
--
should
use
the
type
,
and
then
rely
on
canonical
structure
to
find
the
ucmra
stuff
...
because
the
workaround
here
breaks
other
stuff
*
)
...
...
@@ -88,7 +91,7 @@ Definition refine v ts cs ixs : refine_cmra sΛ K :=
(
∃
cfg0
idx0
,
owne
(
refine
master
∅
(
cfg0
++
[
c
])
idx0
))
%
I
.
Definition
master_own_exact
(
cs
:
list
(
cfg
s
Λ
))
idxs
:=
owne
(
refine
master
∅
cs
idxs
)
%
I
.
From
fri
.
algebra
Require
Import
upred
.
Import
fri
.
algebra
.
upred
.
Definition
snapshot_ownl
tids
(
c
:
cfg
s
Λ
)
:=
(
∃
cfg0
idx0
,
ownle
(
refine
snapshot
tids
(
cfg0
++
[
c
])
idx0
))
%
I
.
...
...
@@ -421,7 +424,7 @@ Qed.
Definition
interp_step
'
:
nat
→
relation
(
interp_codomain
)
:=
λ
i
x
y
,
idx_stepN
1
i
(
snap_vector
x
)
(
snap_vector
y
).
Require
Import
ClassicalEpsilon
.
Import
ClassicalEpsilon
.
Lemma
some_interp_extract
:
∀
(
x
:
interp_codomain
)
(
e
:
trace
interp_step
(
Some
x
)),
...
...
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