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
c905411d
Commit
c905411d
authored
Feb 25, 2016
by
Robbert Krebbers
Browse files
Simplify barrier protocol proofs.
parent
2d9c5f33
Changes
1
Hide whitespace changes
Inline
Sidebyside
barrier/protocol.v
View file @
c905411d
...
...
@@ 17,12 +17,9 @@ Inductive prim_step : relation state :=

ChangeI
p
I2
I1
:
prim_step
(
State
p
I1
)
(
State
p
I2
)

ChangePhase
I
:
prim_step
(
State
Low
I
)
(
State
High
I
).
Definition
change_tok
(
I
:
gset
gname
)
:
set
token
:=
{
[
t

match
t
with
Change
i
=>
i
∉
I

Send
=>
False
end
]
}
.
Definition
send_tok
(
p
:
phase
)
:
set
token
:=
match
p
with
Low
=>
∅

High
=>
{
[
Send
]
}
end
.
Definition
tok
(
s
:
state
)
:
set
token
:=
change_tok
(
state_I
s
)
∪
send_tok
(
state_phase
s
).
{
[
t

∃
i
,
t
=
Change
i
∧
i
∉
state_I
s
]
}
∪
(
if
state_phase
s
is
High
then
{
[
Send
]
}
else
∅
).
Global
Arguments
tok
!
_
/
.
Canonical
Structure
sts
:=
sts
.
STS
prim_step
tok
.
...
...
@@ 35,30 +32,22 @@ Definition low_states : set state := {[ s  state_phase s = Low ]}.
Lemma
i_states_closed
i
:
sts
.
closed
(
i_states
i
)
{
[
Change
i
]
}
.
Proof
.
split
.

intros
[
p
I
].
rewrite
/=
/
i_states
/
change_tok
.
destruct
p
;
set_solver
.

(
*
If
we
do
the
destruct
of
the
states
early
,
and
then
inversion
on
the
proof
of
a
transition
,
it
doesn
'
t
work

we
do
not
obtain
the
equalities
we
need
.
So
we
destruct
the
states
late
,
because
this
means
we
can
use
"destruct"
instead
of
"inversion"
.
*
)
intros
s1
s2
Hs1
[
T1
T2
Hdisj
Hstep
'
].
inversion_clear
Hstep
'
as
[
?
?
?
?
Htrans
_
_
Htok
].
destruct
Htrans
;
simpl
in
*
;
last
done
.
move:
Hs1
Hdisj
Htok
.
rewrite
elem_of_equiv_empty
elem_of_equiv
.
move
=>
?
/
(
_
(
Change
i
))
Hdisj
/
(
_
(
Change
i
));
move
:
Hdisj
.
rewrite
elem_of_intersection
elem_of_union
!
elem_of_mkSet
.
intros
;
apply
dec_stable
.
destruct
p
;
set_solver
.
split
;
first
(
intros
[[]
I
];
set_solver
).
(
*
If
we
do
the
destruct
of
the
states
early
,
and
then
inversion
on
the
proof
of
a
transition
,
it
doesn
'
t
work

we
do
not
obtain
the
equalities
we
need
.
So
we
destruct
the
states
late
,
because
this
means
we
can
use
"destruct"
instead
of
"inversion"
.
*
)
intros
s1
s2
Hs1
[
T1
T2
Hdisj
Hstep
'
].
inversion_clear
Hstep
'
as
[
?
?
?
?
Htrans
_
_
Htok
].
destruct
Htrans
as
[[]
??
];
done

set_solver
.
Qed
.
Lemma
low_states_closed
:
sts
.
closed
low_states
{
[
Send
]
}
.
Proof
.
split
.

intros
[
p
I
].
rewrite
/
low_states
.
set_solver
.

intros
s1
s2
Hs1
[
T1
T2
Hdisj
Hstep
'
].
inversion_clear
Hstep
'
as
[
?
?
?
?
Htrans
_
_
Htok
].
destruct
Htrans
;
simpl
in
*
;
first
by
destruct
p
.
exfalso
;
apply
dec_stable
;
set_solver
.
split
;
first
(
intros
[
??
];
set_solver
).
intros
s1
s2
Hs1
[
T1
T2
Hdisj
Hstep
'
].
inversion_clear
Hstep
'
as
[
?
?
?
?
Htrans
_
_
Htok
].
destruct
Htrans
as
[[]
??
];
done

set_solver
.
Qed
.
(
*
Proof
that
we
can
take
the
steps
we
need
.
*
)
...
...
@@ 70,12 +59,8 @@ Lemma wait_step i I :
sts
.
steps
(
State
High
I
,
{
[
Change
i
]
}
)
(
State
High
(
I
∖
{
[
i
]
}
),
∅
).
Proof
.
intros
.
apply
rtc_once
.
constructor
;
first
constructor
;
rewrite
/=
/
change_tok
;
[
set_solver
by
eauto
..

].
(
*
TODO
this
proof
is
rather
annoying
.
*
)
apply
elem_of_equiv
=>
t
.
rewrite
!
elem_of_union
.
rewrite
!
elem_of_mkSet
/
change_tok
/=
.
destruct
t
as
[
j

];
last
set_solver
.
rewrite
elem_of_difference
elem_of_singleton
.
constructor
;
first
constructor
;
[
set_solver
..

].
apply
elem_of_equiv
=>
[
j

];
last
set_solver
.
destruct
(
decide
(
i
=
j
));
set_solver
.
Qed
.
...
...
@@ 85,17 +70,14 @@ Lemma split_step p i i1 i2 I :
(
State
p
I
,
{
[
Change
i
]
}
)
(
State
p
(
{
[
i1
]
}
∪
(
{
[
i2
]
}
∪
(
I
∖
{
[
i
]
}
))),
{
[
Change
i1
;
Change
i2
]
}
).
Proof
.
intros
.
apply
rtc_once
.
con
struct
or
;
first
constructor
;
simpl
.
intros
.
apply
rtc_once
.
constructor
;
first
constructor
.

de
struct
p
;
set_solver
.

destruct
p
;
set_solver
.
(
*
This
gets
annoying
...
and
I
think
I
can
see
a
pattern
with
all
these
proofs
.
Automatable
?
*
)

apply
elem_of_equiv
=>
t
.
destruct
t
;
last
set_solver
.
rewrite
!
elem_of_mkSet
!
not_elem_of_union
!
not_elem_of_singleton
not_elem_of_difference
elem_of_singleton
!
(
inj_iff
Change
).
destruct
p
;
naive_solver
.

apply
elem_of_equiv
=>
t
.
destruct
t
as
[
j

];
last
set_solver
.
rewrite
!
elem_of_mkSet
!
not_elem_of_union
!
not_elem_of_singleton
not_elem_of_difference
elem_of_singleton
!
(
inj_iff
Change
).
destruct
(
decide
(
i1
=
j
))
as
[
>
];
first
tauto
.
destruct
(
decide
(
i2
=
j
))
as
[
>
];
intuition
.

apply
elem_of_equiv
=>
/=

[
j

];
last
set_solver
.
set_unfold
;
rewrite
!
(
inj_iff
Change
).
assert
(
Change
j
∈
match
p
with
Low
=>
∅

High
=>
{
[
Send
]
}
end
↔
False
)
as
>
by
(
destruct
p
;
set_solver
).
destruct
(
decide
(
i1
=
j
))
as
[
>
];
first
naive_solver
.
destruct
(
decide
(
i2
=
j
))
as
[
>
];
first
naive_solver
.
destruct
(
decide
(
i
=
j
))
as
[
>
];
naive_solver
.
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