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
PierreMarie Pédrot
Iris
Commits
d0c9c6c8
Commit
d0c9c6c8
authored
Feb 25, 2016
by
Ralf Jung
Browse files
make f_equiv behaior more like the original f_equiv: It applies a *single* Proper
parent
e38e903b
Changes
2
Hide whitespace changes
Inline
Sidebyside
algebra/sts.v
View file @
d0c9c6c8
...
...
@@ 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
.
move
=>
s1
s2
Hs
.
simpl
in
HT
.
by
apply
up_preserving
.
f_equiv
;
last
done
.
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
.
...
...
prelude/tactics.v
View file @
d0c9c6c8
...
...
@@ 229,30 +229,23 @@ 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
look
ing
for appropriate "Proper" instance
s.
If it cannot solve an equality, it will leave that to the user
. *)
(** f_equiv
works on
goals of the form "f _ = f _", for any relation and any
number of arguments
. It
look
s
for
an
appropriate "Proper" instance
, and
applies it
. *)
Ltac
f_equiv
:
=
(* Deal with "pointwise_relation" *)
repeat
lazymatch
goal
with


pointwise_relation
_
_
_
_
=>
intros
?
end
;
(* Normalize away equalities. *)
simplify_eq
;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
try
match
goal
with

_
=>
first
[
reflexivity

assumption

symmetry
;
assumption
]
match
goal
with

_
=>
reflexivity
(* We support matches on both sides, *if* they concern the same
variable.
TODO: We should support different variables, provided that we can
derive contradictions for the offdiagonal cases. *)


?R
(
match
?x
with
_
=>
_
end
)
(
match
?x
with
_
=>
_
end
)
=>
destruct
x
;
f_equiv
destruct
x
(* First assume that the arguments need the same relation as the result *)


?R
(
?f
?x
)
(
?f
_
)
=>
apply
(
_
:
Proper
(
R
==>
R
)
f
)
;
f_equiv
apply
(
_
:
Proper
(
R
==>
R
)
f
)


?R
(
?f
?x
?y
)
(
?f
_
_
)
=>
apply
(
_
:
Proper
(
R
==>
R
==>
R
)
f
)
;
f_equiv
apply
(
_
:
Proper
(
R
==>
R
==>
R
)
f
)
(* 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? *)
...
...
@@ 260,15 +253,28 @@ Ltac f_equiv :=
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
_
)
=>
apply
(
_
:
Proper
(
_
==>
R
)
f
)
;
f_equiv
apply
(
_
:
Proper
(
_
==>
R
)
f
)


?R
(
?f
?x
?y
)
(
?f
_
_
)
=>
apply
(
_
:
Proper
(
_
==>
_
==>
R
)
f
)
;
f_equiv
apply
(
_
:
Proper
(
_
==>
_
==>
R
)
f
)
(* 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
apply
H
end
.
(** auto_proper solves goals of the form "f _ = f _", for any relation and any
number of arguments, by repeatedly apply f_equiv and handling trivial cases.
If it cannot solve an equality, it will leave that to the user. *)
Ltac
auto_proper
:
=
(* Deal with "pointwise_relation" *)
repeat
lazymatch
goal
with


pointwise_relation
_
_
_
_
=>
intros
?
end
;
(* Normalize away equalities. *)
simplify_eq
;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
try
(
f_equiv
;
assumption

(
symmetry
;
assumption
)

auto_proper
).
(** 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
...
...
@@ 291,7 +297,7 @@ Ltac solve_proper :=


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


?R
(
?f
_
)
(
?f
_
)
=>
unfold
f
end
;
solve
[
f_equiv
].
solve
[
auto_proper
].
(** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac,
and then reverts them. *)
...
...
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