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
Iris
Iris
Commits
2ee38008
Commit
2ee38008
authored
Feb 25, 2016
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
Conflicts: prelude/tactics.v
parents
df7f6381
77a15fea
Pipeline
#160
passed with stage
Changes
6
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
76 additions
and
13 deletions
+76
-13
algebra/cofe.v
algebra/cofe.v
+0
-2
algebra/sts.v
algebra/sts.v
+1
-1
algebra/upred.v
algebra/upred.v
+1
-1
barrier/proof.v
barrier/proof.v
+6
-8
prelude/tactics.v
prelude/tactics.v
+67
-0
program_logic/saved_prop.v
program_logic/saved_prop.v
+1
-1
No files found.
algebra/cofe.v
View file @
2ee38008
...
...
@@ -40,8 +40,6 @@ Tactic Notation "cofe_subst" :=
|
H
:
@
dist
?A
?d
?n
_
?x
|-
_
=>
symmetry
in
H
;
setoid_subst_aux
(@
dist
A
d
n
)
x
end
.
Tactic
Notation
"solve_ne"
:
=
intros
;
solve_proper
.
Record
chain
(
A
:
Type
)
`
{
Dist
A
}
:
=
{
chain_car
:
>
nat
→
A
;
chain_cauchy
n
i
:
n
<
i
→
chain_car
i
≡
{
n
}
≡
chain_car
(
S
n
)
...
...
algebra/sts.v
View file @
2ee38008
...
...
@@ -77,7 +77,7 @@ Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
Global
Instance
up_set_preserving
:
Proper
((
⊆
)
==>
flip
(
⊆
)
==>
(
⊆
))
up_set
.
Proof
.
intros
S1
S2
HS
T1
T2
HT
.
rewrite
/
up_set
.
f_equiv
;
last
done
.
move
=>
s1
s2
Hs
.
simpl
in
HT
.
by
apply
up_preserving
.
f_equiv
.
move
=>
s1
s2
Hs
.
simpl
in
HT
.
by
apply
up_preserving
.
Qed
.
Global
Instance
up_set_proper
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
up_set
.
Proof
.
by
intros
S1
S2
[??]
T1
T2
[??]
;
split
;
apply
up_set_preserving
.
Qed
.
...
...
algebra/upred.v
View file @
2ee38008
...
...
@@ -648,7 +648,7 @@ Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
Lemma
equiv_eq
{
A
:
cofeT
}
P
(
a
b
:
A
)
:
a
≡
b
→
P
⊑
(
a
≡
b
).
Proof
.
intros
->
;
apply
eq_refl
.
Qed
.
Lemma
eq_sym
{
A
:
cofeT
}
(
a
b
:
A
)
:
(
a
≡
b
)
⊑
(
b
≡
a
).
Proof
.
apply
(
eq_rewrite
a
b
(
λ
b
,
b
≡
a
)%
I
)
;
auto
using
eq_refl
.
solve_
ne
.
Qed
.
Proof
.
apply
(
eq_rewrite
a
b
(
λ
b
,
b
≡
a
)%
I
)
;
auto
using
eq_refl
.
solve_
proper
.
Qed
.
(* BI connectives *)
Lemma
sep_mono
P
P'
Q
Q'
:
P
⊑
Q
→
P'
⊑
Q'
→
(
P
★
P'
)
⊑
(
Q
★
Q'
).
...
...
barrier/proof.v
View file @
2ee38008
...
...
@@ -52,19 +52,17 @@ Definition recv (l : loc) (R : iProp) : iProp :=
saved_prop_own
i
Q
★
▷
(
Q
-
★
R
))%
I
.
(** Setoids *)
(* These lemmas really ought to be doable by just calling a tactic.
It is just application of already registered congruence lemmas. *)
Global
Instance
waiting_ne
n
:
Proper
(
dist
n
==>
(=)
==>
dist
n
)
waiting
.
Proof
.
intros
P
P'
HP
I
?
<-.
rewrite
/
waiting
.
by
setoid_rewrite
HP
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
barrier_inv_ne
n
l
:
Proper
(
dist
n
==>
pointwise_relation
_
(
dist
n
)
)
(
barrier_inv
l
).
Proof
.
intros
P
P'
HP
[[]]
;
rewrite
/
barrier_inv
//=.
by
setoid_rewrite
HP
.
Qed
.
Proper
(
dist
n
==>
eq
==>
dist
n
)
(
barrier_inv
l
).
Proof
.
solve_proper
.
Qed
.
Global
Instance
barrier_ctx_ne
n
γ
l
:
Proper
(
dist
n
==>
dist
n
)
(
barrier_ctx
γ
l
).
Proof
.
intros
P
P'
HP
.
rewrite
/
barrier_ctx
.
by
setoid_rewrite
HP
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
send_ne
n
l
:
Proper
(
dist
n
==>
dist
n
)
(
send
l
).
Proof
.
intros
P
P'
HP
.
rewrite
/
send
.
by
setoid_rewrite
HP
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
recv_ne
n
l
:
Proper
(
dist
n
==>
dist
n
)
(
recv
l
).
Proof
.
intros
R
R'
HR
.
rewrite
/
recv
.
by
setoid_rewrite
HR
.
Qed
.
Proof
.
solve_proper
.
Qed
.
(** Helper lemmas *)
Lemma
waiting_split
i
i1
i2
Q
R1
R2
P
I
:
...
...
prelude/tactics.v
View file @
2ee38008
...
...
@@ -228,6 +228,73 @@ Ltac setoid_subst :=
|
H
:
@
equiv
?A
?e
_
?x
|-
_
=>
symmetry
in
H
;
setoid_subst_aux
(@
equiv
A
e
)
x
end
.
(** f_equiv solves goals of the form "f _ = f _", for any relation and any
number of arguments, by looking for appropriate "Proper" instances.
If it cannot solve an equality, it will leave that to the user. *)
Ltac
f_equiv
:
=
(* Deal with "pointwise_relation" *)
try
lazymatch
goal
with
|
|-
pointwise_relation
_
_
_
_
=>
intros
?
end
;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
first
[
reflexivity
|
assumption
|
symmetry
;
assumption
|
match
goal
with
(* We support matches on both sides, *if* they concern the same
or provably equal variables.
TODO: We should support different variables, provided that we can
derive contradictions for the off-diagonal cases. *)
|
|-
?R
(
match
?x
with
_
=>
_
end
)
(
match
?x
with
_
=>
_
end
)
=>
destruct
x
;
f_equiv
|
|-
?R
(
match
?x
with
_
=>
_
end
)
(
match
?y
with
_
=>
_
end
)
=>
subst
y
;
f_equiv
(* First assume that the arguments need the same relation as the result *)
|
|-
?R
(
?f
?x
)
(
?f
_
)
=>
let
H
:
=
fresh
"Proper"
in
assert
(
Proper
(
R
==>
R
)
f
)
as
H
by
(
eapply
_
)
;
apply
H
;
clear
H
;
f_equiv
|
|-
?R
(
?f
?x
?y
)
(
?f
_
_
)
=>
let
H
:
=
fresh
"Proper"
in
assert
(
Proper
(
R
==>
R
==>
R
)
f
)
as
H
by
(
eapply
_
)
;
apply
H
;
clear
H
;
f_equiv
(* Next, try to infer the relation *)
(* TODO: If some of the arguments are the same, we could also
query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *)
|
|-
?R
(
?f
?x
)
(
?f
_
)
=>
let
R1
:
=
fresh
"R"
in
let
H
:
=
fresh
"Proper"
in
let
T
:
=
type
of
x
in
evar
(
R1
:
relation
T
)
;
assert
(
Proper
(
R1
==>
R
)
f
)
as
H
by
(
subst
R1
;
eapply
_
)
;
subst
R1
;
apply
H
;
clear
H
;
f_equiv
|
|-
?R
(
?f
?x
?y
)
(
?f
_
_
)
=>
let
R1
:
=
fresh
"R"
in
let
R2
:
=
fresh
"R"
in
let
H
:
=
fresh
"Proper"
in
let
T1
:
=
type
of
x
in
evar
(
R1
:
relation
T1
)
;
let
T2
:
=
type
of
y
in
evar
(
R2
:
relation
T2
)
;
assert
(
Proper
(
R1
==>
R2
==>
R
)
f
)
as
H
by
(
subst
R1
R2
;
eapply
_
)
;
subst
R1
R2
;
apply
H
;
clear
H
;
f_equiv
end
|
idtac
(* Let the user solve this goal *)
].
(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
number of relations. All the actual work is done by f_equiv;
solve_proper just introduces the assumptions and unfolds the first
head symbol. *)
Ltac
solve_proper
:
=
(* Introduce everything *)
intros
;
repeat
lazymatch
goal
with
|
|-
Proper
_
_
=>
intros
???
|
|-
(
_
==>
_
)%
signature
_
_
=>
intros
???
end
;
(* Unfold the head symbol, which is the one we are proving a new property about *)
lazymatch
goal
with
|
|-
?R
(
?f
_
_
_
_
)
(
?f
_
_
_
_
)
=>
unfold
f
|
|-
?R
(
?f
_
_
_
)
(
?f
_
_
_
)
=>
unfold
f
|
|-
?R
(
?f
_
_
)
(
?f
_
_
)
=>
unfold
f
|
|-
?R
(
?f
_
)
(
?f
_
)
=>
unfold
f
end
;
solve
[
f_equiv
].
(** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac,
and then reverts them. *)
Ltac
intros_revert
tac
:
=
...
...
program_logic/saved_prop.v
View file @
2ee38008
...
...
@@ -43,6 +43,6 @@ Section saved_prop.
rewrite
agree_equivI
later_equivI
/=
;
apply
later_mono
.
rewrite
-{
2
}(
iProp_fold_unfold
P
)
-{
2
}(
iProp_fold_unfold
Q
).
apply
(
eq_rewrite
(
iProp_unfold
P
)
(
iProp_unfold
Q
)
(
λ
Q'
:
iPreProp
Λ
_
,
iProp_fold
(
iProp_unfold
P
)
≡
iProp_fold
Q'
)%
I
)
;
solve_
ne
||
auto
with
I
.
iProp_fold
(
iProp_unfold
P
)
≡
iProp_fold
Q'
)%
I
)
;
solve_
proper
||
auto
with
I
.
Qed
.
End
saved_prop
.
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