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
cdab1f86
Commit
cdab1f86
authored
Nov 22, 2016
by
Robbert Krebbers
Browse files
Patch naive_solver to deal with Coq bug #2901.
parent
1a57c783
Changes
1
Show whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
8 additions
and
3 deletions
+8
3
theories/tactics.v
theories/tactics.v
+8
3
No files found.
theories/tactics.v
View file @
cdab1f86
...
...
@@ 478,8 +478,12 @@ Tactic Notation "naive_solver" tactic(tac) :=


∀
_
,
_
=>
intro
(**i simplification of assumptions *)

H
:
False

_
=>
destruct
H

H
:
_
∧
_

_
=>
destruct
H

H
:
∃
_
,
_

_
=>
destruct
H

H
:
_
∧
_

_
=>
let
H1
:
=
fresh
in
let
H2
:
=
fresh
in
destruct
H
as
[
H1
H2
]
;
try
clear
H

H
:
∃
_
,
_

_
=>
let
x
:
=
fresh
in
let
Hx
:
=
fresh
in
destruct
H
as
[
x
Hx
]
;
try
clear
H

H
:
?P
→
?Q
,
H2
:
?P

_
=>
specialize
(
H
H2
)

H
:
Is_true
(
bool_decide
_
)

_
=>
apply
(
bool_decide_unpack
_
)
in
H

H
:
Is_true
(
_
&&
_
)

_
=>
apply
andb_True
in
H
;
destruct
H
...
...
@@ 491,7 +495,8 @@ Tactic Notation "naive_solver" tactic(tac) :=


_
∧
_
=>
split


Is_true
(
bool_decide
_
)
=>
apply
(
bool_decide_pack
_
)


Is_true
(
_
&&
_
)
=>
apply
andb_True
;
split

H
:
_
∨
_

_
=>
destruct
H

H
:
_
∨
_

_
=>
let
H1
:
=
fresh
in
destruct
H
as
[
H1

H1
]
;
try
clear
H
(**i solve the goal using the user supplied tactic *)


_
=>
solve
[
tac
]
end
;
...
...
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