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
stdpp
Commits
147b2022
Commit
147b2022
authored
Jan 12, 2016
by
Robbert Krebbers
Browse files
More consistent naming.
parent
28653f29
Changes
2
Hide whitespace changes
Inline
Sidebyside
theories/fin_maps.v
View file @
147b2022
...
...
@@ 1532,7 +1532,7 @@ Tactic Notation "simplify_map_equality" "by" tactic3(tac) :=
repeat
match
goal
with

_
=>
progress
simpl_map
by
tac

_
=>
progress
simplify_equality

_
=>
progress
simpl_option
_monad
by
tac

_
=>
progress
simpl_option
by
tac

H
:
{[
_
↦
_
]}
!!
_
=
None

_
=>
rewrite
lookup_singleton_None
in
H

H
:
{[
_
↦
_
]}
!!
_
=
Some
_

_
=>
rewrite
lookup_singleton_Some
in
H
;
destruct
H
...
...
theories/option.v
View file @
147b2022
...
...
@@ 261,7 +261,7 @@ Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (x : option A) :
(
P
↔
Q
)
→
guard
P
;
x
=
guard
Q
;
x
.
Proof
.
intros
[??].
repeat
case_option_guard
;
intuition
.
Qed
.
Tactic
Notation
"simpl_option
_monad
"
"by"
tactic3
(
tac
)
:
=
Tactic
Notation
"simpl_option"
"by"
tactic3
(
tac
)
:
=
let
assert_Some_None
A
o
H
:
=
first
[
let
x
:
=
fresh
in
evar
(
x
:
A
)
;
let
x'
:
=
eval
unfold
x
in
x
in
clear
x
;
assert
(
o
=
Some
x'
)
as
H
by
tac
...
...
@@ 308,7 +308,7 @@ Tactic Notation "simpl_option_monad" "by" tactic3(tac) :=
Tactic
Notation
"simplify_option_equality"
"by"
tactic3
(
tac
)
:
=
repeat
match
goal
with

_
=>
progress
simplify_equality'

_
=>
progress
simpl_option
_monad
by
tac

_
=>
progress
simpl_option
by
tac

_
:
maybe
_
?x
=
Some
_

_
=>
is_var
x
;
destruct
x

_
:
maybe2
_
?x
=
Some
_

_
=>
is_var
x
;
destruct
x

_
:
maybe3
_
?x
=
Some
_

_
=>
is_var
x
;
destruct
x
...
...
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