Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
stdpp
Commits
436f17c4
Commit
436f17c4
authored
Mar 05, 2016
by
Ralf Jung
Browse files
introduce "fast_done", a tactic that *quickly* tries to solve the goal
parent
4c68a044
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/collections.v
View file @
436f17c4
...
...
@@ -265,7 +265,7 @@ Ltac set_unfold :=
[set_solver] already. We use the [naive_solver] tactic as a substitute.
This tactic either fails or proves the goal. *)
Tactic
Notation
"set_solver"
"by"
tactic3
(
tac
)
:
=
try
(
reflexivity
||
eassumpti
on
)
;
try
fast_d
on
e
;
intros
;
setoid_subst
;
set_unfold
;
intros
;
setoid_subst
;
...
...
theories/tactics.v
View file @
436f17c4
...
...
@@ -34,6 +34,13 @@ is rather efficient when having big hint databases, or expensive [Hint Extern]
declarations as the ones above. *)
Tactic
Notation
"intuition"
:
=
intuition
auto
.
(* [done] can get slow as it calls "trivial". [fast_done] can solve way less
goals, but it will also always finish quickly. *)
Ltac
fast_done
:
=
solve
[
reflexivity
|
eassumption
|
symmetry
;
eassumption
].
Tactic
Notation
"fast_by"
tactic
(
tac
)
:
=
tac
;
fast_done
.
(** A slightly modified version of Ssreflect's finishing tactic [done]. It
also performs [reflexivity] and uses symmetry of negated equalities. Compared
to Ssreflect's [done], it does not compute the goal's [hnf] so as to avoid
...
...
@@ -42,10 +49,9 @@ Coq's [easy] tactic as it does not perform [inversion]. *)
Ltac
done
:
=
trivial
;
intros
;
solve
[
repeat
first
[
solve
[
trivial
]
[
fast_done
|
solve
[
trivial
]
|
solve
[
symmetry
;
trivial
]
|
eassumption
|
reflexivity
|
discriminate
|
contradiction
|
solve
[
apply
not_symmetry
;
trivial
]
...
...
@@ -288,7 +294,7 @@ Ltac auto_proper :=
(* Normalize away equalities. *)
simplify_eq
;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
try
(
f_equiv
;
as
sumption
||
(
symmetry
;
assumption
)
||
auto_proper
).
try
(
f_equiv
;
f
as
t_done
||
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;
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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