Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Tej Chajed
iris
Commits
b863b045
Commit
b863b045
authored
Oct 27, 2016
by
Ralf Jung
Browse files
tactics: rename auto_proper => auto_equiv
parent
4653cb6d
Changes
1
Show whitespace changes
Inline
Sidebyside
prelude/tactics.v
View file @
b863b045
...
@@ 292,9 +292,9 @@ Ltac f_equiv :=
...
@@ 292,9 +292,9 @@ Ltac f_equiv :=
end
.
end
.
(** auto_proper solves goals of the form "f _ = f _", for any relation and any
(** 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.
number of arguments, by repeatedly apply
ing
f_equiv and handling trivial cases.
If it cannot solve an equality, it will leave that to the user. *)
If it cannot solve an equality, it will leave that to the user. *)
Ltac
auto_
proper
:
=
Ltac
auto_
equiv
:
=
(* Deal with "pointwise_relation" *)
(* Deal with "pointwise_relation" *)
repeat
lazymatch
goal
with
repeat
lazymatch
goal
with


pointwise_relation
_
_
_
_
=>
intros
?


pointwise_relation
_
_
_
_
=>
intros
?
...
@@ 302,10 +302,10 @@ Ltac auto_proper :=
...
@@ 302,10 +302,10 @@ Ltac auto_proper :=
(* Normalize away equalities. *)
(* Normalize away equalities. *)
simplify_eq
;
simplify_eq
;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
try
(
f_equiv
;
fast_done

auto_
proper
).
try
(
f_equiv
;
fast_done

auto_
equiv
).
(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
number of relations. All the actual work is done by
f
_equiv;
number of relations. All the actual work is done by
auto
_equiv;
solve_proper just introduces the assumptions and unfolds the first
solve_proper just introduces the assumptions and unfolds the first
head symbol. *)
head symbol. *)
Ltac
solve_proper
:
=
Ltac
solve_proper
:
=
...
@@ 328,7 +328,7 @@ Ltac solve_proper :=
...
@@ 328,7 +328,7 @@ Ltac solve_proper :=


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


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


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


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