Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Rodolphe Lepigre
Iris
Commits
ab9f921d
Commit
ab9f921d
authored
Feb 25, 2016
by
Ralf Jung
Browse files
improve f_equiv and solve_proper; use them in a few more places
parent
c64b9a55
Changes
3
Hide whitespace changes
Inline
Sidebyside
Showing
3 changed files
with
21 additions
and
12 deletions
+21
12
prelude/tactics.v
prelude/tactics.v
+14
3
program_logic/auth.v
program_logic/auth.v
+1
1
program_logic/sts.v
program_logic/sts.v
+6
8
No files found.
prelude/tactics.v
View file @
ab9f921d
...
...
@@ 257,22 +257,28 @@ Ltac f_equiv :=
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 *)
(* Next, try to infer the relation. Unfortunately, there is an instance
of Proper for (eq ==> _), which will always be matched. *)
(* TODO: Can we exclude that instance? *)
(* 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
"Prop
er
"
in
let
R1
:
=
fresh
"R"
in
let
H
:
=
fresh
"
H
Prop"
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
"Prop
er
"
in
let
H
:
=
fresh
"
H
Prop"
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
(* In case the function symbol differs, but the arguments are the same,
maybe we have a pointwise_relation in our context. *)

H
:
pointwise_relation
_
?R
?f
?g

?R
(
?f
?x
)
(
?g
?x
)
=>
apply
H
;
f_equiv
end

idtac
(* Let the user solve this goal *)
].
...
...
@@ 289,6 +295,10 @@ Ltac solve_proper :=
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


?R
(
?f
_
_
_
_
)
(
?f
_
_
_
_
)
=>
unfold
f


?R
(
?f
_
_
_
)
(
?f
_
_
_
)
=>
unfold
f


?R
(
?f
_
_
)
(
?f
_
_
)
=>
unfold
f
...
...
@@ 296,6 +306,7 @@ Ltac solve_proper :=
end
;
solve
[
f_equiv
].
(** Given a tactic [tac2] generating a list of terms, [iter tac1 tac2]
runs [tac x] for each element [x] until [tac x] succeeds. If it does not
suceed for any element of the generated list, the whole tactic wil fail. *)
...
...
program_logic/auth.v
View file @
ab9f921d
...
...
@@ 40,7 +40,7 @@ Section auth.
Implicit
Types
γ
:
gname
.
Global
Instance
auth_own_ne
n
γ
:
Proper
(
dist
n
==>
dist
n
)
(
auth_own
γ
).
Proof
.
by
rewrite
auth_own_eq
/
auth_own_def
=>
a
b
>
.
Qed
.
Proof
.
rewrite
auth_own_eq
;
solve_proper
.
Qed
.
Global
Instance
auth_own_proper
γ
:
Proper
((
≡
)
==>
(
≡
))
(
auth_own
γ
).
Proof
.
by
rewrite
auth_own_eq
/
auth_own_def
=>
a
b
>.
Qed
.
Global
Instance
auth_own_timeless
γ
a
:
TimelessP
(
auth_own
γ
a
).
...
...
program_logic/sts.v
View file @
ab9f921d
...
...
@@ 52,22 +52,20 @@ Section sts.
(** Setoids *)
Global
Instance
sts_inv_ne
n
γ
:
Proper
(
pointwise_relation
_
(
dist
n
)
==>
dist
n
)
(
sts_inv
γ
).
Proof
.
by
intros
φ
1
φ
2
H
φ
;
rewrite
/
sts_inv
;
setoid_rewrite
H
φ
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
sts_inv_proper
γ
:
Proper
(
pointwise_relation
_
(
≡
)
==>
(
≡
))
(
sts_inv
γ
).
Proof
.
by
intros
φ
1
φ
2
H
φ
;
rewrite
/
sts_inv
;
setoid_rewrite
H
φ
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
sts_ownS_proper
γ
:
Proper
((
≡
)
==>
(
≡
)
==>
(
≡
))
(
sts_ownS
γ
).
Proof
.
intros
S1
S2
HS
T1
T2
HT
.
by
rewrite
!
sts_ownS_eq
/
sts_ownS_def
HS
HT
.
Qed
.
Proof
.
rewrite
sts_ownS_eq
.
solve_proper
.
Qed
.
Global
Instance
sts_own_proper
γ
s
:
Proper
((
≡
)
==>
(
≡
))
(
sts_own
γ
s
).
Proof
.
intros
T1
T2
HT
.
by
rewrite
!
sts_own_eq
/
sts_own_def
HT
.
Qed
.
Proof
.
rewrite
sts_own_eq
.
solve_proper
.
Qed
.
Global
Instance
sts_ctx_ne
n
γ
N
:
Proper
(
pointwise_relation
_
(
dist
n
)
==>
dist
n
)
(
sts_ctx
γ
N
).
Proof
.
by
intros
φ
1
φ
2
H
φ
;
rewrite
/
sts_ctx
H
φ
.
Qed
.
Proof
.
solve_proper
.
Qed
.
Global
Instance
sts_ctx_proper
γ
N
:
Proper
(
pointwise_relation
_
(
≡
)
==>
(
≡
))
(
sts_ctx
γ
N
).
Proof
.
by
intros
φ
1
φ
2
H
φ
;
rewrite
/
sts_ctx
H
φ
.
Qed
.
Proof
.
solve_proper
.
Qed
.
(* The same rule as implication does *not* hold, as could be shown using
sts_frag_included. *)
...
...
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