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
Iris
RefinedC
Commits
c1b44eaa
Commit
c1b44eaa
authored
Nov 19, 2021
by
Michael Sammler
Browse files
fast bailout for normalize_and_simpl_goal
parent
fcdbda03
Pipeline
#57425
passed with stage
in 12 minutes and 3 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/lithium/solvers.v
View file @
c1b44eaa
...
@@ -65,6 +65,11 @@ Proof. naive_solver. Qed.
...
@@ -65,6 +65,11 @@ Proof. naive_solver. Qed.
Ltac
normalize_and_simpl_goal_step
:
=
Ltac
normalize_and_simpl_goal_step
:
=
first
[
first
[
lazymatch
goal
with
|
|-
_
∧
_
=>
split
;
[
splitting_fast_done
|]
|
_
=>
splitting_fast_done
end
|
progress
normalize_goal
;
simpl
progress
normalize_goal
;
simpl
|
|
lazymatch
goal
with
lazymatch
goal
with
...
@@ -86,6 +91,7 @@ Ltac normalize_and_simpl_goal_step :=
...
@@ -86,6 +91,7 @@ Ltac normalize_and_simpl_goal_step :=
|
|-
?P
->
?Q
=>
|
|-
?P
->
?Q
=>
lazymatch
type
of
P
with
lazymatch
type
of
P
with
|
Prop
=>
first
[
|
Prop
=>
first
[
assert_is_trivial
P
;
intros
_
|
progress
normalize_goal_impl
|
progress
normalize_goal_impl
|
notypeclasses
refine
(
apply_simpl_impl
_
_
_
_
_
)
;
[
solve
[
refine
_
]
|]
;
simpl
;
notypeclasses
refine
(
apply_simpl_impl
_
_
_
_
_
)
;
[
solve
[
refine
_
]
|]
;
simpl
;
match
goal
with
match
goal
with
...
...
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