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
Iris
stdpp
Commits
52ac9252
Commit
52ac9252
authored
Feb 22, 2016
by
Robbert Krebbers
Browse files
Make naive_solver a bit more robust.
parent
05c5d5fd
Changes
1
Hide whitespace changes
Inline
Sidebyside
theories/tactics.v
View file @
52ac9252
...
...
@@ 320,6 +320,12 @@ Lemma forall_and_distr (A : Type) (P Q : A → Prop) :
(
∀
x
,
P
x
∧
Q
x
)
↔
(
∀
x
,
P
x
)
∧
(
∀
x
,
Q
x
).
Proof
.
firstorder
.
Qed
.
(** The tactic [no_new_unsolved_evars tac] executes [tac] and fails if it
creates any new evars. This trick is by Jonathan Leivent, see:
https://coq.inria.fr/bugs/show_bug.cgi?id=3872 *)
Ltac
no_new_unsolved_evars
tac
:
=
exact
ltac
:
(
tac
).
Tactic
Notation
"naive_solver"
tactic
(
tac
)
:
=
unfold
iff
,
not
in
*
;
repeat
match
goal
with
...
...
@@ 353,23 +359,20 @@ Tactic Notation "naive_solver" tactic(tac) :=
(**i use recursion to enable backtracking on the following clauses. *)
match
goal
with
(**i instantiation of the conclusion *)


∃
x
,
_
=>
eexists
;
go
n


∃
x
,
_
=>
no_new_unsolved_evars
ltac
:
(
eexists
;
go
n
)


_
∨
_
=>
first
[
left
;
go
n

right
;
go
n
]

_
=>
(**i instantiations of assumptions. *)
lazymatch
n
with

S
?n'
=>
(**i we give priority to assumptions that fit on the conclusion. *)
match
goal
with

H
:
_
→
_

_
=>
is_non_dependent
H
;
eapply
H
;
clear
H
;
go
n'
match
goal
with

H
:
_
→
_

_
=>
is_non_dependent
H
;
try
(
eapply
H
;
fail
2
)
;
efeed
pose
proof
H
;
clear
H
;
go
n'
no_new_unsolved_evars
ltac
:
(
first
[
eapply
H

efeed
pose
proof
H
]
;
clear
H
;
go
n'
)
end
end
end
in
iter
(
fun
n'
=>
go
n'
)
(
eval
compute
in
(
seq
0
6
)).
in
iter
(
fun
n'
=>
go
n'
)
(
eval
compute
in
(
seq
1
6
)).
Tactic
Notation
"naive_solver"
:
=
naive_solver
eauto
.
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