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
Pierre-Marie Pédrot
Iris
Commits
4e1a7837
Commit
4e1a7837
authored
Sep 01, 2017
by
Robbert Krebbers
Committed by
Jacques-Henri Jourdan
Oct 30, 2017
Browse files
Use cheaper iDestructHyp in iInv.
parent
74990506
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/lib/invariants.v
View file @
4e1a7837
...
...
@@ -99,18 +99,18 @@ Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
|
tac
Htmp
].
Tactic
Notation
"iInv"
constr
(
N
)
"as"
constr
(
pat
)
constr
(
Hclose
)
:
=
iInvCore
N
as
(
fun
H
=>
iDestruct
H
as
pat
)
Hclose
.
iInvCore
N
as
(
fun
H
=>
iDestruct
Hyp
H
as
pat
)
Hclose
.
Tactic
Notation
"iInv"
constr
(
N
)
"as"
"("
simple_intropattern
(
x1
)
")"
constr
(
pat
)
constr
(
Hclose
)
:
=
iInvCore
N
as
(
fun
H
=>
iDestruct
H
as
(
x1
)
pat
)
Hclose
.
iInvCore
N
as
(
fun
H
=>
iDestruct
Hyp
H
as
(
x1
)
pat
)
Hclose
.
Tactic
Notation
"iInv"
constr
(
N
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
")"
constr
(
pat
)
constr
(
Hclose
)
:
=
iInvCore
N
as
(
fun
H
=>
iDestruct
H
as
(
x1
x2
)
pat
)
Hclose
.
iInvCore
N
as
(
fun
H
=>
iDestruct
Hyp
H
as
(
x1
x2
)
pat
)
Hclose
.
Tactic
Notation
"iInv"
constr
(
N
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
")"
constr
(
pat
)
constr
(
Hclose
)
:
=
iInvCore
N
as
(
fun
H
=>
iDestruct
H
as
(
x1
x2
x3
)
pat
)
Hclose
.
iInvCore
N
as
(
fun
H
=>
iDestruct
Hyp
H
as
(
x1
x2
x3
)
pat
)
Hclose
.
Tactic
Notation
"iInv"
constr
(
N
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
")"
constr
(
pat
)
constr
(
Hclose
)
:
=
iInvCore
N
as
(
fun
H
=>
iDestruct
H
as
(
x1
x2
x3
x4
)
pat
)
Hclose
.
iInvCore
N
as
(
fun
H
=>
iDestruct
Hyp
H
as
(
x1
x2
x3
x4
)
pat
)
Hclose
.
theories/proofmode/tactics.v
View file @
4e1a7837
...
...
@@ -884,7 +884,7 @@ Tactic Notation "iModCore" constr(H) :=
|
env_reflexivity
|].
(** * Basic destruct tactic *)
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
constr
(
pat
)
:
=
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
constr
(
pat
)
:
=
let
rec
go
Hz
pat
:
=
lazymatch
pat
with
|
IAnom
=>
idtac
...
...
@@ -921,33 +921,33 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
let
pats
:
=
intro_pat
.
parse
pat
in
find_pat
false
pats
.
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
")"
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
")"
constr
(
pat
)
:
=
iExistDestruct
H
as
x1
H
;
iDestructHyp
H
as
@
pat
.
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
")"
constr
(
pat
)
:
=
iExistDestruct
H
as
x1
H
;
iDestructHyp
H
as
(
x2
)
pat
.
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
")"
constr
(
pat
)
:
=
iExistDestruct
H
as
x1
H
;
iDestructHyp
H
as
(
x2
x3
)
pat
.
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
")"
constr
(
pat
)
:
=
iExistDestruct
H
as
x1
H
;
iDestructHyp
H
as
(
x2
x3
x4
)
pat
.
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
")"
constr
(
pat
)
:
=
iExistDestruct
H
as
x1
H
;
iDestructHyp
H
as
(
x2
x3
x4
x5
)
pat
.
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
")"
constr
(
pat
)
:
=
iExistDestruct
H
as
x1
H
;
iDestructHyp
H
as
(
x2
x3
x4
x5
x6
)
pat
.
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
")"
constr
(
pat
)
:
=
iExistDestruct
H
as
x1
H
;
iDestructHyp
H
as
(
x2
x3
x4
x5
x6
x7
)
pat
.
Local
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
Tactic
Notation
"iDestructHyp"
constr
(
H
)
"as"
"("
simple_intropattern
(
x1
)
simple_intropattern
(
x2
)
simple_intropattern
(
x3
)
simple_intropattern
(
x4
)
simple_intropattern
(
x5
)
simple_intropattern
(
x6
)
simple_intropattern
(
x7
)
simple_intropattern
(
x8
)
")"
constr
(
pat
)
:
=
...
...
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
