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
Tej Chajed
iris
Commits
efcef7e0
Commit
efcef7e0
authored
Sep 19, 2016
by
Robbert Krebbers
Browse files
Better implementation of iLöb.
parent
75ad3b2e
Changes
1
Show whitespace changes
Inline
Sidebyside
proofmode/tactics.v
View file @
efcef7e0
...
...
@@ 782,6 +782,38 @@ Tactic Notation "iIntros" "(" simple_intropattern(x1) simple_intropattern(x2)
")"
constr
(
p
)
:
=
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
;
iIntros
p
.
Tactic
Notation
"iRevertIntros"
"with"
tactic
(
tac
)
:
=
match
goal
with


of_envs
?
Δ
⊢
_
=>
let
Hs
:
=
constr
:
(
reverse
(
env_dom
(
env_spatial
Δ
)))
in
iRevert
[
"★"
]
;
tac
;
iIntros
Hs
end
.
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
")"
"with"
tactic
(
tac
)
:
=
iRevertIntros
with
(
iRevert
(
x1
)
;
tac
;
iIntros
(
x1
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
")"
"with"
tactic
(
tac
)
:
=
iRevertIntros
with
(
iRevert
(
x1
x2
)
;
tac
;
iIntros
(
x1
x2
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
"with"
tactic
(
tac
)
:
=
iRevertIntros
with
(
iRevert
(
x1
x2
x3
)
;
tac
;
iIntros
(
x1
x2
x3
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
"with"
tactic
(
tac
)
:
=
iRevertIntros
with
(
iRevert
(
x1
x2
x3
x4
)
;
tac
;
iIntros
(
x1
x2
x3
x4
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
"with"
tactic
(
tac
)
:
=
iRevertIntros
with
(
iRevert
(
x1
x2
x3
x4
x5
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
")"
"with"
tactic
(
tac
)
:
=
iRevertIntros
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
"with"
tactic
(
tac
)
:
=
iRevertIntros
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
x7
)).
Tactic
Notation
"iRevertIntros"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
"with"
tactic
(
tac
)
:
=
iRevertIntros
with
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
)
;
tac
;
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)).
(** * Destruct tactic *)
Tactic
Notation
"iDestructCore"
open_constr
(
lem
)
"as"
constr
(
p
)
tactic
(
tac
)
:
=
let
intro_destruct
n
:
=
...
...
@@ 843,45 +875,35 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
Tactic
Notation
"iDestruct"
open_constr
(
lem
)
"as"
"%"
simple_intropattern
(
pat
)
:
=
iDestructCore
lem
as
true
(
fun
H
=>
iPure
H
as
pat
).
(* This is pretty ugly, but without Ltac support for manipulating lists of
idents I do not know how to do this better. *)
Local
Ltac
iL
ö
bHelp
IH
tac_before
tac_after
:
=
match
goal
with


of_envs
?
Δ
⊢
_
=>
let
Hs
:
=
constr
:
(
reverse
(
env_dom
(
env_spatial
Δ
)))
in
iRevert
[
"★"
]
;
tac_before
;
Tactic
Notation
"iLöbCore"
"as"
constr
(
IH
)
:
=
eapply
tac_l
ö
b
with
_
IH
;
[
reflexivity

env_cbv
;
reflexivity

fail
"iLöb:"
IH
"not fresh"
]
;
tac_after
;
iIntros
Hs
end
.

env_cbv
;
reflexivity

fail
"iLöb:"
IH
"not fresh"
].
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
:
=
iL
ö
bHelp
IH
idtac
idtac
.
(** * Löb induction *)
Tactic
Notation
"iLöb"
"as"
constr
(
IH
)
:
=
iRevertIntros
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"("
ident
(
x1
)
")"
"as"
constr
(
IH
)
:
=
i
L
ö
bHelp
IH
ltac
:
(
iRevert
(
x1
))
ltac
:
(
iIntros
(
x1
)
).
i
RevertIntros
(
x1
)
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"("
ident
(
x1
)
ident
(
x2
)
")"
"as"
constr
(
IH
)
:
=
i
L
ö
bHelp
IH
ltac
:
(
iRevert
(
x1
x2
))
ltac
:
(
iIntros
(
x1
x2
)
).
i
RevertIntros
(
x1
x2
)
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
")"
"as"
constr
(
IH
)
:
=
i
L
ö
bHelp
IH
ltac
:
(
iRevert
(
x1
x2
x3
))
ltac
:
(
iIntros
(
x1
x2
x3
)
).
i
RevertIntros
(
x1
x2
x3
)
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
")"
"as"
constr
(
IH
)
:
=
i
L
ö
bHelp
IH
ltac
:
(
iRevert
(
x1
x2
x3
x4
))
ltac
:
(
iIntros
(
x1
x2
x3
x4
)
).
i
RevertIntros
(
x1
x2
x3
x4
)
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
")"
"as"
constr
(
IH
)
:
=
iL
ö
bHelp
IH
ltac
:
(
iRevert
(
x1
x2
x3
x4
x5
))
ltac
:
(
iIntros
(
x1
x2
x3
x4
x5
)).
iRevertIntros
(
x1
x2
x3
x4
x5
)
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
")"
"as"
constr
(
IH
)
:
=
iL
ö
bHelp
IH
ltac
:
(
iRevert
(
x1
x2
x3
x4
x5
x6
))
ltac
:
(
iIntros
(
x1
x2
x3
x4
x5
x6
)).
iRevertIntros
(
x1
x2
x3
x4
x5
x6
)
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
")"
"as"
constr
(
IH
)
:
=
iL
ö
bHelp
IH
ltac
:
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
))
ltac
:
(
iIntros
(
x1
x2
x3
x4
x5
x6
x7
)).
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
)
with
(
iL
ö
bCore
as
IH
).
Tactic
Notation
"iLöb"
"("
ident
(
x1
)
ident
(
x2
)
ident
(
x3
)
ident
(
x4
)
ident
(
x5
)
ident
(
x6
)
ident
(
x7
)
ident
(
x8
)
")"
"as"
constr
(
IH
)
:
=
iL
ö
bHelp
IH
ltac
:
(
iRevert
(
x1
x2
x3
x4
x5
x6
x7
x8
))
ltac
:
(
iIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)).
iRevertIntros
(
x1
x2
x3
x4
x5
x6
x7
x8
)
with
(
iL
ö
bCore
as
IH
).
(** * Assert *)
Tactic
Notation
"iAssertCore"
open_constr
(
Q
)
"with"
constr
(
Hs
)
"as"
tactic
(
tac
)
:
=
...
...
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